Merge branch 'sofia/async-http-server' into sofia/async-http-client

Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>

.github/workflows/build-template.yml

@@ -131,7 +131,7 @@ jobs:
           [ -d build ] || mkdir build
           cd build
           # arguments passed to `cmake`
-          OPTIONS=(-DWFAIL=ON)
+          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
           if [[ -n '${{ matrix.release }}' ]]; then
             # this also enables githash embedding into stage 1 library, which prohibits reusing
             # `.olean`s across commits, so we don't do it in the fast non-release CI
@@ -201,7 +201,6 @@ jobs:
         if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
         run: |
           curl --version
-          cat build/stage1/lib/lean/Leanc.trace
           cd src
           time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
           time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}

.github/workflows/update-stage0.yml

@@ -77,7 +77,7 @@ jobs:
       # sync options with `Linux Lake` to ensure cache reuse
       run: |
         mkdir -p build
-        cmake --preset release -B build -DWFAIL=ON
+        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: |

.gitignore

@@ -34,4 +34,3 @@ wdErr.txt
 wdIn.txt
 wdOut.txt
 downstream_releases/
-.claude/worktrees/

script/release_repos.yml

@@ -28,14 +28,6 @@ repositories:
     branch: main
     dependencies: []
 
-  - name: leansqlite
-    url: https://github.com/leanprover/leansqlite
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies:
-      - plausible
-
   - name: verso
     url: https://github.com/leanprover/verso
     toolchain-tag: true
@@ -108,7 +100,7 @@ repositories:
     toolchain-tag: true
     stable-branch: false
     branch: main
-    dependencies: [lean4-cli, BibtexQuery, mathlib4, leansqlite]
+    dependencies: [lean4-cli, BibtexQuery, mathlib4]
 
   - name: cslib
     url: https://github.com/leanprover/cslib

script/release_steps.py

@@ -481,9 +481,11 @@ def execute_release_steps(repo, version, config):
         run_command("lake update", cwd=repo_path, stream_output=True)
     elif repo_name == "verso":
         # verso has nested Lake projects in test-projects/ that each have their own
-        # lake-manifest.json with a subverso pin and their own lean-toolchain.
-        # After updating the root manifest via `lake update`, sync the de-modulized
-        # subverso rev into all sub-manifests, and update their lean-toolchain files.
+        # lake-manifest.json with a subverso pin. After updating the root manifest via
+        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
+        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
+        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
+        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
         run_command("lake update", cwd=repo_path, stream_output=True)
         print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
         sync_script = (
@@ -496,15 +498,6 @@ def execute_release_steps(repo, version, config):
         )
         run_command(sync_script, cwd=repo_path)
         print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
-        # Update all lean-toolchain files in test-projects/ to match the root
-        print(blue("Updating lean-toolchain files in test-projects/..."))
-        find_result = run_command("find test-projects -name lean-toolchain", cwd=repo_path)
-        for tc_path in find_result.stdout.strip().splitlines():
-            if tc_path:
-                tc_file = repo_path / tc_path
-                with open(tc_file, "w") as f:
-                    f.write(f"leanprover/lean4:{version}\n")
-                print(green(f"  Updated {tc_path}"))
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
@@ -666,61 +659,56 @@ def execute_release_steps(repo, version, config):
         # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
         print(blue("Fetching latest changes from origin..."))
         run_command("git fetch origin", cwd=repo_path)
-
-        # Check if nightly-testing branch exists on origin (use local ref after fetch for exact match)
-        nightly_check = run_command("git show-ref --verify --quiet refs/remotes/origin/nightly-testing", cwd=repo_path, check=False)
-        if nightly_check.returncode != 0:
-            print(yellow("No nightly-testing branch found on origin, skipping merge"))
-        else:
-            try:
-                print(blue("Merging origin/nightly-testing..."))
-                run_command("git merge origin/nightly-testing", cwd=repo_path)
-                print(green("Merge completed successfully"))
-            except subprocess.CalledProcessError:
-                # Merge failed due to conflicts - check which files are conflicted
-                print(blue("Merge conflicts detected, checking which files are affected..."))
-
-                # Get conflicted files using git status
-                status_result = run_command("git status --porcelain", cwd=repo_path)
-                conflicted_files = []
-
-                for line in status_result.stdout.splitlines():
-                    if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                        # Extract filename (skip the first 3 characters which are status codes)
-                        conflicted_files.append(line[3:])
-
-                # Filter out allowed files
-                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-                problematic_files = []
-
+        
+        try:
+            print(blue("Merging origin/nightly-testing..."))
+            run_command("git merge origin/nightly-testing", cwd=repo_path)
+            print(green("Merge completed successfully"))
+        except subprocess.CalledProcessError:
+            # Merge failed due to conflicts - check which files are conflicted
+            print(blue("Merge conflicts detected, checking which files are affected..."))
+            
+            # Get conflicted files using git status
+            status_result = run_command("git status --porcelain", cwd=repo_path)
+            conflicted_files = []
+            
+            for line in status_result.stdout.splitlines():
+                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
+                    # Extract filename (skip the first 3 characters which are status codes)
+                    conflicted_files.append(line[3:])
+            
+            # Filter out allowed files
+            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
+            problematic_files = []
+            
+            for file in conflicted_files:
+                is_allowed = any(pattern in file for pattern in allowed_patterns)
+                if not is_allowed:
+                    problematic_files.append(file)
+            
+            if problematic_files:
+                # There are conflicts in non-allowed files - fail
+                print(red("❌ Merge failed!"))
+                print(red(f"Merging nightly-testing resulted in conflicts in:"))
+                for file in problematic_files:
+                    print(red(f"  - {file}"))
+                print(red("Please resolve these conflicts manually."))
+                return
+            else:
+                # Only allowed files are conflicted - resolve them automatically
+                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
+                print(blue("Resolving conflicts automatically..."))
+                
+                # For lean-toolchain and lake-manifest.json, keep our versions
                 for file in conflicted_files:
-                    is_allowed = any(pattern in file for pattern in allowed_patterns)
-                    if not is_allowed:
-                        problematic_files.append(file)
-
-                if problematic_files:
-                    # There are conflicts in non-allowed files - fail
-                    print(red("❌ Merge failed!"))
-                    print(red(f"Merging nightly-testing resulted in conflicts in:"))
-                    for file in problematic_files:
-                        print(red(f"  - {file}"))
-                    print(red("Please resolve these conflicts manually."))
-                    return
-                else:
-                    # Only allowed files are conflicted - resolve them automatically
-                    print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                    print(blue("Resolving conflicts automatically..."))
-
-                    # For lean-toolchain and lake-manifest.json, keep our versions
-                    for file in conflicted_files:
-                        print(blue(f"Keeping our version of {file}"))
-                        run_command(f"git checkout --ours {file}", cwd=repo_path)
-
-                    # Complete the merge
-                    run_command("git add .", cwd=repo_path)
-                    run_command("git commit --no-edit", cwd=repo_path)
-
-                    print(green("✅ Merge completed successfully with automatic conflict resolution"))
+                    print(blue(f"Keeping our version of {file}"))
+                    run_command(f"git checkout --ours {file}", cwd=repo_path)
+                
+                # Complete the merge
+                run_command("git add .", cwd=repo_path)
+                run_command("git commit --no-edit", cwd=repo_path)
+                
+                print(green("✅ Merge completed successfully with automatic conflict resolution"))
 
     # Build and test (skip for Mathlib)
     if repo_name not in ["mathlib4"]:

src/CMakeLists.txt

@@ -116,19 +116,11 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
-set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
-set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
+set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
 # Temporary, core-only flags. Must be synced with stdlib_flags.h.
-string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
-
-# option used by the CI to fail on warnings
-option(WFAIL "Fail build if warnings are emitted by Lean" ON)
-if(WFAIL MATCHES "ON")
-  string(APPEND LAKE_EXTRA_ARGS " --wfail")
-  string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
-endif()
+string(APPEND LEAN_EXTRA_MAKE_OPTS " -Dbackward.do.legacy=false")
 
 if(LAZY_RC MATCHES "ON")
   set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
@@ -206,7 +198,7 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
 
 # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
 if((MULTI_THREAD MATCHES "ON") AND (CMAKE_SYSTEM_NAME MATCHES "Darwin"))
-  string(APPEND LEAN_EXTRA_OPTS " -s40000")
+  string(APPEND LEAN_EXTRA_MAKE_OPTS " -s40000")
 endif()
 
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
@@ -678,9 +670,6 @@ else()
   set(LEAN_PATH_SEPARATOR ":")
 endif()
 
-# inherit genral options for lean.mk.in and stdlib.make.in
-string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
-
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
 if(STAGE EQUAL 0)
@@ -1065,7 +1054,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
 
-toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML)
+toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
 
 if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
   set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")

src/Init/Data/Array/Basic.lean

@@ -1085,17 +1085,6 @@ Examples:
 def sum {α} [Add α] [Zero α] : Array α → α :=
   foldr (· + ·) 0
 
-/--
-Computes the product of the elements of an array.
-
-Examples:
- * `#[a, b, c].prod = a * (b * (c * 1))`
- * `#[1, 2, 5].prod = 10`
--/
-@[inline, expose]
-def prod {α} [Mul α] [One α] : Array α → α :=
-  foldr (· * ·) 1
-
 /--
 Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`.
 

src/Init/Data/Array/Int.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
-public import Init.Data.List.Int.Prod
 public import Init.Data.Array.MinMax
 import Init.Data.Int.Lemmas
 
@@ -75,17 +74,4 @@ theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)
 
-@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
-  rw [← List.toArray_replicate, List.prod_toArray]
-  simp
-
-theorem prod_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_int (xs : Array Int) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_int {xs : Array Int} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
-
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -4380,47 +4380,6 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
 
-/-! ### prod -/
-
-@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#[] : Array α).prod = 1 := rfl
-theorem prod_eq_foldr [Mul α] [One α] {xs : Array α} :
-    xs.prod = xs.foldr (init := 1) (· * ·) :=
-  rfl
-
-@[simp, grind =]
-theorem prod_toList [Mul α] [One α] {as : Array α} : as.toList.prod = as.prod := by
-  cases as
-  simp [Array.prod, List.prod]
-
-@[simp, grind =]
-theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    {as₁ as₂ : Array α} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toList, List.prod_append]
-
-@[simp, grind =]
-theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
-    #[x].prod = x := by
-  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
-
-@[simp, grind =]
-theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} {x : α} :
-    (xs.push x).prod = xs.prod * x := by
-  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id,
-    ← Array.foldr_assoc]
-
-@[simp, grind =]
-theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.Commutative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Array α) : xs.reverse.prod = xs.prod := by
-  simp [← prod_toList, List.prod_reverse]
-
-theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} :
-    xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp [← prod_toList, List.prod_eq_foldl]
-
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :

src/Init/Data/Array/Nat.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Array.MinMax
 import Init.Data.List.Nat.Sum
-import Init.Data.List.Nat.Prod
 import Init.Data.Array.Lemmas
 
 public section
@@ -82,24 +81,4 @@ theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h)
 
-protected theorem prod_pos_iff_forall_pos_nat {xs : Array Nat} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
-  simp [← prod_toList, List.prod_pos_iff_forall_pos_nat]
-
-protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Array Nat} :
-    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
-  simp [← prod_toList, List.prod_eq_zero_iff_exists_zero_nat]
-
-@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
-  rw [← List.toArray_replicate, List.prod_toArray]
-  simp
-
-theorem prod_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_nat (xs : Array Nat) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_nat {xs : Array Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
-
 end Array

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -271,7 +271,7 @@ private def optionPelim' {α : Type u_1} (t : Option α) {β :  Sort u_2}
 
 /--
 Inserts an `Option` case distinction after the first computation of a call to `MonadAttach.pbind`.
-This lemma is useful for simplifying the second computation, which often involves `match` expressions
+This lemma is useful for simplifying the second computation, which often involes `match` expressions
 that use `pbind`'s proof term.
 -/
 private theorem pbind_eq_pbind_if_isSome [Monad m] [MonadAttach m] (x : m (Option α)) (f : (_ : _) → _ → m β) :

src/Init/Data/List/Basic.lean

@@ -2056,20 +2056,6 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl
 
-/--
-Computes the product of the elements of a list.
-
-Examples:
- * `[a, b, c].prod = a * (b * (c * 1))`
- * `[1, 2, 5].prod = 10`
--/
-def prod {α} [Mul α] [One α] : List α → α :=
-  foldr (· * ·) 1
-
-@[simp, grind =] theorem prod_nil [Mul α] [One α] : ([] : List α).prod = 1 := rfl
-@[simp, grind =] theorem prod_cons [Mul α] [One α] {a : α} {l : List α} : (a::l).prod = a * l.prod := rfl
-theorem prod_eq_foldr [Mul α] [One α] {l : List α} : l.prod = l.foldr (· * ·) 1 := rfl
-
 /-! ### range -/
 
 /--

src/Init/Data/List/Int.lean

@@ -7,4 +7,3 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
-public import Init.Data.List.Int.Prod

src/Init/Data/List/Int/Prod.lean

@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-import Init.Data.List.Lemmas
-import Init.Data.Int.Lemmas
-public import Init.Data.Int.Pow
-public import Init.Data.List.Basic
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace List
-
-@[simp]
-theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
-  induction n <;> simp_all [replicate_succ, Int.pow_succ, Int.mul_comm]
-
-theorem prod_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_int (xs : List Int) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-end List

src/Init/Data/List/Lemmas.lean

@@ -1878,24 +1878,6 @@ theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
       Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
 
-@[simp, grind =]
-theorem prod_append [Mul α] [One α] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    [Std.Associative (α := α) (· * ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
-
-@[simp, grind =]
-theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
-    [x].prod = x := by
-  simp [List.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
-
-@[simp, grind =]
-theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.Commutative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : List α) : xs.reverse.prod = xs.prod := by
-  induction xs <;>
-    simp_all [prod_append, Std.Commutative.comm (α := α) _ 1,
-      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
-
 /-! ### concat
 
 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
@@ -2802,11 +2784,6 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [sum_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
 
-theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : List α} :
-    xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp [prod_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
-
 -- The argument `f : α₁ → α₂` is intentionally explicit, as it is sometimes not found by unification.
 theorem foldl_hom (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁}
     (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by

src/Init/Data/List/Nat.lean

@@ -13,7 +13,6 @@ public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
 public import Init.Data.List.Nat.Sum
-public import Init.Data.List.Nat.Prod
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq

src/Init/Data/List/Nat/Prod.lean

@@ -1,50 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-import Init.Data.List.Lemmas
-public import Init.BinderPredicates
-public import Init.NotationExtra
-import Init.Data.Nat.Lemmas
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace List
-
-protected theorem prod_eq_zero_iff_exists_zero_nat {l : List Nat} : l.prod = 0 ↔ ∃ x ∈ l, x = 0 := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp [Nat.mul_eq_zero, ih, eq_comm (a := (0 : Nat))]
-
-protected theorem prod_pos_iff_forall_pos_nat {l : List Nat} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [prod_cons, mem_cons, forall_eq_or_imp, ← ih]
-    constructor
-    · intro h
-      exact ⟨Nat.pos_of_mul_pos_right h, Nat.pos_of_mul_pos_left h⟩
-    · exact fun ⟨hx, hxs⟩ => Nat.mul_pos hx hxs
-
-@[simp]
-theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
-  induction n <;> simp_all [replicate_succ, Nat.pow_succ, Nat.mul_comm]
-
-theorem prod_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_nat (xs : List Nat) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_nat {xs : List Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
-
-end List

src/Init/Data/List/Perm.lean

@@ -606,13 +606,6 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum :
   | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
   | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
 
-theorem prod_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.prod = l₂.prod := by
-  induction h with
-  | nil => simp
-  | cons _ _ ih => simp [ih]
-  | swap => simpa [List.prod_cons] using Nat.mul_left_comm ..
-  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
-
 theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by
   rw [Bool.eq_iff_iff]; simp [hp.mem_iff]
 
@@ -622,9 +615,6 @@ theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum
 
-grind_pattern Perm.prod_nat => l₁ ~ l₂, l₁.prod
-grind_pattern Perm.prod_nat => l₁ ~ l₂, l₂.prod
-
 end Perm
 
 end List

src/Init/Data/List/ToArray.lean

@@ -213,9 +213,6 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
   simp [Array.sum, List.sum]
 
-@[simp, grind =] theorem prod_toArray [Mul α] [One α] (l : List α) : l.toArray.prod = l.prod := by
-  simp [Array.prod, List.prod]
-
 @[simp, grind =] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
   apply ext'

src/Init/Data/String/Decode.lean

@@ -363,7 +363,7 @@ theorem toBitVec_eq_of_parseFirstByte_eq_threeMore {b : UInt8} (h : parseFirstBy
 public def isInvalidContinuationByte (b : UInt8) : Bool :=
   b &&& 0xc0 != 0x80
 
-theorem isInvalidContinuationByte_eq_false_iff {b : UInt8} :
+theorem isInvalidContinutationByte_eq_false_iff {b : UInt8} :
     isInvalidContinuationByte b = false ↔ b &&& 0xc0 = 0x80 := by
   simp [isInvalidContinuationByte]
 

src/Init/Data/String/Lemmas/Iterate.lean

@@ -31,7 +31,7 @@ namespace Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual programs. Actual programs should use
+This function is not meant to be used in actual progams. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=
@@ -206,7 +206,7 @@ end Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual programs. Actual programs should use
+This function is not meant to be used in actual progams. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=

src/Init/Data/String/Subslice.lean

@@ -23,7 +23,7 @@ Given a {name}`Slice` {name}`s`, the type {lean}`s.Subslice` is the type of half
 in {name}`s` delineated by a valid position on both sides.
 
 This type is useful to track regions of interest within some larger slice that is also of interest.
-In contrast, {name}`Slice` is used to track regions of interest within some larger string that is
+In contrast, {name}`Slice` is used to track regions of interest whithin some larger string that is
 not or no longer relevant.
 
 Equality on {name}`Subslice` is somewhat better behaved than on {name}`Slice`, but note that there

src/Init/Data/Vector/Basic.lean

@@ -506,16 +506,6 @@ Examples:
 @[inline, expose] def sum [Add α] [Zero α] (xs : Vector α n) : α :=
   xs.toArray.sum
 
-/--
-Computes the product of the elements of a vector.
-
-Examples:
- * `#v[a, b, c].prod = a * (b * (c * 1))`
- * `#v[1, 2, 5].prod = 10`
--/
-@[inline, expose] def prod [Mul α] [One α] (xs : Vector α n) : α :=
-  xs.toArray.prod
-
 /--
 Pad a vector on the left with a given element.
 

src/Init/Data/Vector/Int.lean

@@ -30,16 +30,4 @@ theorem sum_reverse_int (xs : Vector Int n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_int {xs : Vector Int n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
 
-@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
-  simp [← prod_toArray, Array.prod_replicate_int]
-
-theorem prod_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toArray]
-
-theorem prod_reverse_int (xs : Vector Int n) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_int {xs : Vector Int n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
-
 end Vector

src/Init/Data/Vector/Lemmas.lean

@@ -278,12 +278,6 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] {xs : Vector α n} :
     xs.toArray.sum = xs.sum := rfl
 
-@[simp] theorem prod_mk [Mul α] [One α] {xs : Array α} (h : xs.size = n) :
-    (Vector.mk xs h).prod = xs.prod := rfl
-
-@[simp, grind =] theorem prod_toArray [Mul α] [One α] {xs : Vector α n} :
-    xs.toArray.prod = xs.prod := rfl
-
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -557,10 +551,6 @@ theorem toArray_toList {xs : Vector α n} : xs.toList.toArray = xs.toArray := rf
     xs.toList.sum = xs.sum := by
   rw [← toList_toArray, Array.sum_toList, sum_toArray]
 
-@[simp, grind =] theorem prod_toList [Mul α] [One α] {xs : Vector α n} :
-    xs.toList.prod = xs.prod := by
-  rw [← toList_toArray, Array.prod_toList, prod_toArray]
-
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
@@ -3144,39 +3134,3 @@ theorem sum_eq_foldl [Zero α] [Add α]
     {xs : Vector α n} :
     xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
-
-/-! ### prod -/
-
-@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#v[] : Vector α 0).prod = 1 := rfl
-theorem prod_eq_foldr [Mul α] [One α] {xs : Vector α n} :
-    xs.prod = xs.foldr (b := 1) (· * ·) :=
-  rfl
-
-@[simp, grind =]
-theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LeftIdentity (α := α) (· * ·) 1] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    {as₁ as₂ : Vector α n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toList, List.prod_append]
-
-@[simp, grind =]
-theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
-    #v[x].prod = x := by
-  simp [← prod_toList, Std.LawfulRightIdentity.right_id x]
-
-@[simp, grind =]
-theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Vector α n} {x : α} :
-    (xs.push x).prod = xs.prod * x := by
-  simp [← prod_toArray]
-
-@[simp, grind =]
-theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.Commutative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Vector α n) : xs.reverse.prod = xs.prod := by
-  simp [← prod_toList, List.prod_reverse]
-
-theorem prod_eq_foldl [One α] [Mul α]
-    [Std.Associative (α := α) (· * ·)] [Std.LawfulIdentity (· * ·) (1 : α)]
-    {xs : Vector α n} :
-    xs.prod = xs.foldl (b := 1) (· * ·) := by
-  simp [← prod_toList, List.prod_eq_foldl]

src/Init/Data/Vector/Nat.lean

@@ -37,23 +37,4 @@ theorem sum_reverse_nat (xs : Vector Nat n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_nat {xs : Vector Nat n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
 
-protected theorem prod_pos_iff_forall_pos_nat {xs : Vector Nat n} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
-  simp [← prod_toArray, Array.prod_pos_iff_forall_pos_nat]
-
-protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Vector Nat n} :
-    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
-  simp [← prod_toArray, Array.prod_eq_zero_iff_exists_zero_nat]
-
-@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
-  simp [← prod_toArray, Array.prod_replicate_nat]
-
-theorem prod_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toArray]
-
-theorem prod_reverse_nat (xs : Vector Nat n) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_nat {xs : Vector Nat n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
-
 end Vector

src/Init/Prelude.lean

@@ -145,7 +145,7 @@ Examples:
 The constant function that ignores its argument.
 
 If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all
-arguments `b : β`, `Function.const β a b = a`. It is often written directly as `fun _ => a`.
+arguments `b : β`, `Function.const β a b = a`.
 
 Examples:
  * `Function.const Bool 10 true = 10`
@@ -3754,7 +3754,7 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) where
   /--
   Mapping a constant function.
 
-  Given `a : α` and `v : f β`, `mapConst a v` is equivalent to `(fun _ => a) <$> v`. For some
+  Given `a : α` and `v : f α`, `mapConst a v` is equivalent to `Function.const _ a <$> v`. For some
   functors, this can be implemented more efficiently; for all other functors, the default
   implementation may be used.
   -/

src/Init/System/IO.lean

@@ -1880,12 +1880,3 @@ lead to undefined behavior.
 -/
 @[extern "lean_runtime_forget"]
 def Runtime.forget (a : α) : BaseIO Unit := return
-
-set_option linter.unusedVariables false in
-/--
-Ensures `a` remains at least alive until the call site by holding a reference to `a`. This can be useful
-for unsafe code (such as an FFI) that relies on a Lean object not being freed until after some point
-in the program. At runtime, this will be a no-op as the C compiler will optimize away this call.
--/
-@[extern "lean_runtime_hold"]
-def Runtime.hold (a : @& α) : BaseIO Unit := return

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -67,7 +67,7 @@ structure ParamMap where
   The set of fvars that were already annotated as borrowed before arriving at this pass. We try to
   preserve the annotations here if possible.
   -/
-  annotatedBorrows : Std.HashSet FVarId := {}
+  annoatedBorrows : Std.HashSet FVarId := {}
 
 namespace ParamMap
 
@@ -95,7 +95,7 @@ where
         modify fun m =>
           { m with
             map := m.map.insert (.decl decl.name) (initParamsIfNotExported exported decl.params),
-            annotatedBorrows := decl.params.foldl (init := m.annotatedBorrows) fun acc p =>
+            annoatedBorrows := decl.params.foldl (init := m.annoatedBorrows) fun acc p =>
               if p.borrow then acc.insert p.fvarId else acc
           }
         goCode decl.name code
@@ -116,7 +116,7 @@ where
       modify fun m =>
         { m with
           map := m.map.insert (.jp declName decl.fvarId) (initParams decl.params),
-          annotatedBorrows := decl.params.foldl (init := m.annotatedBorrows) fun acc p =>
+          annoatedBorrows := decl.params.foldl (init := m.annoatedBorrows) fun acc p =>
             if p.borrow then acc.insert p.fvarId else acc
         }
       goCode declName decl.value
@@ -286,7 +286,7 @@ where
 
   ownFVar (fvarId : FVarId) (reason : OwnReason) : InferM Unit := do
     unless (← get).owned.contains fvarId do
-      if !reason.isForced && (← get).paramMap.annotatedBorrows.contains fvarId then
+      if !reason.isForced && (← get).paramMap.annoatedBorrows.contains fvarId then
         trace[Compiler.inferBorrow] "user annotation blocked owning {← PP.run <| PP.ppFVar fvarId}: {← reason.toString}"
       else
         trace[Compiler.inferBorrow] "own {← PP.run <| PP.ppFVar fvarId}: {← reason.toString}"

src/Lean/Compiler/LCNF/PassManager.lean

@@ -121,7 +121,7 @@ def mkPerDeclaration (name : Name) (phase : Phase)
   occurrence := occurrence
   phase := phase
   name := name
-  run := fun xs => xs.mapM fun decl => do checkSystem "LCNF compiler"; run decl
+  run := fun xs => xs.mapM run
 
 end Pass
 

src/Lean/Compiler/LCNF/ResetReuse.lean

@@ -28,7 +28,7 @@ inserts addition instructions to attempt to reuse the memory right away instead
 allocator.
 
 For this the paper defines three functions:
-- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be eligible for
+- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be elligible for
   reuse. For these variables it invokes `D`.
 - `D` which looks for code regions in which the target variable is dead (i.e. no longer read from),
   it then invokes `S`. If `S` succeeds it inserts a `reset` instruction to match the `reuse`

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -217,8 +217,6 @@ Simplify `code`
 -/
 partial def simp (code : Code .pure) : SimpM (Code .pure) := withIncRecDepth do
   incVisited
-  if (← get).visited % 128 == 0 then
-    checkSystem "LCNF simp"
   match code with
   | .let decl k =>
     let baseDecl := decl

src/Lean/Compiler/LCNF/SimpCase.lean

@@ -24,7 +24,7 @@ In particular we perform:
 - folding of the most common cases arm into the default arm if possible
 
 Note: Currently the simplifier still contains almost equivalent simplifications to the ones shown
-here. We know that this causes unforeseen behavior and do plan on changing it eventually.
+here. We know that this causes unforseen behavior and do plan on changing it eventually.
 -/
 
 -- TODO: the following functions are duplicated from simp and should be deleted in simp once we

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -171,7 +171,7 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
     if compiler.ignoreBorrowAnnotation.get (← getOptions) then
       decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
     if isExport env decl.name && decl.params.any (·.borrow) then
-      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to suppress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also suppress the annotations at the `extern` declaration."
+      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration."
     return decl
 
 end Lean.Compiler.LCNF

src/Lean/CoreM.lean

@@ -20,8 +20,6 @@ register_builtin_option diagnostics : Bool := {
   descr    := "collect diagnostic information"
 }
 
-builtin_initialize registerTraceClass `diagnostics
-
 register_builtin_option diagnostics.threshold : Nat := {
   defValue := 20
   descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
@@ -446,6 +444,10 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
   (·.1) <$> x.toIO ctx s
 
+/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/
+protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
+  controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
+
 /--
 Throws an internal interrupt exception if cancellation has been requested. The exception is not
 caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
@@ -460,12 +462,6 @@ heartbeat tracking (e.g. `SynthInstance`).
     if (← tk.isSet) then
       throwInterruptException
 
-/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`.
-Also checks for cancellation, so that recursive elaboration functions
-(inferType, whnf, isDefEq, …) respond promptly to interrupt requests. -/
-protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
-  controlAt CoreM fun runInBase => do checkInterrupted; withIncRecDepth (runInBase x)
-
 register_builtin_option debug.moduleNameAtTimeout : Bool := {
   defValue := true
   descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"

src/Lean/Elab/Deriving/Basic.lean

@@ -233,41 +233,27 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
         finally
           Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
   let env ← getEnv
-  let isPropType ← isProp result.type
-  if isPropType then
-    let decl ← mkThmOrUnsafeDef {
-      name := instName, levelParams := result.levelParams.toList,
-      type := result.type, value := result.value
-    }
-    addDecl decl
+  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+  let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
+  -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
+  -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
+  unless isNoncomputable || (← read).isNoncomputableSection || (← isProp result.type) do
+    let noncompRef? := preNormValue.foldConsts none fun n acc =>
+      acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
+    if let some noncompRef := noncompRef? then
+      if let some cmdRef := cmdRef? then
+        if let some origText := cmdRef.reprint then
+          let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
+          logInfoAt cmdRef m!"Try this: {newText}"
+      throwError "failed to derive instance because it depends on \
+        `{.ofConstName noncompRef}`, which is noncomputable"
+  if isNoncomputable || (← read).isNoncomputableSection then
+    addDecl <| Declaration.defnDecl decl
+    modifyEnv (addNoncomputable · instName)
   else
-    let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-    let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
-    -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
-    -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
-    unless isNoncomputable || (← read).isNoncomputableSection do
-      let noncompRef? := preNormValue.foldConsts none fun n acc =>
-        acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
-      if let some noncompRef := noncompRef? then
-        if let some cmdRef := cmdRef? then
-          if let some origText := cmdRef.reprint then
-            let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
-            logInfoAt cmdRef m!"Try this: {newText}"
-        throwError "failed to derive instance because it depends on \
-          `{.ofConstName noncompRef}`, which is noncomputable"
-    if isNoncomputable || (← read).isNoncomputableSection then
-      addDecl <| Declaration.defnDecl decl
-      modifyEnv (addNoncomputable · instName)
-    else
-      addAndCompile <| Declaration.defnDecl decl
+    addAndCompile <| Declaration.defnDecl decl
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
-  -- For Prop-typed instances (theorems), skip `implicit_reducible` since reducibility hints are
-  -- irrelevant for theorems. This matches the behavior of the handwritten `instance` command
-  -- (see `MutualDef.lean`).
-  if isPropType then
-    addInstance instName AttributeKind.global (eval_prio default)
-  else
-    registerInstance instName AttributeKind.global (eval_prio default)
+  registerInstance instName AttributeKind.global (eval_prio default)
   addDeclarationRangesFromSyntax instName (← getRef)
 
 end Term

src/Lean/Elab/Deriving/DecEq.lean

@@ -111,7 +111,7 @@ def mkMatchNew (ctx : Context) (header : Header) (indVal : InductiveVal) : TermE
   let x1 := mkIdent header.targetNames[0]!
   let x2 := mkIdent header.targetNames[1]!
   let ctorIdxName := mkCtorIdxName indVal.name
-  -- NB: the getMatcherInfo? assumes all matchers are called `match_`
+  -- NB: the getMatcherInfo? assumes all mathcers are called `match_`
   let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor)
   mkCasesOnSameCtor casesOnSameCtorName indVal.name
   let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do

src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean

@@ -36,7 +36,7 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
   TacticContext.new lratPath cfg
 
 /--
-Prepare an `Expr` that proves `bvExpr.unsat` using native evaluation.
+Prepare an `Expr` that proves `bvExpr.unsat` using native evalution.
 -/
 def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
   let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -357,7 +357,6 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   let mut sats := #[]
   let mut unusedHypotheses := {}
   for hyp in hyps do
-    checkSystem "bv_decide"
     if let (some reflected, lemmas) ← (SatAtBVLogical.of (mkFVar hyp)).run then
       sats := (sats ++ lemmas).push reflected
     else

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -33,7 +33,6 @@ where
   Reify `x`, returns `none` if the reification procedure failed.
   -/
   go (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
-    checkSystem "bv_decide"
     match_expr origExpr with
     | BitVec.ofNat _ _ => goBvLit origExpr
     | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
@@ -341,7 +340,6 @@ where
   Reify `t`, returns `none` if the reification procedure failed.
   -/
   go (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
-    checkSystem "bv_decide"
     match_expr origExpr with
     | Bool.true => ReifiedBVLogical.mkBoolConst true
     | Bool.false => ReifiedBVLogical.mkBoolConst false

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean

@@ -159,7 +159,6 @@ Repeatedly run a list of `Pass` until they either close the goal or an iteration
 the goal anymore.
 -/
 partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : PreProcessM (Option MVarId) := do
-  checkSystem "bv_decide"
   let mut newGoal := goal
   for pass in passes do
     if let some nextGoal ← pass.run newGoal then

src/Lean/Linter.lean

@@ -18,4 +18,3 @@ public import Lean.Linter.List
 public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
-public import Lean.Linter.GlobalAttributeIn

src/Lean/Linter/GlobalAttributeIn.lean

@@ -1,59 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
--/
-module
-
-prelude
-public import Lean.Elab.Command
-public import Lean.Linter.Basic
-
-
-namespace Lean.Linter
-open Elab.Command
-
-private structure TopDownSkipQuot where
-  stx : Syntax
-
-def topDownSkipQuot (stx : Syntax) : TopDownSkipQuot := ⟨stx⟩
-
-partial instance [Monad m] : ForIn m TopDownSkipQuot Syntax where
-  forIn := fun ⟨stx⟩ init f => do
-    let rec @[specialize] loop stx b [Inhabited (type_of% b)] := do
-      if stx.isQuot then return ForInStep.yield b
-      match (← f stx b) with
-      | ForInStep.yield b' =>
-        let mut b := b'
-        if let Syntax.node _ _ args := stx then
-          for arg in args do
-            match (← loop arg b) with
-            | ForInStep.yield b' => b := b'
-            | ForInStep.done b'  => return ForInStep.done b'
-        return ForInStep.yield b
-      | ForInStep.done b => return ForInStep.done b
-    match (← @loop stx init ⟨init⟩) with
-    | ForInStep.yield b => return b
-    | ForInStep.done b  => return b
-
-def getGlobalAttributesIn? : Syntax → Option (Ident × Array (TSyntax `attr))
-  | `(attribute [$x,*] $id in $_) =>
-    let xs := x.getElems.filterMap fun a => match a.raw with
-      | `(Parser.Command.eraseAttr| -$_) => none
-      | `(Parser.Term.attrInstance| local $_attr:attr) => none
-      | `(Parser.Term.attrInstance| scoped $_attr:attr) => none
-      | `(attr| $a) => some a
-    (id, xs)
-  | _ => default
-
-def globalAttributeIn : Linter where run := withSetOptionIn fun stx => do
-  for s in topDownSkipQuot stx do
-    if let some (id, nonScopedNorLocal) := getGlobalAttributesIn? s then
-      for attr in nonScopedNorLocal do
-        logErrorAt attr
-          m!"Despite the `in`, the attribute {attr} is added globally to {id}\n\
-          please remove the `in` or make this a `local {attr}`"
-
-builtin_initialize addLinter globalAttributeIn
-
-end Lean.Linter

src/Lean/Meta/ExprDefEq.lean

@@ -48,16 +48,6 @@ register_builtin_option backward.isDefEq.respectTransparency : Bool := {
   when checking whether implicit arguments are definitionally equal"
 }
 
-/--
-Controls the transparency used to check whether the type of metavariable matches the type of the
-term being assigned to it.
--/
-register_builtin_option backward.isDefEq.respectTransparency.types : Bool := {
-  defValue := false -- TODO: replace with `true` after we fix stage0
-  descr    := "if true, do not bump transparency to `.default` \
-  when checking whether the type of a metavariable matches the type of the term being assigned to it."
-}
-
 /--
 Controls whether *all* implicit arguments (not just instance-implicit `[..]`) get their
 transparency bumped to `TransparencyMode.instances` during `isDefEq`.
@@ -345,10 +335,10 @@ private def isDefEqArgsFirstPass
 
 /--
 Ensure `MetaM` configuration is strong enough for checking definitional equality of
-implicit arguments (e.g., instances) and types.
-For example, we must be able to unfold instances, `beta := true`, `proj := .yesWithDelta` are essential.
+instances. For example, we must be able to unfold instances, `beta := true`, `proj := .yesWithDelta`
+are essential.
 -/
-@[inline] def withImplicitConfig (x : MetaM α) : MetaM α :=
+@[inline] def withInstanceConfig (x : MetaM α) : MetaM α :=
   withAtLeastTransparency .instances do
     let cfg ← getConfig
     if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then
@@ -392,7 +382,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
       -- Bump to `.instances` so that `[implicit_reducible]` definitions (instances, `Nat.add`,
       -- `Array.size`, etc.) are unfolded. The user doesn't choose implicit arguments directly,
       -- so Lean should try harder than the caller's transparency to make them match.
-      unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
+      unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
     else if respectTransparency then
       unless (← Meta.isExprDefEqAux a₁ a₂) do return false
     else
@@ -402,7 +392,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     if respectTransparency && (implicitBump || finfo.paramInfo[i]!.isInstance) then
-      unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
+      unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
     else if !respectTransparency && finfo.paramInfo[i]!.isInstance then
       -- Old behavior
       unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
@@ -464,19 +454,6 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
   let lctx ← getLCtx
   isDefEqBindingAux lctx #[] a b #[]
 
-/--
-Returns `true` if both `backward.isDefEq.respectTransparency` and `backward.isDefEq.respectTransparency.types` is true.
-
-The option `backward.isDefEq.respectTransparency.types` is newer than ``backward.isDefEq.respectTransparency`,
-and is used to enable the transparency bump when checking metavariable assignments.
-
-If `backward.isDefEq.respectTransparency` is `false`, then we automatically disable
-`backward.isDefEq.respectTransparency.types` too.
--/
-abbrev respectTransparencyAtTypes : CoreM Bool := do
-  let opts ← getOptions
-  return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts
-
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
   withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
     if !mvar.isMVar then
@@ -485,24 +462,14 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
-      let vType ← inferType v
-      if (← respectTransparencyAtTypes) then
-        withImplicitConfig do
-          if (← Meta.isExprDefEqAux mvarType vType) then
-            mvar.mvarId!.assign v
-            return true
-          else
-            if (← isDiagnosticsEnabled) then withInferTypeConfig do
-              if (← Meta.isExprDefEqAux mvarType vType) then
-                trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.instances` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`"
-            return false
-      else
-        withInferTypeConfig do
-          if (← Meta.isExprDefEqAux mvarType vType) then
-            mvar.mvarId!.assign v
-            return true
-          else
-            return false
+      -- **TODO**: avoid transparency bump. Let's fix other issues first
+      withInferTypeConfig do
+        let vType ← inferType v
+        if (← Meta.isExprDefEqAux mvarType vType) then
+          mvar.mvarId!.assign v
+          pure true
+        else
+          pure false
 
 /--
 Auxiliary method for solving constraints of the form `?m xs := v`.
@@ -2095,7 +2062,7 @@ private def isDefEqProj : Expr → Expr → MetaM Bool
        for instance-implicit parameters. -/
     let fromClass := isClass (← getEnv) m
     let isDefEqStructArgs (x : MetaM Bool) : MetaM Bool :=
-      if fromClass then withImplicitConfig x else x
+      if fromClass then withInstanceConfig x else x
     if (← read).inTypeClassResolution then
       -- See comment at `inTypeClassResolution`
       pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s)

src/Lean/Meta/Match/Match.lean

@@ -33,12 +33,12 @@ The high-level overview of moves are
   * If there is an alternative, solve its constraints
   * Else use `contradiction` to prove completeness of the match
 * Process “independent prefixes” of patterns. These are patterns that can be processed without
-  affecting the other alternatives, and without side effects in the sense of updating the `mvarId`.
+  affecting the aother alternatives, and without side effects in the sense of updating the `mvarId`.
   These are
   - variable patterns; substitute
   - inaccessible patterns; add equality constraints
   - as-patterns: substitute value and equality
-  After these have been processed, we use `.inaccessible x` where `x` is the variable being matched
+  After thes have been processed, we use `.inaccessible x` where `x` is the variable being matched
   to mark them as “done”.
 * If all patterns start with “done”, drop the first variable
 * The first alt has only “done” patterns, drop remaining alts (they're overlapped)
@@ -1108,9 +1108,6 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) (isSplitte
       -- matcher bodies should always be exported, if not private anyway
       withExporting do
         addDecl decl
-      -- if `matcher` is not private, we mark it as `implicit_reducible` too
-      unless isPrivateName name do
-        setReducibilityStatus name .implicitReducible
       unless isSplitter do
         modifyEnv fun env => matcherExt.modifyState env fun s => s.insert key name
         addMatcherInfo name mi

src/Lean/Meta/Match/Rewrite.lean

@@ -17,7 +17,7 @@ namespace Lean.Meta
 
 /--
 Tries to rewrite the `ite`, `dite` or `cond` expression `e` with the hypothesis `hc`.
-If it fails, it returns a rewrite with `proof? := none` and unchanged expression.
+If it fails, it returns a rewrite with `proof? := none` and unchaged expression.
 -/
 def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
   match_expr e with

src/Lean/Meta/Native.lean

@@ -22,9 +22,9 @@ of that computation as an axiom towards the logic.
 -/
 
 public inductive NativeEqTrueResult where
-  /-- The given expression `e` evaluates to true. `prf` is a proof of `e = true`. -/
+  /-- The given expression `e` evalutes to true. `prf` is a proof of `e = true`. -/
   | success (prf : Expr)
-  /-- The given expression `e` evaluates to false. -/
+  /-- The given expression `e` evalutes to false. -/
   | notTrue
 
 /--

src/Lean/Meta/SameCtorUtils.lean

@@ -14,7 +14,7 @@ This module contains utilities for dealing with equalities between constructor a
 in particular about which fields must be the same a-priori for the equality to type check.
 
 Users include (or will include) the injectivity theorems, the per-constructor no-confusion
-construction and deriving type classes like `BEq`, `DecidableEq` or `Ord`.
+construction and deriving type classes lik `BEq`, `DecidableEq` or `Ord`.
 -/
 
 namespace Lean.Meta

src/Lean/Meta/Sym.lean

@@ -25,7 +25,6 @@ public import Lean.Meta.Sym.Simp
 public import Lean.Meta.Sym.Util
 public import Lean.Meta.Sym.Eta
 public import Lean.Meta.Sym.Canon
-public import Lean.Meta.Sym.Arith
 public import Lean.Meta.Sym.Grind
 public import Lean.Meta.Sym.SynthInstance
 

src/Lean/Meta/Sym/AbstractS.lean

@@ -97,16 +97,4 @@ public def mkLambdaFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
     let type ← abstractFVarsRange decl.type i xs
     mkLambdaS decl.userName decl.binderInfo type b
 
-/--
-Similar to `mkForallFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`,
-and makes the same assumption made by these functions.
--/
-public def mkForallFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
-  let b ← abstractFVars e xs
-  xs.size.foldRevM (init := b) fun i _ b => do
-    let x := xs[i]
-    let decl ← x.fvarId!.getDecl
-    let type ← abstractFVarsRange decl.type i xs
-    mkForallS decl.userName decl.binderInfo type b
-
 end Lean.Meta.Sym

src/Lean/Meta/Sym/AlphaShareBuilder.lean

@@ -189,48 +189,4 @@ def mkAppS₄ (f a₁ a₂ a₃ a₄ : Expr) : m Expr := do
 def mkAppS₅ (f a₁ a₂ a₃ a₄ a₅ : Expr) : m Expr := do
   mkAppS (← mkAppS₄ f a₁ a₂ a₃ a₄) a₅
 
-def mkAppS₆ (f a₁ a₂ a₃ a₄ a₅ a₆ : Expr) : m Expr := do
-  mkAppS (← mkAppS₅ f a₁ a₂ a₃ a₄ a₅) a₆
-
-def mkAppS₇ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ : Expr) : m Expr := do
-  mkAppS (← mkAppS₆ f a₁ a₂ a₃ a₄ a₅ a₆) a₇
-
-def mkAppS₈ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : Expr) : m Expr := do
-  mkAppS (← mkAppS₇ f a₁ a₂ a₃ a₄ a₅ a₆ a₇) a₈
-
-def mkAppS₉ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : Expr) : m Expr := do
-  mkAppS (← mkAppS₈ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈) a₉
-
-def mkAppS₁₀ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ : Expr) : m Expr := do
-  mkAppS (← mkAppS₉ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) a₁₀
-
-def mkAppS₁₁ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ a₁₁ : Expr) : m Expr := do
-  mkAppS (← mkAppS₁₀ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀) a₁₁
-
-/-- `mkAppRangeS f i j #[a₀, ..., aᵢ, ..., aⱼ, ...]` ==> `f aᵢ ... aⱼ₋₁` with max sharing. -/
-partial def mkAppRangeS (f : Expr) (beginIdx endIdx : Nat) (args : Array Expr) : m Expr :=
-  go endIdx f beginIdx
-where
-  go (endIdx : Nat) (b : Expr) (i : Nat) : m Expr := do
-    if endIdx ≤ i then return b
-    else go endIdx (← mkAppS b args[i]!) (i + 1)
-
-/-- `mkAppNS f #[a₀, ..., aₙ]` constructs `f a₀ ... aₙ` with max sharing. -/
-def mkAppNS (f : Expr) (args : Array Expr) : m Expr :=
-  mkAppRangeS f 0 args.size args
-
-/-- `mkAppRevRangeS f b e revArgs` ==> `mkAppRev f (revArgs.extract b e)` with max sharing. -/
-partial def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : m Expr :=
-  go revArgs beginIdx f endIdx
-where
-  go (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : m Expr := do
-    if i ≤ start then return b
-    else
-      let i := i - 1
-      go revArgs start (← mkAppS b revArgs[i]!) i
-
-/-- Same as `mkAppS f args` but reversing `args`, with max sharing. -/
-def mkAppRevS (f : Expr) (revArgs : Array Expr) : m Expr :=
-  mkAppRevRangeS f 0 revArgs.size revArgs
-
 end Lean.Meta.Sym.Internal

src/Lean/Meta/Sym/Arith.lean

@@ -1,20 +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.Arith.Types
-public import Lean.Meta.Sym.Arith.EvalNum
-public import Lean.Meta.Sym.Arith.Classify
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Sym.Arith.MonadRing
-public import Lean.Meta.Sym.Arith.MonadSemiring
-public import Lean.Meta.Sym.Arith.MonadVar
-public import Lean.Meta.Sym.Arith.Functions
-public import Lean.Meta.Sym.Arith.Reify
-public import Lean.Meta.Sym.Arith.DenoteExpr
-public import Lean.Meta.Sym.Arith.ToExpr
-public import Lean.Meta.Sym.Arith.VarRename
-public import Lean.Meta.Sym.Arith.Poly

src/Lean/Meta/Sym/Arith/Classify.lean

@@ -1,143 +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.Arith.EvalNum
-import Lean.Meta.Sym.SynthInstance
-import Lean.Meta.Sym.Canon
-import Lean.Meta.DecLevel
-import Init.Grind.Ring
-public section
-
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Algebraic structure classification
-
-Detects the strongest algebraic structure available for a type and caches
-the classification in `Arith.State.typeClassify`. The detection order is:
-
-1. `Grind.CommRing` (includes `Field` check)
-2. `Grind.Ring` (non-commutative)
-3. `Grind.CommSemiring` (via `OfSemiring.Q` envelope)
-4. `Grind.Semiring` (non-commutative)
-
-Results (including failures) are cached in a single `PHashMap ExprPtr ClassifyResult`
-to avoid repeated synthesis attempts.
--/
-
-private def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : SymM (Option (Expr × Nat)) := do
-  withNewMCtxDepth do
-    let n ← mkFreshExprMVar (mkConst ``Nat)
-    let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
-    let some charInst ← Sym.synthInstance? charType | return none
-    let n ← instantiateMVars n
-    let some n ← evalNat? n | return none
-    return some (charInst, n)
-
-private def getNoZeroDivInst? (u : Level) (type : Expr) : SymM (Option Expr) := do
-  let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
-  let some natModuleInst ← Sym.synthInstance? natModuleType | return none
-  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
-  Sym.synthInstance? noZeroDivType
-
-/-- Try to classify `type` as a `CommRing`. Returns the ring id on success. -/
-private def tryCommRing? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
-  let some commRingInst ← Sym.synthInstance? commRing | return none
-  let ringInst := mkApp2 (mkConst ``Grind.CommRing.toRing [u]) type commRingInst
-  let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
-  let commSemiringInst := mkApp2 (mkConst ``Grind.CommRing.toCommSemiring [u]) type semiringInst
-  let charInst? ← getIsCharInst? u type semiringInst
-  let noZeroDivInst? ← getNoZeroDivInst? u type
-  let fieldInst? ← Sym.synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
-  let semiringId? := none
-  let id := (← getArithState).rings.size
-  let ring : CommRing := {
-    id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-    commRingInst, charInst?, noZeroDivInst?, fieldInst?,
-  }
-  modifyArithState fun s => { s with rings := s.rings.push ring }
-  return some id
-
-/-- Try to classify `type` as a non-commutative `Ring`. -/
-private def tryNonCommRing? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let ring := mkApp (mkConst ``Grind.Ring [u]) type
-  let some ringInst ← Sym.synthInstance? ring | return none
-  let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
-  let charInst? ← getIsCharInst? u type semiringInst
-  let id := (← getArithState).ncRings.size
-  let ring : Ring := {
-    id, type, u, semiringInst, ringInst, charInst?
-  }
-  modifyArithState fun s => { s with ncRings := s.ncRings.push ring }
-  return some id
-
-/-- Helper function for `tryCommSemiring? -/
-private def tryCacheAndCommRing? (type : Expr) : SymM (Option Nat) := do
-  if let some result := (← getArithState).typeClassify.find? { expr := type } then
-    let .commRing id := result | return none
-    return id
-  let id? ← tryCommRing? type
-  let result := match id? with
-    | none => .none
-    | some id => .commRing id
-  modifyArithState fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-  return id?
-
-/-- Try to classify `type` as a `CommSemiring`. Creates the `OfSemiring.Q` envelope ring. -/
-private def tryCommSemiring? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
-  let some commSemiringInst ← Sym.synthInstance? commSemiring | return none
-  let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
-  let q ← shareCommon (← Sym.canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
-  -- The envelope `Q` type must be classifiable as a CommRing.
-  let some ringId ← tryCacheAndCommRing? q
-    | reportIssue! "unexpected failure initializing ring{indentExpr q}"; return none
-  let id := (← getArithState).semirings.size
-  let semiring : CommSemiring := {
-    id, type, ringId, u, semiringInst, commSemiringInst
-  }
-  modifyArithState fun s => { s with semirings := s.semirings.push semiring }
-  -- Link the envelope ring back to this semiring
-  modifyArithState fun s =>
-    let rings := s.rings.modify ringId fun r => { r with semiringId? := some id }
-    { s with rings }
-  return some id
-
-/-- Try to classify `type` as a non-commutative `Semiring`. -/
-private def tryNonCommSemiring? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let semiring := mkApp (mkConst ``Grind.Semiring [u]) type
-  let some semiringInst ← Sym.synthInstance? semiring | return none
-  let id := (← getArithState).ncSemirings.size
-  let semiring : Semiring := { id, type, u, semiringInst }
-  modifyArithState fun s => { s with ncSemirings := s.ncSemirings.push semiring }
-  return some id
-
-/--
-Classify the algebraic structure of `type`, trying the strongest first:
-CommRing > Ring > CommSemiring > Semiring.
-Results are cached in `Arith.State.typeClassify`.
--/
-def classify? (type : Expr) : SymM ClassifyResult := do
-  if let some result := (← getArithState).typeClassify.find? { expr := type } then
-    return result
-  let result ← go
-  modifyArithState fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-  return result
-where
-  go : SymM ClassifyResult := do
-    if let some id ← tryCommRing? type then return .commRing id
-    if let some id ← tryNonCommRing? type then return .nonCommRing id
-    if let some id ← tryCommSemiring? type then return .commSemiring id
-    if let some id ← tryNonCommSemiring? type then return .nonCommSemiring id
-    return .none
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/DenoteExpr.lean

@@ -1,93 +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.Arith.Functions
-public import Lean.Meta.Sym.Arith.MonadVar
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Denotation of reified expressions
-
-Converts reified `RingExpr`, `Poly`, `Mon`, `Power` back into Lean `Expr`s using
-the ring's cached operator functions and variable array.
--/
-
-variable [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m]
-
-/-- Convert an integer to a numeral expression in the ring. Negative values use `getNegFn`. -/
-def denoteNum (k : Int) : m Expr := do
-  let ring ← getRing
-  let n := mkRawNatLit k.natAbs
-  let ofNatInst ← if let some inst ← MonadCanon.synthInstance? (mkApp2 (mkConst ``OfNat [ring.u]) ring.type n) then
-    pure inst
-  else
-    pure <| mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
-  let e := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
-  if k < 0 then
-    return mkApp (← getNegFn) e
-  else
-    return e
-
-/-- Denote a `Power` (variable raised to a power). -/
-def denotePower [MonadGetVar m] (pw : Power) : m Expr := do
-  let x ← getVar pw.x
-  if pw.k == 1 then
-    return x
-  else
-    return mkApp2 (← getPowFn) x (toExpr pw.k)
-
-/-- Denote a `Mon` (product of powers). -/
-def denoteMon [MonadGetVar m] (mn : Mon) : m Expr := do
-  match mn with
-  | .unit => denoteNum 1
-  | .mult pw mn => go mn (← denotePower pw)
-where
-  go (mn : Mon) (acc : Expr) : m Expr := do
-    match mn with
-    | .unit => return acc
-    | .mult pw mn => go mn (mkApp2 (← getMulFn) acc (← denotePower pw))
-
-/-- Denote a `Poly` (sum of coefficient × monomial terms). -/
-def denotePoly [MonadGetVar m] (p : Poly) : m Expr := do
-  match p with
-  | .num k => denoteNum k
-  | .add k mn p => go p (← denoteTerm k mn)
-where
-  denoteTerm (k : Int) (mn : Mon) : m Expr := do
-    if k == 1 then
-      denoteMon mn
-    else
-      return mkApp2 (← getMulFn) (← denoteNum k) (← denoteMon mn)
-
-  go (p : Poly) (acc : Expr) : m Expr := do
-    match p with
-    | .num 0 => return acc
-    | .num k => return mkApp2 (← getAddFn) acc (← denoteNum k)
-    | .add k mn p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k mn))
-
-/-- Denote a `RingExpr` using a variable lookup function. -/
-@[specialize]
-private def denoteRingExprCore (getVarExpr : Nat → Expr) (e : RingExpr) : m Expr := do
-  go e
-where
-  go : RingExpr → m Expr
-  | .num k => denoteNum k
-  | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
-  | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
-  | .var x => return getVarExpr x
-  | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
-  | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)
-  | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
-  | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
-  | .neg a => return mkApp (← getNegFn) (← go a)
-
-/-- Denote a `RingExpr` using an explicit variable array. -/
-def denoteRingExpr (vars : Array Expr) (e : RingExpr) : m Expr := do
-  denoteRingExprCore (fun x => vars[x]!) e
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/EvalNum.lean

@@ -1,90 +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.Arith.Types
-import Lean.Meta.Sym.LitValues
-import Lean.Meta.IntInstTesters
-import Lean.Meta.NatInstTesters
-public section
-
-namespace Lean.Meta.Sym.Arith
-
-/-!
-Functions for evaluating simple `Nat` and `Int` expressions that appear in type classes
-(e.g., `ToInt` and `IsCharP`). Using `whnf` for this purpose is too expensive and can
-exhaust the stack. We considered `evalExpr` as an alternative, but it introduces
-considerable overhead. We may use `evalExpr` as a fallback in the future.
--/
-
-def checkExp (k : Nat) : OptionT SymM Unit := do
-  let exp ← getExpThreshold
-  if k > exp then
-    reportIssue! "exponent {k} exceeds threshold for exponentiation `(exp := {exp})`"
-    failure
-
-/-
-**Note**: It is safe to use (the more efficient) structural instance tests here because
-`Sym.Canon` has already run.
--/
-open Structural in
-mutual
-private partial def evalNatCore (e : Expr) : OptionT SymM Nat := do
-  match_expr e with
-  | Nat.zero => return 0
-  | Nat.succ a => return (← evalNatCore a) + 1
-  | Int.toNat a => return (← evalIntCore a).toNat
-  | Int.natAbs a => return (← evalIntCore a).natAbs
-  | HAdd.hAdd _ _ _ inst a b => guard (← isInstHAddNat inst); return (← evalNatCore a) + (← evalNatCore b)
-  | HMul.hMul _ _ _ inst a b => guard (← isInstHMulNat inst); return (← evalNatCore a) * (← evalNatCore b)
-  | HSub.hSub _ _ _ inst a b => guard (← isInstHSubNat inst); return (← evalNatCore a) - (← evalNatCore b)
-  | HDiv.hDiv _ _ _ inst a b => guard (← isInstHDivNat inst); return (← evalNatCore a) / (← evalNatCore b)
-  | HMod.hMod _ _ _ inst a b => guard (← isInstHModNat inst); return (← evalNatCore a) % (← evalNatCore b)
-  | OfNat.ofNat _ _ _ =>
-    let some n := Sym.getNatValue? e |>.run | failure
-    return n
-  | HPow.hPow _ _ _ inst a k =>
-    guard (← isInstHPowNat inst)
-    let k ← evalNatCore k
-    checkExp k
-    let a ← evalNatCore a
-    return a ^ k
-  | _ => failure
-
-private partial def evalIntCore (e : Expr) : OptionT SymM Int := do
-  match_expr e with
-  | Neg.neg _ i a => guard (← isInstNegInt i); return - (← evalIntCore a)
-  | HAdd.hAdd _ _ _ i a b => guard (← isInstHAddInt i); return (← evalIntCore a) + (← evalIntCore b)
-  | HSub.hSub _ _ _ i a b => guard (← isInstHSubInt i); return (← evalIntCore a) - (← evalIntCore b)
-  | HMul.hMul _ _ _ i a b => guard (← isInstHMulInt i); return (← evalIntCore a) * (← evalIntCore b)
-  | HDiv.hDiv _ _ _ i a b => guard (← isInstHDivInt i); return (← evalIntCore a) / (← evalIntCore b)
-  | HMod.hMod _ _ _ i a b => guard (← isInstHModInt i); return (← evalIntCore a) % (← evalIntCore b)
-  | HPow.hPow _ _ _ i a k =>
-    guard (← isInstHPowInt i)
-    let a ← evalIntCore a
-    let k ← evalNatCore k
-    checkExp k
-    return a ^ k
-  | OfNat.ofNat _ _ _ =>
-    let some n := Sym.getIntValue? e |>.run | failure
-    return n
-  | NatCast.natCast _ i a =>
-    let_expr instNatCastInt ← i | failure
-    return (← evalNatCore a)
-  | Nat.cast _ i a =>
-    let_expr instNatCastInt ← i | failure
-    return (← evalNatCore a)
-  | _ => failure
-
-end
-
-def evalNat? (e : Expr) : SymM (Option Nat) :=
-  evalNatCore e |>.run
-
-def evalInt? (e : Expr) : SymM (Option Int) :=
-  evalIntCore e |>.run
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Functions.lean

@@ -1,171 +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.Arith.MonadRing
-public import Lean.Meta.Sym.Arith.MonadSemiring
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Cached function expressions for arithmetic operators
-
-Synthesizes and caches the canonical Lean expressions for arithmetic operators
-(`+`, `*`, `-`, `^`, `intCast`, `natCast`, etc.). These cached expressions are used
-during reification to validate instances via pointer equality (`isSameExpr`).
-
-Each getter checks the cache field first. On a miss, it synthesizes the instance,
-verifies it against the expected instance from the ring structure using `isDefEqI`,
-canonicalizes the result via `canonExpr`, and stores it.
--/
-
-variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
-
-private def checkInst (declName : Name) (inst inst' : Expr) : MetaM Unit := do
-  unless (← withReducibleAndInstances <| isDefEq inst inst') do
-    throwError "error while initializing arithmetic operators:\ninstance for `{declName}` {indentExpr inst}\nis not definitionally equal to the expected one {indentExpr inst'}\nwhen only reducible definitions and instances are reduced"
-
-private def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp (mkConst instDeclName [u]) type
-  checkInst declName inst expectedInst
-  canonExpr <| mkApp2 (mkConst declName [u]) type inst
-
-private def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
-  checkInst declName inst expectedInst
-  canonExpr <| mkApp4 (mkConst declName [u, u, u]) type type type inst
-
-private def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.npow [u]) type semiringInst
-  checkInst ``HPow.hPow inst inst'
-  canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
-
-private def mkNatCastFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.natCast [u]) type semiringInst
-  let instType := mkApp (mkConst ``NatCast [u]) type
-  -- Note: `Semiring.natCast` is not a global instance, so `NatCast α` may not be available.
-  -- When present, verify defeq; otherwise fall back to the semiring field.
-  let inst ← match (← MonadCanon.synthInstance? instType) with
-  | none => pure inst'
-  | some inst => checkInst ``NatCast.natCast inst inst'; pure inst
-  canonExpr <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
-
-section RingFns
-variable [MonadRing m]
-
-def getAddFn : m Expr := do
-  let ring ← getRing
-  if let some addFn := ring.addFn? then return addFn
-  let expectedInst := mkApp2 (mkConst ``instHAdd [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [ring.u]) ring.type ring.semiringInst
-  let addFn ← mkBinHomoFn ring.type ring.u ``HAdd ``HAdd.hAdd expectedInst
-  modifyRing fun s => { s with addFn? := some addFn }
-  return addFn
-
-def getMulFn : m Expr := do
-  let ring ← getRing
-  if let some mulFn := ring.mulFn? then return mulFn
-  let expectedInst := mkApp2 (mkConst ``instHMul [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [ring.u]) ring.type ring.semiringInst
-  let mulFn ← mkBinHomoFn ring.type ring.u ``HMul ``HMul.hMul expectedInst
-  modifyRing fun s => { s with mulFn? := some mulFn }
-  return mulFn
-
-def getSubFn : m Expr := do
-  let ring ← getRing
-  if let some subFn := ring.subFn? then return subFn
-  let expectedInst := mkApp2 (mkConst ``instHSub [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Ring.toSub [ring.u]) ring.type ring.ringInst
-  let subFn ← mkBinHomoFn ring.type ring.u ``HSub ``HSub.hSub expectedInst
-  modifyRing fun s => { s with subFn? := some subFn }
-  return subFn
-
-def getNegFn : m Expr := do
-  let ring ← getRing
-  if let some negFn := ring.negFn? then return negFn
-  let expectedInst := mkApp2 (mkConst ``Grind.Ring.toNeg [ring.u]) ring.type ring.ringInst
-  let negFn ← mkUnaryFn ring.type ring.u ``Neg ``Neg.neg expectedInst
-  modifyRing fun s => { s with negFn? := some negFn }
-  return negFn
-
-def getPowFn : m Expr := do
-  let ring ← getRing
-  if let some powFn := ring.powFn? then return powFn
-  let powFn ← mkPowFn ring.u ring.type ring.semiringInst
-  modifyRing fun s => { s with powFn? := some powFn }
-  return powFn
-
-def getIntCastFn : m Expr := do
-  let ring ← getRing
-  if let some intCastFn := ring.intCastFn? then return intCastFn
-  let inst' := mkApp2 (mkConst ``Grind.Ring.intCast [ring.u]) ring.type ring.ringInst
-  let instType := mkApp (mkConst ``IntCast [ring.u]) ring.type
-  -- Note: `Ring.intCast` is not a global instance. Same pattern as `mkNatCastFn`.
-  let inst ← match (← MonadCanon.synthInstance? instType) with
-    | none => pure inst'
-    | some inst => checkInst ``Int.cast inst inst'; pure inst
-  let intCastFn ← canonExpr <| mkApp2 (mkConst ``IntCast.intCast [ring.u]) ring.type inst
-  modifyRing fun s => { s with intCastFn? := some intCastFn }
-  return intCastFn
-
-def getNatCastFn : m Expr := do
-  let ring ← getRing
-  if let some natCastFn := ring.natCastFn? then return natCastFn
-  let natCastFn ← mkNatCastFn ring.u ring.type ring.semiringInst
-  modifyRing fun s => { s with natCastFn? := some natCastFn }
-  return natCastFn
-
-end RingFns
-
-section CommRingFns
-variable [MonadCommRing m]
-
-def getInvFn : m Expr := do
-  let ring ← getCommRing
-  let some fieldInst := ring.fieldInst?
-    | throwError "internal error: type is not a field{indentExpr ring.type}"
-  if let some invFn := ring.invFn? then return invFn
-  let expectedInst := mkApp2 (mkConst ``Grind.Field.toInv [ring.u]) ring.type fieldInst
-  let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv expectedInst
-  modifyCommRing fun s => { s with invFn? := some invFn }
-  return invFn
-
-end CommRingFns
-
-section SemiringFns
-variable [MonadSemiring m]
-
-def getAddFn' : m Expr := do
-  let sr ← getSemiring
-  if let some addFn := sr.addFn? then return addFn
-  let expectedInst := mkApp2 (mkConst ``instHAdd [sr.u]) sr.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [sr.u]) sr.type sr.semiringInst
-  let addFn ← mkBinHomoFn sr.type sr.u ``HAdd ``HAdd.hAdd expectedInst
-  modifySemiring fun s => { s with addFn? := some addFn }
-  return addFn
-
-def getMulFn' : m Expr := do
-  let sr ← getSemiring
-  if let some mulFn := sr.mulFn? then return mulFn
-  let expectedInst := mkApp2 (mkConst ``instHMul [sr.u]) sr.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [sr.u]) sr.type sr.semiringInst
-  let mulFn ← mkBinHomoFn sr.type sr.u ``HMul ``HMul.hMul expectedInst
-  modifySemiring fun s => { s with mulFn? := some mulFn }
-  return mulFn
-
-def getPowFn' : m Expr := do
-  let sr ← getSemiring
-  if let some powFn := sr.powFn? then return powFn
-  let powFn ← mkPowFn sr.u sr.type sr.semiringInst
-  modifySemiring fun s => { s with powFn? := some powFn }
-  return powFn
-
-def getNatCastFn' : m Expr := do
-  let sr ← getSemiring
-  if let some natCastFn := sr.natCastFn? then return natCastFn
-  let natCastFn ← mkNatCastFn sr.u sr.type sr.semiringInst
-  modifySemiring fun s => { s with natCastFn? := some natCastFn }
-  return natCastFn
-
-end SemiringFns
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadRing.lean

@@ -1,39 +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.Arith.MonadCanon
-public section
-namespace Lean.Meta.Sym.Arith
-
-class MonadRing (m : Type → Type) where
-  getRing : m Ring
-  modifyRing : (Ring → Ring) → m Unit
-
-export MonadRing (getRing modifyRing)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadRing m] : MonadRing n where
-  getRing    := liftM (getRing : m Ring)
-  modifyRing f := liftM (modifyRing f : m Unit)
-
-class MonadCommRing (m : Type → Type) where
-  getCommRing : m CommRing
-  modifyCommRing : (CommRing → CommRing) → m Unit
-
-export MonadCommRing (getCommRing modifyCommRing)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCommRing m] : MonadCommRing n where
-  getCommRing      := liftM (getCommRing : m CommRing)
-  modifyCommRing f := liftM (modifyCommRing f : m Unit)
-
-@[always_inline]
-instance (m) [Monad m] [MonadCommRing m] : MonadRing m where
-  getRing := return (← getCommRing).toRing
-  modifyRing f := modifyCommRing fun s => { s with toRing := f s.toRing }
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadSemiring.lean

@@ -1,39 +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.Arith.MonadCanon
-public section
-namespace Lean.Meta.Sym.Arith
-
-class MonadSemiring (m : Type → Type) where
-  getSemiring : m Semiring
-  modifySemiring : (Semiring → Semiring) → m Unit
-
-export MonadSemiring (getSemiring modifySemiring)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadSemiring m] : MonadSemiring n where
-  getSemiring    := liftM (getSemiring : m Semiring)
-  modifySemiring f := liftM (modifySemiring f : m Unit)
-
-class MonadCommSemiring (m : Type → Type) where
-  getCommSemiring : m CommSemiring
-  modifyCommSemiring : (CommSemiring → CommSemiring) → m Unit
-
-export MonadCommSemiring (getCommSemiring modifyCommSemiring)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCommSemiring m] : MonadCommSemiring n where
-  getCommSemiring      := liftM (getCommSemiring : m CommSemiring)
-  modifyCommSemiring f := liftM (modifyCommSemiring f : m Unit)
-
-@[always_inline]
-instance (m) [Monad m] [MonadCommSemiring m] : MonadSemiring m where
-  getSemiring := return (← getCommSemiring).toSemiring
-  modifySemiring f := modifyCommSemiring fun s => { s with toSemiring := f s.toSemiring }
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadVar.lean

@@ -1,32 +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.Arith.Types
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-- Read a variable's Lean expression by index. Used by `DenoteExpr` and diagnostics (PP). -/
-class MonadGetVar (m : Type → Type) where
-  getVar : Var → m Expr
-
-export MonadGetVar (getVar)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadGetVar m] : MonadGetVar n where
-  getVar x := liftM (getVar x : m Expr)
-
-/-- Create or lookup a variable for a Lean expression. Used by reification. -/
-class MonadMkVar (m : Type → Type) where
-  mkVar : Expr → m Var
-
-export MonadMkVar (mkVar)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadMkVar m] : MonadMkVar n where
-  mkVar e := liftM (mkVar e : m Var)
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Reify.lean

@@ -1,205 +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.Arith.Functions
-public import Lean.Meta.Sym.Arith.MonadVar
-public import Lean.Meta.Sym.LitValues
-public section
-namespace Lean.Meta.Sym.Arith
-open Sym.Arith (MonadCanon)
-
-/-!
-# Reification of arithmetic expressions
-
-Converts Lean expressions into `CommRing.Expr` (ring) or `CommSemiring.Expr`
-(semiring) for reflection-based normalization.
-
-Instance validation uses pointer equality (`isSameExpr`) against cached function
-expressions from `Functions.lean`.
-
-## Differences from grind's `Reify.lean`
-
-- Uses `MonadMkVar` for variable creation instead of grind's `internalize` + `mkVarCore`
-- Uses `Sym.getNatValue?`/`Sym.getIntValue?` (pure) instead of `MetaM` versions
-- No `MonadSetTermId` — term-to-ring-id tracking is grind-specific
--/
-
-section RingReify
-
-variable [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] [MonadMkVar m]
-
-def isAddInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getAddFn).appArg! inst
-def isMulInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getMulFn).appArg! inst
-def isSubInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getSubFn).appArg! inst
-def isNegInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getNegFn).appArg! inst
-def isPowInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getPowFn).appArg! inst
-def isIntCastInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getIntCastFn).appArg! inst
-def isNatCastInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getNatCastFn).appArg! inst
-
-private def reportRingAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
-  reportIssue! "ring term with unexpected instance{indentExpr e}"
-
-/--
-Converts a Lean expression `e` into a `RingExpr`.
-
-If `skipVar` is `true`, returns `none` if `e` is not an interpreted ring term
-(used for equalities/disequalities). If `false`, treats non-interpreted terms
-as variables (used for inequalities).
--/
-partial def reifyRing? (e : Expr) (skipVar : Bool := true) : m (Option RingExpr) := do
-  let toVar (e : Expr) : m RingExpr := do
-    return .var (← mkVar e)
-  let asVar (e : Expr) : m RingExpr := do
-    reportRingAppIssue e
-    return .var (← mkVar e)
-  let rec go (e : Expr) : m RingExpr := do
-    match_expr e with
-    | HAdd.hAdd _ _ _ i a b =>
-      if (← isAddInst i) then return .add (← go a) (← go b) else asVar e
-    | HMul.hMul _ _ _ i a b =>
-      if (← isMulInst i) then return .mul (← go a) (← go b) else asVar e
-    | HSub.hSub _ _ _ i a b =>
-      if (← isSubInst i) then return .sub (← go a) (← go b) else asVar e
-    | HPow.hPow _ _ _ i a b =>
-      let some k := Sym.getNatValue? b |>.run | toVar e
-      if (← isPowInst i) then return .pow (← go a) k else asVar e
-    | Neg.neg _ i a =>
-      if (← isNegInst i) then return .neg (← go a) else asVar e
-    | IntCast.intCast _ i a =>
-      if (← isIntCastInst i) then
-        let some k := Sym.getIntValue? a |>.run | toVar e
-        return .intCast k
-      else
-        asVar e
-    | NatCast.natCast _ i a =>
-      if (← isNatCastInst i) then
-        let some k := Sym.getNatValue? a |>.run | toVar e
-        return .natCast k
-      else
-        asVar e
-    | OfNat.ofNat _ n _ =>
-      /-
-      **Note**: We extract `n` directly as a raw nat literal. The grind version uses `MetaM`'s
-      `getNatValue?` which handles multiple encodings (raw literals, nested `OfNat`, etc.).
-      In `SymM`, we assume terms have been canonicalized by `Sym.canon` before reification,
-      so `OfNat.ofNat _ n _` always has a raw nat literal at position 1.
-      -/
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | BitVec.ofNat _ n =>
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | _ => toVar e
-  let toTopVar (e : Expr) : m (Option RingExpr) := do
-    if skipVar then
-      return none
-    else
-      return some (← toVar e)
-  let asTopVar (e : Expr) : m (Option RingExpr) := do
-    reportRingAppIssue e
-    toTopVar e
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if (← isAddInst i) then return some (.add (← go a) (← go b)) else asTopVar e
-  | HMul.hMul _ _ _ i a b =>
-    if (← isMulInst i) then return some (.mul (← go a) (← go b)) else asTopVar e
-  | HSub.hSub _ _ _ i a b =>
-    if (← isSubInst i) then return some (.sub (← go a) (← go b)) else asTopVar e
-  | HPow.hPow _ _ _ i a b =>
-    let some k := Sym.getNatValue? b |>.run | asTopVar e
-    if (← isPowInst i) then return some (.pow (← go a) k) else asTopVar e
-  | Neg.neg _ i a =>
-    if (← isNegInst i) then return some (.neg (← go a)) else asTopVar e
-  | IntCast.intCast _ i a =>
-    if (← isIntCastInst i) then
-      let some k := Sym.getIntValue? a |>.run | toTopVar e
-      return some (.intCast k)
-    else
-      asTopVar e
-  | NatCast.natCast _ i a =>
-    if (← isNatCastInst i) then
-      let some k := Sym.getNatValue? a |>.run | toTopVar e
-      return some (.natCast k)
-    else
-      asTopVar e
-  | OfNat.ofNat _ n _ =>
-    let .lit (.natVal k) := n | asTopVar e
-    return some (.num k)
-  | _ => toTopVar e
-
-end RingReify
-
-section SemiringReify
-
-variable [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] [MonadMkVar m]
-
-private def reportSemiringAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
-  reportIssue! "semiring term with unexpected instance{indentExpr e}"
-
-/--
-Converts a Lean expression `e` into a `SemiringExpr`.
-Only recognizes `add`, `mul`, `pow`, `natCast`, and numerals (no `sub`, `neg`, `intCast`).
--/
-partial def reifySemiring? (e : Expr) : m (Option SemiringExpr) := do
-  let toVar (e : Expr) : m SemiringExpr := do
-    return .var (← mkVar e)
-  let asVar (e : Expr) : m SemiringExpr := do
-    reportSemiringAppIssue e
-    return .var (← mkVar e)
-  let rec go (e : Expr) : m SemiringExpr := do
-    match_expr e with
-    | HAdd.hAdd _ _ _ i a b =>
-      if isSameExpr (← getAddFn').appArg! i then return .add (← go a) (← go b) else asVar e
-    | HMul.hMul _ _ _ i a b =>
-      if isSameExpr (← getMulFn').appArg! i then return .mul (← go a) (← go b) else asVar e
-    | HPow.hPow _ _ _ i a b =>
-      let some k := Sym.getNatValue? b |>.run | toVar e
-      if isSameExpr (← getPowFn').appArg! i then return .pow (← go a) k else asVar e
-    | NatCast.natCast _ i a =>
-      if isSameExpr (← getNatCastFn').appArg! i then
-        let some k := Sym.getNatValue? a |>.run | toVar e
-        return .num k
-      else
-        asVar e
-    | OfNat.ofNat _ n _ =>
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | _ => toVar e
-  let toTopVar (e : Expr) : m (Option SemiringExpr) := do
-    return some (← toVar e)
-  let asTopVar (e : Expr) : m (Option SemiringExpr) := do
-    reportSemiringAppIssue e
-    toTopVar e
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if isSameExpr (← getAddFn').appArg! i then return some (.add (← go a) (← go b)) else asTopVar e
-  | HMul.hMul _ _ _ i a b =>
-    if isSameExpr (← getMulFn').appArg! i then return some (.mul (← go a) (← go b)) else asTopVar e
-  | HPow.hPow _ _ _ i a b =>
-    let some k := Sym.getNatValue? b |>.run | return none
-    if isSameExpr (← getPowFn').appArg! i then return some (.pow (← go a) k) else asTopVar e
-  | NatCast.natCast _ i a =>
-    if isSameExpr (← getNatCastFn').appArg! i then
-      let some k := Sym.getNatValue? a |>.run | toTopVar e
-      return some (.num k)
-    else
-      asTopVar e
-  | OfNat.ofNat _ n _ =>
-    let .lit (.natVal k) := n | asTopVar e
-    return some (.num k)
-  | _ => toTopVar e
-
-end SemiringReify
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Types.lean

@@ -1,137 +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 Init.Grind.Ring.CommSemiringAdapter
-public import Lean.Meta.Sym.SymM
-public section
-
-namespace Lean.Meta.Sym.Arith
-export Lean.Grind.CommRing (Var Power Mon Poly)
-abbrev RingExpr := Grind.CommRing.Expr
-/-
-**Note**: recall that we use ring expressions to represent semiring expressions,
-and ignore non-applicable constructors.
--/
-abbrev SemiringExpr := Grind.CommRing.Expr
-
-/-- Classification state for a type with a `Semiring` instance. -/
-structure Semiring where
-  id             : Nat
-  type           : Expr
-  /-- Cached `getDecLevel type` -/
-  u              : Level
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
-  addFn?         : Option Expr := none
-  mulFn?         : Option Expr := none
-  powFn?         : Option Expr := none
-  natCastFn?     : Option Expr := none
-  deriving Inhabited
-
-/-- Classification state for a type with a `Ring` instance. -/
-structure Ring where
-  id             : Nat
-  type           : Expr
-  /-- Cached `getDecLevel type` -/
-  u              : Level
-  /-- `Ring` instance for `type` -/
-  ringInst       : Expr
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
-  /-- `IsCharP` instance for `type` if available. -/
-  charInst?      : Option (Expr × Nat)
-  addFn?         : Option Expr := none
-  mulFn?         : Option Expr := none
-  subFn?         : Option Expr := none
-  negFn?         : Option Expr := none
-  powFn?         : Option Expr := none
-  intCastFn?     : Option Expr := none
-  natCastFn?     : Option Expr := none
-  one?           : Option Expr := none
-  deriving Inhabited
-
-/-- Classification state for a type with a `CommRing` instance. -/
-structure CommRing extends Ring where
-  /-- Inverse function if `fieldInst?` is `some inst` -/
-  invFn?             : Option Expr := none
-  /--
-  If this is a `OfSemiring.Q α` ring, this field contains the
-  `semiringId` for `α`.
-  -/
-  semiringId?        : Option Nat
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `CommRing` instance for `type` -/
-  commRingInst       : Expr
-  /-- `NoNatZeroDivisors` instance for `type` if available. -/
-  noZeroDivInst?     : Option Expr
-  /-- `Field` instance for `type` if available. -/
-  fieldInst?         : Option Expr
-  deriving Inhabited
-
-/--
-Classification state for a type with a `CommSemiring` instance.
-Recall that `CommSemiring` types are normalized using the `OfSemiring.Q` envelope.
--/
-structure CommSemiring extends Semiring where
-  /-- Id of the envelope ring `OfSemiring.Q type` -/
-  ringId             : Nat
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `AddRightCancel` instance for `type` if available. -/
-  addRightCancelInst? : Option (Option Expr) := none
-  toQFn?             : Option Expr := none
-  deriving Inhabited
-
-/-- Result of classifying a type's algebraic structure. -/
-inductive ClassifyResult where
-  | commRing (id : Nat)
-  | nonCommRing (id : Nat)
-  | commSemiring (id : Nat)
-  | nonCommSemiring (id : Nat)
-  | /-- No algebraic structure found. -/ none
-  deriving Inhabited
-
-/-- Arith type classification state, stored as a `SymExtension`. -/
-structure State where
-  /-- Exponent threshold for `HPow` evaluation. -/
-  exp            : Nat := 8
-  /-- Commutative rings. -/
-  rings          : Array CommRing := {}
-  /-- Commutative semirings. -/
-  semirings      : Array CommSemiring := {}
-  /-- Non-commutative rings. -/
-  ncRings        : Array Ring := {}
-  /-- Non-commutative semirings. -/
-  ncSemirings    : Array Semiring := {}
-  /-- Mapping from types to their classification result. Caches failures as `.none`. -/
-  typeClassify   : PHashMap ExprPtr ClassifyResult := {}
-  deriving Inhabited
-
-builtin_initialize arithExt : SymExtension State ← registerSymExtension (return {})
-
-def getArithState : SymM State :=
-  arithExt.getState
-
-@[inline] def modifyArithState (f : State → State) : SymM Unit :=
-  arithExt.modifyState f
-
-/-- Get the exponent threshold. -/
-def getExpThreshold : SymM Nat :=
-  return (← getArithState).exp
-
-/-- Set the exponent threshold. -/
-def setExpThreshold (exp : Nat) : SymM Unit :=
-  modifyArithState fun s => { s with exp }
-
-/-- Run `k` with a temporary exponent threshold. -/
-def withExpThreshold (exp : Nat) (k : SymM α) : SymM α := do
-  let oldExp := (← getArithState).exp
-  setExpThreshold exp
-  try k finally setExpThreshold oldExp
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Canon.lean

@@ -24,19 +24,10 @@ builtin_initialize registerTraceClass `sym.debug.canon
 
 Canonicalizes expressions by normalizing types and instances. At the top level, it traverses
 applications, foralls, lambdas, and let-bindings, classifying each argument as a type, instance,
-implicit, or value using `shouldCanon`. Targeted reductions (projection, match/ite/cond, Nat
-arithmetic) are applied to all positions; instances are re-synthesized.
+implicit, or value using `shouldCanon`. Values are recursively visited but not normalized.
+Types and instances receive targeted reductions.
 
-**Note about types:** `grind` is not built for reasoning about types that are not propositions.
-We assume that definitionally equal types will be structurally identical after we apply the
-canonicalizer. We also erase most of the subsingleton markers occurring inside types.
-
-## Reductions
-
-It also normalizes expressions using the following reductions. We can view it as a cheap/custom `dsimp`.
-We used to reduce only terms inside types, but it restricted important normalizations that were important
-when, for example, a term had a forward dependency. That is, the term is not directly in a type, but
-there is a type that depends on it.
+## Reductions (applied only in type positions)
 
 - **Eta**: `fun x => f x` → `f`
 - **Projection**: `⟨a, b⟩.1` → `a` (structure projections, not class projections)
@@ -44,30 +35,11 @@ there is a type that depends on it.
 - **Nat arithmetic**: ground evaluation (`2 + 1` → `3`) and offset normalization
   (`n.succ + 1` → `n + 2`)
 
-**Note**: Eta is applied only if the lambda is occurring inside of a type. For lambdas occurring
-in non type positions, we want to leverage the support in `grind` for lambda-expressions.
-
 ## Instance canonicalization
 
 Instances are re-synthesized via `synthInstance`. The instance type is first normalized
 using the type-level reductions above, so that `OfNat (Fin (2+1)) 0` and `OfNat (Fin 3) 0`
-produce the same canonical instance. Two special cases:
-
-- **`Decidable` instances** (`Grind.nestedDecidable`): the proposition is recursively
-  canonicalized, then the `Decidable` instance is re-synthesized. If resynthesis fails,
-  the original instance is kept (users often provide these via `haveI`).
-  A `checkDefEqInst` guard is required because structurally different `Decidable` instances
-  are not necessarily definitionally equal.
-
-- **Propositional instances** (`Grind.nestedProof`): the proposition is recursively
-  canonicalized, then the proof is re-synthesized. If resynthesis fails, the original
-  proof is kept. No definitional-equality check is needed thanks to proof irrelevance.
-
-In both cases, resynthesis failure is silent — the original instance or proof is kept.
-Ideally we would report an issue when resynthesis fails inside a type (where structural
-agreement matters most), but in practice users provide non-synthesizable instances via `haveI`,
-and these instances propagate into types through forward dependencies. Reporting failures
-for such instances produces noise that obscures real issues.
+produce the same canonical instance.
 
 ## Two caches
 
@@ -241,7 +213,7 @@ def checkDefEqInst (e : Expr) (inst : Expr) : SymM Expr := do
     return e
   return inst
 
-/-- Canonicalize `e`. Applies targeted reductions and re-synthesizes instances. -/
+/-- Canonicalize `e`. Applies targeted reductions in type positions; recursively visits value positions. -/
 partial def canon (e : Expr) : CanonM Expr := do
   match e with
   | .forallE ..    => withCaching e <| canonForall #[] e
@@ -274,91 +246,23 @@ where
     else
       withReader (fun ctx => { ctx with insideType := true }) <| canon e
 
-  /--
-  Canonicalize `e : type` where `e` is an instance by trying to resynthesize `type`.
-  If `report` is `true`, we report an issue when the instance cannot be resynthesized.
-  -/
-  canonInstCore (e : Expr) (type : Expr) (report := true) : CanonM Expr := do
-    let some inst ← Sym.synthInstance? type |
-      if report then
-        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type}"
-      return e
-    checkDefEqInst e inst
-
-  /--
-  Canonicalize an instance by trying to resynthesize it without caching.
-  Recall that we have special support for `Decidable` and propositional instances.
-  -/
-  canonInst' (e : Expr) (report := true) : CanonM Expr := do
-    /-
-    We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
-    the same instances.
-    -/
-    let type ← inferType e
-    let type' ← canonInsideType' type
-    canonInstCore e type' report
-
-  /-- `withCaching` + `canonInst'` -/
-  canonInst (e : Expr) (report := true) : CanonM Expr := withCaching e do
-    canonInst' e report
-
-  /--
-  Canonicalize a proposition that is also a term instance.
-  Given a term `e` of the form `@Grind.nestedProof prop h`, where `g` is the constant `Grind.nestedProof`,
-  we canonicalize it as follows:
-  1- We recursively canonicalize the proposition `prop`.
-  2- Try to resynthesize the instance, but keep the original one in case of failure since users often
-  provide them using `haveI`.
-  -/
-  canonInstProp (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
-    let prop' ← canon prop
-    if (← read).insideType then
-      /- We suppress reporting here because `haveI`-provided instances propagate into types
-         through forward dependencies, and reporting them produces noise. See module doc. -/
-      canonInstCore h prop' (report := false)
+  canonInst (e : Expr) : CanonM Expr := do
+    if let some inst := (← get).canon.cacheInsts.get? e then
+      checkDefEqInst e inst
     else
       /-
-      **Note**: We try to resynthesize the proposition, but if it fails we keep the current one.
-      This may happen because propositional instances are often provided manually using `haveI`.
+      We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
+      the same instances.
       -/
-      let h' := (← Sym.synthInstance? prop').getD h
-      /- **Note**: We don't need to check whether `h` and `h'` are definitionally equal because of proof irrelevance. -/
-      return if isSameExpr prop prop' && isSameExpr h h' then e else mkApp2 g prop' h'
-
-  /--
-  Canonicalize a decidable instance without checking the cache.
-  Given a term `e` of the form `@Grind.nestedDecidable prop inst`, where `g` is the constant `Grind.nestedDecidable`,
-  we canonicalize it as follows:
-  1- We recursively canonicalize the proposition `prop`.
-  2- Try to resynthesize the instance, but keep the original one in case of failure since users often
-  provide them using `haveI`.
-  -/
-  canonInstDec' (g : Expr) (prop : Expr) (inst : Expr) (e : Expr) : CanonM Expr := do
-    let prop' ← canon prop
-    let type := mkApp (mkConst ``Decidable) prop'
-    if (← read).insideType then
-      /- See comment in `canonInstProp` for why we suppress reporting here. -/
-      canonInstCore inst type (report := false)
-    else
-      /-
-      **Note**: We try to resynthesize the instance, but if it fails we keep the current one.
-      We use `checkDefEqInst` here because two structurally different decidable instances are not necessarily
-      definitionally equal.
-      This may happen because propositional instances are often provided manually using `haveI`.
-      -/
-      let inst' := (← Sym.synthInstance? type).getD inst
-      let inst' ← checkDefEqInst inst inst'
-      return if isSameExpr prop prop' && isSameExpr inst inst' then e else mkApp2 g prop' inst'
-
-  /-- `withCaching` + `canonInstDec'` -/
-  canonInstDec (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
-    canonInstDec' g prop h e
-
-  /-- `canonInstDec` variant for normalizing `if-then-else` expressions. -/
-  canonInstDecCore (e : Expr) : CanonM Expr := do
-    match_expr e with
-    | g@Grind.nestedDecidable prop inst => canonInstDec g prop inst e
-    | _  => canonInst e (report := false)
+      let type ← inferType e
+      let type' ← canonInsideType' type
+      let some inst ← Sym.synthInstance? type' |
+        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type'}"
+        return e
+      let inst ← checkDefEqInst e inst
+      -- Remark: we cache result using the type **before** canonicalization.
+      modify fun s => { s with canon.cacheInsts := s.canon.cacheInsts.insert e inst }
+      return inst
 
   canonLambda (e : Expr) : CanonM Expr := do
     if (← read).insideType then
@@ -391,56 +295,60 @@ where
       mkLetFVars (generalizeNondepLet := false) fvars (← canon (e.instantiateRev fvars))
 
   canonAppDefault (e : Expr) : CanonM Expr := e.withApp fun f args => do
-    if args.size == 2 then
-      if f.isConstOf ``Grind.nestedProof then
-        /- **Note**: We don't have special treatment if `e` inside a type. -/
-        let prop := args[0]!
-        let prop' ← canon prop
-        let e' := if isSameExpr prop prop' then e else mkApp2 f prop' args[1]!
-        return e'
-      else if f.isConstOf ``Grind.nestedDecidable then
-        return (← canonInstDec' f args[0]! args[1]! e)
-    let mut modified := false
-    let args ← if f.isConstOf ``OfNat.ofNat then
-      let some args ← normOfNatArgs? args | pure args
-      modified := true
-      pure args
+    if f.isConstOf ``Grind.nestedProof && args.size == 2 then
+      let prop := args[0]!
+      let prop' ← canon prop
+      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
+      return e'
+    else if f.isConstOf ``Grind.nestedDecidable && args.size == 2 then
+      let prop := args[0]!
+      let prop' ← canon prop
+      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
+      return e'
     else
-      pure args
-    let mut f := f
-    let f' ← canon f
-    unless isSameExpr f f' do
-      f := f'
-      modified := true
-    let pinfos := (← getFunInfo f).paramInfo
-    let mut args := args.toVector
-    for h : i in *...args.size do
-      let arg := args[i]
-      trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
-      let arg' ← match (← shouldCanon pinfos i arg) with
-        | .canonType =>
-          /-
-          The type may have nested propositions and terms that may need to be canonicalized too.
-          So, we must recurse over it. See issue #10232
-          -/
-          canonInsideType' arg
-        | .canonImplicit => canon arg
-        | .visit => canon arg
-        | .canonInst =>
-          match_expr arg with
-          | g@Grind.nestedDecidable prop h => canonInstDec g prop h arg
-          | g@Grind.nestedProof prop h => canonInstProp g prop h arg
-          | _ => canonInst arg
-      unless isSameExpr arg arg' do
-        args := args.set i arg'
+      let mut modified := false
+      let args ← if f.isConstOf ``OfNat.ofNat then
+        let some args ← normOfNatArgs? args | pure args
         modified := true
-    return if modified then mkAppN f args.toArray else e
+        pure args
+      else
+        pure args
+      let mut f := f
+      let f' ← canon f
+      unless isSameExpr f f' do
+        f := f'
+        modified := true
+      let pinfos := (← getFunInfo f).paramInfo
+      let mut args := args.toVector
+      for h : i in *...args.size do
+        let arg := args[i]
+        trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
+        let arg' ← match (← shouldCanon pinfos i arg) with
+          | .canonType =>
+            /-
+            The type may have nested propositions and terms that may need to be canonicalized too.
+            So, we must recurse over it. See issue #10232
+            -/
+            canonInsideType' arg
+          | .canonImplicit => canon arg
+          | .visit => canon arg
+          | .canonInst =>
+            if arg.isAppOfArity ``Grind.nestedDecidable 2 then
+              let prop := arg.appFn!.appArg!
+              let prop' ← canon prop
+              if isSameExpr prop prop' then pure arg else pure (mkApp2 arg.appFn!.appFn! prop' arg.appArg!)
+            else
+              canonInst arg
+        unless isSameExpr arg arg' do
+          args := args.set i arg'
+          modified := true
+      return if modified then mkAppN f args.toArray else e
 
   canonIte (f : Expr) (α c inst a b : Expr) : CanonM Expr := do
     let c ← canon c
     if isTrueCond c then canon a
     else if isFalseCond c then canon b
-    else return mkApp5 f (← canonInsideType α) c (← canonInstDecCore inst) (← canon a) (← canon b)
+    else return mkApp5 f (← canonInsideType α) c (← canonInst inst) (← canon a) (← canon b)
 
   canonCond (f : Expr) (α c a b : Expr) : CanonM Expr := do
     let c ← canon c
@@ -481,24 +389,30 @@ where
         return e
 
   canonApp (e : Expr) : CanonM Expr := do
-    match_expr e with
-    | f@ite α c i a b => canonIte f α c i a b
-    | f@cond α c a b => canonCond f α c a b
-    -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
-    | _ =>
-      let f := e.getAppFn
-      let .const declName _ := f | canonAppAndPost e
-      if (← isMatcher declName) then
-        canonMatch e
-      else
-        canonAppAndPost e
+    if (← read).insideType then
+      match_expr e with
+      | f@ite α c i a b => canonIte f α c i a b
+      | f@cond α c a b => canonCond f α c a b
+      -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
+      | _ =>
+        let f := e.getAppFn
+        let .const declName _ := f | canonAppAndPost e
+        if (← isMatcher declName) then
+          canonMatch e
+        else
+          canonAppAndPost e
+    else
+      canonAppDefault e
 
   canonProj (e : Expr) : CanonM Expr := do
     let e := e.updateProj! (← canon e.projExpr!)
-    return (← reduceProj? e).getD e
+    if (← read).insideType then
+      return (← reduceProj? e).getD e
+    else
+      return e
 
 /--
-Returns `true` if `shouldCanon pinfos i arg` is not `.visit`.
+Returns `true` if `shouldCannon pinfos i arg` is not `.visit`.
 This is a helper function used to implement mbtc.
 -/
 public def isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Bool := do
@@ -509,8 +423,8 @@ end Canon
 
 /--
 Canonicalize `e` by normalizing types, instances, and support arguments.
-Applies targeted reductions (projection, match/ite/cond, Nat arithmetic) in all positions;
-eta reduction is applied only inside types. Instances are re-synthesized.
+Types receive targeted reductions (eta, projection, match/ite, Nat arithmetic).
+Instances are re-synthesized. Values are traversed but not reduced.
 Runs at reducible transparency.
 -/
 public def canon (e : Expr) : SymM Expr := do profileitM Exception "sym canon" (← getOptions) do

src/Lean/Meta/Sym/InstantiateS.lean

@@ -86,8 +86,22 @@ It assumes the input is maximally shared, and ensures the output is too.
 public def instantiateS  (e : Expr) (subst : Array Expr) : SymM Expr :=
   liftBuilderM <| instantiateS' e subst
 
-/-- Internal variant of `betaRevS` that runs in `AlphaShareBuilderM`. -/
-private partial def betaRevS' (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
+/-- `mkAppRevRangeS f b e args == mkAppRev f (revArgs.extract b e)` -/
+def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
+  loop revArgs beginIdx f endIdx
+where
+  loop (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : AlphaShareBuilderM Expr := do
+  if i ≤ start then
+    return b
+  else
+    let i := i - 1
+    loop revArgs start (← mkAppS b revArgs[i]!) i
+
+/--
+Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
+`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
+-/
+partial def betaRevS (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
   if revArgs.size == 0 then
     return f
   else
@@ -159,7 +173,7 @@ where
     | .bvar bidx =>
       let f' ← visitBVar f bidx offset
       if modified || !isSameExpr f f' then
-        betaRevS' f' argsRev
+        betaRevS f' argsRev
       else
         return e
     | _ => unreachable!
@@ -201,18 +215,4 @@ public def instantiateRevBetaS (e : Expr) (subst : Array Expr) : SymM Expr := do
   if !e.hasLooseBVars || subst.isEmpty then return e
   else liftBuilderM <| instantiateRevBetaS' e subst
 
-/--
-Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
-`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
--/
-public def betaRevS (f : Expr) (revArgs : Array Expr) : SymM Expr :=
-  liftBuilderM <| betaRevS' f revArgs
-
-/--
-Apply the given arguments to `f`, beta-reducing if `f` is a lambda expression,
-ensuring maximally shared terms. See `betaRevS` for details.
--/
-public def betaS (f : Expr) (args : Array Expr) : SymM Expr :=
-  betaRevS f args.reverse
-
 end Lean.Meta.Sym

src/Lean/Meta/Sym/SymM.lean

@@ -152,6 +152,8 @@ structure Canon.State where
   cache       : Std.HashMap Expr Expr := {}
   /-- Cache for type-level canonicalization (reductions applied). -/
   cacheInType : Std.HashMap Expr Expr := {}
+  /-- Cache mapping instances to their canonical synthesized instances. -/
+  cacheInsts  : Std.HashMap Expr Expr := {}
 
 /-- Mutable state for the symbolic computation framework. -/
 structure State where

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

@@ -44,7 +44,7 @@ def isCbvNoncomputable (p : Name) : CoreM Bool := do
   return evalLemmas.isNone && Lean.isNoncomputable (← getEnv) p
 
 /--
-Attempts to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
+Attemps to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
 -/
 def trySynthComputableInstance (p : Expr) : SymM <| Option Expr := do
   let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p) | return .none
@@ -112,7 +112,7 @@ builtin_cbv_simproc ↓ simpIteCbv (@ite _ _ _ _ _) := fun e => do
       else if (← isFalseExpr c') then
         return .step b (mkApp (e.replaceFn ``ite_cond_eq_false) h) (contextDependent := cd)
       else
-        -- If we got stuck with simplifying `p` then let's try evaluating the original instance
+        -- If we got stuck with simplifying `p` then let's try evaluating the original isntance
         simpAndMatchIteDecidable f α c inst a b do
           -- If we get stuck here, maybe the problem is that we need to look at `Decidable c'`
           let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
@@ -317,7 +317,7 @@ public def reduceRecMatcher : Simproc := fun e => do
   else
     return .rfl
 
-builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) :=
+builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) := 
   (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher
 
 def tryMatchEquations (appFn : Name) : Simproc := fun e => do

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

@@ -272,7 +272,7 @@ def handleProj : Simproc := fun e => do
         let reduced ← Sym.share reduced
         return .step reduced (← Sym.mkEqRefl reduced)
       | .none =>
-       -- If we failed to reduce it, we turn to a last resort; we try use heterogeneous congruence lemma that we then try to turn into an equality.
+       -- If we failed to reduce it, we turn to a last resort; we try use heterogenous congruence lemma that we then try to turn into an equality.
         unless (← isDefEq struct e') do
           -- If we rewrote the projection body using something that holds up to propositional equality, then there is nothing we can do.
           -- TODO: Check if there is a need to report this to a user, or shall we fail silently.
@@ -283,7 +283,6 @@ def handleProj : Simproc := fun e => do
         let newProof ← mkEqOfHEq newProof (check := false)
         return .step (← Lean.Expr.updateProjS! e e') newProof
 
-open Sym.Internal in
 /--
 For an application whose head is neither a constant nor a lambda (e.g. a projection
 like `p.1 x`), simplify the function head and lift the proof via `congrArg`.

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

@@ -24,6 +24,9 @@ namespace Lean.Meta.Tactic.Cbv
 
 open Lean.Meta.Sym.Simp
 
+public def mkAppNS (f : Expr) (args : Array Expr) : Sym.SymM Expr := do
+  args.foldlM Sym.Internal.mkAppS f
+
 abbrev isNatValue (e : Expr) : Bool := (Sym.getNatValue? e).isSome
 abbrev isStringValue (e : Expr) : Bool := (Sym.getStringValue? e).isSome
 abbrev isIntValue (e : Expr) : Bool := (Sym.getIntValue? e).isSome

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -5,9 +5,11 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
@@ -19,6 +21,8 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Action

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 /-!
 Helper functions for converting reified terms back into their denotations.
 -/

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
 
 section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-import Lean.Meta.Sym.Arith.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.lean

@@ -1,23 +1,24 @@
 /-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Copyright (c) 2025 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.Arith.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public section
-namespace Lean.Meta.Sym.Arith
+namespace Lean.Meta.Grind.Arith.CommRing
 
 class MonadCanon (m : Type → Type) where
   /--
-  Canonicalize an expression (types, instances, support arguments).
-  In `SymM`, this is `Sym.canon`. In `PP.M` (diagnostics), this is the identity.
+  Helper function for removing dependency on `GoalM`.
+  In `RingM` and `SemiringM`, this is just `sharedCommon (← canon e)`
+  When printing counterexamples, we are at `MetaM`, and this is just the identity function.
   -/
   canonExpr : Expr → m Expr
   /--
-  Synthesize an instance, returning `none` on failure.
-  In `SymM`, this is `Sym.synthInstance?`. In `PP.M`, this is `Meta.synthInstance?`.
+  Helper function for removing dependency on `GoalM`. During search we
+  want to track the instances synthesized by `grind`, and this is `Grind.synthInstance`.
   -/
   synthInstance? : Expr → m (Option Expr)
 
@@ -30,7 +31,7 @@ instance (m n) [MonadLift m n] [MonadCanon m] : MonadCanon n where
 
 def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr := do
   let some inst ← synthInstance? type
-    | throwError "failed to find instance{indentExpr type}"
+    | throwError "`grind` failed to find instance{indentExpr type}"
   return inst
 
-end Lean.Meta.Sym.Arith
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.lean

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.lean

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.lean

@@ -8,7 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
+
 structure NonCommRingM.Context where
   ringId : Nat
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
 
 structure NonCommSemiringM.Context where
   semiringId : Nat

src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean

@@ -10,7 +10,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Init.Omega
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 private abbrev M := StateT CommRing MetaM
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -12,14 +12,12 @@ import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-import Lean.Meta.Sym.Arith.ToExpr
-import Lean.Meta.Sym.Arith.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
-
 /--
 Returns a context of type `RArray α` containing the variables `vars` where
 `α` is the type of the ring.

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
 
 variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m]
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 def checkMaxSteps : GoalM Bool := do
   return (← get').steps >= (← getConfig).ringSteps

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-public import Lean.Meta.Sym.Arith.Poly
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 import Lean.Meta.Tactic.Grind.Arith.EvalNum
 import Init.Data.Nat.Linear
 public section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean

@@ -11,7 +11,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 structure SemiringM.Context where
   semiringId : Nat

src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean

@@ -8,7 +8,7 @@ prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.ToExpr
 public section
-namespace Lean.Meta.Sym.Arith
+namespace Lean.Meta.Grind.Arith.CommRing
 open Grind.CommRing
 /-!
 `ToExpr` instances for `CommRing.Poly` types.
@@ -57,4 +57,4 @@ instance : ToExpr CommRing.Expr where
   toExpr := ofRingExpr
   toTypeExpr := mkConst ``CommRing.Expr
 
-end Lean.Meta.Sym.Arith
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -7,7 +7,7 @@ module
 prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Sym.Arith.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section
 
 namespace Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -14,8 +14,8 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
-import Lean.Meta.Sym.Arith.VarRename
-import Lean.Meta.Sym.Arith.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section

src/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.Arith.Linear.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.Linear
-open Sym.Arith (MonadCanon)
 
 def get' : GoalM State := do
   linearExt.getState

src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean

@@ -11,8 +11,8 @@ import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Arith.Linear.ToExpr
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
-import Lean.Meta.Sym.Arith.VarRename
-import Lean.Meta.Sym.Arith.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.VarRename
 public import Lean.Meta.Tactic.Grind.Arith.Linear.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.Linear.OfNatModule

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

@@ -172,7 +172,7 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
       trueEqFalse := true
     else
       let hasHEq := isHEq || lhsRoot.heqProofs || rhsRoot.heqProofs
-      -- **Note**: We only have to check the types if there are heterogeneous equalities.
+      -- **Note**: We only have to check the types if there are heterogenous equalities.
       if (← pure !hasHEq <||> hasSameType lhsRoot.self rhsRoot.self) then
         valueInconsistency := true
   if    (lhsRoot.interpreted && !rhsRoot.interpreted)

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -97,8 +97,6 @@ def mkCnstrNorm0 (s : Struct) (ringInst : Expr) (kind : CnstrKind) (lhs rhs : Ex
   | .le => mkLeNorm0 s ringInst lhs rhs
   | .lt => mkLtNorm0 s ringInst lhs rhs
 
-open Sym.Arith (MonadCanon)
-
 /--
 Returns `rel lhs (rhs + 0)`
 -/

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

@@ -1973,7 +1973,7 @@ def SolverExtension.markTerm (ext : SolverExtension σ) (e : Expr) : GoalM Unit
     | .next id' e' sTerms' =>
       if id == id' then
         -- Skip if `e` and `e'` have different types (e.g., they were merged via `HEq` from `cast`).
-        -- This can happen when we have heterogeneous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
+        -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
         if (← pure !root.heqProofs <||> hasSameType e e') then
           (← solverExtensionsRef.get)[id]!.newEq e e'
         return sTerms
@@ -2056,7 +2056,7 @@ where
     | .nil => return ()
     | .eq solverId lhs rhs rest =>
       -- Skip if `lhs` and `rhs` have different types (e.g., they were merged via `HEq` from `cast`).
-      -- This can happen when we have heterogeneous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
+      -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
       let root ← getRootENode lhs
       if (← pure !root.heqProofs <||> hasSameType lhs rhs) then
         (← solverExtensionsRef.get)[solverId]!.newEq lhs rhs

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

@@ -242,6 +242,7 @@ def ppSimpTheorem [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m Me
 instance : BEq SimpTheorem where
   beq e₁ e₂ := e₁.proof == e₂.proof
 
+
 /--
 Configuration for `MetaM` used to process global simp theorems
 -/
@@ -255,6 +256,8 @@ def simpGlobalConfig : ConfigWithKey :=
 @[inline] def withSimpGlobalConfig : MetaM α → MetaM α :=
   withConfigWithKey simpGlobalConfig
 
+
+
 private partial def isPerm : Expr → Expr → MetaM Bool
   | .app f₁ a₁, .app f₂ a₂ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
   | .mdata _ s, t => isPerm s t
@@ -367,32 +370,11 @@ private def mkSimpTheoremKeys (type : Expr) (noIndexAtArgs : Bool) : MetaM (Arra
     | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
     | none => throwError "Unexpected kind of simp theorem{indentExpr type}"
 
-register_builtin_option simp.rfl.checkTransparency: Bool := {
-  defValue := false
-  descr    := "if true, Lean generates a warning if the left and right-hand sides of the `[simp]` equation are not definitionally equal at the restricted transparency level used by `simp` "
-}
-
-private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr)
-    (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
+private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr) (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
   assert! origin != .fvar ⟨.anonymous⟩
   let type ← instantiateMVars (← inferType e)
   let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs
-  let rfl ← isRflProof proof
-  if rfl && simp.rfl.checkTransparency.get (← getOptions) then
-    forallTelescopeReducing type fun _ type => do
-      let checkDefEq (lhs rhs : Expr) := do
-        unless (← withTransparency .instances <| isDefEq lhs rhs) do
-          logWarning m!"`{origin.key}` is a `rfl` simp theorem, but its left-hand side{indentExpr lhs}\n\
-            is not definitionally equal to the right-hand side{indentExpr rhs}\n\
-            at `.instances` transparency. Possible solutions:\n\
-            1- use `id rfl` as the proof\n\
-            2- mark constants occurring in the lhs and rhs as `[implicit_reducible]`"
-      match_expr type with
-      | Eq _ lhs rhs => checkDefEq lhs rhs
-      | Iff lhs rhs => checkDefEq lhs rhs
-      | _ =>
-        logWarning m!"'{origin.key}' is a 'rfl' simp theorem, unexpected resulting type{indentExpr type}"
-  return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl }
+  return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }
 
 /--
 Creates a `SimpTheorem` from a global theorem.

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -192,7 +192,7 @@ private def matchEndPos (query : String) (startPos : String.Pos.Raw) : String.Po
   startPos + query
 
 @[specialize]
-private def highlightStringMatches? (query text : String) (matchPositions : Array String.Pos.Raw)
+private def hightlightStringMatches? (query text : String) (matchPositions : Array String.Pos.Raw)
     (highlight : α) (offset : String.Pos.Raw := ⟨0⟩) (mapIdx : Nat → Nat := id) :
     Option (TaggedText α) := Id.run do
   if query.isEmpty || text.isEmpty || matchPositions.isEmpty then
@@ -245,7 +245,7 @@ private def advanceTaggedTextHighlightState (text : String) (highlighted : α) :
   let query := (← get).query
   let p := (← get).p
   let ms := (← get).ms
-  let highlighted? := highlightStringMatches? query text ms highlighted (offset := p)
+  let highlighted? := hightlightStringMatches? query text ms highlighted (offset := p)
     (mapIdx := fun i => ms.size - i - 1)
   updateState text highlighted?.isSome
   return highlighted?.getD (.text text)

src/Std/Internal/Async/Select.lean

@@ -10,6 +10,8 @@ public import Init.Data.Random
 public import Std.Internal.Async.Basic
 import Init.Data.ByteArray.Extra
 import Init.Data.Array.Lemmas
+public import Std.Sync.Mutex
+public import Std.Sync.Barrier
 import Init.Omega
 
 public section
@@ -132,6 +134,8 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
   let gen := mkStdGen seed
   let selectables := shuffleIt selectables gen
 
+  let gate ← IO.Promise.new
+
   for selectable in selectables do
     if let some val ← selectable.selector.tryFn then
       let result ← selectable.cont val
@@ -141,6 +145,9 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
   let promise ← IO.Promise.new
 
   for selectable in selectables do
+    if ← finished.get then
+      break
+
     let waiterPromise ← IO.Promise.new
     let waiter := Waiter.mk finished waiterPromise
     selectable.selector.registerFn waiter
@@ -157,18 +164,20 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
         let async : Async _ :=
           try
             let res ← IO.ofExcept res
+            discard <| await gate.result?
 
             for selectable in selectables do
               selectable.selector.unregisterFn
 
-            let contRes ← selectable.cont res
-            promise.resolve (.ok contRes)
+            promise.resolve (.ok (← selectable.cont res))
           catch e =>
             promise.resolve (.error e)
 
         async.toBaseIO
 
-  Async.ofPromise (pure promise)
+  gate.resolve ()
+  let result ← Async.ofPromise (pure promise)
+  return result
 
 /--
 Performs fair and data-loss free non-blocking multiplexing on the `Selectable`s in `selectables`.
@@ -224,6 +233,8 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
         let derivedWaiter := Waiter.mk waiter.finished waiterPromise
         selectable.selector.registerFn derivedWaiter
 
+        let barrier ← IO.Promise.new
+
         discard <| IO.bindTask (t := waiterPromise.result?) fun res? => do
           match res? with
           | none => return (Task.pure (.ok ()))
@@ -231,6 +242,7 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
             let async : Async _ := do
               let mainPromise := waiter.promise
 
+              await barrier
               for selectable in selectables do
                 selectable.selector.unregisterFn
 

src/Std/Internal/Http.lean

@@ -6,4 +6,190 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data
+public import Std.Internal.Http.Server
+public import Std.Internal.Http.Client
+public import Std.Internal.Http.Test.Helpers
+
+public section
+
+/-!
+# HTTP Library
+
+A low-level HTTP/1.1 server implementation for Lean. This library provides a pure,
+sans-I/O protocol implementation that can be used with the `Async` library or with
+custom connection handlers.
+
+## Overview
+
+This module provides a complete HTTP/1.1 server implementation with support for:
+
+- Request/response handling with directional streaming bodies
+- Keep-alive connections
+- Chunked transfer encoding
+- Header validation and management
+- Configurable timeouts and limits
+
+**Sans I/O Architecture**: The core protocol logic doesn't perform any actual I/O itself -
+it just defines how data should be processed. This separation allows the protocol implementation
+to remain pure and testable, while different transports (TCP sockets, mock clients) handle
+the actual reading and writing of bytes.
+
+## Quick Start
+
+The main entry point is `Server.serve`, which starts an HTTP/1.1 server. Implement the
+`Server.Handler` type class to define how the server handles requests, errors, and
+`Expect: 100-continue` headers:
+
+```lean
+import Std.Internal.Http
+
+open Std Internal IO Async
+open Std Http Server
+
+structure MyHandler
+
+instance : Handler MyHandler where
+  onRequest _ req := do
+    Response.ok |>.text "Hello, World!"
+
+def main : IO Unit := Async.block do
+  let addr : Net.SocketAddress := .v4 ⟨.ofParts 127 0 0 1, 8080⟩
+  let server ← Server.serve addr MyHandler.mk
+  server.waitShutdown
+```
+
+## Working with Requests
+
+Incoming requests are represented by `Request Body.Stream`, which bundles the request
+line, parsed headers, and a lazily-consumed body. Headers are available immediately,
+while the body can be streamed or collected on demand, allowing handlers to process both
+small and large payloads efficiently.
+
+### Reading Headers
+
+```lean
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+  -- Access request method and URI
+  let method := req.head.method      -- Method.get, Method.post, etc.
+  let uri := req.head.uri            -- RequestTarget
+
+  -- Read a specific header
+  if let some contentType := req.head.headers.get? (.mk "content-type") then
+    IO.println s!"Content-Type: {contentType}"
+
+  Response.ok |>.text "OK"
+```
+
+### URI Query Semantics
+
+`RequestTarget.query` is parsed using form-style key/value conventions (`k=v&...`), and `+` is decoded as a
+space in query components. If you need RFC 3986 opaque query handling, use the raw request target string
+(`toString req.head.uri`) and parse it with custom logic.
+
+### Reading the Request Body
+
+The request body is exposed as `Body.Stream`, which can be consumed incrementally or
+collected into memory. The `readAll` method reads the entire body, with an optional size
+limit to protect against unbounded payloads.
+
+```lean
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+  -- Collect entire body as a String
+  let bodyStr : String ← req.body.readAll
+
+  -- Or with a maximum size limit
+  let bodyStr : String ← req.body.readAll (maximumSize := some 1024)
+
+  Response.ok |>.text s!"Received: {bodyStr}"
+```
+
+## Building Responses
+
+Responses are constructed using a builder API that starts from a status code and adds
+headers and a body. Common helpers exist for text, HTML, JSON, and binary responses, while
+still allowing full control over status codes and header values.
+
+Response builders produce `Async (Response Body.Stream)`.
+
+```lean
+-- Text response
+Response.ok |>.text "Hello!"
+
+-- HTML response
+Response.ok |>.html "<h1>Hello!</h1>"
+
+-- JSON response
+Response.ok |>.json "{\"key\": \"value\"}"
+
+-- Binary response
+Response.ok |>.bytes someByteArray
+
+-- Custom status
+Response.new |>.status .created |>.text "Resource created"
+
+-- With custom headers
+Response.ok
+  |>.header! "X-Custom-Header" "value"
+  |>.header! "Cache-Control" "no-cache"
+  |>.text "Response with headers"
+```
+
+### Streaming Responses
+
+For large responses or server-sent events, use streaming:
+
+```lean
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+  Response.ok
+    |>.header! "Content-Type" "text/plain"
+    |>.stream fun stream => do
+      for i in [0:10] do
+        stream.send { data := s!"chunk {i}\n".toUTF8 }
+        Async.sleep 1000
+      stream.close
+```
+
+## Server Configuration
+
+Configure server behavior with `Config`:
+
+```lean
+def config : Config := {
+  maxRequests := 10000000,
+  lingeringTimeout := 5000,
+}
+
+let server ← Server.serve addr MyHandler.mk config
+```
+
+## Handler Type Class
+
+Implement `Server.Handler` to define how the server processes events. The class has three
+methods, all with default implementations:
+
+- `onRequest` — called for each incoming request; returns a response inside `ContextAsync`
+- `onFailure` — called when an error occurs while processing a request
+- `onContinue` — called when a request includes an `Expect: 100-continue` header; return
+  `true` to accept the body or `false` to reject it
+
+```lean
+structure MyHandler where
+  greeting : String
+
+instance : Handler MyHandler where
+  onRequest self req := do
+    Response.ok |>.text self.greeting
+
+  onFailure self err := do
+    IO.eprintln s!"Error: {err}"
+```
+
+The handler methods operate in the following monads:
+
+- `onRequest` uses `ContextAsync` — an asynchronous monad (`ReaderT CancellationContext Async`) that provides:
+  - Full access to `Async` operations (spawning tasks, sleeping, concurrent I/O)
+  - A `CancellationContext` tied to the client connection — when the client disconnects, the
+    context is cancelled, allowing your handler to detect this and stop work early
+- `onFailure` uses `Async`
+- `onContinue` uses `Async`
+-/

src/Std/Internal/Http/Client.lean

@@ -0,0 +1,313 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Client.Pool
+
+public section
+
+namespace Std.Http
+
+set_option linter.all true
+
+open Std Internal IO Async TCP Protocol
+open Time
+
+/-!
+# Client
+
+A top-level HTTP client backed by a connection pool, similar to `reqwest::Client`.
+Use `Client.builder` to construct, then `client.get "https://..."` etc.
+
+```lean
+let client ← Client.builder
+  |>.proxy! "http://proxy.example.com:8080"
+  |>.build
+
+let res ← client.get (URI.parse! "https://api.example.com/data")
+  |>.header! "Accept" "application/json"
+  |>.send
+```
+-/
+
+/--
+A top-level HTTP client backed by a connection pool.
+-/
+abbrev Client := Client.Agent.Pool
+
+/--
+Builder for `Client`. Chain configuration setters then call `.build`.
+-/
+public structure Client.Builder where
+
+  /--
+  Configuration applied to all sessions created by this client.
+  -/
+  config : Config := {}
+
+  /--
+  Maximum number of pooled connections per host.
+  -/
+  maxPerHost : Nat := 4
+
+namespace Client.Builder
+
+/--
+Routes all connections through a proxy.
+`host` is the proxy hostname, `port` is the proxy port.
+Only HTTP proxies are supported.
+-/
+def proxy (b : Client.Builder) (host : String) (port : UInt16) : Client.Builder :=
+  { b with config := { b.config with proxy := some (host, port) } }
+
+/--
+Routes all connections through a proxy specified as a URL string.
+Returns `none` if the URL is invalid or has no authority component.
+Only HTTP proxies are supported. The scheme determines the default port
+when no explicit port is specified (`http` → 80, `https` → 443). TLS
+(HTTPS proxy CONNECT tunnels) is not supported.
+-/
+def proxy? (b : Client.Builder) (url : String) : Option Client.Builder := do
+  let uri ← URI.parse? url
+  let auth ← uri.authority
+  let host := toString auth.host
+  let port : UInt16 := match auth.port with
+    | .value p => p
+    | _ => URI.Scheme.defaultPort uri.scheme
+  pure { b with config := { b.config with proxy := some (host, port) } }
+
+/--
+Sets the request timeout (send + receive).
+DNS resolution and TCP connect are not covered by this timeout;
+use the OS-level socket timeout for those.
+-/
+def timeout (b : Client.Builder) (ms : Time.Millisecond.Offset) : Client.Builder :=
+  if h : 0 < ms then
+    { b with config := { b.config with requestTimeout := ⟨ms, h⟩ } }
+  else b
+
+/--
+Sets the `User-Agent` header sent with every request.
+-/
+def userAgent (b : Client.Builder) (ua : String) : Client.Builder :=
+  { b with config := { b.config with userAgent := Header.Value.ofString? ua } }
+
+/--
+Sets the maximum number of pooled connections per host.
+-/
+def maxConnectionsPerHost (b : Client.Builder) (n : Nat) : Client.Builder :=
+  { b with maxPerHost := n }
+
+/--
+Sets the maximum number of redirects to follow automatically.
+-/
+def maxRedirects (b : Client.Builder) (n : Nat) : Client.Builder :=
+  { b with config := { b.config with maxRedirects := n } }
+
+/--
+Sets the predicate that decides whether a response status is acceptable.
+When set, the final response status is passed to `f`; if `f` returns `false`
+an `IO.Error` is thrown with the numeric status code.
+-/
+def validateStatus (b : Client.Builder) (f : Status → Bool) : Client.Builder :=
+  { b with config := { b.config with validateStatus := some f } }
+
+/--
+Builds the `Client`.
+-/
+def build (b : Client.Builder) : Async Client := do
+  Agent.Pool.new b.config b.maxPerHost
+
+end Builder
+
+/--
+A request builder bound to a `Client`. Build up headers, query parameters, and body,
+then dispatch with one of the `send*` methods.
+-/
+public structure RequestBuilder where
+
+  /--
+  The client that will dispatch this request.
+  -/
+  client : Client
+
+  /--
+  URI scheme for this request (`"http"` or `"https"`).
+  Used as part of the pool key and for the `Host` header.
+  -/
+  scheme : URI.Scheme
+
+  /--
+  Resolved hostname for this request.
+  -/
+  host : URI.Host
+
+  /--
+  Target port.
+  -/
+  port : UInt16
+
+  /--
+  The underlying request builder.
+  -/
+  builder : Request.Builder
+
+namespace RequestBuilder
+
+/--
+Injects a `Host` header if not already present.
+-/
+private def withHostHeader (rb : RequestBuilder) : RequestBuilder :=
+  if rb.builder.line.headers.contains Header.Name.host then rb
+  else
+    let defaultPort := URI.Scheme.defaultPort rb.scheme
+    let hostValue :=
+      if rb.port == defaultPort then toString rb.host
+      else s!"{rb.host}:{rb.port}"
+    { rb with builder := rb.builder.header! "Host" hostValue }
+
+/--
+Adds a typed header to the request.
+-/
+def header (rb : RequestBuilder) (key : Header.Name) (value : Header.Value) : RequestBuilder :=
+  { rb with builder := rb.builder.header key value }
+
+/--
+Adds a header to the request. Panics if the name or value is invalid.
+-/
+def header! (rb : RequestBuilder) (key : String) (value : String) : RequestBuilder :=
+  { rb with builder := rb.builder.header! key value }
+
+/--
+Adds a header to the request. Returns `none` if the name or value is invalid.
+-/
+def header? (rb : RequestBuilder) (key : String) (value : String) : Option RequestBuilder := do
+  let builder ← rb.builder.header? key value
+  pure { rb with builder }
+
+/--
+Sets the request URI from a string. Panics if the string is not a valid request target.
+-/
+def uri! (rb : RequestBuilder) (u : String) : RequestBuilder :=
+  { rb with builder := rb.builder.uri! u }
+
+/--
+Adds a query parameter to the request URI.
+-/
+def queryParam (rb : RequestBuilder) (key : String) (value : String) : RequestBuilder :=
+  let newTarget := match rb.builder.line.uri with
+    | .originForm path query =>
+        .originForm path (some ((query.getD URI.Query.empty).insert key value))
+    | .absoluteForm af =>
+        .absoluteForm { af with query := af.query.insert key value }
+    | other => other
+  { rb with builder := { rb.builder with line := { rb.builder.line with uri := newTarget } } }
+
+/--
+Sends the request with an empty body.
+-/
+def send (rb : RequestBuilder) : Async (Response Body.Stream) := do
+  let rb := rb.withHostHeader
+  rb.client.send rb.host rb.port rb.scheme (← rb.builder.empty)
+
+/--
+Sends the request with a plain-text body. Sets `Content-Type: text/plain; charset=utf-8`.
+-/
+def text (rb : RequestBuilder) (content : String) : Async (Response Body.Stream) := do
+  let rb := rb.withHostHeader
+  rb.client.send rb.host rb.port rb.scheme (← rb.builder.text content)
+
+/--
+Sends the request with a JSON body. Sets `Content-Type: application/json`.
+-/
+def json (rb : RequestBuilder) (content : String) : Async (Response Body.Stream) := do
+  let rb := rb.withHostHeader
+  rb.client.send rb.host rb.port rb.scheme (← rb.builder.json content)
+
+/--
+Sends the request with a raw binary body. Sets `Content-Type: application/octet-stream`.
+-/
+def bytes (rb : RequestBuilder) (content : ByteArray) : Async (Response Body.Stream) := do
+  let rb := rb.withHostHeader
+  rb.client.send rb.host rb.port rb.scheme (← rb.builder.bytes content)
+
+/--
+Sends the request with a streaming body produced by `gen`.
+-/
+def stream (rb : RequestBuilder) (gen : Body.Stream → Async Unit) : Async (Response Body.Stream) := do
+  let rb := rb.withHostHeader
+  rb.client.send rb.host rb.port rb.scheme (← rb.builder.stream gen)
+
+end RequestBuilder
+
+/--
+Returns a `Client.Builder` with default configuration.
+-/
+def new : Client.Builder := {}
+
+/--
+Builds a `RequestBuilder` from a parsed `URI`, extracting host, port, and origin-form target.
+-/
+private def mkRequest
+    (method : Request.Builder → Request.Builder)
+    (client : Client) (url : URI) : Client.RequestBuilder :=
+  let target : RequestTarget :=
+    .originForm url.path (if url.query.isEmpty then none else some url.query)
+  let host := (url.authority.map (·.host)).getD default
+  let scheme := url.scheme
+  let port : UInt16 := match url.authority with
+    | some auth => match auth.port with
+      | .value p => p
+      | _ => URI.Scheme.defaultPort scheme
+    | none => URI.Scheme.defaultPort scheme
+  { client, scheme, host, port, builder := method (Request.new |>.uri target) }
+
+/--
+Creates a GET request builder for `url`.
+-/
+def get (client : Client) (url : URI) : Client.RequestBuilder :=
+  mkRequest (·.method .get) client url
+
+/--
+Creates a POST request builder for `url`.
+-/
+def post (client : Client) (url : URI) : Client.RequestBuilder :=
+  mkRequest (·.method .post) client url
+
+/--
+Creates a PUT request builder for `url`.
+-/
+def put (client : Client) (url : URI) : Client.RequestBuilder :=
+  mkRequest (·.method .put) client url
+
+/--
+Creates a DELETE request builder for `url`.
+-/
+def delete (client : Client) (url : URI) : Client.RequestBuilder :=
+  mkRequest (·.method .delete) client url
+
+/--
+Creates a PATCH request builder for `url`.
+-/
+def patch (client : Client) (url : URI) : Client.RequestBuilder :=
+  mkRequest (·.method .patch) client url
+
+/--
+Creates a HEAD request builder for `url`.
+-/
+def head (client : Client) (url : URI) : Client.RequestBuilder :=
+  mkRequest (·.method .head) client url
+
+/--
+Creates an OPTIONS request builder for `url`.
+-/
+def options (client : Client) (url : URI) : Client.RequestBuilder :=
+  mkRequest (·.method .options) client url
+
+end Client
+end Http
+end Std

src/Std/Internal/Http/Client/Agent.lean

@@ -0,0 +1,556 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Client.Session
+public import Std.Internal.Http.Data.Cookie
+import Init.Data.Array
+
+public section
+
+namespace Std
+namespace Http
+namespace Client
+
+set_option linter.all true
+
+open Std Internal IO Async TCP Protocol
+open Time
+
+/-!
+# Agent
+
+This module defines `Client.Agent`, a transport-agnostic HTTP user-agent that wraps a `Session`
+and adds automatic redirect following, cookie jar support, response interceptors, and configurable
+retries.
+
+`Agent` is parameterized by the transport type `α` and contains no TCP-specific code.
+Use `Agent.ofTransport` to create an `Agent` from any connected transport. Pass a `connectTo`
+factory to enable cross-host redirect following and automatic reconnection on error.
+
+On each redirect the `Location` header is parsed as a URI. If the redirect targets a different
+host or port the agent closes the current session and opens a new one using `connectTo` (when
+available). A `Array URI` tracks every URI visited in the current redirect chain so that cycles
+are detected and broken immediately.
+
+When crossing to a different host the `Authorization` header is stripped from the redirected
+request to prevent credential leakage.
+-/
+
+/--
+An HTTP user-agent that manages a connection to a host. It follows redirects, maintains a cookie
+jar for automatic cookie handling, applies response interceptors, and retries on connection errors.
+-/
+public structure Agent (α : Type) where
+  /--
+  The underlying HTTP session over the transport.
+  -/
+  session : Session α
+
+  /--
+  URI scheme for this connection (e.g., `"http"` or `"https"`).
+  Used when constructing absolute-form request URIs for proxy requests and some redirects.
+  -/
+  scheme : URI.Scheme
+
+  /--
+  The hostname this agent is currently connected to.
+  -/
+  host : URI.Host
+
+  /--
+  The port this agent is currently connected to.
+  -/
+  port : UInt16
+
+  /--
+  Cookie jar shared across all requests and redirects through this agent.
+  -/
+  cookieJar : Cookie.Jar
+
+  /--
+  Response interceptors applied (in order) after every response, including intermediate
+  redirect responses.  Each interceptor receives the response and returns a (possibly
+  modified) response.  Interceptors run before cookie processing and redirect evaluation
+  so they can, e.g., unwrap envelopes or transparently decompress bodies.
+  -/
+  interceptors : Array (Response Body.Stream → Async (Response Body.Stream)) := #[]
+
+  /--
+  Optional factory for opening a new session to `(scheme, host, port)`. Used for:
+  * Automatic retry after connection errors (`maxRetries`): reconnects to the same origin.
+  * Cross-host redirects: connects to the new origin.
+  The scheme is included so that http→https redirects open the correct pool entry.
+  `none` for agents created via `Agent.ofTransport` without a factory; cross-host redirects
+  are not followed and connection errors are not retried automatically for such agents.
+  -/
+  connectTo : Option (URI.Scheme → URI.Host → UInt16 → Async (Session α)) := none
+
+  /--
+  Called when a connection error is confirmed (i.e., `session.send` threw and all retries
+  are committed to using a fresh session).  Receives the broken session together with the
+  scheme, host, and port so the caller can:
+  * For pool agents: evict the session from the pool so the next retry gets a fresh one.
+  * For standalone agents: close the session's request channel so the background loop exits.
+  The default closes the session channel; pool agents set this to an eviction function.
+  -/
+  onBrokenSession : Session α → URI.Scheme → URI.Host → UInt16 → Async Unit :=
+    fun s _ _ _ => discard <| s.close
+
+namespace Agent
+
+/--
+Returns `true` for HTTP methods that are safe to retry on connection failure.
+Non-idempotent methods (POST, PATCH) must not be retried automatically because
+the server may have already processed the request before the connection dropped.
+-/
+private def isIdempotentMethod (m : Method) : Bool :=
+  m == .get || m == .head || m == .put || m == .delete || m == .options || m == .trace
+
+/--
+Rewrites an origin-form request target to absolute-form for proxy forwarding.
+`GET /path?q=1 HTTP/1.1` becomes `GET http://host:port/path?q=1 HTTP/1.1`.
+No-op for targets that are already in absolute-form or do not carry a path.
+-/
+def toAbsoluteFormRequest
+    (request : Request Body.Any)
+    (scheme : URI.Scheme) (host : URI.Host) (port : UInt16) : Request Body.Any :=
+  match request.line.uri with
+  | .originForm path query =>
+    { request with
+        line := { request.line with uri := .absoluteForm {
+          scheme,
+          path,
+          query := query.getD URI.Query.empty,
+          authority := some { host, port := .value port }
+          fragment := none
+        }
+      }
+    }
+  | _ => request
+
+/--
+Creates an `Agent` from an already-connected transport `socket`.
+Pass a `connectTo` factory to enable automatic reconnection on error and cross-host redirect
+following; omit it (or pass `none`) to disable both.
+-/
+def ofTransport [Transport α] (socket : α) (scheme : URI.Scheme)
+    (host : URI.Host) (port : UInt16)
+    (connectTo : Option (URI.Scheme → URI.Host → UInt16 → Async (Session α)) := none)
+    (config : Config := {}) : Async (Agent α) := do
+
+  let session ← Session.new socket config
+  let cookieJar ← Cookie.Jar.new
+  pure { session, scheme, host, port, cookieJar, connectTo }
+
+/--
+Injects matching cookies from `cookieJar` into the request headers for `host`.
+Does nothing if the jar contains no matching cookies.
+-/
+def injectCookies (cookieJar : Cookie.Jar) (host : URI.Host) (scheme : URI.Scheme)
+    (request : Request Body.Any) : Async (Request Body.Any) := do
+
+  -- Respect an explicit Cookie header set by the caller.
+  if request.line.headers.contains .cookie then return request
+
+  let path := match request.line.uri with
+    | .originForm path _ => path
+    | .absoluteForm af => af.path
+    | _ => URI.Path.parseOrRoot "/"
+
+  match ← cookieJar.cookiesFor host path (secure := scheme.val == "https") with
+  | none => return request
+  | some cookieValue =>
+    let newHeaders := request.line.headers.insert .cookie cookieValue
+    return { request with line := { request.line with headers := newHeaders } }
+
+/--
+Reads all `Set-Cookie` headers from `responseHeaders` and stores the cookies in `cookieJar`.
+-/
+def processCookies (cookieJar : Cookie.Jar) (host : URI.Host)
+    (responseHeaders : Headers) : BaseIO Unit := do
+  if let some values := responseHeaders.getAll? Header.Name.setCookie then
+    for v in values do
+      cookieJar.processSetCookie host v.value
+
+/--
+Applies all response interceptors to `response` in order, returning the final result.
+-/
+def applyInterceptors
+    (interceptors : Array (Response Body.Stream → Async (Response Body.Stream)))
+    (response : Response Body.Stream) : Async (Response Body.Stream) :=
+  interceptors.foldlM (init := response) (fun r f => f r)
+
+/--
+Outcome of evaluating whether a response should trigger an automatic redirect.
+-/
+inductive RedirectDecision where
+  /--
+  Response is final, should validate status and return it.
+  -/
+  | done
+
+  /--
+  Follow a redirect to `(host, port, scheme)` with `request`, updating `history`.
+  -/
+  | follow (host : URI.Host) (port : UInt16) (scheme : URI.Scheme) (request : Request Body.Any)
+
+/--
+Inspects `response` and decides whether to follow a redirect.
+
+Returns `.done` when:
+- `remaining` is 0 or the response is not a redirection,
+- the `Location` header is absent, or
+- the `Location` value cannot be parsed.
+
+Returns `.follow` with the rewritten request (method, body, and headers adjusted per
+RFC 9110 §15.4, including `Authorization` stripped on cross-origin hops) when a valid
+redirect target is found. The response body is drained (up to `drainLimit` bytes) before
+returning `.follow`; if the body exceeds `drainLimit` the incoming channel is closed and
+the connection is left to recover or time out.
+-/
+def decideRedirect
+    (remaining : Nat)
+    (currentHost : URI.Host) (currentPort : UInt16) (currentScheme : URI.Scheme)
+    (request : Request Body.Any) (response : Response Body.Stream)
+    (drainLimit : Nat)
+    : Async RedirectDecision := do
+
+  if remaining == 0 ∨ !response.line.status.isRedirection then
+    return .done
+
+  let some locationValue := response.line.headers.get? .location
+    | return .done
+
+  let locationStr := locationValue.value
+
+  let some target := RequestTarget.parse? locationStr
+    | return .done
+
+  -- Drain
+  discard <| ContextAsync.run do
+    try
+      discard <| response.body.readAll (α := ByteArray) (maximumSize := some drainLimit.toUInt64)
+    catch _ =>
+      response.body.close
+
+  let newMethod := match response.line.status with
+    | .seeOther => .get
+    | .movedPermanently | .found =>
+        if request.line.method == .post then .get else request.line.method
+    | _ => request.line.method
+
+  let (newHost, newPort, newScheme) := match target with
+    | .absoluteForm af =>
+      let h := af.authority.map URI.Authority.host |>.getD currentHost
+      let p : UInt16 :=
+        match af.authority with
+        | some auth => match auth.port with
+          | URI.Port.value v => v
+          | _ => URI.Scheme.defaultPort af.scheme
+        | none => URI.Scheme.defaultPort af.scheme
+      (h, p, af.scheme)
+    | _ => (currentHost, currentPort, currentScheme)
+
+  -- Avoid SSRF.
+  if newScheme.val != "http" && newScheme.val != "https" then
+    return .done
+
+  -- Strip Authorization
+  let isCrossOrigin := newHost != currentHost || newPort != currentPort || newScheme != currentScheme
+
+  let newHeaders :=
+    if isCrossOrigin then
+      request.line.headers
+        |>.erase Header.Name.authorization
+        |>.erase Header.Name.proxyAuthorization
+        |>.erase Header.Name.cookie
+    else request.line.headers
+
+  -- For method-changing redirects (301/302 POST→GET, 303) drop the body.
+  -- For method-preserving redirects (307/308) reuse the body if re-readable (Body.Full).
+  -- A Body.Stream is a live producer whose bytes have already been sent and cannot be replayed;
+  -- follow the redirect with an empty body rather than silently sending a stale/empty stream.
+  let newBody : Body.Any ←
+    if newMethod == .get || newMethod == .head || newMethod != request.line.method then
+      pure (Body.Any.ofBody Body.Empty.mk)
+    else if request.body.isReplayable then do
+      request.body.resetInPlace
+      pure request.body
+    else
+      -- Body.Stream: already consumed, send empty body on redirect
+      pure (Body.Any.ofBody Body.Empty.mk)
+
+  return .follow newHost newPort newScheme
+    { line := { request.line with uri := target, method := newMethod, headers := newHeaders }
+      body := newBody
+      extensions := request.extensions }
+
+private partial def sendWithRedirects [Transport α]
+    (agent : Agent α) (request : Request Body.Any)
+    (remaining : Nat) (retriesLeft : Nat)
+    (history : Array (URI.Host × UInt16 × String) := #[]) : Async (Response Body.Stream) := do
+
+  -- Record the current URL in the history and detect redirect cycles.
+  let currentKey := (agent.host, agent.port, toString request.line.uri)
+  let history := history.push currentKey
+
+  -- Rewrite to absolute-form when a proxy is configured.
+  let request :=
+    if agent.session.config.proxy.isSome then
+      toAbsoluteFormRequest request agent.scheme agent.host agent.port
+    else
+      request
+
+  let request ← injectCookies agent.cookieJar agent.host agent.scheme request
+
+  let response ← try agent.session.send request
+    catch err => do
+      agent.onBrokenSession agent.session agent.scheme agent.host agent.port
+
+      if retriesLeft > 0 && isIdempotentMethod request.line.method then
+        if let some factory := agent.connectTo then
+          let attempt := agent.session.config.maxRetries - retriesLeft
+          let delay : Time.Millisecond.Offset := ⟨min (agent.session.config.retryDelay.val * (2 : Int) ^ attempt) 32000⟩
+          sleep delay
+          let newSession ← factory agent.scheme agent.host agent.port
+          return ← sendWithRedirects { agent with session := newSession } request remaining (retriesLeft - 1) history
+
+      throw err
+
+  let response ← applyInterceptors agent.interceptors response
+  processCookies agent.cookieJar agent.host response.line.headers
+
+  match ← decideRedirect remaining agent.host agent.port agent.scheme request response
+      agent.session.config.redirectBodyDrainLimit with
+  | .done =>
+    if let some validate := agent.session.config.validateStatus then
+      if !validate response.line.status then
+        throw (.userError s!"unexpected HTTP status: {response.line.status.toCode}")
+    return response
+  | .follow newHost newPort newScheme newRequest =>
+    if let some policy := agent.session.config.redirectPolicy then
+      if !policy newHost newPort then
+        return response
+
+    let nextKey := (newHost, newPort, toString newRequest.line.uri)
+    if history.contains nextKey then
+      return response
+
+    if newHost != agent.host || newPort != agent.port then
+
+      -- For custom transports without a connectTo factory we cannot open a new
+      -- connection to a different host; return the redirect response as-is.
+      let some factory := agent.connectTo
+        | return response
+
+      let newSession ← factory newScheme newHost newPort
+
+      sendWithRedirects
+        { session := newSession
+          scheme := newScheme
+          host := newHost
+          port := newPort
+          cookieJar := agent.cookieJar
+          interceptors := agent.interceptors
+          connectTo := some factory
+          onBrokenSession := agent.onBrokenSession }
+        newRequest (remaining - 1) retriesLeft history
+    else
+      sendWithRedirects agent newRequest (remaining - 1) retriesLeft history
+
+/--
+Send a request, automatically following redirects up to `config.maxRedirects` hops and
+retrying on connection errors up to `config.maxRetries` times.
+For cross-host redirects the agent reconnects using its `connectTo` factory (if set).
+Cookies are automatically injected from the jar and `Set-Cookie` responses are stored.
+Response interceptors are applied after every response.
+-/
+def send {β : Type} [Coe β Body.Any] [Transport α] (agent : Agent α) (request : Request β) : Async (Response Body.Stream) :=
+  sendWithRedirects
+    agent
+    { line := request.line, body := (request.body : Body.Any), extensions := request.extensions }
+    agent.session.config.maxRedirects
+    agent.session.config.maxRetries
+
+end Agent
+
+/-!
+# Agent.RequestBuilder
+
+A fluent builder that attaches an `Agent` to a `Request.Builder`, letting callers chain header
+and query-parameter setters before dispatching with a typed `send*` terminal.
+
+```lean
+let response ←
+  agent.get "/api/items"
+  |>.header! "Accept" "application/json"
+  |>.queryParam "page" "2"
+  |>.send
+```
+-/
+
+/--
+A `Request.Builder` bound to a specific `Agent`.  Build up headers, query parameters, and body,
+then call one of the `send*` methods to dispatch the request.
+-/
+public structure Agent.RequestBuilder (α : Type) where
+  /--
+  The agent that will send this request.
+  -/
+  agent : Agent α
+
+  /--
+  The underlying request builder.
+  -/
+  builder : Request.Builder
+
+
+namespace Agent.RequestBuilder
+
+/--
+Injects a `Host` header derived from the agent's `host` and `port` if no `Host` header
+is already present.
+-/
+private def withHostHeader [Transport α] (rb : Agent.RequestBuilder α) : Agent.RequestBuilder α :=
+  if rb.builder.line.headers.contains Header.Name.host then
+    rb
+  else
+    let defaultPort := URI.Scheme.defaultPort rb.agent.scheme
+    let hostValue :=
+      if rb.agent.port == defaultPort then toString rb.agent.host
+      else s!"{rb.agent.host}:{rb.agent.port}"
+    { rb with builder := rb.builder.header! "Host" hostValue }
+
+/--
+Prepares the builder by injecting the `Host` header, then calls `f` to build and send the
+request. Cookie injection is handled by `Agent.injectCookies` inside `sendWithRedirects`.
+-/
+private def prepare [Transport α] (rb : Agent.RequestBuilder α)
+    (f : Agent.RequestBuilder α → Async (Response Body.Stream)) : Async (Response Body.Stream) :=
+  f rb.withHostHeader
+
+/--
+Adds a typed header to the request.
+-/
+def header [Transport α] (rb : Agent.RequestBuilder α) (key : Header.Name) (value : Header.Value) : Agent.RequestBuilder α :=
+  { rb with builder := rb.builder.header key value }
+
+/--
+Adds a header to the request. Panics if the name or value is invalid.
+-/
+def header! [Transport α] (rb : Agent.RequestBuilder α) (key : String) (value : String) : Agent.RequestBuilder α :=
+  { rb with builder := rb.builder.header! key value }
+
+/--
+Adds a header to the request. Returns `none` if the name or value is invalid.
+-/
+def header? [Transport α] (rb : Agent.RequestBuilder α) (key : String) (value : String) : Option (Agent.RequestBuilder α) := do
+  let builder ← rb.builder.header? key value
+  pure { rb with builder }
+
+/--
+Sets the request URI from a string. Panics if the string is not a valid request target.
+-/
+def uri! [Transport α] (rb : Agent.RequestBuilder α) (u : String) : Agent.RequestBuilder α :=
+  { rb with builder := rb.builder.uri! u }
+
+/--
+Adds a query parameter to the request URI.
+Works for both origin-form (e.g. set by `agent.get "/path"`) and absolute-form targets.
+-/
+def queryParam [Transport α] (rb : Agent.RequestBuilder α) (key : String) (value : String) : Agent.RequestBuilder α :=
+  let newTarget := match rb.builder.line.uri with
+    | .originForm path query =>
+        .originForm path (some ((query.getD URI.Query.empty).insert key value))
+    | .absoluteForm af =>
+        .absoluteForm { af with query := af.query.insert key value }
+    | other => other
+  { rb with builder := { rb.builder with line := { rb.builder.line with uri := newTarget } } }
+
+/--
+Sends the request with an empty body.
+-/
+def send [Transport α] (rb : Agent.RequestBuilder α) : Async (Response Body.Stream) :=
+  rb.prepare fun rb => do rb.agent.send (← rb.builder.empty)
+
+/--
+Sends the request with a plain-text body.
+Sets `Content-Type: text/plain; charset=utf-8`.
+-/
+def text [Transport α] (rb : Agent.RequestBuilder α) (content : String) : Async (Response Body.Stream) :=
+  rb.prepare fun rb => do rb.agent.send (← rb.builder.text content)
+
+/--
+Sends the request with a JSON body.
+Sets `Content-Type: application/json`.
+-/
+def json [Transport α] (rb : Agent.RequestBuilder α) (content : String) : Async (Response Body.Stream) :=
+  rb.prepare fun rb => do rb.agent.send (← rb.builder.json content)
+
+/--
+Sends the request with a raw binary body.
+Sets `Content-Type: application/octet-stream`.
+-/
+def bytes [Transport α] (rb : Agent.RequestBuilder α) (content : ByteArray) : Async (Response Body.Stream) :=
+  rb.prepare fun rb => do rb.agent.send (← rb.builder.bytes content)
+
+/--
+Sends the request with a streaming body produced by `gen`.
+-/
+def sendStream [Transport α]
+    (rb : Agent.RequestBuilder α)
+    (gen : Body.Stream → Async Unit) : Async (Response Body.Stream) :=
+  rb.prepare fun rb => do rb.agent.send (← rb.builder.stream gen)
+
+end Agent.RequestBuilder
+
+namespace Agent
+
+/--
+Creates a GET request builder for the given path or URL
+-/
+def get [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
+  { agent, builder := Request.get (RequestTarget.parse! path) }
+
+/--
+Creates a POST request builder for the given path or URL
+-/
+def post [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
+  { agent, builder := Request.post (RequestTarget.parse! path) }
+
+/--
+Creates a PUT request builder for the given path or URL
+-/
+def put [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
+  { agent, builder := Request.put (RequestTarget.parse! path) }
+
+/--
+Creates a DELETE request builder for the given path or URL
+-/
+def delete [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
+  { agent, builder := Request.delete (RequestTarget.parse! path) }
+
+/--
+Creates a PATCH request builder for the given path or URL
+-/
+def patch [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
+  { agent, builder := Request.patch (RequestTarget.parse! path) }
+
+/--
+Creates a HEAD request builder for the given path or URL
+-/
+def headReq [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
+  { agent, builder := Request.head (RequestTarget.parse! path) }
+
+/--
+Creates an OPTIONS request builder for the given path or URL.
+-/
+def options [Transport α] (agent : Agent α) (path : String) : Agent.RequestBuilder α :=
+  { agent, builder := Request.options (RequestTarget.parse! path) }
+
+end Std.Http.Client.Agent

src/Std/Internal/Http/Client/Config.lean

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Time
+public import Std.Internal.Http.Protocol.H1
+
+public section
+
+/-!
+# Config
+
+This module exposes the `Config` structure describing timeouts, connection,
+and header configurations for an HTTP client.
+-/
+
+namespace Std.Http.Client
+
+set_option linter.all true
+
+/--
+Client connection configuration with validation.
+-/
+structure Config where
+  /--
+  Maximum number of requests per connection (for keep-alive).
+  -/
+  maxRequestsPerConnection : Nat := 1000
+
+  /--
+  Maximum number of headers allowed per response.
+  -/
+  maxResponseHeaders : Nat := 200
+
+  /--
+  Maximum size of a single header name in bytes.
+  -/
+  maxHeaderNameSize : Nat := 256
+
+  /--
+  Maximum size of a single header value in bytes.
+  -/
+  maxHeaderValueSize : Nat := 16384
+
+  /--
+  Maximum waiting time for additional data before timing out.
+  -/
+  readTimeout : Time.Millisecond.Offset := 30000
+
+  /--
+  Timeout duration for keep-alive connections.
+  -/
+  keepAliveTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨4000, by decide⟩
+
+  /--
+  Timeout for the request lifecycle (send + receive) per connection.
+  DNS resolution and TCP connect are not covered by this timeout.
+  -/
+  requestTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨120000, by decide⟩
+
+  /--
+  Whether to enable keep-alive connections.
+  -/
+  enableKeepAlive : Bool := true
+
+  /--
+  Maximum number of bytes to receive in a single read call.
+  -/
+  maxRecvChunkSize : Nat := 16384
+
+  /--
+  Default buffer size for request payloads.
+  -/
+  defaultRequestBufferSize : Nat := 16384
+
+  /--
+  The user-agent string to send by default.
+  -/
+  userAgent : Option Header.Value := some (.mk "lean-http/1.1")
+
+  /--
+  Maximum number of redirects to follow automatically.
+  Set to 0 to disable automatic redirect following.
+  -/
+  maxRedirects : Nat := 10
+
+  /--
+  Maximum number of times to retry a request after a connection error.
+  Set to 0 to disable automatic retries.
+  -/
+  maxRetries : Nat := 3
+
+  /--
+  Base delay in milliseconds for exponential backoff between retry attempts.
+  The actual delay for attempt `n` (0-indexed) is `min(retryDelay * 2^n, 32000)`.
+  -/
+  retryDelay : Time.Millisecond.Offset := 1000
+
+  /--
+  Optional HTTP proxy address as `(host, port)`.
+  When set, all TCP connections are routed through this proxy and
+  request URIs are rewritten to absolute-form (`GET http://host/path HTTP/1.1`).
+  -/
+  proxy : Option (String × UInt16) := none
+
+  /--
+  Maximum number of bytes allowed in a single response body.
+  When `some n`, reading more than `n` bytes from the body resolves the current
+  request with an error and closes the connection.
+  `none` (default) imposes no limit.
+  -/
+  maxResponseBodySize : Option Nat := none
+
+  /--
+  Optional predicate that decides whether a response status is acceptable.
+  When `none`, all status codes are accepted (no error is thrown).
+  When `some f`, the final response status is passed to `f`; if `f` returns `false`
+  an `IO.Error` is thrown with the numeric status code.
+  Only applied to the final (non-redirect) response, not intermediate `3xx` responses.
+
+  Example — reject anything outside 2xx:
+  ```lean
+  validateStatus := some (fun s => s.toCode / 100 == 2)
+  ```
+  -/
+  validateStatus : Option (Status → Bool) := none
+
+  /--
+  Maximum number of bytes drained from an intermediate redirect response body before
+  -/
+  redirectBodyDrainLimit : Nat := 1024 * 1024
+
+  /--
+  Optional predicate called before following each redirect.
+  -/
+  redirectPolicy : Option (URI.Host → UInt16 → Bool) := none
+
+namespace Config
+
+/--
+Convert this client config into an HTTP/1.1 protocol configuration.
+-/
+def toH1Config (config : Config) : Std.Http.Protocol.H1.Config :=
+  { maxMessages := config.maxRequestsPerConnection
+    maxHeaders := config.maxResponseHeaders
+    maxHeaderNameLength := config.maxHeaderNameSize
+    maxHeaderValueLength := config.maxHeaderValueSize
+    enableKeepAlive := config.enableKeepAlive
+    agentName := config.userAgent
+  }
+
+end Config
+end Std.Http.Client

src/Std/Internal/Http/Client/Connection.lean

@@ -0,0 +1,604 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async.TCP
+public import Std.Internal.Async.ContextAsync
+public import Std.Internal.Http.Transport
+public import Std.Internal.Http.Protocol.H1
+public import Std.Internal.Http.Client.Config
+public import Std.Sync.Watch
+
+public section
+
+namespace Std.Http.Client
+
+open Std Internal IO Async TCP Protocol
+open Time
+
+/--
+Type-erased body operations for use in the request pipeline.
+Captures `Reader` and `Writer` methods as closures so the connection state
+is not parameterized by the body type.
+-/
+structure Body.Operations where
+  /--
+  Selector that resolves when a chunk is available or the body reaches EOF.
+  -/
+  recvSelector : Selector (Option Chunk)
+
+  /--
+  Returns `true` when the body is closed for reading.
+  -/
+  isClosed : Async Bool
+
+  /--
+  Closes the body for reading.
+  -/
+  close : Async Unit
+
+  /--
+  Returns the known content length if available.
+  -/
+  getKnownSize : Async (Option Body.Length)
+
+namespace Body.Operations
+
+/--
+Creates a `Body.Operations` from any type with a `Body` instance.
+-/
+def of [Body β] (body : β) : Body.Operations where
+  recvSelector := Body.recvSelector body
+  isClosed := Body.isClosed body
+  close := Body.close body
+  getKnownSize := Body.getKnownSize body
+
+end Body.Operations
+
+/-!
+# Connection
+
+This module defines the `Connection.handle` loop, used to manage one persistent HTTP/1.1 client
+connection and handle sequential request/response exchanges over it.
+-/
+
+set_option linter.all true
+
+/--
+A request packet queued to the background connection loop.
+-/
+structure RequestPacket where
+  /--
+  The request to send.
+  -/
+  request : Request Body.Operations
+
+  /--
+  Promise resolved with the eventual response.
+  -/
+  responsePromise : IO.Promise (Except Error (Response Body.Stream))
+
+  /--
+  Watch channel updated with the cumulative number of request-body bytes sent.
+  `none` when the caller does not need upload-progress tracking.
+  -/
+  uploadProgress : Option (Watch UInt64) := none
+
+  /--
+  Watch channel updated with the cumulative number of response bytes received.
+  `none` when the caller does not need download-progress tracking.
+  -/
+  downloadProgress : Option (Watch UInt64) := none
+
+namespace RequestPacket
+
+/--
+Resolve the packet with an error.
+-/
+def onError (packet : RequestPacket) (error : Error) : BaseIO Unit :=
+  discard <| packet.responsePromise.resolve (.error error)
+
+/--
+Resolve the packet with a response.
+-/
+def onResponse (packet : RequestPacket) (response : Response Body.Stream) : BaseIO Unit :=
+  discard <| packet.responsePromise.resolve (.ok response)
+
+end RequestPacket
+
+namespace Connection
+
+/--
+Events produced by the async select loop in `pollNextEvent`.
+Each variant corresponds to one possible outcome of waiting for I/O.
+-/
+private inductive Recv
+  | bytes (x : Option ByteArray)
+  | requestBody (x : Option Chunk)
+  | bodyInterest (x : Bool)
+  | packet (x : Option RequestPacket)
+  | timeout
+  | shutdown
+  | close
+
+/--
+The set of I/O sources to wait on during a single poll iteration.
+Each `Option` field is `none` when that source is not currently active.
+-/
+private structure PollSources (α : Type) where
+  socket : Option α
+  expect : Option Nat
+  requestBody : Option Body.Operations
+  requestChannel : Option (Std.CloseableChannel RequestPacket)
+  responseBody : Option Body.Stream
+  timeout : Millisecond.Offset
+  keepAliveTimeout : Option Millisecond.Offset
+  connectionContext : CancellationContext
+
+/--
+All mutable state carried through the connection processing loop.
+Bundled into a struct so it can be passed to and returned from helper functions.
+-/
+private structure ConnectionState where
+  machine : H1.Machine .sending
+  currentTimeout : Millisecond.Offset
+  keepAliveTimeout : Option Millisecond.Offset
+  currentRequest : Option RequestPacket
+  requestBody : Option Body.Operations
+  responseStream : Option Body.Stream
+  requiresData : Bool
+  expectData : Option Nat
+  waitingForRequest : Bool
+  isInformationalResponse : Bool
+  waitingForContinue : Bool
+  pendingRequestBody : Option Body.Operations
+  uploadProgress : Option (Watch UInt64) := none
+  uploadBytes : UInt64 := 0
+  downloadProgress : Option (Watch UInt64) := none
+  downloadBytes : UInt64 := 0
+  downloadBodyBytes : UInt64 := 0
+
+@[inline]
+private def requestHasExpectContinue (request : Request Body.Operations) : Bool :=
+  match request.line.headers.getAll? Header.Name.expect with
+  | some #[value] =>
+      match Header.Expect.parse value with
+      | some res => res.expect
+      | none => false
+  | _ => false
+
+/--
+Waits for the next I/O event across all active sources described by `sources`.
+Computes the socket recv size from `config`, then races all active selectables.
+Returns `.close` on transport errors.
+-/
+private def pollNextEvent
+    [Transport α]
+    (config : Config) (sources : PollSources α) : Async Recv := do
+
+  let expectedBytes := sources.expect
+    |>.getD config.defaultRequestBufferSize
+    |>.min config.maxRecvChunkSize
+    |>.toUInt64
+
+  let mut selectables : Array (Selectable Recv) := #[
+    .case sources.connectionContext.doneSelector (fun _ => do
+      let reason ← sources.connectionContext.getCancellationReason
+      match reason with
+      | some .deadline => pure .timeout
+      | _ => pure .shutdown)
+  ]
+
+  if let some socket := sources.socket then
+    selectables := selectables.push (.case (Transport.recvSelector socket expectedBytes) (Recv.bytes · |> pure))
+
+    if let some keepAliveTimeout := sources.keepAliveTimeout then
+      selectables := selectables.push (.case (← Selector.sleep keepAliveTimeout) (fun _ => pure .timeout))
+    else
+      selectables := selectables.push (.case (← Selector.sleep sources.timeout) (fun _ => pure .timeout))
+
+  if let some requestBody := sources.requestBody then
+    selectables := selectables.push (.case requestBody.recvSelector (Recv.requestBody · |> pure))
+
+  if let some requestChannel := sources.requestChannel then
+    selectables := selectables.push (.case requestChannel.recvSelector (Recv.packet · |> pure))
+
+  if let some responseBody := sources.responseBody then
+    selectables := selectables.push (.case (responseBody.interestSelector) (Recv.bodyInterest · |> pure))
+
+  try Selectable.one selectables catch _ => pure .close
+
+/--
+Processes all H1 events from a single machine step, updating the connection state.
+Handles keep-alive resets, body-size tracking, `Expect: 100-continue`, and parse errors.
+Returns the updated state and `true` if a parse failure was encountered.
+-/
+private def processH1Events
+    (config : Config)
+    (events : Array (H1.Event .sending))
+    (state : ConnectionState) : Async (ConnectionState × Bool) := do
+
+  let mut st := state
+  let mut sawFailure := false
+
+  for event in events do
+    match event with
+    | .needMoreData expect =>
+      st := { st with requiresData := true, expectData := expect }
+
+    -- `.needAnswer` is emitted by processWrite when the writer is in `waitingHeaders`
+    -- state in `.sending` mode, signalling that the client machine needs the next request.
+    -- The client loop tracks this through `waitingForRequest` instead, so this event
+    -- is intentionally a no-op here.
+    | .needAnswer => pure ()
+
+    | .endHeaders head =>
+      if head.status.isInformational then
+        -- Informational (1xx) responses are interim; do not resolve the caller's
+        -- promise. The machine loops back to read the real response.
+        st := { st with isInformationalResponse := true }
+
+        -- A `100 Continue` response authorises the body: move it from the
+        -- pending slot into `requestBody` so the pump loop starts sending.
+        if head.status == .continue && st.waitingForContinue then
+          st := { st with
+            requestBody := st.pendingRequestBody
+            pendingRequestBody := none
+            waitingForContinue := false
+          }
+      else
+        st := { st with
+          isInformationalResponse := false
+          currentTimeout := config.readTimeout
+          keepAliveTimeout := none
+        }
+
+        -- A non-informational response while we were still waiting for
+        -- `100 Continue`: the server rejected (or bypassed) the expectation.
+        -- Discard the pending body — it must not be sent.
+        if st.waitingForContinue then
+          if let some body := st.pendingRequestBody then
+            if !(← body.isClosed) then body.close
+          st := { st with pendingRequestBody := none, waitingForContinue := false }
+
+        if let some body := st.responseStream then
+          if let some length := head.getSize true then
+            Body.setKnownSize body (some length)
+
+        if let some packet := st.currentRequest then
+          if let some incoming := st.responseStream then
+            packet.onResponse { line := head, body := incoming }
+
+    | .closeBody =>
+      -- Skip closing for informational (1xx) responses; the channel stays
+      -- open for the real response body that follows.
+      if !st.isInformationalResponse then
+        if let some body := st.responseStream then
+          if ¬(← Body.isClosed body) then Body.close body
+
+    | .next =>
+      -- Reset all per-request state for the next pipelined request.
+      if let some body := st.requestBody then
+        if ¬(← body.isClosed) then body.close
+
+      if let some body := st.pendingRequestBody then
+        if ¬(← body.isClosed) then body.close
+
+      if let some body := st.responseStream then
+        if ¬(← Body.isClosed body) then Body.close body
+
+      if let some w := st.uploadProgress then Watch.close w
+      if let some w := st.downloadProgress then Watch.close w
+
+      st := { st with
+        requestBody := none
+        pendingRequestBody := none
+        waitingForContinue := false
+        responseStream := none
+        currentRequest := none
+        isInformationalResponse := false
+        waitingForRequest := true
+        keepAliveTimeout := some config.keepAliveTimeout.val
+        currentTimeout := config.keepAliveTimeout.val
+        uploadProgress := none
+        uploadBytes := 0
+        downloadProgress := none
+        downloadBytes := 0
+        downloadBodyBytes := 0
+      }
+
+    | .failed err =>
+      if let some packet := st.currentRequest then
+        packet.onError (.userError (toString err))
+      sawFailure := true
+
+    | .«continue» => pure ()
+
+    | .close => pure ()
+
+  return (st, sawFailure)
+
+/--
+Computes the active `PollSources` for the current connection state.
+Determines which I/O sources need attention and whether to include the socket.
+-/
+private def buildPollSources
+    [Transport α]
+    (socket : α) (requestChannel : Std.CloseableChannel RequestPacket)
+    (connectionContext : CancellationContext) (state : ConnectionState)
+    : Async (PollSources α) := do
+  -- Always include an active request body, even if already closed.
+  -- A closed body's recvSelector resolves immediately with `none`, which
+  -- triggers `userClosedBody` so the H1 machine can finalize chunked encoding.
+  let requestBodySource :=
+    state.requestBody
+
+  let responseBodySource ←
+    if state.machine.canPullBodyNow then
+      if let some body := state.responseStream then
+        if ¬(← Body.isClosed body) then pure (some body) else pure none
+      else
+        pure none
+    else
+      pure none
+
+  let pollSocket :=
+    state.requiresData ∨
+    state.machine.writer.sentMessage ∨
+    !state.waitingForRequest ∨
+    requestBodySource.isSome ∨
+    state.machine.canPullBody
+
+  return {
+    socket := if pollSocket then some socket else none
+    expect := state.expectData
+    requestBody := requestBodySource
+    requestChannel := if state.waitingForRequest then some requestChannel else none
+    responseBody := responseBodySource
+    timeout := state.currentTimeout
+    keepAliveTimeout := state.keepAliveTimeout
+    connectionContext := connectionContext
+  }
+
+/--
+Processes a single async I/O event and updates the connection state.
+Returns the updated state and `true` if the connection should be closed immediately.
+-/
+private def handleRecvEvent
+    (config : Config)
+    (event : Recv) (state : ConnectionState) : Async (ConnectionState × Bool) := do
+
+  match event with
+  | .bytes (some bytes) =>
+    let newDownloadBytes := state.downloadBytes + bytes.size.toUInt64
+    if let some w := state.downloadProgress then
+      Watch.send w newDownloadBytes
+    return ({ state with machine := state.machine.feed bytes, downloadBytes := newDownloadBytes }, false)
+
+  | .bytes none =>
+    return ({ state with machine := state.machine.noMoreInput }, false)
+
+  | .requestBody (some chunk) =>
+    let newUploadBytes := state.uploadBytes + chunk.data.size.toUInt64
+    if let some w := state.uploadProgress then
+      Watch.send w newUploadBytes
+    return ({ state with machine := state.machine.sendData #[chunk], uploadBytes := newUploadBytes }, false)
+
+  | .requestBody none =>
+    if let some body := state.requestBody then
+      if ¬(← body.isClosed) then body.close
+    return ({ state with machine := state.machine.userClosedBody, requestBody := none }, false)
+
+  | .bodyInterest interested =>
+    if interested then
+      let (newMachine, pulledChunk) := state.machine.pullBody
+      let mut st := { state with machine := newMachine }
+
+      if let some pulled := pulledChunk then
+        let newBodyBytes := st.downloadBodyBytes + pulled.chunk.data.size.toUInt64
+        st := { st with downloadBodyBytes := newBodyBytes }
+
+        -- Enforce the response body size limit before writing data to the caller.
+        if let some maxSize := config.maxResponseBodySize then
+          if newBodyBytes > maxSize.toUInt64 then
+            if let some packet := st.currentRequest then
+              packet.onError (.userError "response body exceeds maximum allowed size")
+            if let some body := st.responseStream then
+              if ¬(← Body.isClosed body) then Body.close body
+            if let some w := st.downloadProgress then Watch.close w
+            return ({ st with
+              machine := st.machine.closeWriter.closeReader.noMoreInput
+              currentRequest := none
+              responseStream := none
+              downloadProgress := none
+            }, false)
+
+        if let some body := st.responseStream then
+          -- If the caller has dropped/closed the incoming side, the write fails.
+          -- Silently swallowing the error is correct: the loop must continue pulling
+          -- wire bytes to keep the connection in a valid state for reuse.
+          try body.send pulled.chunk pulled.incomplete
+          catch _ => pure ()
+
+          if pulled.final then
+            if ¬(← Body.isClosed body) then Body.close body
+            st := { st with responseStream := none }
+
+      return (st, false)
+    else
+      return (state, false)
+
+  | .packet (some packet) =>
+    let mut machine := state.machine.send packet.request.line
+    let mut requestBody : Option Body.Operations := none
+    let mut pendingRequestBody : Option Body.Operations := none
+    let mut waitingForContinue := false
+
+    if requestHasExpectContinue packet.request then
+      -- Defer body pumping until the server sends `100 Continue`, but still
+      -- set the known size so that `Content-Length` is included in the request
+      -- headers (required by RFC 9112; servers need it to fire checkContinue).
+      if let some size ← packet.request.body.getKnownSize then
+        machine := machine.setKnownSize size
+      waitingForContinue := true
+      pendingRequestBody := some packet.request.body
+    else
+      if let some size ← packet.request.body.getKnownSize then
+        machine := machine.setKnownSize size
+      requestBody := some packet.request.body
+
+    let responseStream ← Body.mkStream
+
+    return ({ state with
+      machine := machine
+      currentRequest := some packet
+      waitingForRequest := false
+      currentTimeout := config.requestTimeout.val
+      keepAliveTimeout := none
+      requestBody := requestBody
+      pendingRequestBody := pendingRequestBody
+      waitingForContinue := waitingForContinue
+      responseStream := some responseStream
+      uploadProgress := packet.uploadProgress
+      uploadBytes := 0
+      downloadProgress := packet.downloadProgress
+      downloadBytes := 0
+    }, false)
+
+  | .packet none => return (state, true)
+
+  | .close => return (state, true)
+
+  | .timeout =>
+    if let some packet := state.currentRequest then
+      packet.onError (.userError "request timeout")
+    if let some body := state.responseStream then
+      if ¬(← Body.isClosed body) then Body.close body
+    if let some w := state.uploadProgress then Watch.close w
+    if let some w := state.downloadProgress then Watch.close w
+    return ({ state with
+      machine := state.machine.closeWriter.closeReader.noMoreInput
+      currentRequest := none
+      responseStream := none
+      uploadProgress := none
+      downloadProgress := none
+    }, false)
+
+  | .shutdown =>
+    if let some packet := state.currentRequest then
+      packet.onError (.userError "connection shutdown")
+    if let some body := state.responseStream then
+      if ¬(← Body.isClosed body) then Body.close body
+    if let some w := state.uploadProgress then Watch.close w
+    if let some w := state.downloadProgress then Watch.close w
+    return ({ state with
+      machine := state.machine.closeWriter.closeReader.noMoreInput
+      currentRequest := none
+      responseStream := none
+      uploadProgress := none
+      downloadProgress := none
+    }, false)
+
+/--
+Runs the main request/response processing loop for a single connection.
+Drives the HTTP/1.1 state machine through four phases each iteration:
+close finished readers, send buffered output, process H1 events, poll for I/O.
+-/
+protected def handle
+    [Transport α]
+    (socket : α)
+    (machine : H1.Machine .sending)
+    (config : Config)
+    (connectionContext : CancellationContext)
+    (requestChannel : Std.CloseableChannel RequestPacket) : Async Unit := do
+
+  let mut state : ConnectionState := {
+    machine := machine
+    currentTimeout := config.keepAliveTimeout.val
+    keepAliveTimeout := some config.keepAliveTimeout.val
+    currentRequest := none
+    requestBody := none
+    responseStream := none
+    requiresData := false
+    expectData := none
+    waitingForRequest := true
+    isInformationalResponse := false
+    waitingForContinue := false
+    pendingRequestBody := none
+  }
+
+  while ¬state.machine.halted do
+
+    -- Phase 1: close any reader that the user has signalled is done.
+    if let some body := state.requestBody then
+      if ← body.isClosed then
+        state := { state with machine := state.machine.userClosedBody, requestBody := none }
+
+    -- Phase 2: advance the state machine and flush any output.
+    let (newMachine, step) := state.machine.step
+    state := { state with machine := newMachine }
+
+    if step.output.size > 0 then
+      try Transport.sendAll socket #[step.output.toByteArray]
+      catch _ =>
+        if let some packet := state.currentRequest then
+          packet.onError (.userError "connection write failed")
+        if let some body := state.responseStream then
+          if ¬(← Body.isClosed body) then Body.close body
+        state := { state with
+          machine := state.machine.closeWriter.closeReader.noMoreInput
+          currentRequest := none
+          responseStream := none
+        }
+        break
+
+    -- Phase 3: process all events emitted by this step.
+    let (newState, sawFailure) ← processH1Events config step.events state
+    state := newState
+    if sawFailure then break
+
+    -- Phase 4: wait for the next IO event when any source needs attention.
+    if state.requiresData ∨ state.waitingForRequest ∨ state.currentRequest.isSome ∨ state.requestBody.isSome ∨ state.machine.canPullBody then
+      let sources ← buildPollSources socket requestChannel connectionContext state
+      state := { state with requiresData := false }
+      let event ← pollNextEvent config sources
+      let (newState, shouldClose) ← handleRecvEvent config event state
+      state := newState
+      if shouldClose then break
+
+  -- Clean up: notify any in-flight request and close all open streams.
+  if let some packet := state.currentRequest then
+    packet.onError (.userError "connection closed")
+
+  if let some w := state.uploadProgress then
+    Watch.close w
+
+  if let some w := state.downloadProgress then
+    Watch.close w
+
+  if let some body := state.responseStream then
+    if ¬(← Body.isClosed body) then Body.close body
+
+  if let some body := state.requestBody then
+    if ¬(← body.isClosed) then body.close
+
+  if let some body := state.pendingRequestBody then
+    if ¬(← body.isClosed) then body.close
+
+  discard <| EIO.toBaseIO requestChannel.close
+
+  -- Drain any remaining queued packets.
+  repeat do
+    match ← requestChannel.tryRecv with
+    | some packet => packet.onError (.userError "connection closed")
+    | none => break
+
+  Transport.close socket
+
+end Connection
+
+end Std.Http.Client