fix: tests

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

.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

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/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/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/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/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,189 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data
+public import Std.Internal.Http.Server
+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/Data/Headers/Basic.lean

@@ -6,6 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
+public import Std.Internal.Http.Data.URI
 public import Std.Internal.Http.Data.Headers.Name
 public import Std.Internal.Http.Data.Headers.Value
 public import Std.Internal.Parsec.Basic
@@ -215,4 +216,97 @@ def serialize (connection : Connection) : Header.Name × Header.Value :=
 
 instance : Header Connection := ⟨parse, serialize⟩
 
-end Std.Http.Header.Connection
+end Connection
+
+/--
+The `Host` header.
+
+Represents the authority component of a URI:
+  host [ ":" port ]
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-host-and-authority
+-/
+structure Host where
+  /--
+  Host name (reg-name, IPv4, or IPv6 literal).
+  -/
+  host : URI.Host
+
+  /--
+  Optional port.
+  -/
+  port : URI.Port
+deriving Repr, BEq
+
+namespace Host
+
+/--
+Parses a `Host` header value.
+-/
+def parse (v : Value) : Option Host :=
+  let parsed := (Std.Http.URI.Parser.parseHostHeader <* Std.Internal.Parsec.eof).run v.value.toUTF8
+  match parsed with
+  | .ok ⟨host, port⟩ => some ⟨host, port⟩
+  | .error _ => none
+
+/--
+Serializes a `Host` header back to a name and a value.
+-/
+def serialize (host : Host) : Header.Name × Header.Value :=
+  let value := match host.port with
+    | .value port => Header.Value.ofString! s!"{host.host}:{port}"
+    | .empty => Header.Value.ofString! s!"{host.host}:"
+    | .omitted => Header.Value.ofString! <| toString host.host
+
+  (.mk "host", value)
+
+instance : Header Host := ⟨parse, serialize⟩
+
+end Host
+
+/--
+The `Expect` header.
+
+Represents an expectation token.
+The only standardized expectation is `100-continue`.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-expect
+-/
+structure Expect where
+
+  /--
+  True if the client expects `100-continue`.
+  -/
+  expect : Bool
+deriving Repr, BEq
+
+namespace Expect
+
+/--
+Parses an `Expect` header.
+
+Succeeds only if the value is exactly `100-continue`
+(case-insensitive, trimmed).
+-/
+def parse (v : Value) : Option Expect :=
+  let normalized := v.value.trimAscii.toString.toLower
+
+  if normalized == "100-continue" then
+    some ⟨true⟩
+  else
+    none
+
+/--
+Serializes an `Expect` header.
+-/
+def serialize (e : Expect) : Header.Name × Header.Value :=
+  if e.expect then
+    (Header.Name.expect, Value.ofString! "100-continue")
+  else
+    (Header.Name.expect, Value.ofString! "")
+
+instance : Header Expect := ⟨parse, serialize⟩
+
+end Expect
+
+end Std.Http.Header

src/Std/Internal/Http/Data/URI/Parser.lean

@@ -52,13 +52,13 @@ private def parseScheme (config : URI.Config) : Parser URI.Scheme := do
   if config.maxSchemeLength = 0 then
     fail "scheme length limit is 0 (no scheme allowed)"
 
-  let first ← takeWhileUpTo1 isAlphaByte 1
-  let rest ← takeWhileUpTo
+  let first : UInt8 ← satisfy isAlphaByte
+  let rest ← takeWhileAtMost
     (fun c =>
       isAlphaNum c ∨
       c = '+'.toUInt8 ∨ c = '-'.toUInt8 ∨ c = '.'.toUInt8)
     (config.maxSchemeLength - 1)
-  let schemeBytes := first.toByteArray ++ rest.toByteArray
+  let schemeBytes := ByteArray.empty.push first ++ rest.toByteArray
   let str := String.fromUTF8! schemeBytes |>.toLower
 
   if h : URI.IsValidScheme str then
@@ -68,7 +68,7 @@ private def parseScheme (config : URI.Config) : Parser URI.Scheme := do
 
 -- port = 1*DIGIT
 private def parsePortNumber : Parser UInt16 := do
-  let portBytes ← takeWhileUpTo1 isDigitByte 5
+  let portBytes ← takeWhileAtMost isDigitByte 5
 
   let portStr := String.fromUTF8! portBytes.toByteArray
 
@@ -82,7 +82,7 @@ private def parsePortNumber : Parser UInt16 := do
 
 -- userinfo = *( unreserved / pct-encoded / sub-delims / ":" )
 private def parseUserInfo (config : URI.Config) : Parser URI.UserInfo := do
-  let userBytesName ← takeWhileUpTo
+  let userBytesName ← takeWhileAtMost
     (fun x =>
       x ≠ ':'.toUInt8 ∧
       (isUserInfoChar x ∨ x = '%'.toUInt8))
@@ -94,7 +94,7 @@ private def parseUserInfo (config : URI.Config) : Parser URI.UserInfo := do
   let userPassEncoded ← if ← peekIs (· == ':'.toUInt8) then
       skip
 
-      let userBytesPass ← takeWhileUpTo
+      let userBytesPass ← takeWhileAtMost
         (fun x => isUserInfoChar x ∨ x = '%'.toUInt8)
         config.maxUserInfoLength
 
@@ -113,7 +113,7 @@ private def parseUserInfo (config : URI.Config) : Parser URI.UserInfo := do
 private def parseIPv6 : Parser Net.IPv6Addr := do
   skipByte '['.toUInt8
 
-  let result ← takeWhileUpTo1
+  let result ← takeWhile1AtMost
     (fun x => x = ':'.toUInt8 ∨ x = '.'.toUInt8 ∨ isHexDigitByte x)
     256
 
@@ -127,7 +127,7 @@ private def parseIPv6 : Parser Net.IPv6Addr := do
 
 -- IPv4address = dec-octet "." dec-octet "." dec-octet "." dec-octet
 private def parseIPv4 : Parser Net.IPv4Addr := do
-  let result ← takeWhileUpTo1
+  let result ← takeWhile1AtMost
     (fun x => x = '.'.toUInt8 ∨ isDigitByte x)
     256
 
@@ -148,8 +148,8 @@ private def parseHost (config : URI.Config) : Parser URI.Host := do
       if let some ipv4 ← tryOpt parseIPv4 then
         return .ipv4 ipv4
 
-    -- We intentionally parse DNS names here (not full RFC 3986 reg-name).
-    let some str := String.fromUTF8? (← takeWhileUpTo1
+    -- It needs to be a legal DNS label, so it differs from reg-name.
+    let some str := String.fromUTF8? (← takeWhile1AtMost
       (fun x => isAlphaNum x ∨ x = '-'.toUInt8 ∨ x = '.'.toUInt8)
       config.maxHostLength).toByteArray
       | fail s!"invalid host"
@@ -187,7 +187,7 @@ private def parseAuthority (config : URI.Config) : Parser URI.Authority := do
 
 -- segment = *pchar
 private def parseSegment (config : URI.Config) : Parser ByteSlice := do
-  takeWhileUpTo (fun c => isPChar c ∨ c = '%'.toUInt8) config.maxSegmentLength
+  takeWhileAtMost (fun c => isPChar c ∨ c = '%'.toUInt8) config.maxSegmentLength
 
 /-
 path = path-abempty ; begins with "/" or is empty
@@ -272,7 +272,7 @@ def parsePath (config : URI.Config) (forceAbsolute : Bool) (allowEmpty : Bool) :
 -- query = *( pchar / "/" / "?" )
 private def parseQuery (config : URI.Config) : Parser URI.Query := do
   let queryBytes ←
-    takeWhileUpTo (fun c => isQueryChar c ∨ c = '%'.toUInt8) config.maxQueryLength
+    takeWhileAtMost (fun c => isQueryChar c ∨ c = '%'.toUInt8) config.maxQueryLength
 
   let some queryStr := String.fromUTF8? queryBytes.toByteArray
     | fail "invalid query string"
@@ -304,7 +304,7 @@ private def parseQuery (config : URI.Config) : Parser URI.Query := do
 --  fragment = *( pchar / "/" / "?" )
 private def parseFragment (config : URI.Config) : Parser URI.EncodedFragment := do
   let fragmentBytes ←
-    takeWhileUpTo (fun c => isFragmentChar c ∨ c = '%'.toUInt8) config.maxFragmentLength
+    takeWhileAtMost (fun c => isFragmentChar c ∨ c = '%'.toUInt8) config.maxFragmentLength
 
   let some fragmentStr := URI.EncodedFragment.ofByteArray? fragmentBytes.toByteArray
     | fail "invalid percent encoding in fragment"

src/Std/Internal/Http/Protocol/H1/Config.lean

@@ -0,0 +1,134 @@
+/-
+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.Data
+public import Std.Internal.Http.Internal
+
+public section
+
+/-!
+# HTTP/1.1 Configuration
+
+This module defines the configuration options for HTTP/1.1 protocol processing,
+including connection limits, header constraints, and various size limits.
+-/
+
+namespace Std.Http.Protocol.H1
+
+set_option linter.all true
+
+open Std Internal Parsec ByteArray
+open Internal
+
+/--
+Connection limits and parser bounds configuration.
+-/
+structure Config where
+  /--
+  Maximum number of requests (server) or responses (client) per connection.
+  -/
+  maxMessages : Nat := 100
+
+  /--
+  Maximum number of headers allowed per message.
+  -/
+  maxHeaders : Nat := 100
+
+  /--
+  Maximum aggregate byte size of all header field lines in a single message
+  (name + value bytes plus 4 bytes per line for `: ` and `\r\n`). Default: 64 KiB.
+  -/
+  maxHeaderBytes : Nat := 65536
+
+  /--
+  Whether to enable keep-alive connections by default.
+  -/
+  enableKeepAlive : Bool := true
+
+  /--
+  The `Server` header value injected into outgoing responses (receiving mode) or the
+  `User-Agent` header value injected into outgoing requests (sending mode).
+  `none` suppresses the header entirely.
+  -/
+  agentName : Option Header.Value := none
+
+  /--
+  Maximum length of request URI (default: 8192 bytes).
+  -/
+  maxUriLength : Nat := 8192
+
+  /--
+  Maximum number of bytes consumed while parsing request/status start-lines (default: 8192 bytes).
+  -/
+  maxStartLineLength : Nat := 8192
+
+  /--
+  Maximum length of header field name (default: 256 bytes).
+  -/
+  maxHeaderNameLength : Nat := 256
+
+  /--
+  Maximum length of header field value (default: 8192 bytes).
+  -/
+  maxHeaderValueLength : Nat := 8192
+
+  /--
+  Maximum number of spaces in delimiter sequences (default: 16).
+  -/
+  maxSpaceSequence : Nat := 16
+
+  /--
+  Maximum number of leading empty lines (bare CRLF) to skip before a request-line
+  (RFC 9112 §2.2 robustness). Default: 8.
+  -/
+  maxLeadingEmptyLines : Nat := 8
+
+  /--
+  Maximum number of extensions on a single chunk-size line (default: 16).
+  -/
+  maxChunkExtensions : Nat := 16
+
+  /--
+  Maximum length of chunk extension name (default: 256 bytes).
+  -/
+  maxChunkExtNameLength : Nat := 256
+
+  /--
+  Maximum length of chunk extension value (default: 256 bytes).
+  -/
+  maxChunkExtValueLength : Nat := 256
+
+  /--
+  Maximum number of bytes consumed while parsing one chunk-size line with extensions (default: 8192 bytes).
+  -/
+  maxChunkLineLength : Nat := 8192
+
+  /--
+  Maximum allowed chunk payload size in bytes (default: 8 MiB).
+  -/
+  maxChunkSize : Nat := 8 * 1024 * 1024
+
+  /--
+  Maximum allowed total body size per message in bytes (default: 64 MiB).
+  This limit applies across all body framing modes. For chunked transfer encoding,
+  chunk-size lines (including extensions) and the trailer section also count toward
+  this limit, so the total wire bytes consumed by the body cannot exceed this value.
+  -/
+  maxBodySize : Nat := 64 * 1024 * 1024
+
+  /--
+  Maximum length of reason phrase (default: 512 bytes).
+  -/
+  maxReasonPhraseLength : Nat := 512
+
+  /--
+  Maximum number of trailer headers (default: 20).
+  -/
+  maxTrailerHeaders : Nat := 20
+
+end Std.Http.Protocol.H1

src/Std/Internal/Http/Protocol/H1/Error.lean

@@ -0,0 +1,110 @@
+/-
+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.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+
+public section
+
+/-!
+# HTTP/1.1 Errors
+
+This module defines the error types for HTTP/1.1 protocol processing,
+including parsing errors, timeout errors, and connection errors.
+-/
+
+namespace Std.Http.Protocol.H1
+
+set_option linter.all true
+
+/--
+Specific HTTP processing errors with detailed information.
+-/
+inductive Error
+  /--
+  Malformed start line (request-line or status-line).
+  -/
+  | invalidStatusLine
+
+  /--
+  Invalid or malformed header.
+  -/
+  | invalidHeader
+
+  /--
+  Request timeout occurred.
+  -/
+  | timeout
+
+  /--
+  Request entity too large.
+  -/
+  | entityTooLarge
+
+  /--
+  Request URI is too long.
+  -/
+  | uriTooLong
+
+  /--
+  Unsupported HTTP version.
+  -/
+  | unsupportedVersion
+
+  /--
+  Invalid chunk encoding.
+  -/
+  | invalidChunk
+
+  /--
+  Connection closed.
+  -/
+  | connectionClosed
+
+  /--
+  Bad request or response message.
+  -/
+  | badMessage
+
+  /--
+  The number of header fields in the message exceeds the configured limit.
+  Maps to HTTP 431 Request Header Fields Too Large.
+  -/
+  | tooManyHeaders
+
+  /--
+  The aggregate byte size of all header fields exceeds the configured limit.
+  Maps to HTTP 431 Request Header Fields Too Large.
+  -/
+  | headersTooLarge
+
+  /--
+  Generic error with message.
+  -/
+  | other (message : String)
+deriving Repr, BEq
+
+instance : ToString Error where
+  toString
+  | .invalidStatusLine => "Invalid status line"
+  | .invalidHeader => "Invalid header"
+  | .timeout => "Timeout"
+  | .entityTooLarge => "Entity too large"
+  | .uriTooLong => "URI too long"
+  | .unsupportedVersion => "Unsupported version"
+  | .invalidChunk => "Invalid chunk"
+  | .connectionClosed => "Connection closed"
+  | .badMessage => "Bad message"
+  | .tooManyHeaders => "Too many headers"
+  | .headersTooLarge => "Headers too large"
+  | .other msg => s!"Other error: {msg}"
+

src/Std/Internal/Http/Protocol/H1/Event.lean

@@ -0,0 +1,73 @@
+/-
+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.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Internal.Http.Protocol.H1.Error
+
+public section
+
+/-!
+# HTTP/1.1 Events
+
+This module defines the events that can occur during HTTP/1.1 message processing,
+including header completion and control/error signals.
+-/
+
+namespace Std.Http.Protocol.H1
+
+set_option linter.all true
+
+/--
+Events emitted during HTTP message processing.
+-/
+inductive Event (dir : Direction)
+  /--
+  Indicates that all headers have been successfully parsed.
+  -/
+  | endHeaders (head : Message.Head dir)
+
+  /--
+  Signals that additional input data is required to continue processing.
+  -/
+  | needMoreData (size : Option Nat)
+
+  /--
+  Indicates a failure during parsing or processing.
+  -/
+  | failed (err : Error)
+
+  /--
+  Requests that the connection be closed.
+  -/
+  | close
+
+  /--
+  The body should be closed.
+  -/
+  | closeBody
+
+  /--
+  Indicates that a response is required.
+  -/
+  | needAnswer
+
+  /--
+  Indicates readiness to process the next message.
+  -/
+  | next
+
+  /--
+  Signals that an `Expect: 100-continue` decision is pending.
+  -/
+  | «continue»
+deriving Inhabited, Repr

src/Std/Internal/Http/Protocol/H1/Message.lean

@@ -0,0 +1,139 @@
+/-
+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
+import Init.Data.Array
+public import Std.Internal.Http.Data
+
+public section
+
+/-!
+# Message
+
+This module provides types and operations for HTTP/1.1 messages, centered around the `Direction`
+type which models the server's role in message exchange: `Direction.receiving` for parsing incoming
+requests from clients, and `Direction.sending` for generating outgoing responses to clients.
+The `Message.Head` type is parameterized by `Direction` and resolves to `Request.Head` or
+`Response.Head` accordingly, enabling generic code that works uniformly across both phases
+while exposing common operations such as headers, version, and `shouldKeepAlive`
+-/
+
+namespace Std.Http.Protocol.H1
+
+set_option linter.all true
+
+/--
+Direction of message flow from the server's perspective.
+-/
+inductive Direction
+  /--
+  Receiving and parsing incoming requests from clients.
+  -/
+  | receiving
+
+  /--
+  Client perspective: writing outgoing requests and reading incoming responses.
+  -/
+  | sending
+deriving BEq
+
+/--
+Inverts the message direction.
+-/
+@[expose]
+abbrev Direction.swap : Direction → Direction
+  | .receiving => .sending
+  | .sending => .receiving
+
+/--
+Gets the message head type based on direction.
+-/
+@[expose]
+def Message.Head : Direction → Type
+  | .receiving => Request.Head
+  | .sending => Response.Head
+
+/--
+Gets the headers of a `Message`.
+-/
+def Message.Head.headers (m : Message.Head dir) : Headers :=
+  match dir with
+  | .receiving => Request.Head.headers m
+  | .sending => Response.Head.headers m
+
+/--
+Gets the version of a `Message`.
+-/
+def Message.Head.version (m : Message.Head dir) : Version :=
+  match dir with
+  | .receiving => Request.Head.version m
+  | .sending => Response.Head.version m
+
+/--
+Determines the message body size based on the `Content-Length` header and the `Transfer-Encoding` (chunked) flag.
+-/
+def Message.Head.getSize (message : Message.Head dir) (allowEOFBody : Bool) : Option Body.Length :=
+  let contentLength := message.headers.getAll? .contentLength
+
+  match message.headers.getAll? .transferEncoding with
+  | none =>
+      match contentLength with
+      | some #[cl] => .fixed <$> cl.value.toNat?
+      | some _ => none -- To avoid request smuggling with malformed/multiple content-length headers.
+      | none => if allowEOFBody then some (.fixed 0) else none
+
+  -- Single transfer-encoding header.
+  | some #[header] =>
+    let te := Header.TransferEncoding.parse header
+
+    match Header.TransferEncoding.isChunked <$> te, contentLength with
+    | some true, none =>
+        -- HTTP/1.0 does not define chunked transfer encoding (RFC 2068 §19.4.6).
+        -- A server MUST NOT use chunked with an HTTP/1.0 peer; likewise, an
+        -- HTTP/1.0 request carrying Transfer-Encoding: chunked is malformed.
+        if message.version == .v10 then none else some .chunked
+    | _, _ => none -- To avoid request smuggling when TE and CL are mixed.
+
+  -- We disallow multiple transfer-encoding headers.
+  | some _ => none
+/--
+Checks whether the message indicates that the connection should be kept alive.
+-/
+def Message.Head.shouldKeepAlive (message : Message.Head dir) : Bool :=
+  let tokens? : Option (Array String) :=
+    match message.headers.getAll? .connection with
+    | none => some #[]
+    | some values =>
+        values.foldl (fun acc raw => do
+          let acc ← acc
+          let parsed ← Header.Connection.parse raw
+          pure (acc ++ parsed.tokens)
+        ) (some #[])
+
+  match tokens? with
+  | none =>false
+  | some tokens =>
+      if message.version == .v11 then
+        !tokens.any (· == "close")
+      else
+        tokens.any (· == "keep-alive")
+
+instance : Repr (Message.Head dir) :=
+  match dir with
+  | .receiving => inferInstanceAs (Repr Request.Head)
+  | .sending => inferInstanceAs (Repr Response.Head)
+
+instance : Internal.Encode .v11 (Message.Head dir) :=
+  match dir with
+  | .receiving => inferInstanceAs (Internal.Encode .v11 Request.Head)
+  | .sending => inferInstanceAs (Internal.Encode .v11 Response.Head)
+
+instance : EmptyCollection (Message.Head dir) where
+  emptyCollection :=
+    match dir with
+    | .receiving => { method := .get, version := .v11 }
+    | .sending => {}

src/Std/Internal/Http/Protocol/H1/Parser.lean

@@ -0,0 +1,548 @@
+/-
+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.Parsec
+public import Std.Internal.Http.Data
+public import Std.Internal.Parsec.ByteArray
+public import Std.Internal.Http.Protocol.H1.Config
+
+/-!
+This module defines parsers for HTTP/1.1 request and response lines, headers, and body framing. The
+reference used is https://httpwg.org/specs/rfc9112.html.
+-/
+
+namespace Std.Http.Protocol.H1
+
+open Std Internal Parsec ByteArray Internal Internal.Char
+
+set_option linter.all true
+
+/--
+Checks if a byte may appear inside a field value.
+
+This parser enforces strict ASCII-only field values and allows only `field-content`
+(`HTAB / SP / VCHAR`).
+-/
+@[inline]
+def isFieldVChar (c : UInt8) : Bool :=
+  fieldContent (Char.ofUInt8 c)
+
+/--
+Checks if a byte may appear unescaped inside a quoted-string value.
+
+Allows `HTAB / SP / %x21 / %x23-5B / %x5D-7E` (strict ASCII-only; no obs-text).
+-/
+@[inline]
+def isQdText (c : UInt8) : Bool :=
+  qdtext (Char.ofUInt8 c)
+
+/--
+Checks if a byte is optional whitespace (`OWS = SP / HTAB`, RFC 9110 §5.6.3).
+-/
+@[inline]
+def isOwsByte (c : UInt8) : Bool :=
+  ows (Char.ofUInt8 c)
+
+-- Parser blocks
+
+/--
+Repeatedly applies `parser` until it returns `none` or the `maxCount` limit is
+exceeded. Returns the collected results as an array.
+-/
+partial def manyItems {α : Type} (parser : Parser (Option α)) (maxCount : Nat) : Parser (Array α) := do
+  let rec go (acc : Array α) : Parser (Array α) := do
+    let step ← optional <| attempt do
+      match ← parser with
+      | none => fail "end of items"
+      | some x => return x
+
+    match step with
+    | none =>
+      return acc
+    | some x =>
+      let acc := acc.push x
+
+      if acc.size > maxCount then
+        fail s!"too many items: {acc.size} > {maxCount}"
+
+      go acc
+  go #[]
+
+
+/--
+Lifts an `Option` into the parser monad, failing with a generic message if the value is `none`.
+-/
+def liftOption (x : Option α) : Parser α :=
+  if let some res := x then
+    return res
+  else
+    fail "expected value but got none"
+
+/--
+Parses an HTTP token (RFC 9110 §5.6.2): one or more token characters, up to `limit` bytes.
+Fails if the input starts with a non-token character or is empty.
+-/
+@[inline]
+def parseToken (limit : Nat) : Parser ByteSlice :=
+  takeWhileUpTo1 (fun c => tchar (Char.ofUInt8 c)) limit
+
+/--
+Parses a line terminator.
+-/
+@[inline]
+def crlf : Parser Unit := do
+  skipBytes "\r\n".toUTF8
+
+/--
+Consumes and ignores empty lines (`CRLF`) that appear before a request-line.
+
+https://httpwg.org/specs/rfc9112.html#rfc.section.2.2:
+
+"In the interest of robustness, a server that is expecting to receive and parse a request-line SHOULD
+ignore at least one empty line (CRLF) received prior to the request-line."
+-/
+def skipLeadingRequestEmptyLines (limits : H1.Config) : Parser Unit := do
+  let mut count := 0
+  while (← peekWhen? (· == '\r'.toUInt8)).isSome do
+    if count >= limits.maxLeadingEmptyLines then
+      fail "too many leading empty lines"
+    crlf
+    count := count + 1
+
+/--
+Parses a single space (SP, 0x20).
+-/
+@[inline]
+def sp : Parser Unit :=
+  skipByte ' '.toUInt8
+
+/--
+Parses optional whitespace (OWS = *(SP / HTAB), RFC 9110 §5.6.3), bounded by
+`limits.maxSpaceSequence`. Fails if more whitespace follows the limit, so oversized
+padding is rejected rather than silently truncated.
+-/
+@[inline]
+def ows (limits : H1.Config) : Parser Unit := do
+  discard <| takeWhileUpTo isOwsByte limits.maxSpaceSequence
+
+  if (← peekWhen? isOwsByte) |>.isSome then
+    fail "invalid space sequence"
+  else
+    pure ()
+
+/--
+Parses a single ASCII hex digit and returns its numeric value (`0`–`15`).
+-/
+def hexDigit : Parser UInt8 := do
+  let b ← any
+  if isHexDigitByte b then
+    if b ≥ '0'.toUInt8 && b ≤ '9'.toUInt8 then return b - '0'.toUInt8
+    else if b ≥ 'A'.toUInt8 && b ≤ 'F'.toUInt8 then return b - 'A'.toUInt8 + 10
+    else return b - 'a'.toUInt8 + 10
+  else fail s!"invalid hex digit {Char.ofUInt8 b |>.quote}"
+
+/--
+Parses a hexadecimal integer (one or more hex digits, up to 16 digits).
+Used for chunk-size lines in chunked transfer encoding.
+-/
+partial def hex : Parser Nat := do
+  let rec go (acc : Nat) (count : Nat) : Parser Nat := do
+    match ← optional (attempt hexDigit) with
+    | some d =>
+        if count + 1 > 16 then
+          fail "chunk size too large"
+        else
+          go (acc * 16 + d.toNat) (count + 1)
+    | none =>
+        if count = 0 then
+          -- Preserve EOF as incremental chunk-size parsing can request more data.
+          -- For non-EOF invalid bytes, keep the specific parse failure.
+          let _ ← peek!
+          fail "expected hex digit"
+        else
+          return acc
+  go 0 0
+
+-- Actual parsers
+
+/--
+Parses `HTTP-version = HTTP-name "/" DIGIT "." DIGIT` and returns the major and
+minor version numbers as a pair.
+-/
+def parseHttpVersionNumber : Parser (Nat × Nat) := do
+  skipBytes "HTTP/".toUTF8
+  let major ← digit
+  skipByte '.'.toUInt8
+  let minor ← digit
+  pure ((major.toNat - 48), (minor.toNat - 48))
+
+/--
+Parses an HTTP version string and returns the corresponding `Version` value.
+Fails if the version is not recognized by `Version.ofNumber?`.
+-/
+def parseHttpVersion : Parser Version := do
+  let (major, minor) ← parseHttpVersionNumber
+  liftOption <| Version.ofNumber? major minor
+
+/-
+method         = token
+
+Every branch is wrapped in `attempt` so that `<|>` always backtracks on
+failure, even after consuming bytes. This is strictly necessary only for the
+P-group (POST / PUT / PATCH) which share a common first byte, but wrapping
+all alternatives keeps the parser defensively correct if new methods are
+added in the future.
+-/
+def parseMethod : Parser Method :=
+  (attempt <| skipBytes "GET".toUTF8 <&> fun _ => Method.get)
+  <|> (attempt <| skipBytes "HEAD".toUTF8 <&> fun _ => Method.head)
+  <|> (attempt <| skipBytes "DELETE".toUTF8 <&> fun _ => Method.delete)
+  <|> (attempt <| skipBytes "TRACE".toUTF8 <&> fun _ => Method.trace)
+  <|> (attempt <| skipBytes "ACL".toUTF8 <&> fun _ => Method.acl)
+  <|> (attempt <| skipBytes "QUERY".toUTF8 <&> fun _ => Method.query)
+  <|> (attempt <| skipBytes "SEARCH".toUTF8 <&> fun _ => Method.search)
+  <|> (attempt <| skipBytes "BASELINE-CONTROL".toUTF8 <&> fun _ => Method.baselineControl)
+  <|> (attempt <| skipBytes "BIND".toUTF8 <&> fun _ => Method.bind)
+  <|> (attempt <| skipBytes "CONNECT".toUTF8 <&> fun _ => Method.connect)
+  <|> (attempt <| skipBytes "CHECKIN".toUTF8 <&> fun _ => Method.checkin)
+  <|> (attempt <| skipBytes "CHECKOUT".toUTF8 <&> fun _ => Method.checkout)
+  <|> (attempt <| skipBytes "COPY".toUTF8 <&> fun _ => Method.copy)
+  <|> (attempt <| skipBytes "LABEL".toUTF8 <&> fun _ => Method.label)
+  <|> (attempt <| skipBytes "LINK".toUTF8 <&> fun _ => Method.link)
+  <|> (attempt <| skipBytes "LOCK".toUTF8 <&> fun _ => Method.lock)
+  <|> (attempt <| skipBytes "MERGE".toUTF8 <&> fun _ => Method.merge)
+  <|> (attempt <| skipBytes "MKACTIVITY".toUTF8 <&> fun _ => Method.mkactivity)
+  <|> (attempt <| skipBytes "MKCALENDAR".toUTF8 <&> fun _ => Method.mkcalendar)
+  <|> (attempt <| skipBytes "MKCOL".toUTF8 <&> fun _ => Method.mkcol)
+  <|> (attempt <| skipBytes "MKREDIRECTREF".toUTF8 <&> fun _ => Method.mkredirectref)
+  <|> (attempt <| skipBytes "MKWORKSPACE".toUTF8 <&> fun _ => Method.mkworkspace)
+  <|> (attempt <| skipBytes "MOVE".toUTF8 <&> fun _ => Method.move)
+  <|> (attempt <| skipBytes "OPTIONS".toUTF8 <&> fun _ => Method.options)
+  <|> (attempt <| skipBytes "ORDERPATCH".toUTF8 <&> fun _ => Method.orderpatch)
+  <|> (attempt <| skipBytes "POST".toUTF8 <&> fun _ => Method.post)
+  <|> (attempt <| skipBytes "PUT".toUTF8 <&> fun _ => Method.put)
+  <|> (attempt <| skipBytes "PATCH".toUTF8 <&> fun _ => Method.patch)
+  <|> (attempt <| skipBytes "PRI".toUTF8 <&> fun _ => Method.pri)
+  <|> (attempt <| skipBytes "PROPFIND".toUTF8 <&> fun _ => Method.propfind)
+  <|> (attempt <| skipBytes "PROPPATCH".toUTF8 <&> fun _ => Method.proppatch)
+  <|> (attempt <| skipBytes "REBIND".toUTF8 <&> fun _ => Method.rebind)
+  <|> (attempt <| skipBytes "REPORT".toUTF8 <&> fun _ => Method.report)
+  <|> (attempt <| skipBytes "UNBIND".toUTF8 <&> fun _ => Method.unbind)
+  <|> (attempt <| skipBytes "UNCHECKOUT".toUTF8 <&> fun _ => Method.uncheckout)
+  <|> (attempt <| skipBytes "UNLINK".toUTF8 <&> fun _ => Method.unlink)
+  <|> (attempt <| skipBytes "UNLOCK".toUTF8 <&> fun _ => Method.unlock)
+  <|> (attempt <| skipBytes "UPDATEREDIRECTREF".toUTF8 <&> fun _ => Method.updateredirectref)
+  <|> (attempt <| skipBytes "UPDATE".toUTF8 <&> fun _ => Method.update)
+  <|> (attempt <| skipBytes "VERSION-CONTROL".toUTF8 <&> fun _ => Method.versionControl)
+  <|> (parseToken 64 *> fail "unrecognized method")
+
+/--
+Parses a request-target URI, up to `limits.maxUriLength` bytes.
+Fails with `"uri too long"` if the target exceeds the configured limit.
+-/
+def parseURI (limits : H1.Config) : Parser ByteArray := do
+  let uri ← takeUntilUpTo (· == ' '.toUInt8) limits.maxUriLength
+  if uri.size == limits.maxUriLength then
+    if (← peekWhen? (· != ' '.toUInt8)) |>.isSome then
+      fail "uri too long"
+
+  return uri.toByteArray
+
+/--
+Shared core for request-line parsing: parses `request-target SP HTTP-version CRLF`
+and returns the `RequestTarget` together with the raw major/minor version numbers.
+
+Both `parseRequestLine` and `parseRequestLineRawVersion` call this after consuming
+the method token, keeping URI validation and version parsing in one place.
+-/
+private def parseRequestLineBody (limits : H1.Config) : Parser (RequestTarget × Nat × Nat) := do
+  let rawUri ← parseURI limits <* sp
+  let uri ← match (Std.Http.URI.Parser.parseRequestTarget <* eof).run rawUri with
+  | .ok res => pure res
+  | .error res => fail res
+  let versionPair ← parseHttpVersionNumber <* crlf
+  return (uri, versionPair)
+
+/--
+Parses a request line and returns a fully-typed `Request.Head`.
+`request-line = method SP request-target SP HTTP-version`
+-/
+public def parseRequestLine (limits : H1.Config) : Parser Request.Head := do
+  skipLeadingRequestEmptyLines limits
+  let method ← parseMethod <* sp
+  let (uri, (major, minor)) ← parseRequestLineBody limits
+  if major == 1 ∧ minor == 1 then
+    return ⟨method, .v11, uri, .empty⟩
+  else if major == 1 ∧ minor == 0 then
+    return ⟨method, .v10, uri, .empty⟩
+  else
+    fail "unsupported HTTP version"
+
+/--
+Parses a request line and returns the recognized HTTP method and version when available.
+
+request-line = method SP request-target SP HTTP-version
+-/
+public def parseRequestLineRawVersion (limits : H1.Config) : Parser (Method × RequestTarget × Option Version) := do
+  skipLeadingRequestEmptyLines limits
+  let method ← parseMethod <* sp
+  let (uri, (major, minor)) ← parseRequestLineBody limits
+  return (method, uri, Version.ofNumber? major minor)
+
+/--
+Parses a single header field line.
+
+`field-line = field-name ":" OWS field-value OWS`
+-/
+def parseFieldLine (limits : H1.Config) : Parser (String × String) := do
+  let name ← parseToken limits.maxHeaderNameLength
+  let value ← skipByte ':'.toUInt8 *> ows limits *> optional (takeWhileUpTo isFieldVChar limits.maxHeaderValueLength) <* ows limits
+
+  let name ← liftOption <| String.fromUTF8? name.toByteArray
+  let value ← liftOption <| String.fromUTF8? <| value.map (·.toByteArray) |>.getD .empty
+  let value := value.trimAsciiEnd.toString
+
+  return (name, value)
+
+/--
+Parses a single header field line, or returns `none` when it sees the blank line that
+terminates the header section.
+
+```
+field-line = field-name ":" OWS field-value OWS CRLF
+```
+-/
+public def parseSingleHeader (limits : H1.Config) : Parser (Option (String × String)) := do
+  let next ← peek?
+  if next == some '\r'.toUInt8 ∨ next == some '\n'.toUInt8 then
+    crlf
+    pure none
+  else
+    some <$> (parseFieldLine limits <* crlf)
+
+/--
+Parses a backslash-escaped character inside a quoted-string.
+
+`quoted-pair = "\" ( HTAB / SP / VCHAR )` — strict ASCII-only (no obs-text).
+-/
+def parseQuotedPair : Parser UInt8 := do
+  skipByte '\\'.toUInt8
+  let b ← any
+
+  if quotedPairChar (Char.ofUInt8 b) then
+    return b
+  else
+    fail s!"invalid quoted-pair byte: {Char.ofUInt8 b |>.quote}"
+
+/--
+Parses a quoted-string value, unescaping quoted-pairs.
+
+`quoted-string = DQUOTE *( qdtext / quoted-pair ) DQUOTE`
+-/
+partial def parseQuotedString (maxLength : Nat) : Parser String := do
+  skipByte '"'.toUInt8
+
+  let rec loop (buf : ByteArray) (length : Nat) : Parser ByteArray := do
+    let b ← any
+
+    if b == '"'.toUInt8 then
+      return buf
+    else if b == '\\'.toUInt8 then
+      let next ← any
+      if quotedPairChar (Char.ofUInt8 next)
+        then
+          let length := length + 1
+          if length > maxLength then
+            fail "quoted-string too long"
+          else
+            loop (buf.push next) length
+        else fail s!"invalid quoted-pair byte: {Char.ofUInt8 next |>.quote}"
+    else if isQdText b then
+      let length := length + 1
+      if length > maxLength then
+        fail "quoted-string too long"
+      else
+        loop (buf.push b) length
+    else
+      fail s!"invalid qdtext byte: {Char.ofUInt8 b |>.quote}"
+
+  liftOption <| String.fromUTF8? (← loop .empty 0)
+
+-- chunk-ext = *( BWS ";" BWS chunk-ext-name [ BWS "=" BWS chunk-ext-val] )
+def parseChunkExt (limits : H1.Config) : Parser (Chunk.ExtensionName × Option Chunk.ExtensionValue) := do
+  ows limits *> skipByte ';'.toUInt8 *> ows limits
+  let name ← (liftOption =<< String.fromUTF8? <$> ByteSlice.toByteArray <$> parseToken limits.maxChunkExtNameLength) <* ows limits
+
+  let some name := Chunk.ExtensionName.ofString? name
+    | fail "invalid extension name"
+
+  if (← peekWhen? (· == '='.toUInt8)) |>.isSome then
+    -- RFC 9112 §7.1.1: BWS is allowed around "=".
+    -- The `<* ows limits` after the name already consumed any trailing whitespace,
+    -- so these ows calls are no-ops in practice, but kept for explicit grammar correspondence.
+    ows limits *> skipByte '='.toUInt8 *> ows limits
+    let value ← ows limits *> (parseQuotedString limits.maxChunkExtValueLength <|> liftOption =<< (String.fromUTF8? <$> ByteSlice.toByteArray <$> parseToken limits.maxChunkExtValueLength))
+
+    let some value := Chunk.ExtensionValue.ofString? value
+      | fail "invalid extension value"
+
+    return (name, some value)
+
+  return (name, none)
+
+/--
+Parses the size and extensions of a chunk.
+-/
+public def parseChunkSize (limits : H1.Config) : Parser (Nat × Array (Chunk.ExtensionName × Option Chunk.ExtensionValue)) := do
+  let size ← hex
+  let ext ← manyItems (optional (attempt (parseChunkExt limits))) limits.maxChunkExtensions
+  crlf
+  return (size, ext)
+
+/--
+Result of parsing partial or complete information.
+-/
+public inductive TakeResult
+  | complete (data : ByteSlice)
+  | incomplete (data : ByteSlice) (remaining : Nat)
+
+/--
+Parses a single chunk in chunked transfer encoding.
+-/
+public def parseChunkPartial (limits : H1.Config) : Parser (Option (Nat × Array (Chunk.ExtensionName × Option Chunk.ExtensionValue) × ByteSlice)) := do
+  let (size, ext) ← parseChunkSize limits
+  if size == 0 then
+    return none
+  else
+    let data ← take size
+    return some ⟨size, ext, data⟩
+
+/--
+Parses fixed-size data that can be incomplete.
+-/
+public def parseFixedSizeData (size : Nat) : Parser TakeResult := fun it =>
+  if it.remainingBytes = 0 then
+    .error it .eof
+  else if it.remainingBytes < size then
+    .success (it.forward it.remainingBytes) (.incomplete it.array[it.idx...(it.idx+it.remainingBytes)] (size - it.remainingBytes))
+  else
+    .success (it.forward size) (.complete (it.array[it.idx...(it.idx+size)]))
+
+/--
+Parses fixed-size chunk data that can be incomplete.
+-/
+public def parseChunkSizedData (size : Nat) : Parser TakeResult := do
+  match ← parseFixedSizeData size with
+  | .complete data => crlf *> return .complete data
+  | .incomplete data res => return .incomplete data res
+
+/--
+Returns `true` if `name` (compared case-insensitively) is a field that MUST NOT appear in HTTP/1.1
+trailer sections per RFC 9112 §6.5. Forbidden fields are those required for message framing
+(`content-length`, `transfer-encoding`), routing (`host`), or connection management (`connection`).
+-/
+private def isForbiddenTrailerField (name : String) : Bool :=
+  let n := name.toLower
+  n == "content-length" || n == "transfer-encoding" || n == "host" ||
+  n == "connection" || n == "expect" || n == "te" ||
+  n == "authorization" || n == "max-forwards" || n == "cache-control" ||
+  n == "content-encoding" || n == "upgrade" || n == "trailer"
+
+/--
+Parses a trailer header (used after a chunked body), rejecting forbidden field names per RFC 9112
+§6.5. Fields used for message framing (`content-length`, `transfer-encoding`), routing (`host`),
+or connection management (`connection`, `te`, `upgrade`) are rejected to prevent trailer injection
+attacks where a downstream proxy might re-interpret them.
+-/
+def parseTrailerHeader (limits : H1.Config) : Parser (Option (String × String)) := do
+  let result ← parseSingleHeader limits
+  if let some (name, _) := result then
+    if isForbiddenTrailerField name then
+      fail s!"forbidden trailer field: {name}"
+  return result
+
+/--
+Parses trailer headers after a chunked body and returns them as an array of name-value pairs.
+
+This is exposed for callers that need the trailer values directly (e.g. clients). The
+internal protocol machine uses `parseLastChunkBody` instead, which discards trailer values.
+-/
+public def parseTrailers (limits : H1.Config) : Parser (Array (String × String)) := do
+  let trailers ← manyItems (parseTrailerHeader limits) limits.maxTrailerHeaders
+  crlf
+  return trailers
+
+/--
+Returns `true` if `c` is a valid reason-phrase byte (`HTAB / SP / VCHAR`, strict ASCII-only).
+-/
+@[inline]
+def isReasonPhraseByte (c : UInt8) : Bool :=
+  fieldContent (Char.ofUInt8 c)
+
+/--
+Parses a reason phrase (text after status code).
+
+Allows only `HTAB / SP / VCHAR` bytes (strict ASCII-only).
+-/
+def parseReasonPhrase (limits : H1.Config) : Parser String := do
+  let bytes ← takeWhileUpTo isReasonPhraseByte limits.maxReasonPhraseLength
+  liftOption <| String.fromUTF8? bytes.toByteArray
+
+/--
+Parses a status-code (3 decimal digits), the following reason phrase, and the
+terminating CRLF; returns a typed `Status`.
+-/
+def parseStatusCode (limits : H1.Config) : Parser Status := do
+  let d1 ← digit
+  let d2 ← digit
+  let d3 ← digit
+  let code := (d1.toNat - 48) * 100 + (d2.toNat - 48) * 10 + (d3.toNat - 48)
+  sp
+  let phrase ← parseReasonPhrase limits <* crlf
+
+  if h : IsValidReasonPhrase phrase then
+    if let some status := Status.ofCode (some ⟨phrase, h⟩) code.toUInt16 then
+      return status
+
+  fail "invalid status code"
+
+/--
+Parses a status line and returns a fully-typed `Response.Head`.
+`status-line = HTTP-version SP status-code SP [ reason-phrase ]`
+Accepts only HTTP/1.1. For parsing where the version may be unrecognized and must be
+mapped to an error event, use `parseStatusLineRawVersion`.
+-/
+public def parseStatusLine (limits : H1.Config) : Parser Response.Head := do
+  let (major, minor) ← parseHttpVersionNumber <* sp
+  let status ← parseStatusCode limits
+  if major == 1 ∧ minor == 1 then
+    return { status, version := .v11, headers := .empty }
+  else if major == 1 ∧ minor == 0 then
+    return { status, version := .v10, headers := .empty }
+  else
+    fail "unsupported HTTP version"
+
+/--
+Parses a status line and returns the status code plus recognized HTTP version when available.
+Consumes and discards the reason phrase.
+
+status-line = HTTP-version SP status-code SP [ reason-phrase ] CRLF
+-/
+public def parseStatusLineRawVersion (limits : H1.Config) : Parser (Status × Option Version) := do
+  let (major, minor) ← parseHttpVersionNumber <* sp
+  let status ← parseStatusCode limits
+  return (status, Version.ofNumber? major minor)
+
+/--
+Parses the trailer section that follows the last chunk size line (`0\r\n`).
+-/
+public def parseLastChunkBody (limits : H1.Config) : Parser Unit := do
+  discard <| manyItems (parseTrailerHeader limits) limits.maxTrailerHeaders
+  crlf
+
+end Std.Http.Protocol.H1

src/Std/Internal/Http/Protocol/H1/Reader.lean

@@ -0,0 +1,319 @@
+/-
+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.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Internal.Http.Protocol.H1.Error
+
+public section
+
+/-!
+# HTTP/1.1 Reader
+
+This module defines the reader state machine for parsing incoming HTTP/1.1 messages.
+It tracks the parsing state including start line, headers, and body handling for
+both fixed-length and chunked transfer encodings.
+-/
+
+namespace Std.Http.Protocol.H1
+
+set_option linter.all true
+
+/--
+The body-framing sub-state of the `Reader` state machine.
+-/
+inductive Reader.BodyState where
+  /--
+  Parse fixed-length body bytes, tracking the number of bytes remaining.
+  -/
+  | fixed (remaining : Nat)
+
+  /--
+  Parse the next chunk-size line in chunked transfer encoding.
+  -/
+  | chunkedSize
+
+  /--
+  Parse chunk data for the current chunk.
+  -/
+  | chunkedBody (ext : Array (Chunk.ExtensionName × Option Chunk.ExtensionValue)) (remaining : Nat)
+
+  /--
+  Parse body bytes until EOF (connection close).
+  -/
+  | closeDelimited
+deriving Inhabited, Repr, BEq
+
+/--
+The state of the `Reader` state machine.
+-/
+inductive Reader.State (dir : Direction) : Type
+  /--
+  Initial state waiting for HTTP start line.
+  -/
+  | needStartLine : State dir
+
+  /--
+  State waiting for HTTP headers, tracking number of headers parsed.
+  -/
+  | needHeader : Nat → State dir
+
+  /--
+  Unified body-reading state.
+  -/
+  | readBody : Reader.BodyState → State dir
+
+  /--
+  Paused waiting for a `canContinue` decision, carrying the next state.
+  -/
+  | continue : State dir → State dir
+
+  /--
+  State waiting to be able to read new data.
+  -/
+  | pending : State dir
+
+  /--
+  State that it completed a single request or response and can go to the next one
+  -/
+  | complete
+
+  /--
+  State that it has completed and cannot process more data.
+  -/
+  | closed
+
+  /--
+  The input is malformed.
+  -/
+  | failed (error : Error) : State dir
+deriving Inhabited, Repr, BEq
+
+/--
+Manages the reading state of the HTTP parsing and processing machine.
+-/
+structure Reader (dir : Direction) where
+  /--
+  The current state of the machine.
+  -/
+  state : Reader.State dir := match dir with | .receiving => .needStartLine | .sending => .pending
+
+  /--
+  The input byte array.
+  -/
+  input : ByteArray.Iterator := ByteArray.emptyWithCapacity 4096 |>.iter
+
+  /--
+  The incoming message head.
+  -/
+  messageHead : Message.Head dir := {}
+
+  /--
+  Count of messages that this connection has already parsed.
+  -/
+  messageCount : Nat := 0
+
+  /--
+  Number of body bytes read for the current message.
+  -/
+  bodyBytesRead : Nat := 0
+
+  /--
+  Number of header bytes accumulated for the current message.
+  Counts name + value bytes plus 4 bytes per line for `: ` and `\r\n`.
+  -/
+  headerBytesRead : Nat := 0
+
+  /--
+  Set when no further input bytes will arrive (the remote end has closed the connection).
+  -/
+  noMoreInput : Bool := false
+
+namespace Reader
+
+/--
+Checks if the reader is in a closed state and cannot process more messages.
+-/
+@[inline]
+def isClosed (reader : Reader dir) : Bool :=
+  match reader.state with
+  | .closed => true
+  | _ => false
+
+/--
+Checks if the reader has completed parsing the current message.
+-/
+@[inline]
+def isComplete (reader : Reader dir) : Bool :=
+  match reader.state with
+  | .complete => true
+  | _ => false
+
+/--
+Checks if the reader has encountered an error.
+-/
+@[inline]
+def hasFailed (reader : Reader dir) : Bool :=
+  match reader.state with
+  | .failed _ => true
+  | _ => false
+
+/--
+Feeds new data into the reader's input buffer.
+If the current input is exhausted, replaces it; otherwise compacts the buffer
+by discarding already-parsed bytes before appending.
+-/
+@[inline]
+def feed (data : ByteArray) (reader : Reader dir) : Reader dir :=
+  { reader with input :=
+    if reader.input.atEnd
+      then data.iter
+      else (reader.input.array.extract reader.input.pos reader.input.array.size ++ data).iter }
+
+/--
+Replaces the reader's input iterator with a new one.
+-/
+@[inline]
+def setInput (input : ByteArray.Iterator) (reader : Reader dir) : Reader dir :=
+  { reader with input }
+
+/--
+Updates the message head being constructed.
+-/
+@[inline]
+def setMessageHead (messageHead : Message.Head dir) (reader : Reader dir) : Reader dir :=
+  { reader with messageHead }
+
+/--
+Adds a header to the current message head.
+-/
+@[inline]
+def addHeader (name : Header.Name) (value : Header.Value) (reader : Reader dir) : Reader dir :=
+  match dir with
+  | .sending | .receiving => { reader with messageHead := { reader.messageHead with headers := reader.messageHead.headers.insert name value } }
+
+/--
+Closes the reader, transitioning to the closed state.
+-/
+@[inline]
+def close (reader : Reader dir) : Reader dir :=
+  { reader with state := .closed, noMoreInput := true }
+
+/--
+Marks the current message as complete and prepares for the next message.
+-/
+@[inline]
+def markComplete (reader : Reader dir) : Reader dir :=
+  { reader with
+    state := .complete
+    messageCount := reader.messageCount + 1 }
+
+/--
+Transitions the reader to a failed state with the given error.
+-/
+@[inline]
+def fail (error : Error) (reader : Reader dir) : Reader dir :=
+  { reader with state := .failed error }
+
+/--
+Resets the reader to parse a new message on the same connection.
+-/
+@[inline]
+def reset (reader : Reader dir) : Reader dir :=
+  { reader with
+    state := .needStartLine
+    bodyBytesRead := 0
+    headerBytesRead := 0
+    messageHead := {} }
+
+/--
+Checks if more input is needed to continue parsing.
+-/
+@[inline]
+def needsMoreInput (reader : Reader dir) : Bool :=
+  reader.input.atEnd && !reader.noMoreInput &&
+  match reader.state with
+  | .complete | .closed | .failed _ | .«continue» _ => false
+  | _ => true
+
+/--
+Returns the current parse error if the reader has failed.
+-/
+@[inline]
+def getError (reader : Reader dir) : Option Error :=
+  match reader.state with
+  | .failed err => some err
+  | _ => none
+
+/--
+Gets the number of bytes remaining in the input buffer.
+-/
+@[inline]
+def remainingBytes (reader : Reader dir) : Nat :=
+  reader.input.array.size - reader.input.pos
+
+/--
+Advances the input iterator by n bytes.
+-/
+@[inline]
+def advance (n : Nat) (reader : Reader dir) : Reader dir :=
+  { reader with input := reader.input.forward n }
+
+/--
+Transitions to the state for reading headers.
+-/
+@[inline]
+def startHeaders (reader : Reader dir) : Reader dir :=
+  { reader with state := .needHeader 0, bodyBytesRead := 0, headerBytesRead := 0 }
+
+/--
+Adds body bytes parsed for the current message.
+-/
+@[inline]
+def addBodyBytes (n : Nat) (reader : Reader dir) : Reader dir :=
+  { reader with bodyBytesRead := reader.bodyBytesRead + n }
+
+/--
+Adds header bytes accumulated for the current message.
+-/
+@[inline]
+def addHeaderBytes (n : Nat) (reader : Reader dir) : Reader dir :=
+  { reader with headerBytesRead := reader.headerBytesRead + n }
+
+/--
+Transitions to the state for reading a fixed-length body.
+-/
+@[inline]
+def startFixedBody (size : Nat) (reader : Reader dir) : Reader dir :=
+  { reader with state := .readBody (.fixed size) }
+
+/--
+Transitions to the state for reading chunked transfer encoding.
+-/
+@[inline]
+def startChunkedBody (reader : Reader dir) : Reader dir :=
+  { reader with state := .readBody .chunkedSize }
+
+/--
+Marks that no more input will be provided (connection closed).
+-/
+@[inline]
+def markNoMoreInput (reader : Reader dir) : Reader dir :=
+  { reader with noMoreInput := true }
+
+/--
+Checks if the connection should be kept alive for the next message.
+-/
+def shouldKeepAlive (reader : Reader dir) : Bool :=
+  reader.messageHead.shouldKeepAlive
+
+end Reader

src/Std/Internal/Http/Protocol/H1/Writer.lean

@@ -0,0 +1,280 @@
+/-
+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.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Internal.Http.Protocol.H1.Error
+
+public section
+
+/-!
+# HTTP/1.1 Writer
+
+This module defines the writer state machine for generating outgoing HTTP/1.1 messages.
+It handles encoding headers and body content for both fixed-length and chunked
+transfer encodings.
+-/
+
+namespace Std.Http.Protocol.H1
+
+set_option linter.all true
+
+open Internal
+
+/--
+The state of the `Writer` state machine.
+-/
+inductive Writer.State
+  /--
+  Initial state before any outgoing message has been prepared.
+  -/
+  | pending
+
+  /--
+  Waiting for the application to provide the outgoing message head via `send`.
+  -/
+  | waitingHeaders
+
+  /--
+  The message head has been provided; waiting for `shouldFlush` to become true before
+  serializing headers to output.
+  -/
+  | waitingForFlush
+
+  /--
+  Writing the body output (either fixed-length or chunked).
+  -/
+  | writingBody (mode : Body.Length)
+
+  /--
+  Completed writing a single message and ready to begin the next one.
+  -/
+  | complete
+
+  /--
+  Closed; no further data can be written.
+  -/
+  | closed
+deriving Inhabited, Repr, BEq
+
+/--
+Manages the writing state of the HTTP generating and writing machine.
+-/
+structure Writer (dir : Direction) where
+  /--
+  Body chunks supplied by the user, accumulated before being flushed to output.
+  -/
+  userData : Array Chunk := .empty
+
+  /--
+  All the data produced by the writer, ready to be sent to the socket.
+  -/
+  outputData : ChunkedBuffer := .empty
+
+  /--
+  The state of the writer machine.
+  -/
+  state : Writer.State := match dir with | .receiving => .pending | .sending => .waitingHeaders
+
+  /--
+  When the user specifies the exact body size upfront, `Content-Length` framing is
+  used instead of chunked transfer encoding.
+  -/
+  knownSize : Option Body.Length := none
+
+  /--
+  The outgoing message that will be written to the output.
+  -/
+  messageHead : Message.Head dir.swap := {}
+
+  /--
+  Whether the user has called `send` to provide the outgoing message head.
+  -/
+  sentMessage : Bool := false
+
+  /--
+  Set when the user has finished sending body data, allowing fixed-size framing
+  to be determined upfront.
+  -/
+  userClosedBody : Bool := false
+
+  /--
+  When `true`, body bytes are intentionally omitted from the wire for this message
+  (e.g. HEAD responses), while headers/framing metadata may still describe the
+  hypothetical representation.
+  -/
+  omitBody : Bool := false
+
+  /--
+  Running total of bytes across all `userData` chunks, maintained incrementally
+  to avoid an O(n) fold on every fixed-length write step.
+  -/
+  userDataBytes : Nat := 0
+
+namespace Writer
+
+/--
+Returns `true` when no more user body data will arrive: either the user called
+`closeBody`, or the writer has already transitioned to `complete` or `closed`.
+
+Note: this does **not** mean the wire is ready to accept new bytes — a `closed`
+writer cannot send anything. Use this to decide whether to flush pending body
+data rather than to check writability.
+-/
+@[inline]
+def noMoreUserData {dir} (writer : Writer dir) : Bool :=
+  match writer.state with
+  | .closed | .complete => true
+  | _ => writer.userClosedBody
+
+/--
+Checks if the writer is closed (cannot process more data).
+-/
+@[inline]
+def isClosed (writer : Writer dir) : Bool :=
+  match writer.state with
+  | .closed => true
+  | _ => false
+
+/--
+Checks if the writer has completed processing a request.
+-/
+@[inline]
+def isComplete (writer : Writer dir) : Bool :=
+  match writer.state with
+  | .complete => true
+  | _ => false
+
+/--
+Checks if the writer can accept more data from the user.
+-/
+@[inline]
+def canAcceptData (writer : Writer dir) : Bool :=
+  match writer.state with
+  | .waitingHeaders => true
+  | .waitingForFlush => true
+  | .writingBody _ => !writer.userClosedBody
+  | _ => false
+
+/--
+Marks the body as closed, indicating no more user data will be added.
+-/
+@[inline]
+def closeBody (writer : Writer dir) : Writer dir :=
+  { writer with userClosedBody := true }
+
+/--
+Determines the transfer encoding mode based on explicit setting, body closure state, or defaults to chunked.
+-/
+def determineTransferMode (writer : Writer dir) : Body.Length :=
+  if let some mode := writer.knownSize then
+    mode
+  else if writer.userClosedBody then
+    .fixed writer.userDataBytes
+  else
+    .chunked
+
+/--
+Adds user data chunks to the writer's buffer if the writer can accept data.
+-/
+@[inline]
+def addUserData (data : Array Chunk) (writer : Writer dir) : Writer dir :=
+  if writer.canAcceptData then
+    let extraBytes := data.foldl (fun acc c => acc + c.data.size) 0
+    { writer with userData := writer.userData ++ data, userDataBytes := writer.userDataBytes + extraBytes }
+  else
+    writer
+
+/--
+Writes accumulated user data to output using fixed-size encoding.
+-/
+def writeFixedBody (writer : Writer dir) (limitSize : Nat) : Writer dir × Nat :=
+  if writer.userData.size = 0 then
+    (writer, limitSize)
+  else
+    let (chunks, pending, totalSize) := writer.userData.foldl (fun (state : Array ByteArray × Array Chunk × Nat) chunk =>
+      let (acc, pending, size) := state
+      if size >= limitSize then
+        (acc, pending.push chunk, size)
+      else
+        let remaining := limitSize - size
+        let takeSize := min chunk.data.size remaining
+        let dataPart := chunk.data.extract 0 takeSize
+        let acc := if takeSize = 0 then acc else acc.push dataPart
+        let size := size + takeSize
+        if takeSize < chunk.data.size then
+          let pendingChunk : Chunk := { chunk with data := chunk.data.extract takeSize chunk.data.size }
+          (acc, pending.push pendingChunk, size)
+        else
+          (acc, pending, size)
+    ) (#[], #[], 0)
+    let outputData := writer.outputData.append (ChunkedBuffer.ofArray chunks)
+    let remaining := limitSize - totalSize
+    ({ writer with userData := pending, outputData, userDataBytes := writer.userDataBytes - totalSize }, remaining)
+
+/--
+Writes accumulated user data to output using chunked transfer encoding.
+-/
+def writeChunkedBody (writer : Writer dir) : Writer dir :=
+  if writer.userData.size = 0 then
+    writer
+  else
+    let data := writer.userData
+    { writer with userData := #[], userDataBytes := 0, outputData := data.foldl (Encode.encode .v11) writer.outputData }
+
+/--
+Writes the final chunk terminator (0\r\n\r\n) and transitions to complete state.
+-/
+def writeFinalChunk (writer : Writer dir) : Writer dir :=
+  let writer := writer.writeChunkedBody
+  { writer with
+    outputData := writer.outputData.write "0\r\n\r\n".toUTF8
+    state := .complete
+  }
+
+/--
+Extracts all accumulated output data and returns it with a cleared output buffer.
+-/
+@[inline]
+def takeOutput (writer : Writer dir) : Option (Writer dir × ByteArray) :=
+  let output := writer.outputData.toByteArray
+  some ({ writer with outputData := ChunkedBuffer.empty }, output)
+
+/--
+Updates the writer's state machine to a new state.
+-/
+@[inline]
+def setState (state : Writer.State) (writer : Writer dir) : Writer dir :=
+  { writer with state }
+
+/--
+Writes the message headers to the output buffer.
+-/
+private def writeHeaders (messageHead : Message.Head dir.swap) (writer : Writer dir) : Writer dir :=
+  { writer with outputData := Internal.Encode.encode (v := .v11) writer.outputData messageHead }
+
+/--
+Checks if the connection should be kept alive based on the Connection header.
+-/
+def shouldKeepAlive (writer : Writer dir) : Bool :=
+  writer.messageHead.headers.get? .connection
+  |>.map (fun v => v.value.toLower != "close")
+  |>.getD true
+
+/--
+Closes the writer, transitioning to the closed state.
+-/
+@[inline]
+def close (writer : Writer dir) : Writer dir :=
+  { writer with state := .closed }
+
+end Writer

src/Std/Internal/Http/Server.lean

@@ -0,0 +1,188 @@
+/-
+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
+public import Std.Internal.Async.TCP
+public import Std.Sync.CancellationToken
+public import Std.Sync.Semaphore
+public import Std.Internal.Http.Server.Config
+public import Std.Internal.Http.Server.Handler
+public import Std.Internal.Http.Server.Connection
+
+public section
+
+/-!
+# HTTP Server
+
+This module defines a simple, asynchronous HTTP/1.1 server implementation.
+
+It provides the `Std.Http.Server` structure, which encapsulates all server state, and functions for
+starting, managing, and gracefully shutting down the server.
+
+The server runs entirely using `Async` and uses a shared `CancellationContext` to signal shutdowns.
+Each active client connection is tracked, and the server automatically resolves its shutdown
+promise once all connections have closed.
+-/
+
+namespace Std.Http
+open Std.Internal.IO.Async TCP
+
+set_option linter.all true
+
+/--
+The `Server` structure holds all state required to manage the lifecycle of an HTTP server, including
+connection tracking and shutdown coordination.
+-/
+structure Server where
+
+  /--
+  The context used for shutting down all connections and the server.
+  -/
+  context : Std.CancellationContext
+
+  /--
+  Active HTTP connections
+  -/
+  activeConnections : Std.Mutex UInt64
+
+  /--
+  Semaphore used to enforce the maximum number of simultaneous active connections.
+  `none` means no connection limit.
+  -/
+  connectionLimit : Option Std.Semaphore
+
+  /--
+  Indicates when the server has successfully shut down.
+  -/
+  shutdownPromise : Std.Channel Unit
+
+  /--
+  Configuration of the server
+  -/
+  config : Std.Http.Config
+
+namespace Server
+
+/--
+Create a new `Server` structure with an optional configuration.
+-/
+def new (config : Std.Http.Config := {}) : IO Server := do
+  let context ← Std.CancellationContext.new
+  let activeConnections ← Std.Mutex.new 0
+  let connectionLimit ←
+    if config.maxConnections = 0 then
+      pure none
+    else
+      some <$> Std.Semaphore.new config.maxConnections
+  let shutdownPromise ← Std.Channel.new
+
+  return { context, activeConnections, connectionLimit, shutdownPromise, config }
+
+/--
+Triggers cancellation of all requests and the accept loop in the server. This function should be used
+in conjunction with `waitShutdown` to properly coordinate the shutdown sequence.
+-/
+@[inline]
+def shutdown (s : Server) : Async Unit :=
+  s.context.cancel .shutdown
+
+/--
+Waits for the server to shut down. Blocks until another task or async operation calls the `shutdown` function.
+-/
+@[inline]
+def waitShutdown (s : Server) : Async Unit := do
+  Async.ofAsyncTask ((← s.shutdownPromise.recv).map Except.ok)
+
+/--
+Returns a `Selector` that waits for the server to shut down.
+-/
+@[inline]
+def waitShutdownSelector (s : Server) : Selector Unit :=
+  s.shutdownPromise.recvSelector
+
+/--
+Triggers cancellation of all requests and the accept loop, then waits for the server to fully shut down.
+This is a convenience function combining `shutdown` and then `waitShutdown`.
+-/
+@[inline]
+def shutdownAndWait (s : Server) : Async Unit := do
+  s.context.cancel .shutdown
+  s.waitShutdown
+
+@[inline]
+private def frameCancellation (s : Server) (releaseConnectionPermit : Bool := false)
+    (action : ContextAsync α) : ContextAsync α := do
+  s.activeConnections.atomically (modify (· + 1))
+  try
+    action
+  finally
+    if releaseConnectionPermit then
+      if let some limit := s.connectionLimit then
+        limit.release
+
+    s.activeConnections.atomically do
+      modify (· - 1)
+
+      if (← get) = 0 ∧ (← s.context.isCancelled) then
+        discard <| s.shutdownPromise.send ()
+
+/--
+Start a new HTTP/1.1 server on the given socket address. This function uses `Async` to handle tasks
+and TCP connections, and returns a `Server` structure that can be used to cancel the server.
+-/
+def serve {σ : Type} [Handler σ]
+    (addr : Net.SocketAddress)
+    (handler : σ)
+    (config : Config := {}) (backlog : UInt32 := 1024) : Async Server := do
+
+  let httpServer ← Server.new config
+
+  let server ← Socket.Server.mk
+  server.bind addr
+  server.listen backlog
+  server.noDelay
+
+  let runServer := do
+    frameCancellation httpServer (action := do
+      while true do
+        let permitAcquired ←
+          if let some limit := httpServer.connectionLimit then
+            let permit ← limit.acquire
+            await permit
+            pure true
+          else
+            pure false
+
+        let result ← Selectable.one #[
+          .case (server.acceptSelector) (fun x => pure <| some x),
+          .case (← ContextAsync.doneSelector) (fun _ => pure none)
+        ]
+
+        match result with
+        | some client =>
+          let extensions ← do
+            match (← EIO.toBaseIO client.getPeerName) with
+            | .ok addr => pure <| Extensions.empty.insert (Server.RemoteAddr.mk addr)
+            | .error _ => pure Extensions.empty
+
+          ContextAsync.background
+            (frameCancellation httpServer (releaseConnectionPermit := permitAcquired)
+              (action := do
+                serveConnection client handler config extensions))
+        | none =>
+          if permitAcquired then
+            if let some limit := httpServer.connectionLimit then
+              limit.release
+          break
+    )
+
+  background (runServer httpServer.context)
+
+  return httpServer
+
+end Std.Http.Server

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

@@ -0,0 +1,196 @@
+/-
+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`, a structure that describes timeout, request and headers
+configuration of an HTTP Server.
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+/--
+Connection limits configuration with validation.
+-/
+structure Config where
+  /--
+  Maximum number of simultaneous active connections (default: 1024).
+  Setting this to `0` disables the limit entirely: the server will accept any number of
+  concurrent connections and no semaphore-based cap is enforced. Use with care — an
+  unconstrained server may exhaust file descriptors or memory under adversarial load.
+  -/
+  maxConnections : Nat := 1024
+
+  /--
+  Maximum number of requests per connection.
+  -/
+  maxRequests : Nat := 100
+
+  /--
+  Maximum number of headers allowed per request.
+  -/
+  maxHeaders : Nat := 50
+
+  /--
+  Maximum aggregate byte size of all header field lines in a single message
+  (name + value bytes plus 4 bytes per line for `: ` and `\r\n`). Default: 64 KiB.
+  -/
+  maxHeaderBytes : Nat := 65536
+
+  /--
+  Timeout (in milliseconds) for receiving additional data while a request is actively being
+  processed (e.g. reading the request body). Applies after the request headers have been parsed
+  and replaces the keep-alive timeout for the duration of the request.
+  -/
+  lingeringTimeout : Time.Millisecond.Offset := 10000
+
+  /--
+  Timeout for keep-alive connections
+  -/
+  keepAliveTimeout : { x : Time.Millisecond.Offset // 0 < x } :=  ⟨12000, by decide⟩
+
+  /--
+  Maximum time (in milliseconds) allowed to receive the complete request headers after the first
+  byte of a new request arrives. This prevents Slowloris-style attacks where a client sends bytes
+  at a slow rate to hold a connection slot open without completing a request. Once a request starts,
+  each individual read must complete within this window. Default: 5 seconds.
+  -/
+  headerTimeout : Time.Millisecond.Offset := 5000
+
+  /--
+  Whether to enable keep-alive connections by default.
+  -/
+  enableKeepAlive : Bool := true
+
+  /--
+  The maximum size that the connection can receive in a single recv call.
+  -/
+  maximumRecvSize : Nat := 8192
+
+  /--
+  Default buffer size for the connection
+  -/
+  defaultPayloadBytes : Nat := 8192
+
+  /--
+  Whether to automatically generate the `Date` header in responses.
+  -/
+  generateDate : Bool := true
+
+  /--
+  The `Server` header value injected into outgoing responses.
+  `none` suppresses the header entirely.
+  -/
+  serverName : Option Header.Value := some (.mk "LeanHTTP/1.1")
+
+  /--
+  Maximum length of request URI (default: 8192 bytes)
+  -/
+  maxUriLength : Nat := 8192
+
+  /--
+  Maximum number of bytes consumed while parsing request start-lines (default: 8192 bytes).
+  -/
+  maxStartLineLength : Nat := 8192
+
+  /--
+  Maximum length of header field name (default: 256 bytes)
+  -/
+  maxHeaderNameLength : Nat := 256
+
+  /--
+  Maximum length of header field value (default: 8192 bytes)
+  -/
+  maxHeaderValueLength : Nat := 8192
+
+  /--
+  Maximum number of spaces in delimiter sequences (default: 16)
+  -/
+  maxSpaceSequence : Nat := 16
+
+  /--
+  Maximum number of leading empty lines (bare CRLF) to skip before a request-line
+  (RFC 9112 §2.2 robustness). Default: 8.
+  -/
+  maxLeadingEmptyLines : Nat := 8
+
+  /--
+  Maximum length of chunk extension name (default: 256 bytes)
+  -/
+  maxChunkExtNameLength : Nat := 256
+
+  /--
+  Maximum length of chunk extension value (default: 256 bytes)
+  -/
+  maxChunkExtValueLength : Nat := 256
+
+  /--
+  Maximum number of bytes consumed while parsing one chunk-size line with extensions (default: 8192 bytes).
+  -/
+  maxChunkLineLength : Nat := 8192
+
+  /--
+  Maximum allowed chunk payload size in bytes (default: 8 MiB).
+  -/
+  maxChunkSize : Nat := 8 * 1024 * 1024
+
+  /--
+  Maximum allowed total body size per request in bytes (default: 64 MiB).
+  -/
+  maxBodySize : Nat := 64 * 1024 * 1024
+
+  /--
+  Maximum length of reason phrase (default: 512 bytes)
+  -/
+  maxReasonPhraseLength : Nat := 512
+
+  /--
+  Maximum number of trailer headers (default: 20)
+  -/
+  maxTrailerHeaders : Nat := 20
+
+  /--
+  Maximum number of extensions on a single chunk-size line (default: 16).
+  -/
+  maxChunkExtensions : Nat := 16
+
+namespace Config
+
+/--
+Converts to HTTP/1.1 config.
+-/
+def toH1Config (config : Config) : Protocol.H1.Config where
+  maxMessages := config.maxRequests
+  maxHeaders := config.maxHeaders
+  maxHeaderBytes := config.maxHeaderBytes
+  enableKeepAlive := config.enableKeepAlive
+  agentName := config.serverName
+  maxUriLength := config.maxUriLength
+  maxStartLineLength := config.maxStartLineLength
+  maxHeaderNameLength := config.maxHeaderNameLength
+  maxHeaderValueLength := config.maxHeaderValueLength
+  maxSpaceSequence := config.maxSpaceSequence
+  maxLeadingEmptyLines := config.maxLeadingEmptyLines
+  maxChunkExtensions := config.maxChunkExtensions
+  maxChunkExtNameLength := config.maxChunkExtNameLength
+  maxChunkExtValueLength := config.maxChunkExtValueLength
+  maxChunkLineLength := config.maxChunkLineLength
+  maxChunkSize := config.maxChunkSize
+  maxBodySize := config.maxBodySize
+  maxReasonPhraseLength := config.maxReasonPhraseLength
+  maxTrailerHeaders := config.maxTrailerHeaders
+
+end Std.Http.Config

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

@@ -0,0 +1,530 @@
+/-
+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.Server.Config
+public import Std.Internal.Http.Server.Handler
+
+public section
+
+namespace Std
+namespace Http
+namespace Server
+
+open Std Internal IO Async TCP Protocol
+open Time
+
+/-!
+# Connection
+
+This module defines `Server.Connection`, a structure used to handle a single HTTP connection with
+possibly multiple requests.
+-/
+
+set_option linter.all true
+
+/--
+Represents the remote address of a client connection.
+-/
+public structure RemoteAddr where
+  /--
+  The socket address of the remote client.
+  -/
+  addr : Net.SocketAddress
+deriving TypeName
+
+instance : ToString RemoteAddr where
+  toString addr := toString addr.addr.ipAddr ++ ":" ++ toString addr.addr.port
+
+/--
+A single HTTP connection.
+-/
+public structure Connection (α : Type) where
+  /--
+  The client connection.
+  -/
+  socket : α
+
+  /--
+  The processing machine for HTTP/1.1.
+  -/
+  machine : H1.Machine .receiving
+
+  /--
+  Extensions to attach to each request (e.g., remote address).
+  -/
+  extensions : Extensions := .empty
+
+namespace Connection
+
+/--
+Events produced by the async select loop in `receiveWithTimeout`.
+Each variant corresponds to one possible outcome of waiting for I/O.
+-/
+private inductive Recv (β : Type)
+  | bytes (x : Option ByteArray)
+  | responseBody (x : Option Chunk)
+  | bodyInterest (x : Bool)
+  | response (x : (Except Error (Response β)))
+  | timeout
+  | keepAliveTimeout
+  | 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
+  response : Option (Std.Channel (Except Error (Response β)))
+  responseBody : Option β
+  requestBody : Option Body.Stream
+  timeout : Millisecond.Offset
+  keepAliveTimeout : Option Millisecond.Offset
+  headerTimeout : Option Timestamp
+  connectionContext : CancellationContext
+
+/--
+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.
+Calls `Handler.onFailure` and returns `.close` on transport errors.
+-/
+private def pollNextEvent
+    {σ β : Type} [Transport α] [Handler σ] [Body β]
+    (config : Config) (handler : σ) (sources : PollSources α β)
+    : Async (Recv β) := do
+  let expectedBytes := sources.expect
+    |>.getD config.defaultPayloadBytes
+    |>.min config.maximumRecvSize
+    |>.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 .keepAliveTimeout))
+    else if let some timeout := sources.headerTimeout then
+      selectables := selectables.push (.case (← Selector.sleep (timeout - (← Timestamp.now)).toMilliseconds) (fun _ => pure .timeout))
+    else
+      selectables := selectables.push (.case (← Selector.sleep sources.timeout) (fun _ => pure .timeout))
+
+  if let some responseBody := sources.responseBody then
+    selectables := selectables.push (.case (Body.recvSelector responseBody) (Recv.responseBody · |> pure))
+
+  if let some requestBody := sources.requestBody then
+    selectables := selectables.push (.case (requestBody.interestSelector) (Recv.bodyInterest · |> pure))
+
+  if let some response := sources.response then
+    selectables := selectables.push (.case response.recvSelector (Recv.response · |> pure))
+
+  try Selectable.one selectables
+  catch e =>
+    Handler.onFailure handler e
+    pure .close
+
+/--
+Handles the `Expect: 100-continue` protocol for a pending request head.
+Races between the handler's decision (`Handler.onContinue`), the connection being
+cancelled, and a lingering timeout. Returns the updated machine and whether
+`pendingHead` should be cleared (i.e. when the request is rejected).
+-/
+private def handleContinueEvent
+    {σ : Type} [Handler σ]
+    (handler : σ) (machine : H1.Machine .receiving) (head : Request.Head)
+    (config : Config) (connectionContext : CancellationContext)
+    : Async (H1.Machine .receiving × Bool) := do
+
+  let continueChannel : Std.Channel Bool ← Std.Channel.new
+  let continueTask ← Handler.onContinue handler head |>.asTask
+
+  BaseIO.chainTask continueTask fun
+    | .ok v => discard <| continueChannel.send v
+    | .error _ => discard <| continueChannel.send false
+
+  let canContinue ← Selectable.one #[
+    .case continueChannel.recvSelector pure,
+    .case connectionContext.doneSelector (fun _ => pure false),
+    .case (← Selector.sleep config.lingeringTimeout) (fun _ => pure false)
+  ]
+
+  let status := if canContinue then Status.«continue» else Status.expectationFailed
+  return (machine.canContinue status, !canContinue)
+
+/--
+Injects a `Date` header into a response head if `Config.generateDate` is set
+and the response does not already include one.
+-/
+private def prepareResponseHead (config : Config) (head : Response.Head) : Async Response.Head := do
+  if config.generateDate ∧ ¬head.headers.contains Header.Name.date then
+    let now ← Std.Time.DateTime.now (tz := .UTC)
+    return { head with headers := head.headers.insert Header.Name.date (Header.Value.ofString! now.toRFC822String) }
+  else
+    return head
+
+/--
+Applies a successful handler response to the machine.
+Optionally injects a `Date` header, records the known body size, and sends the
+response head. Returns the updated machine and the body stream to drain, or `none`
+when the body should be omitted (e.g., for HEAD requests).
+-/
+private def applyResponse
+    {β : Type} [Body β]
+    (config : Config) (machine : H1.Machine .receiving) (res : Response β)
+    : Async (H1.Machine .receiving × Option β) := do
+  let size ← Body.getKnownSize res.body
+  let machineSized :=
+    if let some knownSize := size then machine.setKnownSize knownSize
+    else machine
+  let responseHead ← prepareResponseHead config res.line
+  let machineWithHead := machineSized.send responseHead
+  if machineWithHead.writer.omitBody then
+    if ¬(← Body.isClosed res.body) then
+      Body.close res.body
+    return (machineWithHead, none)
+  else
+    return (machineWithHead, some res.body)
+
+/--
+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 (β : Type) where
+  machine : H1.Machine .receiving
+  requestStream : Body.Stream
+  keepAliveTimeout : Option Millisecond.Offset
+  currentTimeout : Millisecond.Offset
+  headerTimeout : Option Timestamp
+  response : Std.Channel (Except Error (Response β))
+  respStream : Option β
+  requiresData : Bool
+  expectData : Option Nat
+  handlerDispatched : Bool
+  pendingHead : Option Request.Head
+
+/--
+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; stops early on `.failed`.
+-/
+private def processH1Events
+    {σ β : Type} [Handler σ] [Body β]
+    (handler : σ) (config : Config) (connectionContext : CancellationContext)
+    (events : Array (H1.Event .receiving))
+    (state : ConnectionState β)
+    : Async (ConnectionState β) := do
+
+  let mut st := state
+
+  for event in events do
+    match event with
+    | .needMoreData expect =>
+      st := { st with requiresData := true, expectData := expect }
+
+    | .needAnswer => pure ()
+
+    | .endHeaders head =>
+
+      -- Sets the pending head and removes the KeepAlive or Header timeout.
+      st := { st with
+        currentTimeout := config.lingeringTimeout
+        keepAliveTimeout := none
+        headerTimeout := none
+        pendingHead := some head
+      }
+
+      if let some length := head.getSize true then
+        -- Sets the size of the body that is going out of the connection.
+        Body.setKnownSize st.requestStream (some length)
+
+    | .«continue» =>
+      if let some head := st.pendingHead then
+        let (newMachine, clearPending) ← handleContinueEvent handler st.machine head config connectionContext
+        st := { st with machine := newMachine }
+        if clearPending then
+          st := { st with pendingHead := none }
+
+    | .next =>
+      -- Reset all per-request state for the next pipelined request.
+      if ¬(← Body.isClosed st.requestStream) then
+        Body.close st.requestStream
+
+      if let some res := st.respStream then
+        if ¬(← Body.isClosed res) then
+          Body.close res
+
+      let newStream ← Body.mkStream
+
+      st := { st with
+        requestStream := newStream
+        response := ← Std.Channel.new
+        respStream := none
+        keepAliveTimeout := some config.keepAliveTimeout.val
+        currentTimeout := config.keepAliveTimeout.val
+        headerTimeout := none
+        handlerDispatched := false
+      }
+
+    | .failed err =>
+      Handler.onFailure handler (toString err)
+
+      if ¬(← Body.isClosed st.requestStream) then
+        Body.close st.requestStream
+
+      st := { st with requiresData := false, pendingHead := none }
+      break
+
+    | .closeBody =>
+      if ¬(← Body.isClosed st.requestStream) then
+        Body.close st.requestStream
+
+    | .close => pure ()
+
+  return st
+
+/--
+Dispatches a pending request head to the handler if one is waiting.
+Spawns the handler as an async task and routes its result back through `state.response`.
+Returns the updated state with `pendingHead` cleared and `handlerDispatched` set.
+-/
+private def dispatchPendingRequest
+    {σ : Type} [Handler σ]
+    (handler : σ) (extensions : Extensions) (connectionContext : CancellationContext)
+    (state : ConnectionState (Handler.ResponseBody σ))
+    : Async (ConnectionState (Handler.ResponseBody σ)) := do
+  if let some line := state.pendingHead then
+
+    let task ← Handler.onRequest handler { line, body := state.requestStream, extensions } connectionContext
+      |>.asTask
+
+    BaseIO.chainTask task (discard ∘ state.response.send)
+    return { state with pendingHead := none, handlerDispatched := true }
+  else
+    return state
+
+/--
+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
+    {σ β : Type} [Handler σ] [Body β]
+    (handler : σ) (config : Config)
+    (event : Recv β) (state : ConnectionState β)
+    : Async (ConnectionState β × Bool) := do
+
+  match event with
+  | .bytes (some bs) =>
+
+    let mut st := state
+
+    -- After the first byte after idle we switch from keep-alive timeout to per-request header timeout.
+    if st.keepAliveTimeout.isSome then
+      st := { st with
+        keepAliveTimeout := none
+        headerTimeout := some <| (← Timestamp.now) + config.headerTimeout
+      }
+
+    return ({ st with machine := st.machine.feed bs }, false)
+
+  | .bytes none =>
+    return ({ state with machine := state.machine.noMoreInput }, false)
+
+  | .responseBody (some chunk) =>
+    return ({ state with machine := state.machine.sendData #[chunk] }, false)
+
+  | .responseBody none =>
+    if let some res := state.respStream then
+      if ¬(← Body.isClosed res) then Body.close res
+    return ({ state with machine := state.machine.userClosedBody, respStream := 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
+        try st.requestStream.send pulled.chunk pulled.incomplete
+        catch e => Handler.onFailure handler e
+        if pulled.final then
+          if ¬(← Body.isClosed st.requestStream) then
+            Body.close st.requestStream
+
+      return (st, false)
+    else
+      return (state, false)
+
+  | .close => return (state, true)
+
+  | .timeout =>
+    Handler.onFailure handler "request header timeout"
+    return ({ state with machine := state.machine.closeWithError .requestTimeout, handlerDispatched := false }, false)
+
+  | .keepAliveTimeout =>
+    return ({ state with machine := state.machine.closeWithError .requestTimeout, handlerDispatched := false }, false)
+
+  | .shutdown =>
+    return ({ state with machine := state.machine.closeWithError .serviceUnavailable, handlerDispatched := false }, false)
+
+  | .response (.error err) =>
+    Handler.onFailure handler err
+    return ({ state with machine := state.machine.closeWithError .internalServerError, handlerDispatched := false }, false)
+
+  | .response (.ok res) =>
+    if state.machine.failed then
+      if ¬(← Body.isClosed res.body) then Body.close res.body
+      return ({ state with handlerDispatched := false }, false)
+    else
+      let (newMachine, newRespStream) ← applyResponse config state.machine res
+      return ({ state with machine := newMachine, handlerDispatched := false, respStream := newRespStream }, false)
+
+/--
+Computes the active `PollSources` for the current connection state.
+Determines which IO sources need attention and whether to include the socket.
+-/
+private def buildPollSources
+    {α β : Type} [Transport α]
+    (socket : α) (connectionContext : CancellationContext) (state : ConnectionState β)
+    : Async (PollSources α β) := do
+  let requestBodyOpen ←
+    if state.machine.canPullBody then pure !(← Body.isClosed state.requestStream)
+    else pure false
+
+  let requestBodyInterested ←
+    if state.machine.canPullBody ∧ requestBodyOpen then state.requestStream.hasInterest
+    else pure false
+
+  let requestBody ←
+    if state.machine.canPullBodyNow ∧ requestBodyOpen then pure (some state.requestStream)
+    else pure none
+
+  -- Include the socket only when there is more to do than waiting for the handler alone.
+  let pollSocket :=
+    state.requiresData ∨ !state.handlerDispatched ∨ state.respStream.isSome ∨
+    state.machine.writer.sentMessage ∨ (state.machine.canPullBody ∧ requestBodyInterested)
+
+  return {
+    socket := if pollSocket then some socket else none
+    expect := state.expectData
+    response := if state.handlerDispatched then some state.response else none
+    responseBody := state.respStream
+    requestBody := requestBody
+    timeout := state.currentTimeout
+    keepAliveTimeout := state.keepAliveTimeout
+    headerTimeout := state.headerTimeout
+    connectionContext := connectionContext
+  }
+
+/--
+Runs the main request/response processing loop for a single connection.
+Drives the HTTP/1.1 state machine through four phases each iteration:
+send buffered output, process H1 events, dispatch pending requests, poll for I/O.
+-/
+private def handle
+    {σ : Type} [Transport α] [h : Handler σ]
+    (connection : Connection α)
+    (config : Config)
+    (connectionContext : CancellationContext)
+    (handler : σ) : Async Unit := do
+
+  let _ : Body (Handler.ResponseBody σ) := Handler.responseBodyInstance
+
+  let socket := connection.socket
+  let initStream ← Body.mkStream
+
+  let mut state : ConnectionState (Handler.ResponseBody σ) := {
+    machine := connection.machine
+    requestStream := initStream
+    keepAliveTimeout := some config.keepAliveTimeout.val
+    currentTimeout := config.keepAliveTimeout.val
+    headerTimeout := none
+    response := ← Std.Channel.new
+    respStream := none
+    requiresData := false
+    expectData := none
+    handlerDispatched := false
+    pendingHead := none
+  }
+
+  while ¬state.machine.halted do
+
+    -- Phase 1: 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.data
+      catch e =>
+        Handler.onFailure handler e
+        break
+
+    -- Phase 2: process all events emitted by this step.
+    state ← processH1Events handler config connectionContext step.events state
+
+    -- Phase 3: dispatch any newly parsed request to the handler.
+    state ← dispatchPendingRequest handler connection.extensions connectionContext state
+
+    -- Phase 4: wait for the next IO event when any source needs attention.
+    if state.requiresData ∨ state.handlerDispatched ∨ state.respStream.isSome ∨ state.machine.canPullBody then
+      state := { state with requiresData := false }
+      let sources ← buildPollSources socket connectionContext state
+      let event ← pollNextEvent config handler sources
+      let (newState, shouldClose) ← handleRecvEvent handler config event state
+      state := newState
+      if shouldClose then break
+
+  -- Clean up: close all open streams and the socket.
+  if ¬(← Body.isClosed state.requestStream) then
+    Body.close state.requestStream
+
+  if let some res := state.respStream then
+    if ¬(← Body.isClosed res) then Body.close res
+
+  Transport.close socket
+
+end Connection
+
+/--
+Handles request/response processing for a single connection using an `Async` handler.
+The library-level entry point for running a server is `Server.serve`.
+This function can be used with a `TCP.Socket` or any other type that implements
+`Transport` to build custom server loops.
+
+# Example
+
+```lean
+-- Create a TCP socket server instance
+let server ← Socket.Server.mk
+server.bind addr
+server.listen backlog
+
+-- Enter an infinite loop to handle incoming client connections
+while true do
+  let client ← server.accept
+  background (serveConnection client handler config)
+```
+-/
+def serveConnection
+    {σ : Type} [Transport t] [Handler σ]
+    (client : t) (handler : σ)
+    (config : Config) (extensions : Extensions := .empty) : ContextAsync Unit := do
+  (Connection.mk client { config := config.toH1Config } extensions)
+  |>.handle config (← ContextAsync.getContext) handler
+
+end Std.Http.Server

src/Std/Internal/Http/Server/Handler.lean

@@ -0,0 +1,60 @@
+/-
+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
+public import Std.Internal.Http.Data
+public import Std.Internal.Async.ContextAsync
+
+public section
+
+namespace Std.Http.Server
+
+open Std.Internal.IO.Async
+
+set_option linter.all true
+
+/--
+A type class for handling HTTP server requests. Implement this class to define how the server
+responds to incoming requests, failures, and `Expect: 100-continue` headers.
+-/
+class Handler (σ : Type) where
+  /--
+  Concrete body type produced by `onRequest`.
+  Defaults to `Body.Any`, but handlers may override it with any reader/writer-compatible body.
+  -/
+  ResponseBody : Type := Body.Any
+
+  /--
+  Body instance required by the connection loop for receiving response chunks.
+  -/
+  [responseBodyInstance : Body ResponseBody]
+
+  /--
+  Called for each incoming HTTP request.
+  -/
+  onRequest (self : σ) (request : Request Body.Stream) : ContextAsync (Response ResponseBody)
+
+  /--
+  Called when an I/O or transport error occurs while processing a request (e.g. broken socket,
+  handler exception). This is a **notification only**: the connection will close regardless of
+  the handler's response. Use this for logging and metrics. The default implementation does nothing.
+  -/
+  onFailure (self : σ) (error : IO.Error) : Async Unit :=
+    pure ()
+
+  /--
+  Called when a request includes an `Expect: 100-continue` header. Return `true` to send a
+  `100 Continue` response and accept the body. If `false` is returned the server sends
+  `417 Expectation Failed`, disables keep-alive, and closes the request body reader.
+  This function is guarded by `Config.lingeringTimeout` and may be cancelled on server shutdown.
+  The default implementation always returns `true`.
+  -/
+  onContinue (self : σ) (request : Request.Head) : Async Bool :=
+    pure true
+
+end Std.Http.Server

src/Std/Internal/Http/Test/Helpers.lean

@@ -0,0 +1,243 @@
+/-
+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.Server
+public import Std.Internal.Async
+public import Std.Internal.Async.Timer
+import Init.Data.String.Legacy
+
+public section
+
+open Std.Internal.IO Async
+open Std Http
+
+namespace Std.Http.Test
+
+abbrev TestHandler := Request Body.Stream → ContextAsync (Response Body.Any)
+
+instance : Std.Http.Server.Handler TestHandler where
+  onRequest handler request := handler request
+
+/--
+Default config for server tests. Short lingering timeout, no Date header.
+-/
+def defaultConfig : Config :=
+  { lingeringTimeout := 1000, generateDate := false }
+
+private def sendRaw
+    (client : Mock.Client) (server : Mock.Server) (raw : ByteArray)
+    (handler : TestHandler) (config : Config) : IO ByteArray :=
+  Async.block do
+    client.send raw
+    Std.Http.Server.serveConnection server handler config |>.run
+    let res ← client.recv?
+    pure (res.getD .empty)
+
+private def sendClose
+    (client : Mock.Client) (server : Mock.Server) (raw : ByteArray)
+    (handler : TestHandler) (config : Config) : IO ByteArray :=
+  Async.block do
+    client.send raw
+    client.getSendChan.close
+    Std.Http.Server.serveConnection server handler config |>.run
+    let res ← client.recv?
+    pure (res.getD .empty)
+
+-- Timeout wrapper
+
+private def withTimeout {α : Type} (name : String) (ms : Nat) (action : IO α) : IO α := do
+  let task ← IO.asTask action
+  let ticks := (ms + 9) / 10
+  let rec loop : Nat → IO α
+    | 0 => do IO.cancel task; throw <| IO.userError s!"'{name}' timed out after {ms}ms"
+    | n + 1 => do
+      if (← IO.getTaskState task) == .finished then
+        match ← IO.wait task with
+        | .ok x => pure x
+        | .error e => throw e
+      else IO.sleep 10; loop n
+  loop ticks
+
+-- Test grouping
+
+/--
+Run `tests` and wrap any failure message with the group name.
+Use as `#eval runGroup "Topic" do ...`.
+-/
+def runGroup (name : String) (tests : IO Unit) : IO Unit :=
+  try tests
+  catch e => throw (IO.userError s!"[{name}]\n{e}")
+
+-- Per-test runners
+
+/--
+Create a fresh mock connection, send `raw`, and run assertions.
+-/
+def check
+    (name : String)
+    (raw : String)
+    (handler : TestHandler)
+    (expect : ByteArray → IO Unit)
+    (config : Config := defaultConfig) : IO Unit := do
+  let (client, server) ← Mock.new
+  let response ← sendRaw client server raw.toUTF8 handler config
+  try expect response
+  catch e => throw (IO.userError s!"[{name}] {e}")
+
+/--
+Like `check` but closes the client channel before running the server.
+Use for tests involving truncated input or silent-close (EOF-triggered behavior).
+-/
+def checkClose
+    (name : String)
+    (raw : String)
+    (handler : TestHandler)
+    (expect : ByteArray → IO Unit)
+    (config : Config := defaultConfig) : IO Unit := do
+  let (client, server) ← Mock.new
+  let response ← sendClose client server raw.toUTF8 handler config
+  try expect response
+  catch e => throw (IO.userError s!"[{name}] {e}")
+
+/--
+Like `check` wrapped in a wall-clock timeout.
+Required when the test involves streaming, async timers, or keep-alive behavior.
+-/
+def checkTimed
+    (name : String)
+    (ms : Nat := 2000)
+    (raw : String)
+    (handler : TestHandler)
+    (expect : ByteArray → IO Unit)
+    (config : Config := defaultConfig) : IO Unit :=
+  withTimeout name ms <| check name raw handler expect config
+
+-- Assertion helpers
+
+/--
+Assert the response starts with `prefix_` (e.g. `"HTTP/1.1 200"`).
+-/
+def assertStatus (response : ByteArray) (prefix_ : String) : IO Unit := do
+  let text := String.fromUTF8! response
+  unless text.startsWith prefix_ do
+    throw <| IO.userError s!"expected status {prefix_.quote}, got:\n{text.quote}"
+
+/--
+Assert the response is byte-for-byte equal to `expected`.
+Use sparingly — prefer `assertStatus` + `assertContains` for 200 responses.
+-/
+def assertExact (response : ByteArray) (expected : String) : IO Unit := do
+  let text := String.fromUTF8! response
+  unless text == expected do
+    throw <| IO.userError s!"expected:\n{expected.quote}\ngot:\n{text.quote}"
+
+/--
+Assert `needle` appears anywhere in the response.
+-/
+def assertContains (response : ByteArray) (needle : String) : IO Unit := do
+  let text := String.fromUTF8! response
+  unless text.contains needle do
+    throw <| IO.userError s!"expected to contain {needle.quote}, got:\n{text.quote}"
+
+/--
+Assert `needle` does NOT appear in the response.
+-/
+def assertAbsent (response : ByteArray) (needle : String) : IO Unit := do
+  let text := String.fromUTF8! response
+  if text.contains needle then
+    throw <| IO.userError s!"expected NOT to contain {needle.quote}, got:\n{text.quote}"
+
+/--
+Assert the response contains exactly `n` occurrences of `"HTTP/1.1 "`.
+-/
+def assertResponseCount (response : ByteArray) (n : Nat) : IO Unit := do
+  let text := String.fromUTF8! response
+  let got := (text.splitOn "HTTP/1.1 ").length - 1
+  unless got == n do
+    throw <| IO.userError s!"expected {n} HTTP/1.1 responses, got {got}:\n{text.quote}"
+
+-- Common fixed response strings
+
+def r400 : String :=
+  "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r408 : String :=
+  "HTTP/1.1 408 Request Timeout\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r413 : String :=
+  "HTTP/1.1 413 Content Too Large\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r417 : String :=
+  "HTTP/1.1 417 Expectation Failed\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r431 : String :=
+  "HTTP/1.1 431 Request Header Fields Too Large\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def r505 : String :=
+  "HTTP/1.1 505 HTTP Version Not Supported\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+-- Standard handlers
+
+/--
+Always respond 200 "ok" without reading the request body.
+-/
+def okHandler : TestHandler := fun _ => Response.ok |>.text "ok"
+
+/--
+Read the full request body and echo it back as text/plain.
+-/
+def echoHandler : TestHandler := fun req => do
+  Response.ok |>.text (← req.body.readAll)
+
+/--
+Respond 200 with the request URI as the body.
+-/
+def uriHandler : TestHandler := fun req =>
+  Response.ok |>.text (toString req.line.uri)
+
+-- Request builder helpers
+
+/--
+Minimal GET request. `extra` is appended as raw header lines (each ending with `\x0d\n`)
+before the blank line.
+-/
+def mkGet (path : String := "/") (extra : String := "") : String :=
+  s!"GET {path} HTTP/1.1\x0d\nHost: example.com\x0d\n{extra}\x0d\n"
+
+/--
+GET with `Connection: close`.
+-/
+def mkGetClose (path : String := "/") : String :=
+  mkGet path "Connection: close\x0d\n"
+
+/--
+POST with a fixed Content-Length body. `extra` is appended before the blank line.
+-/
+def mkPost (path : String) (body : String) (extra : String := "") : String :=
+  s!"POST {path} HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: {body.toUTF8.size}\x0d\n{extra}\x0d\n{body}"
+
+/--
+POST with Transfer-Encoding: chunked. `chunkedBody` is the pre-formatted body
+(use `chunk` + `chunkEnd` to build it).
+-/
+def mkChunked (path : String) (chunkedBody : String) (extra : String := "") : String :=
+  s!"POST {path} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\n{extra}\x0d\n{chunkedBody}"
+
+/--
+Format a single chunk: `<hex-size>\x0d\n<data>\x0d\n`.
+-/
+def chunk (data : String) : String :=
+  let hexSize := Nat.toDigits 16 data.toUTF8.size |> String.ofList
+  s!"{hexSize}\x0d\n{data}\x0d\n"
+
+/--
+The terminal zero-chunk that ends a chunked body.
+-/
+def chunkEnd : String := "0\x0d\n\x0d\n"
+
+end Std.Http.Test

src/Std/Internal/Http/Transport.lean

@@ -0,0 +1,249 @@
+/-
+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.Protocol.H1
+
+public section
+
+/-!
+# Transport
+
+This module exposes a `Transport` type class that is used to represent different transport mechanisms
+that can be used with an HTTP connection.
+-/
+
+namespace Std.Http
+open Std Internal IO Async TCP
+
+set_option linter.all true
+
+/--
+Generic HTTP interface that abstracts over different transport mechanisms.
+-/
+class Transport (α : Type) where
+  /--
+  Receive data from the client connection, up to the expected size.
+  Returns None if the connection is closed or no data is available.
+  -/
+  recv : α → UInt64 → Async (Option ByteArray)
+
+  /--
+  Send all data through the client connection.
+  -/
+  sendAll : α → Array ByteArray → Async Unit
+
+  /--
+  Get a selector for receiving data asynchronously.
+  -/
+  recvSelector : α → UInt64 → Selector (Option ByteArray)
+
+  /--
+  Close the transport connection.
+  The default implementation is a no-op; override this for transports that require explicit teardown.
+  For `Socket.Client`, the runtime closes the file descriptor when the object is finalized.
+  -/
+  close : α → IO Unit := fun _ => pure ()
+
+instance : Transport Socket.Client where
+  recv client expect := client.recv? expect
+  sendAll client data := client.sendAll data
+  recvSelector client expect := client.recvSelector expect
+
+open Internal.IO.Async in
+
+/--
+Shared state for a bidirectional mock connection.
+-/
+private structure MockLink.SharedState where
+  /--
+  Client to server direction.
+  -/
+  clientToServer : Std.CloseableChannel ByteArray
+
+  /--
+  Server to client direction.
+  -/
+  serverToClient : Std.CloseableChannel ByteArray
+
+/--
+Mock client endpoint for testing.
+-/
+structure Mock.Client where
+  private shared : MockLink.SharedState
+
+/--
+Mock server endpoint for testing.
+-/
+structure Mock.Server where
+  private shared : MockLink.SharedState
+
+namespace Mock
+
+/--
+Creates a mock server and client that are connected to each other and share the
+same underlying state, enabling bidirectional communication.
+-/
+def new : BaseIO (Mock.Client × Mock.Server) := do
+  let first ← Std.CloseableChannel.new
+  let second ← Std.CloseableChannel.new
+
+  return (⟨⟨first, second⟩⟩, ⟨⟨first, second⟩⟩)
+
+/--
+Receives data from a channel, joining all available data up to the expected size. First does a
+blocking recv, then greedily consumes available data with tryRecv until `expect` bytes are reached.
+-/
+def recvJoined (recvChan : Std.CloseableChannel ByteArray) (expect : Option UInt64) : Async (Option ByteArray) := do
+  match ← await (← recvChan.recv) with
+  | none => return none
+  | some first =>
+    let mut result := first
+    repeat
+      if let some expect := expect then
+        if result.size.toUInt64 ≥ expect then break
+
+      match ← recvChan.tryRecv with
+      | none => break
+      | some chunk => result := result ++ chunk
+    return some result
+
+/--
+Sends a single ByteArray through a channel.
+-/
+def send (sendChan : Std.CloseableChannel ByteArray) (data : ByteArray) : Async Unit := do
+  Async.ofAsyncTask ((← sendChan.send data) |>.map (Except.mapError (IO.userError ∘ toString)))
+
+/--
+Sends ByteArrays through a channel.
+-/
+def sendAll (sendChan : Std.CloseableChannel ByteArray) (data : Array ByteArray) : Async Unit := do
+  for chunk in data do
+    send sendChan chunk
+
+/--
+Creates a selector for receiving from a channel.
+-/
+def recvSelector (recvChan : Std.CloseableChannel ByteArray) : Selector (Option ByteArray) :=
+  recvChan.recvSelector
+
+end Mock
+
+namespace Mock.Client
+
+/--
+Gets the receive channel for a client (server to client direction).
+-/
+def getRecvChan (client : Mock.Client) : Std.CloseableChannel ByteArray :=
+  client.shared.serverToClient
+
+/--
+Gets the send channel for a client (client to server direction).
+-/
+def getSendChan (client : Mock.Client) : Std.CloseableChannel ByteArray :=
+  client.shared.clientToServer
+
+/--
+Sends a single ByteArray.
+-/
+def send (client : Mock.Client) (data : ByteArray) : Async Unit :=
+  Mock.send (getSendChan client) data
+
+/--
+Receives data, joining all available chunks.
+-/
+def recv? (client : Mock.Client) (expect : Option UInt64 := none) : Async (Option ByteArray) :=
+  Mock.recvJoined (getRecvChan client) expect
+
+/--
+Tries to receive data without blocking, joining all immediately available chunks.
+Returns `none` if no data is available.
+-/
+def tryRecv? (client : Mock.Client) (_expect : UInt64 := 0) : BaseIO (Option ByteArray) := do
+  match ← (getRecvChan client).tryRecv with
+  | none => return none
+  | some first =>
+    let mut result := first
+    repeat
+      match ← (getRecvChan client).tryRecv with
+      | none => break
+      | some chunk => result := result ++ chunk
+    return some result
+
+/--
+Closes the mock server and client.
+-/
+def close (client : Mock.Client) : IO Unit := do
+  if !(← client.shared.clientToServer.isClosed) then client.shared.clientToServer.close
+  if !(← client.shared.serverToClient.isClosed) then client.shared.serverToClient.close
+
+end Mock.Client
+
+namespace Mock.Server
+
+/--
+Gets the receive channel for a server (client to server direction).
+-/
+def getRecvChan (server : Mock.Server) : Std.CloseableChannel ByteArray :=
+  server.shared.clientToServer
+
+/--
+Gets the send channel for a server (server to client direction).
+-/
+def getSendChan (server : Mock.Server) : Std.CloseableChannel ByteArray :=
+  server.shared.serverToClient
+
+/--
+Sends a single ByteArray.
+-/
+def send (server : Mock.Server) (data : ByteArray) : Async Unit :=
+  Mock.send (getSendChan server) data
+
+/--
+Receives data, joining all available chunks.
+-/
+def recv? (server : Mock.Server) (expect : Option UInt64 := none) : Async (Option ByteArray) :=
+  Mock.recvJoined (getRecvChan server) expect
+
+/--
+Tries to receive data without blocking, joining all immediately available chunks. Returns `none` if no
+data is available.
+-/
+def tryRecv? (server : Mock.Server) (_expect : UInt64 := 0) : BaseIO (Option ByteArray) := do
+  match ← (getRecvChan server).tryRecv with
+  | none => return none
+  | some first =>
+    let mut result := first
+    repeat
+      match ← (getRecvChan server).tryRecv with
+      | none => break
+      | some chunk => result := result ++ chunk
+    return some result
+
+/--
+Closes the mock server and client.
+-/
+def close (server : Mock.Server) : IO Unit := do
+  if !(← server.shared.clientToServer.isClosed) then server.shared.clientToServer.close
+  if !(← server.shared.serverToClient.isClosed) then server.shared.serverToClient.close
+
+
+end Mock.Server
+
+instance : Transport Mock.Client where
+  recv client expect := Mock.recvJoined (Mock.Client.getRecvChan client) (some expect)
+  sendAll client data := Mock.sendAll (Mock.Client.getSendChan client) data
+  recvSelector client _ := Mock.recvSelector (Mock.Client.getRecvChan client)
+  close client := client.close
+
+instance : Transport Mock.Server where
+  recv server expect := Mock.recvJoined (Mock.Server.getRecvChan server) (some expect)
+  sendAll server data := Mock.sendAll (Mock.Server.getSendChan server) data
+  recvSelector server _ := Mock.recvSelector (Mock.Server.getRecvChan server)
+  close server := server.close
+
+end Std.Http

src/Std/Internal/Parsec/ByteArray.lean

@@ -44,8 +44,15 @@ protected def Parser.run (p : Parser α) (arr : ByteArray) : Except String α :=
 Parse a single byte equal to `b`, fails if different.
 -/
 @[inline]
-def pbyte (b : UInt8) : Parser UInt8 := attempt do
-  if (← any) = b then pure b else fail s!"expected: '{b}'"
+def pbyte (b : UInt8) : Parser UInt8 := fun it =>
+  if h : it.hasNext then
+    let got := it.curr' h
+    if got = b then
+      .success (it.next' h) got
+    else
+      .error it (.other s!"expected: '{b}'")
+  else
+    .error it .eof
 
 /--
 Skip a single byte equal to `b`, fails if different.
@@ -57,16 +64,29 @@ def skipByte (b : UInt8) : Parser Unit :=
 /--
 Skip a sequence of bytes equal to the given `ByteArray`.
 -/
-def skipBytes (arr : ByteArray) : Parser Unit := do
-  for b in arr do
-    skipByte b
+def skipBytes (arr : ByteArray) : Parser Unit := fun it =>
+  let rec go (idx : Nat) (it : ByteArray.Iterator) : ParseResult Unit ByteArray.Iterator :=
+    if h : idx < arr.size then
+      if hnext : it.hasNext then
+        let got := it.curr' hnext
+        let want := arr[idx]
+        if got = want then
+          go (idx + 1) (it.next' hnext)
+        else
+          .error it (.other s!"expected byte {want}, got {got}")
+      else
+        .error it .eof
+    else
+      .success it ()
+  go 0 it
 
 /--
 Parse a string by matching its UTF-8 bytes, returns the string on success.
 -/
 @[inline]
 def pstring (s : String) : Parser String := do
-  skipBytes s.toUTF8
+  let utf8 := s.toUTF8
+  skipBytes utf8
   return s
 
 /--
@@ -193,19 +213,47 @@ def take (n : Nat) : Parser ByteSlice := fun it =>
   else
     .success (it.forward n) (it.array[it.idx...(it.idx+n)])
 
+/--
+Scans while `pred` is satisfied. Returns `(count, iterator, hitEof)`.
+-/
+private partial def scanWhile (pred : UInt8 → Bool) (count : Nat) (iter : ByteArray.Iterator) :
+    Nat × ByteArray.Iterator × Bool :=
+  if h : iter.hasNext then
+    if pred (iter.curr' h) then
+      scanWhile pred (count + 1) (iter.next' h)
+    else
+      (count, iter, false)
+  else
+    (count, iter, true)
+
+/--
+Scans while `pred` is satisfied, bounded by `limit`.
+Returns `(count, iterator, hitEof)`.
+-/
+private partial def scanWhileUpTo (pred : UInt8 → Bool) (limit : Nat) (count : Nat)
+    (iter : ByteArray.Iterator) : Nat × ByteArray.Iterator × Bool :=
+  if count ≥ limit then
+    (count, iter, false)
+  else if h : iter.hasNext then
+    if pred (iter.curr' h) then
+      scanWhileUpTo pred limit (count + 1) (iter.next' h)
+    else
+      (count, iter, false)
+  else
+    (count, iter, true)
+
 /--
 Parses while a predicate is satisfied.
+Fails with `.eof` if input ends while the predicate still holds.
 -/
 @[inline]
 partial def takeWhile (pred : UInt8 → Bool) : Parser ByteSlice :=
   fun it =>
-    let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : Nat × ByteArray.Iterator :=
-      if ¬iter.hasNext then (count, iter)
-      else if pred iter.curr then findEnd (count + 1) iter.next
-      else (count, iter)
-
-    let (length, newIt) := findEnd 0 it
-    .success newIt (it.array[it.idx...(it.idx + length)])
+    let (length, newIt, hitEof) := scanWhile pred 0 it
+    if hitEof then
+      .error newIt .eof
+    else
+      .success newIt (it.array[it.idx...(it.idx + length)])
 
 /--
 Parses until a predicate is satisfied (exclusive).
@@ -216,16 +264,16 @@ def takeUntil (pred : UInt8 → Bool) : Parser ByteSlice :=
 
 /--
 Skips while a predicate is satisfied.
+Fails with `.eof` if input ends while the predicate still holds.
 -/
 @[inline]
 partial def skipWhile (pred : UInt8 → Bool) : Parser Unit :=
   fun it =>
-    let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : ByteArray.Iterator :=
-      if ¬iter.hasNext then iter
-      else if pred iter.curr then findEnd (count + 1) iter.next
-      else iter
-
-    .success (findEnd 0 it) ()
+    let (_, newIt, hitEof) := scanWhile pred 0 it
+    if hitEof then
+      .error newIt .eof
+    else
+      .success newIt ()
 
 /--
 Skips until a predicate is satisfied.
@@ -236,34 +284,31 @@ def skipUntil (pred : UInt8 → Bool) : Parser Unit :=
 
 /--
 Parses while a predicate is satisfied, up to a given limit.
+Fails with `.eof` if input ends before stopping or reaching the limit.
 -/
 @[inline]
 partial def takeWhileUpTo (pred : UInt8 → Bool) (limit : Nat) : Parser ByteSlice :=
   fun it =>
-    let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : Nat × ByteArray.Iterator :=
-      if count ≥ limit then (count, iter)
-      else if ¬iter.hasNext then (count, iter)
-      else if pred iter.curr then findEnd (count + 1) iter.next
-      else (count, iter)
+    let (length, newIt, hitEof) := scanWhileUpTo pred limit 0 it
 
-    let (length, newIt) := findEnd 0 it
-    .success newIt (it.array[it.idx...(it.idx + length)])
+    if hitEof then
+      .error newIt .eof
+    else
+      .success newIt (it.array[it.idx...(it.idx + length)])
 
 /--
 Parses while a predicate is satisfied, up to a given limit, requiring at least one byte.
+Fails with `.eof` if input ends before stopping or reaching the limit.
 -/
 @[inline]
 def takeWhileUpTo1 (pred : UInt8 → Bool) (limit : Nat) : Parser ByteSlice :=
   fun it =>
-    let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : Nat × ByteArray.Iterator :=
-      if count ≥ limit then (count, iter)
-      else if ¬iter.hasNext then (count, iter)
-      else if pred iter.curr then findEnd (count + 1) iter.next
-      else (count, iter)
+    let (length, newIt, hitEof) := scanWhileUpTo pred limit 0 it
 
-    let (length, newIt) := findEnd 0 it
-    if length = 0 then
-      .error it (if newIt.atEnd then .eof else .other "expected at least one char")
+    if hitEof then
+      .error newIt .eof
+    else if length = 0 then
+      .error it (.other "expected at least one char")
     else
       .success newIt (it.array[it.idx...(it.idx + length)])
 
@@ -274,19 +319,42 @@ Parses until a predicate is satisfied (exclusive), up to a given limit.
 def takeUntilUpTo (pred : UInt8 → Bool) (limit : Nat) : Parser ByteSlice :=
   takeWhileUpTo (fun b => ¬pred b) limit
 
+/--
+Parses while a predicate is satisfied, consuming at most `limit` bytes.
+Unlike `takeWhileUpTo`, succeeds even if input ends before the predicate stops holding.
+-/
+@[inline]
+def takeWhileAtMost (pred : UInt8 → Bool) (limit : Nat) : Parser ByteSlice :=
+  fun it =>
+    let (length, newIt, _) := scanWhileUpTo pred limit 0 it
+    .success newIt (it.array[it.idx...(it.idx + length)])
+
+/--
+Parses while a predicate is satisfied, consuming at most `limit` bytes, requiring at least one.
+Unlike `takeWhileUpTo1`, succeeds even if input ends before the predicate stops holding.
+-/
+@[inline]
+def takeWhile1AtMost (pred : UInt8 → Bool) (limit : Nat) : Parser ByteSlice :=
+  fun it =>
+    let (length, newIt, _) := scanWhileUpTo pred limit 0 it
+    if length = 0 then
+      .error it (.other "expected at least one char")
+    else
+      .success newIt (it.array[it.idx...(it.idx + length)])
+
 /--
 Skips while a predicate is satisfied, up to a given limit.
+Fails with `.eof` if input ends before stopping or reaching the limit.
 -/
 @[inline]
 partial def skipWhileUpTo (pred : UInt8 → Bool) (limit : Nat) : Parser Unit :=
   fun it =>
-    let rec findEnd (count : Nat) (iter : ByteArray.Iterator) : ByteArray.Iterator :=
-      if count ≥ limit then iter
-      else if ¬iter.hasNext then iter
-      else if pred iter.curr then findEnd (count + 1) iter.next
-      else iter
+    let (_, newIt, hitEof) := scanWhileUpTo pred limit 0 it
 
-    .success (findEnd 0 it) ()
+    if hitEof then
+      .error newIt .eof
+    else
+      .success newIt ()
 
 /--
 Skips until a predicate is satisfied, up to a given limit.

src/Std/Sync.lean

@@ -11,6 +11,7 @@ public import Std.Sync.Channel
 public import Std.Sync.Mutex
 public import Std.Sync.RecursiveMutex
 public import Std.Sync.Barrier
+public import Std.Sync.Semaphore
 public import Std.Sync.SharedMutex
 public import Std.Sync.Notify
 public import Std.Sync.Broadcast

src/Std/Sync/Semaphore.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean FRO Contributors
+-/
+module
+
+prelude
+public import Init.Data.Queue
+public import Init.System.Promise
+public import Std.Sync.Mutex
+
+public section
+
+namespace Std
+
+private structure SemaphoreState where
+  permits : Nat
+  waiters : Std.Queue (IO.Promise Unit) := ∅
+deriving Nonempty
+
+/--
+Counting semaphore.
+
+`Semaphore.acquire` returns a promise that is resolved once a permit is available.
+If a permit is currently available, the returned promise is already resolved.
+`Semaphore.release` either resolves one waiting promise or increments the available permits.
+-/
+structure Semaphore where private mk ::
+  private lock : Mutex SemaphoreState
+
+/--
+Creates a resolved promise.
+-/
+private def mkResolvedPromise [Nonempty α] (a : α) : BaseIO (IO.Promise α) := do
+  let promise ← IO.Promise.new
+  promise.resolve a
+  return promise
+
+/--
+Creates a new semaphore with `permits` initially available permits.
+-/
+def Semaphore.new (permits : Nat) : BaseIO Semaphore := do
+  return { lock := ← Mutex.new { permits } }
+
+/--
+Requests one permit.
+Returns a promise that resolves once the permit is acquired.
+-/
+def Semaphore.acquire (sem : Semaphore) : BaseIO (IO.Promise Unit) := do
+  sem.lock.atomically do
+    let st ← get
+    if st.permits > 0 then
+      set { st with permits := st.permits - 1 }
+      mkResolvedPromise ()
+    else
+      let promise ← IO.Promise.new
+      set { st with waiters := st.waiters.enqueue promise }
+      return promise
+
+/--
+Tries to acquire a permit without blocking. Returns `true` on success.
+-/
+def Semaphore.tryAcquire (sem : Semaphore) : BaseIO Bool := do
+  sem.lock.atomically do
+    let st ← get
+    if st.permits > 0 then
+      set { st with permits := st.permits - 1 }
+      return true
+    else
+      return false
+
+/--
+Releases one permit and resolves one waiting acquirer, if any.
+-/
+def Semaphore.release (sem : Semaphore) : BaseIO Unit := do
+  let waiter? ← sem.lock.atomically do
+    let st ← get
+    match st.waiters.dequeue? with
+    | some (waiter, waiters) =>
+      set { st with waiters }
+      return some waiter
+    | none =>
+      set { st with permits := st.permits + 1 }
+      return none
+  if let some waiter := waiter? then
+    waiter.resolve ()
+
+/--
+Returns the number of currently available permits.
+-/
+def Semaphore.availablePermits (sem : Semaphore) : BaseIO Nat :=
+  sem.lock.atomically do
+    return (← get).permits
+
+end Std

src/Std/Tactic/BVDecide/Syntax.lean

@@ -53,7 +53,7 @@ structure BVDecideConfig where
   /--
   Split hypotheses of the form `h : (x && y) = true` into `h1 : x = true` and `h2 : y = true`.
   This has synergy potential with embedded constraint substitution. Because embedded constraint
-  substitution is the only use case for this feature it is automatically disabled whenever embedded
+  subsitution is the only use case for this feature it is automatically disabled whenever embedded
   constraint substitution is disabled.
   -/
   andFlattening : Bool := true

src/include/lean/lean.h

@@ -3168,10 +3168,6 @@ static inline lean_obj_res lean_manual_get_root(lean_obj_arg _unit) {
     return lean_mk_string(LEAN_MANUAL_ROOT);
 }
 
-static inline lean_obj_res lean_runtime_hold(b_lean_obj_arg a) {
-    return lean_box(0);
-}
-
 #ifdef LEAN_EMSCRIPTEN
 #define LEAN_SCALAR_PTR_LITERAL(b1, b2, b3, b4, b5, b6, b7, b8) (lean_object*)((uint32_t)b1 | ((uint32_t)b2 << 8) | ((uint32_t)b3 << 16) | ((uint32_t)b4 << 24)), (lean_object*)((uint32_t)b5 | ((uint32_t)b6 << 8) | ((uint32_t)b7 << 16) | ((uint32_t)b8 << 24))
 #else

src/kernel/declaration.h

@@ -226,7 +226,7 @@ public:
     bool is_unsafe() const;
     /** \brief Only definitions have values for the purpose of reduction and
         type checking. Theorems used to be like that; now they are treated like
-        opaque declarations. */
+        opaque declations. */
     bool has_value() const { return is_definition(); }
 
     axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_get_ref(raw(), 0)); }

src/lake/Lake/Build/Common.lean

@@ -271,7 +271,7 @@ Returns `true` if the saved trace exists and its hash matches `inputHash`.
 
 If up-to-date, replays the saved log from the trace and sets the current
 build action to `replay`. Otherwise, if the log is empty and trace is synthetic,
-or if the trace is not up-to-date, the build action will be set to `fetch`.
+or if the trace is not up-to-date, the build action will be set ot `fetch`.
 -/
 public def SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
   if let .ok data := self then

src/lake/Lake/Build/InitFacets.lean

@@ -19,7 +19,7 @@ import Lake.Build.InputFile
 namespace Lake
 
 /-- The initial set of Lake facets. -/
-public def initFacetConfigs : FacetConfigMap :=
+public def initFacetConfigs : DNameMap FacetConfig :=
   DNameMap.empty
   |> insert Module.initFacetConfigs
   |> insert Package.initFacetConfigs
@@ -30,4 +30,4 @@ public def initFacetConfigs : FacetConfigMap :=
   |> insert InputDir.initFacetConfigs
 where
   insert {k} (group : DNameMap (KFacetConfig k)) map :=
-    group.foldl (init := map) fun m _ v => m.insert v.toFacetConfig
+    group.foldl (init := map) fun m k v => m.insert k v.toFacetConfig

src/lake/Lake/Build/Module.lean

@@ -705,7 +705,7 @@ private def Module.restoreAllArtifacts (mod : Module) (cached : ModuleOutputArti
 where
   @[inline] restoreSome file art? := art?.mapM (restoreArtifact file ·)
 
-public def Module.checkArtifactsExist (self : Module) (isModule : Bool) : BaseIO Bool := do
+public def Module.checkArtifactsExsist (self : Module) (isModule : Bool) : BaseIO Bool := do
   unless (← self.oleanFile.pathExists) do return false
   unless (← self.ileanFile.pathExists) do return false
   unless (← self.cFile.pathExists) do return false
@@ -718,7 +718,7 @@ public def Module.checkArtifactsExist (self : Module) (isModule : Bool) : BaseIO
   return true
 
 public protected def Module.checkExists (self : Module) (isModule : Bool) : BaseIO Bool := do
-  self.ltarFile.pathExists <||> self.checkArtifactsExist isModule
+  self.ltarFile.pathExists <||> self.checkArtifactsExsist isModule
 
 @[deprecated Module.checkExists (since := "2025-03-04")]
 public instance : CheckExists Module := ⟨Module.checkExists (isModule := false)⟩
@@ -788,7 +788,7 @@ instance : ToOutputJson ModuleOutputArtifacts := ⟨(toJson ·.descrs)⟩
 
 def Module.packLtar (self : Module) (arts : ModuleOutputArtifacts) : JobM Artifact := do
   let arts ← id do
-    if (← self.checkArtifactsExist arts.isModule) then
+    if (← self.checkArtifactsExsist arts.isModule) then
       return arts
     else self.restoreAllArtifacts arts
   let args ← id do
@@ -941,7 +941,7 @@ where
       | .inr savedTrace =>
         let status ← savedTrace.replayIfUpToDate' (oldTrace := srcTrace.mtime) mod depTrace
         if status.isUpToDate then
-          unless (← mod.checkArtifactsExist setup.isModule) do
+          unless (← mod.checkArtifactsExsist setup.isModule) do
             mod.unpackLtar mod.ltarFile
         else
           discard <| mod.buildLean depTrace srcFile setup
@@ -953,7 +953,7 @@ where
           mod.computeArtifacts setup.isModule
     else
       if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then
-        unless (← mod.checkArtifactsExist setup.isModule) do
+        unless (← mod.checkArtifactsExsist setup.isModule) do
           mod.unpackLtar mod.ltarFile
         mod.computeArtifacts setup.isModule
       else

src/lake/Lake/Build/Trace.lean

@@ -151,7 +151,7 @@ public def ofDecimal? (s : String) : Option Hash :=
 @[inline] public def ofString? (s : String) : Option Hash :=
   ofHex? s
 
-/-- Load a hash from a `.hash` file. -/
+/-- Laod a hash from a `.hash` file. -/
 public def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
   ofString? <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
 

src/lake/Lake/CLI/Help.lean

@@ -356,9 +356,9 @@ USAGE:
 
 COMMANDS:
   get [<mappings>]      download build outputs into the local Lake cache
-  put <mappings>        upload build outputs to a remote cache
+  put <mappings>        upload build ouptuts to a remote cache
   add <mappings>        add input-to-output mappings to the Lake cache
-  clean                 removes ALL from the local Lake cache
+  clean                 removes ALL froms the local Lake cache
   services              print configured remote cache services
 
 STAGING COMMANDS:
@@ -415,7 +415,7 @@ will search the repository's entire history (or as far as Git will allow).
 
 By default, Lake will download both the input-to-output mappings and the
 output artifacts for a package. By using `--mappings-onlys`, Lake will only
-download the mappings and delay downloading artifacts until they are needed.
+download the mappings abd delay downloading artifacts until they are needed.
 
 If a download for an artifact fails or the download process for a whole
 package fails, Lake will report this and continue on to the next. Once done,
@@ -469,7 +469,7 @@ OPTIONS:
   --scope=<remote-scope>          the prefix of artifacts within the service
   --repo=<github-repo>            for Reservoir, a GitHub repository scope
 
-Reads a list of input-to-output mappings from the provided file and adds
+Reads a list of input-to-output mapppings from the provided file and adds
 them to the local Lake cache. If `--service` is provided, the output artifacts
 can then be fetched lazily from that service during a Lake build. The service
 must either be `reservoir` or  be configured through the Lake system