fix: avoid error when keep alive connectioon times out

This PR adds `EquivBEq` and `LawfulHashable` instances to
`String.Slice`.

To this end, we redefine `String.Slice.hash`, which used to be
completely opaque, to be defined as `String.hash s.copy` (and then
`String.hash` remains opaque). We add tests that the `lean_slice_hash`
and `lean_string_hash` functions do indeed satisfy this relationship.

Of course, it would be even better to have a streaming MurmurHash64A
implementation in core that could be used to implement both of these so
that we can avoid the `opaque`, but that is a project for another day.

.github/workflows/build-template.yml

@@ -33,7 +33,7 @@ jobs:
         include: ${{fromJson(inputs.config)}}
       # complete all jobs
       fail-fast: false
-    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-5gb"]', matrix.os)) || matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}

.github/workflows/check-empty-pr.yml

@@ -0,0 +1,29 @@
+name: Check for empty PR
+
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-empty-pr:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v6
+      with:
+        ref: ${{ github.event_name == 'pull_request' && github.event.pull_request.head.sha || github.sha }}
+        fetch-depth: 0
+        filter: tree:0
+
+    - name: Check for empty diff
+      run: |
+        if [[ "${{ github.event_name }}" == "pull_request" ]]; then
+          base=$(git merge-base "origin/${{ github.base_ref }}" HEAD)
+        else
+          base=$(git rev-parse HEAD^1)
+        fi
+        if git diff --quiet "$base" HEAD --; then
+          echo "This PR introduces no changes compared to its base branch." | tee "$GITHUB_STEP_SUMMARY"
+          echo "It may be a duplicate of an already-merged PR." | tee -a "$GITHUB_STEP_SUMMARY"
+          exit 1
+        fi
+      shell: bash

script/release_checklist.py

@@ -236,7 +236,7 @@ def parse_version(version_str):
 def is_version_gte(version1, version2):
     """Check if version1 >= version2, including proper handling of release candidates."""
     # Check if version1 is a nightly toolchain
-    if version1.startswith("leanprover/lean4:nightly-"):
+    if version1.startswith("leanprover/lean4:nightly-") or version1.startswith("leanprover/lean4-nightly:"):
         return False
     return parse_version(version1) >= parse_version(version2)
 

src/Init/Data/BEq.lean

@@ -66,3 +66,8 @@ theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
 instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
   symm h := beq_iff_eq.2 <| Eq.symm <| beq_iff_eq.1 h
   trans hab hbc := beq_iff_eq.2 <| (beq_iff_eq.1 hab).trans <| beq_iff_eq.1 hbc
+
+theorem equivBEq_of_iff_apply_eq [BEq α] (f : α → β) (hf : ∀ a b, a == b ↔ f a = f b) : EquivBEq α where
+  rfl := by simp [hf]
+  symm := by simp [hf, eq_comm]
+  trans hab hbc := (hf _ _).2 (Eq.trans ((hf _ _).1 hab) ((hf _ _).1 hbc))

src/Init/Data/String/Iter.lean

@@ -6,29 +6,5 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.Iterators.Combinators.FilterMap
-public import Init.Data.Iterators.Consumers.Collect
-
-set_option doc.verso true
-
-namespace Std
-
-/--
-Convenience function for turning an iterator into a list of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : List String :=
-  it.map toString |>.toList
-
-/--
-Convenience function for turning an iterator into an array of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : Array String :=
-  it.map toString |>.toArray
-
-end Std
+public import Init.Data.String.Iter.Basic
+public import Init.Data.String.Iter.Intercalate

src/Init/Data/String/Iter/Basic.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.FilterMap
+public import Init.Data.Iterators.Consumers.Collect
+
+set_option doc.verso true
+
+namespace Std
+
+/--
+Convenience function for turning an iterator into a list of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : List String :=
+  it.map toString |>.toList
+
+/--
+Convenience function for turning an iterator into an array of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : Array String :=
+  it.map toString |>.toArray
+
+end Std

src/Init/Data/String/Iter/Intercalate.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.Monadic.FilterMap
+public import Init.Data.String.Basic
+import Init.Data.String.Slice
+
+set_option doc.verso true
+
+namespace Std
+
+/--
+Appends all the elements in the iterator, in order.
+-/
+public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
+    (it : Std.Iter (α := α) β) : String :=
+  (it.map toString).fold (init := "") (· ++ ·)
+
+/--
+Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
+-/
+@[inline]
+public def Iter.intercalateString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
+    (s : String.Slice) (it : Std.Iter (α := α) β) : String :=
+  it.map toString
+    |>.fold (init := none) (fun
+      | none, sl => some sl
+      | some str, sl => some (str ++ s ++ sl))
+    |>.getD ""
+
+end Std

src/Init/Data/String/Lemmas.lean

@@ -17,6 +17,8 @@ public import Init.Data.String.Lemmas.Pattern
 public import Init.Data.String.Lemmas.Slice
 public import Init.Data.String.Lemmas.Iterate
 public import Init.Data.String.Lemmas.Intercalate
+public import Init.Data.String.Lemmas.Iter
+public import Init.Data.String.Lemmas.Hashable
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas

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

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Slice
+public import Init.Data.LawfulHashable
+import all Init.Data.String.Slice
+import Init.Data.String.Lemmas.Slice
+
+namespace String
+
+public theorem hash_eq {s : String} : hash s = String.hash s := rfl
+
+namespace Slice
+
+public theorem hash_eq {s : String.Slice} : hash s = String.hash s.copy := (rfl)
+
+public instance : LawfulHashable String.Slice where
+  hash_eq a b hab := by simp [hash_eq, beq_eq_true_iff.1 hab]
+
+end String.Slice

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

@@ -10,6 +10,7 @@ public import Init.Data.String.Defs
 import all Init.Data.String.Defs
 public import Init.Data.String.Slice
 import all Init.Data.String.Slice
+import Init.ByCases
 
 public section
 
@@ -42,6 +43,16 @@ theorem intercalate_cons_of_ne_nil {s t : String} {l : List String} (h : l ≠ [
   match l, h with
   | u::l, _ => by simp
 
+theorem intercalate_append_of_ne_nil {l m : List String} {s : String} (hl : l ≠ []) (hm : m ≠ []) :
+    s.intercalate (l ++ m) = s.intercalate l ++ s ++ s.intercalate m := by
+  induction l with
+  | nil => simp_all
+  | cons hd tl ih =>
+    rw [List.cons_append, intercalate_cons_of_ne_nil (by simp_all)]
+    by_cases ht : tl = []
+    · simp_all
+    · simp [ih ht, intercalate_cons_of_ne_nil ht, String.append_assoc]
+
 @[simp]
 theorem toList_intercalate {s : String} {l : List String} :
     (s.intercalate l).toList = s.toList.intercalate (l.map String.toList) := by

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

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Iter.Intercalate
+public import Init.Data.String.Slice
+import all Init.Data.String.Iter.Intercalate
+import all Init.Data.String.Defs
+import Init.Data.String.Lemmas.Intercalate
+import Init.Data.Iterators.Lemmas.Consumers.Loop
+import Init.Data.Iterators.Lemmas.Combinators.FilterMap
+
+namespace Std.Iter
+
+@[simp]
+public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
+    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β]
+    {it : Std.Iter (α := α) β} : it.joinString = String.join (it.toList.map toString) := by
+  rw [joinString, String.join, ← foldl_toList, toList_map]
+
+@[simp]
+public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
+    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β] {s : String.Slice}
+    {it : Std.Iter (α := α) β} :
+    it.intercalateString s = s.copy.intercalate (it.toList.map toString) := by
+  simp only [intercalateString, String.appendSlice_eq, ← foldl_toList, toList_map]
+  generalize s.copy = s
+  suffices ∀ (l m : List String),
+      (l.foldl (init := if m = [] then none else some (s.intercalate m))
+        (fun | none, sl => some sl | some str, sl => some (str ++ s ++ sl))).getD ""
+        = s.intercalate (m ++ l) by
+    simpa [-foldl_toList] using this (it.toList.map toString) []
+  intro l m
+  induction l generalizing m with
+  | nil => cases m <;> simp
+  | cons hd tl ih =>
+    rw [List.append_cons, ← ih, List.foldl_cons]
+    congr
+    simp only [List.append_eq_nil_iff, List.cons_ne_self, and_false, ↓reduceIte]
+    match m with
+    | [] => simp
+    | x::xs =>
+      simp only [reduceCtorEq, ↓reduceIte, List.cons_append, Option.some.injEq]
+      rw [← List.cons_append, String.intercalate_append_of_ne_nil (by simp) (by simp),
+        String.intercalate_singleton]
+
+end Std.Iter

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

@@ -36,6 +36,9 @@ theorem beq_eq_false_iff {s t : Slice} : (s == t) = false ↔ s.copy ≠ t.copy
 theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) := by
   cases h : s == t <;> simp_all
 
+instance : EquivBEq String.Slice :=
+  equivBEq_of_iff_apply_eq copy (by simp)
+
 end BEq
 
 end String.Slice

src/Init/Data/String/Slice.lean

@@ -11,7 +11,7 @@ public import Init.Data.Ord.Basic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Subslice
-public import Init.Data.String.Iter
+public import Init.Data.String.Iter.Basic
 public import Init.Data.String.Iterate
 import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Consumers.Loop
@@ -84,10 +84,11 @@ instance : ToString String.Slice where
 theorem toStringToString_eq : ToString.toString = String.Slice.copy := (rfl)
 
 @[extern "lean_slice_hash"]
-opaque hash (s : @& Slice) : UInt64
+protected def hash (s : @& Slice) : UInt64 :=
+  String.hash s.copy
 
 instance : Hashable Slice where
-  hash := hash
+  hash := Slice.hash
 
 instance : LT Slice where
   lt x y := x.copy < y.copy

src/Init/Grind/Interactive.lean

@@ -107,6 +107,9 @@ syntax (name := showLocalThms) "show_local_thms" : grind
 -/
 syntax (name := showTerm) "show_term " grindSeq : grind
 
+/-- Shows the pending goals. -/
+syntax (name := showGoals) "show_goals" : grind
+
 declare_syntax_cat grind_ref (behavior := both)
 
 syntax:max anchor : grind_ref
@@ -315,5 +318,8 @@ Only available in `sym =>` mode.
 -/
 syntax (name := symSimp) "simp" (ppSpace colGt ident)? (" [" ident,* "]")? : grind
 
+/-- `exact e` closes the main goal if its target type matches that of `e`. -/
+macro "exact " e:term : grind => `(grind| tactic => exact $e:term)
+
 end Grind
 end Lean.Parser.Tactic

src/Init/Sym/Simp/SimprocDSL.lean

@@ -49,6 +49,14 @@ syntax (name := ground) "ground" : sym_simproc
 /-- Simplify telescope binders but not the final body. -/
 syntax (name := telescope) "telescope" : sym_simproc
 
+/-- Simplify control-flow expressions (`if-then-else`, `match`, `cond`, `dite`).
+Visits only conditions and discriminants. Intended as a `pre` simproc. -/
+syntax (name := control) "control" : sym_simproc
+
+/-- Simplify arrow telescopes (`p₁ → p₂ → ... → q`) without entering binders.
+Simplifies each `pᵢ` and `q` individually. Intended as a `pre` simproc. -/
+syntax (name := arrowTelescope) "arrow_telescope" : sym_simproc
+
 /-- Rewrite using a named theorem set. Optionally specify a discharger for conditional rewrites. -/
 syntax (name := rewriteSet) "rewrite" ident (" with " sym_discharger)? : sym_simproc
 

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -213,6 +213,8 @@ inductive OwnReason where
   | jpArgPropagation (jpFVar : FVarId)
   /-- Tail call preservation at a join point jump. -/
   | jpTailCallPreservation (jpFVar : FVarId)
+  /-- Annotated as an owned parameter (currently only triggerable through `@[export]`)-/
+  | ownedAnnotation
 
 def OwnReason.toString (reason : OwnReason) : CompilerM String := do
   PP.run do
@@ -229,6 +231,7 @@ def OwnReason.toString (reason : OwnReason) : CompilerM String := do
     | .tailCallPreservation funcName => return s!"tail call preservation of {funcName}"
     | .jpArgPropagation jpFVar => return s!"backward propagation from JP {← PP.ppFVar jpFVar}"
     | .jpTailCallPreservation jpFVar => return s!"JP tail call preservation {← PP.ppFVar jpFVar}"
+    | .ownedAnnotation => return s!"Annotated as owned"
 
 /--
 Determine whether an `OwnReason` is necessary for correctness (forced) or just an optimization
@@ -245,7 +248,7 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
-  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
+  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation .. | .ownedAnnotation
   | .forwardProjectionProp .. | .backwardProjectionProp .. => true
 
 /--
@@ -256,10 +259,19 @@ partial def infer (decls : Array (Decl .impure)) : CompilerM ParamMap := do
   return map.paramMap
 where
   go : InferM Unit := do
+    for (_, params) in (← get).paramMap.map do
+      for param in params do
+        if !param.borrow && param.type.isPossibleRef then
+          -- if the param already disqualifies as borrow now this is because of an annotation
+          ownFVar param.fvarId .ownedAnnotation
+    modify fun s => { s with modified := false }
+    loop
+
+  loop : InferM Unit := do
     step
     if (← get).modified then
       modify fun s => { s with modified := false }
-      go
+      loop
     else
       return ()
 

src/Lean/Elab/BuiltinTerm.lean

@@ -329,7 +329,8 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
     -- Normalize to instance normal form.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors)
+    let isMeta := (← read).isMetaSection
+    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/Command.lean

@@ -666,7 +666,8 @@ private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Contex
   return {
     macroStack             := ctx.macroStack
     sectionVars            := sectionVars
-    isNoncomputableSection := scope.isNoncomputable }
+    isNoncomputableSection := scope.isNoncomputable
+    isMetaSection          := scope.isMeta }
 
 /--
 Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.

src/Lean/Elab/Deriving/Basic.lean

@@ -220,10 +220,12 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
+            let isMeta := (← read).isMetaSection
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 normalizeInstance result.instVal result.instType
                   (logCompileErrors := false)  -- covered by noncomputable check below
+                  (isMeta := isMeta)
             else
               pure result.instVal
             let closure ← Closure.mkValueTypeClosure result.instType inst (zetaDelta := true)

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

@@ -25,10 +25,16 @@ structure Context extends Tactic.Context where
 
 open Meta.Grind (Goal)
 
-/-- Cache key for `Sym.simp` variant invocations: variant name + ordered extra theorem names. -/
+/-- An extra theorem passed to `simp` in `sym =>` mode. -/
+inductive ExtraTheorem where
+  | const (declName : Name)
+  | fvar  (fvarId : FVarId)
+  deriving BEq, Hashable
+
+/-- Cache key for `Sym.simp` variant invocations. -/
 structure SimpCacheKey where
   variant : Name
-  extras  : List Name
+  extras  : Array ExtraTheorem
   deriving BEq, Hashable
 
 structure Cache where

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

@@ -76,6 +76,10 @@ def evalGrindSeq : GrindTactic := fun stx =>
 @[builtin_grind_tactic skip] def evalSkip : GrindTactic := fun _ =>
   return ()
 
+@[builtin_grind_tactic showGoals] def evalShowGoals : GrindTactic := fun _ => do
+  let goals ← getUnsolvedGoalMVarIds
+  addRawTrace (goalsToMessageData goals)
+
 @[builtin_grind_tactic paren] def evalParen : GrindTactic := fun stx =>
   evalGrindTactic stx[1]
 

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

@@ -9,6 +9,8 @@ import Lean.Elab.Tactic.Grind.SimprocDSL
 import Init.Sym.Simp.SimprocDSL
 import Lean.Meta.Sym.Simp.EvalGround
 import Lean.Meta.Sym.Simp.Telescope
+import Lean.Meta.Sym.Simp.ControlFlow
+import Lean.Meta.Sym.Simp.Forall
 import Lean.Meta.Sym.Simp.Rewrite
 namespace Lean.Elab.Tactic.Grind
 open Meta Sym.Simp
@@ -23,6 +25,14 @@ def elabSimprocGround : SymSimprocElab := fun _ =>
 def elabSimprocTelescope : SymSimprocElab := fun _ =>
   return simpTelescope
 
+@[builtin_sym_simproc Lean.Parser.Sym.Simp.control]
+def elabSimprocControl : SymSimprocElab := fun _ =>
+  return simpControl
+
+@[builtin_sym_simproc Lean.Parser.Sym.Simp.arrowTelescope]
+def elabSimprocArrowTelescope : SymSimprocElab := fun _ =>
+  return simpArrowTelescope
+
 @[builtin_sym_simproc self]
 def elabSimprocSelf : SymSimprocElab := fun _ =>
   return simp

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

@@ -153,39 +153,54 @@ def elabOptSimproc (stx? : Option Syntax) : GrindTacticM Simproc := do
   let some stx := stx? | return trivialSimproc
   elabSymSimproc stx
 
-def addExtraTheorems (post : Simproc) (extraNames : Array Name) : GrindTacticM Simproc := do
-  if extraNames.isEmpty then return post
+def resolveExtraTheorems (ids? :  Option (Array (TSyntax `ident))) : GrindTacticM (Array ExtraTheorem × Array Theorem) := do
+  let some ids := ids? | return (#[], #[])
+  let mut extras := #[]
+  let mut thms := #[]
+  let lctx ← getLCtx
+  for id in ids do
+    if let some decl := lctx.findFromUserName? id.getId then
+      extras := extras.push <| .fvar decl.fvarId
+      thms := thms.push (← mkTheoremFromExpr decl.toExpr)
+    else
+      let declName ← realizeGlobalConstNoOverload id
+      extras := extras.push <| .const declName
+      thms := thms.push (← mkTheoremFromDecl declName)
+  return (extras, thms)
+
+def addExtraTheorems (post : Simproc) (extraThms : Array Theorem) : GrindTacticM Simproc := do
+  if extraThms.isEmpty then return post
   let mut thms : Theorems := {}
-  for name in extraNames do
-    thms := thms.insert (← mkTheoremFromDecl name)
+  for thm in extraThms do
+    thms := thms.insert thm
   return post >> thms.rewrite
 
-def mkDefaultMethods (extraNames : Array Name) : GrindTacticM Sym.Simp.Methods := do
+def mkDefaultMethods (extraThms : Array Theorem) : GrindTacticM Sym.Simp.Methods := do
   let thms ← getSymSimpTheorems
   let pre := simpControl >> simpArrowTelescope
-  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraNames
+  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraThms
   return { pre, post }
 
-def elabVariant (variantName : Name) (extraNames : Array Name) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
+def elabVariant (variantName : Name) (extraThms : Array Theorem) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
   if variantName.isAnonymous then
-    return (← mkDefaultMethods extraNames, {})
+    return (← mkDefaultMethods extraThms, {})
   let some v := getSymSimpVariant? (← getEnv) variantName
     | throwError "unknown Sym.simp variant `{variantName}`"
   let pre ← elabOptSimproc v.pre?
-  let post ← addExtraTheorems (← elabOptSimproc v.post?) extraNames
+  let post ← addExtraTheorems (← elabOptSimproc v.post?) extraThms
   return ({ pre, post}, v.config)
 
-@[builtin_grind_tactic Parser.Tactic.Grind.symSimp] def evalSymSimp : GrindTactic := fun stx => do
+@[builtin_grind_tactic Parser.Tactic.Grind.symSimp] def evalSymSimp : GrindTactic := fun stx => withMainContext do
   ensureSym
   let `(grind| simp $[$variantId?]? $[[ $[$extraIds],* ]]?) := stx | throwUnsupportedSyntax
   -- Resolve variant
   let variantName := variantId?.map (·.getId) |>.getD .anonymous
-  -- Compose extra theorems into post
-  let extraNames ← (extraIds.getD #[]).mapM fun id => realizeGlobalConstNoOverload id
+  -- Resolve extra theorems (local hypotheses first, then global constants)
+  let (extras, thms) ← resolveExtraTheorems extraIds
   -- Cache lookup/creation
-  let cacheKey : SimpCacheKey := { variant := variantName, extras := extraNames.toList }
+  let cacheKey : SimpCacheKey := { variant := variantName, extras }
   let simpState := (← get).cache.simpState[cacheKey]?.getD {}
-  let (methods, config) ← elabVariant variantName extraNames
+  let (methods, config) ← elabVariant variantName thms
   let goal ← getMainGoal
   let (simpResult, simpState) ← liftGrindM <| goal.withContext do
     Sym.Simp.SimpM.run (Sym.Simp.simp (← goal.mvarId.getType)) methods config simpState

src/Lean/Elab/Term/TermElabM.lean

@@ -309,6 +309,8 @@ structure Context where
   heedElabAsElim     : Bool            := true
   /-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
   isNoncomputableSection : Bool        := false
+  /-- `true` when inside a `meta section`. -/
+  isMetaSection : Bool                 := false
   /-- When `true` we skip TC failures. We use this option when processing patterns. -/
   ignoreTCFailures : Bool := false
   /-- `true` when elaborating patterns. It affects how we elaborate named holes. -/

src/Lean/Meta/InstanceNormalForm.lean

@@ -99,7 +99,7 @@ Normalize an instance value to "instance normal form".
 See the module docstring for the full algorithm specification.
 -/
 partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
-    (logCompileErrors : Bool := true) : MetaM Expr := withTransparency .instances do
+    (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
   withTraceNode `Meta.instanceNormalForm
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
@@ -124,9 +124,11 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             return inst
           else
             let name ← mkAuxDeclName
-            let wrapped ← mkAuxDefinition name expectedType inst (compile := compile)
-              (logCompileErrors := logCompileErrors)
+            let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
             setReducibilityStatus name .implicitReducible
+            if isMeta then modifyEnv (markMeta · name)
+            if compile then
+              compileDecls (logErrors := logCompileErrors) #[name]
             enableRealizationsForConst name
             return wrapped
         else
@@ -169,7 +171,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             catch _ => pure ()
 
           mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
-            (logCompileErrors := logCompileErrors))
+            (logCompileErrors := logCompileErrors) (isMeta := isMeta))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.
           if backward.inferInstanceAs.wrap.data.get (← getOptions) then
@@ -180,6 +182,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
               let name ← mkAuxDeclName
               mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
               setInlineAttribute name
+              if isMeta then modifyEnv (markMeta · name)
               if compile then
                 compileDecls (logErrors := logCompileErrors) #[name]
               enableRealizationsForConst name

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

@@ -9,6 +9,7 @@ public import Lean.Meta.Sym.Simp.Simproc
 public import Lean.Meta.Sym.Simp.Theorems
 public import Lean.Meta.Sym.Simp.App
 public import Lean.Meta.Sym.Simp.Discharger
+import Lean.Meta.ACLt
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.InstantiateMVarsS
 import Init.Data.Range.Polymorphic.Iterators
@@ -71,10 +72,16 @@ public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischar
     let expr  ← instantiateRevBetaS rhs args.toArray
     if isSameExpr e expr then
       return mkRflResultCD isCD
+    else if !(← checkPerm thm.perm e expr) then
+      return mkRflResultCD isCD
     else
       return .step expr proof (contextDependent := isCD)
   else
     return .rfl
+where
+  checkPerm (perm : Bool) (e result : Expr) : MetaM Bool := do
+    if !perm then return true
+    acLt result e
 
 public def Theorems.rewrite (thms : Theorems) (d : Discharger := dischargeNone) : Simproc := fun e => do
   -- Track `cd` across all attempted theorems. If theorem A fails with cd=true

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

@@ -10,6 +10,7 @@ public import Lean.Meta.DiscrTree
 import Lean.Meta.Sym.Simp.DiscrTree
 import Lean.Meta.AppBuilder
 import Lean.ExtraModUses
+import Init.Omega
 public section
 namespace Lean.Meta.Sym.Simp
 
@@ -26,6 +27,10 @@ structure Theorem where
   pattern : Pattern
   /-- Right-hand side of the equation. -/
   rhs     : Expr
+  /-- If `true`, the theorem is a permutation rule (e.g., `x + y = y + x`).
+  Rewriting is only applied when the result is strictly less than the input
+  (using `acLt`), preventing infinite loops. -/
+  perm    : Bool := false
   deriving Inhabited
 
 instance : BEq Theorem where
@@ -45,6 +50,49 @@ def Theorems.getMatch (thms : Theorems) (e : Expr) : Array Theorem :=
 def Theorems.getMatchWithExtra (thms : Theorems) (e : Expr) : Array (Theorem × Nat) :=
   Sym.getMatchWithExtra thms.thms e
 
+/--
+Check whether `lhs` and `rhs` (with `numVars` pattern variables represented as `.bvar` indices
+`≥ 0` before any binder entry) are permutations of each other — same structure with only
+pattern variable indices rearranged via a consistent bijection.
+
+Bvars with index `< offset` are "local" (introduced by binders inside the pattern) and must
+match exactly. Bvars with index `≥ offset` are pattern variables and may be permuted,
+but the mapping must be a bijection.
+
+Simplified compared to `Meta.simp`'s `isPerm`:
+- Uses de Bruijn indices instead of metavariables
+- No `.proj` (folded into applications) or `.letE` (zeta-expanded) cases
+-/
+private abbrev IsPermM := ReaderT Nat $ StateT (Array (Option Nat)) $ Except Unit
+
+private partial def isPermAux (a b : Expr) : IsPermM Unit := do
+  match a, b with
+  | .bvar i, .bvar j =>
+    let offset ← read
+    if i < offset && j < offset then
+      unless i == j do throw ()
+    else if i >= offset && j >= offset then
+      let pi := i - offset
+      let pj := j - offset
+      let fwd ← get
+      if h : pi >= fwd.size then throw () else
+      match fwd[pi] with
+      | none =>
+        -- Check injectivity: pj must not already be a target of another mapping
+        if fwd.contains (some pj) then throw ()
+        set (fwd.set pi (some pj))
+      | some pj' => unless pj == pj' do throw ()
+    else throw ()
+  | .app f₁ a₁, .app f₂ a₂ => isPermAux f₁ f₂; isPermAux a₁ a₂
+  | .mdata _ s, t => isPermAux s t
+  | s, .mdata _ t => isPermAux s t
+  | .forallE _ d₁ b₁ _, .forallE _ d₂ b₂ _ => isPermAux d₁ d₂; withReader (· + 1) (isPermAux b₁ b₂)
+  | .lam _ d₁ b₁ _, .lam _ d₂ b₂ _ => isPermAux d₁ d₂; withReader (· + 1) (isPermAux b₁ b₂)
+  | s, t => unless s == t do throw ()
+
+def isPerm (numVars : Nat) (lhs rhs : Expr) : Bool :=
+  ((isPermAux lhs rhs).run 0 |>.run (Array.replicate numVars none)) matches .ok _
+
 /-- Describes how a theorem's conclusion was adapted to an equality for use in `Sym.simp`. -/
 private inductive EqAdaptation where
   /-- Already an equality `lhs = rhs`. Proof is used as-is. -/
@@ -99,13 +147,15 @@ where
 def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
   let (pattern, (rhs, adaptation)) ← mkPatternFromDeclWithKey declName selectEqKey
   let expr ← wrapProof pattern.varTypes.size (mkConst declName) adaptation
-  return { expr, pattern, rhs }
+  let perm := isPerm pattern.varTypes.size pattern.pattern rhs
+  return { expr, pattern, rhs, perm }
 
 /-- Create a `Theorem` from a proof expression. Handles equalities, `¬`, `↔`, and propositions. -/
 def mkTheoremFromExpr (e : Expr) : MetaM Theorem := do
   let (pattern, (rhs, adaptation)) ← mkPatternFromExprWithKey e [] selectEqKey
   let expr ← wrapProof pattern.varTypes.size e adaptation
-  return { expr, pattern, rhs }
+  let perm := isPerm pattern.varTypes.size pattern.pattern rhs
+  return { expr, pattern, rhs, perm }
 
 /--
 Environment extension storing a set of `Sym.Simp` theorems.

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -52,6 +52,12 @@ builtin_dsimproc [simp, seval] reduceSingleton (String.singleton _) := fun e =>
   let some c ← Char.fromExpr? e.appArg! | return .continue
   return .done <| toExpr (String.singleton c)
 
+builtin_dsimproc_decl reduceToSingleton ((_ : String)) := fun e => do
+  let some s ← fromExpr? e | return .continue
+  let l := s.toList
+  let [c] := l | return .continue
+  return .done <| mkApp (mkConst ``String.singleton) (toExpr c)
+
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue

src/Std/Data/String/ToInt.lean

@@ -98,18 +98,34 @@ end Slice
 public theorem isInt_toSlice {s : String} : s.toSlice.isInt = s.isInt :=
   (rfl)
 
+@[simp]
+public theorem isInt_comp_toSlice : String.Slice.isInt ∘ String.toSlice = String.isInt := by
+  ext; simp
+
 @[simp]
 public theorem toInt?_toSlice {s : String} : s.toSlice.toInt? = s.toInt? :=
   (rfl)
 
+@[simp]
+public theorem toInt?_comp_toSlice : String.Slice.toInt? ∘ String.toSlice = String.toInt? := by
+  ext; simp
+
 @[simp]
 public theorem Slice.isInt_copy {s : Slice} : s.copy.isInt = s.isInt := by
   simpa [← isInt_toSlice] using Slice.isInt_congr (by simp)
 
+@[simp]
+public theorem Slice.isInt_comp_copy : String.isInt ∘ String.Slice.copy = String.Slice.isInt := by
+  ext; simp
+
 @[simp]
 public theorem Slice.toInt?_copy {s : Slice} : s.copy.toInt? = s.toInt? := by
   simpa [← isInt_toSlice] using Slice.toInt?_congr (by simp)
 
+@[simp]
+public theorem Slice.toInt?_comp_copy : String.toInt? ∘ String.Slice.copy = String.Slice.toInt? := by
+  ext; simp
+
 public theorem toInt?_eq_some_iff {s : String} {a : Int} :
     s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = (b : Int)) ∨ ∃ t, s = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -(b : Int) := by
   simp [← toInt?_toSlice, Slice.toInt?_eq_some_iff]

src/Std/Data/String/ToNat.lean

@@ -221,18 +221,34 @@ namespace String
 public theorem isNat_toSlice {s : String} : s.toSlice.isNat = s.isNat :=
   (rfl)
 
+@[simp]
+public theorem isNat_comp_toSlice : String.Slice.isNat ∘ String.toSlice = String.isNat := by
+  ext; simp
+
 @[simp]
 public theorem toNat?_toSlice {s : String} : s.toSlice.toNat? = s.toNat? :=
   (rfl)
 
+@[simp]
+public theorem toNat?_comp_toSlice : String.Slice.toNat? ∘ String.toSlice = String.toNat? := by
+  ext; simp
+
 @[simp]
 public theorem Slice.isNat_copy {s : Slice} : s.copy.isNat = s.isNat := by
   simpa [← isNat_toSlice] using Slice.isNat_congr (by simp)
 
+@[simp]
+public theorem Slice.isNat_comp_copy : String.isNat ∘ String.Slice.copy = String.Slice.isNat := by
+  ext; simp
+
 @[simp]
 public theorem Slice.toNat?_copy {s : Slice} : s.copy.toNat? = s.toNat? := by
   simpa [← isNat_toSlice] using Slice.toNat?_congr (by simp)
 
+@[simp]
+public theorem Slice.toNat?_comp_copy : String.toNat? ∘ String.Slice.copy = String.Slice.toNat? := by
+  ext; simp
+
 public theorem isNat_iff {s : String} :
     s.isNat = true ↔
       s ≠ "" ∧

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

@@ -14,6 +14,7 @@ public import Std.Internal.Http.Data.Status
 public import Std.Internal.Http.Data.Chunk
 public import Std.Internal.Http.Data.Headers
 public import Std.Internal.Http.Data.URI
+public import Std.Internal.Http.Data.Body
 
 /-!
 # HTTP Data Types

src/Std/Internal/Http/Data/Body.lean

@@ -0,0 +1,24 @@
+/-
+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.Body.Basic
+public import Std.Internal.Http.Data.Body.Length
+public import Std.Internal.Http.Data.Body.Any
+public import Std.Internal.Http.Data.Body.Stream
+public import Std.Internal.Http.Data.Body.Empty
+public import Std.Internal.Http.Data.Body.Full
+
+public section
+
+/-!
+# Body
+
+This module re-exports all HTTP body types: `Body.Empty`, `Body.Full`, `Body.Stream`,
+`Body.Any`, and `Body.Length`, along with the `Http.Body` typeclass and conversion
+utilities (`ToByteArray`, `FromByteArray`).
+-/

src/Std/Internal/Http/Data/Body/Any.lean

@@ -0,0 +1,83 @@
+/-
+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.Body.Basic
+
+public section
+
+/-!
+# Body.Any
+
+A type-erased body backed by closures. Implements `Http.Body` and can be constructed from any
+type that also implements `Http.Body`. Used as the default handler response body type.
+-/
+
+namespace Std.Http.Body
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+A type-erased body handle. Operations are stored as closures, making it open to any body type
+that implements `Http.Body`.
+-/
+structure Any where
+
+  /--
+  Receives the next body chunk. Returns `none` at end-of-stream.
+  -/
+  recv : Async (Option Chunk)
+
+  /--
+  Closes the body stream.
+  -/
+  close : Async Unit
+
+  /--
+  Returns `true` when the body stream is closed.
+  -/
+  isClosed : Async Bool
+
+  /--
+  Selector that resolves when a chunk is available or EOF is reached.
+  -/
+  recvSelector : Selector (Option Chunk)
+
+  /--
+  Returns the declared size.
+  -/
+  getKnownSize : Async (Option Body.Length)
+
+  /--
+  Sets the size of the body.
+  -/
+  setKnownSize : Option Body.Length → Async Unit
+namespace Any
+
+/--
+Erases a body of any `Http.Body` instance into a `Body.Any`.
+-/
+def ofBody [Http.Body α] (body : α) : Any where
+  recv := Http.Body.recv body
+  close := Http.Body.close body
+  isClosed := Http.Body.isClosed body
+  recvSelector := Http.Body.recvSelector body
+  getKnownSize := Http.Body.getKnownSize body
+  setKnownSize := Http.Body.setKnownSize body
+
+end Any
+
+instance : Http.Body Any where
+  recv := Any.recv
+  close := Any.close
+  isClosed := Any.isClosed
+  recvSelector := Any.recvSelector
+  getKnownSize := Any.getKnownSize
+  setKnownSize := Any.setKnownSize
+
+end Std.Http.Body

src/Std/Internal/Http/Data/Body/Basic.lean

@@ -0,0 +1,102 @@
+/-
+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.ContextAsync
+public import Std.Internal.Http.Data.Chunk
+public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.Body.Length
+
+public section
+
+/-!
+# Body.Basic
+
+This module defines the `Body` typeclass for HTTP body streams, and shared conversion types
+`ToByteArray` and `FromByteArray` used for encoding and decoding body content.
+-/
+
+namespace Std.Http
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+Typeclass for values that can be read as HTTP body streams.
+-/
+class Body (α : Type) where
+  /--
+  Receives the next body chunk. Returns `none` at end-of-stream.
+  -/
+  recv : α → Async (Option Chunk)
+
+  /--
+  Closes the body stream.
+  -/
+  close : α → Async Unit
+
+  /--
+  Returns `true` when the body stream is closed.
+  -/
+  isClosed : α → Async Bool
+
+  /--
+  Selector that resolves when a chunk is available or EOF is reached.
+  -/
+  recvSelector : α → Selector (Option Chunk)
+
+  /--
+  Gets the declared size of the body.
+  -/
+  getKnownSize : α → Async (Option Body.Length)
+
+  /--
+  Sets the declared size of a body.
+  -/
+  setKnownSize : α → Option Body.Length → Async Unit
+end Std.Http
+
+namespace Std.Http.Body
+
+/--
+Typeclass for types that can be converted to a `ByteArray`.
+-/
+class ToByteArray (α : Type) where
+
+  /--
+  Transforms into a `ByteArray`.
+  -/
+  toByteArray : α → ByteArray
+
+instance : ToByteArray ByteArray where
+  toByteArray := id
+
+instance : ToByteArray String where
+  toByteArray := String.toUTF8
+
+/--
+Typeclass for types that can be decoded from a `ByteArray`. The conversion may fail with an error
+message if the bytes are not valid for the target type.
+-/
+class FromByteArray (α : Type) where
+
+  /--
+  Attempts to decode a `ByteArray` into the target type, returning an error message on failure.
+  -/
+  fromByteArray : ByteArray → Except String α
+
+instance : FromByteArray ByteArray where
+  fromByteArray := .ok
+
+instance : FromByteArray String where
+  fromByteArray bs :=
+    match String.fromUTF8? bs with
+    | some s => .ok s
+    | none => .error "invalid UTF-8 encoding"
+
+end Std.Http.Body

src/Std/Internal/Http/Data/Body/Empty.lean

@@ -0,0 +1,116 @@
+/-
+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.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Body.Any
+
+public section
+
+/-!
+# Body.Empty
+
+Represents an always-empty, already-closed body handle.
+-/
+
+namespace Std.Http.Body
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+An empty body handle.
+-/
+structure Empty where
+deriving Inhabited, BEq
+
+namespace Empty
+
+/--
+Receives from an empty body, always returning end-of-stream.
+-/
+@[inline]
+def recv (_ : Empty) : Async (Option Chunk) :=
+  pure none
+
+/--
+Closes an empty body (no-op).
+-/
+@[inline]
+def close (_ : Empty) : Async Unit :=
+  pure ()
+
+/--
+Empty bodies are always closed for reading.
+-/
+@[inline]
+def isClosed (_ : Empty) : Async Bool :=
+  pure true
+
+/--
+Selector that immediately resolves with end-of-stream for an empty body.
+-/
+@[inline]
+def recvSelector (_ : Empty) : Selector (Option Chunk) where
+  tryFn := pure (some none)
+  registerFn waiter := do
+    let lose := pure ()
+    let win promise := do
+      promise.resolve (.ok none)
+    waiter.race lose win
+  unregisterFn := pure ()
+
+end Empty
+
+instance : Http.Body Empty where
+  recv := Empty.recv
+  close := Empty.close
+  isClosed := Empty.isClosed
+  recvSelector := Empty.recvSelector
+  getKnownSize _ := pure (some <| .fixed 0)
+  setKnownSize _ _ := pure ()
+
+
+instance : Coe Empty Any := ⟨Any.ofBody⟩
+
+instance : Coe (Response Empty) (Response Any) where
+  coe f := { f with }
+
+instance : Coe (ContextAsync (Response Empty)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+instance : Coe (Async (Response Empty)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+end Body
+
+namespace Request.Builder
+open Internal.IO.Async
+
+/--
+Builds a request with no body.
+-/
+def empty (builder : Builder) : Async (Request Body.Empty) :=
+  pure <| builder.body {}
+
+end Request.Builder
+
+namespace Response.Builder
+open Internal.IO.Async
+
+/--
+Builds a response with no body.
+-/
+def empty (builder : Builder) : Async (Response Body.Empty) :=
+  pure <| builder.body {}
+
+end Response.Builder

src/Std/Internal/Http/Data/Body/Full.lean

@@ -0,0 +1,232 @@
+/-
+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.Sync
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Body.Any
+public import Init.Data.ByteArray
+
+public section
+
+/-!
+# Body.Full
+
+A body backed by a fixed `ByteArray` held in a `Mutex`.
+
+The byte array is consumed at most once: the first call to `recv` atomically takes the data
+and returns it as a single chunk; subsequent calls return `none` (end-of-stream).
+Closing the body discards any unconsumed data.
+-/
+
+namespace Std.Http.Body
+open Std Internal IO Async
+
+set_option linter.all true
+
+/--
+A body backed by a fixed, mutex-protected `ByteArray`.
+
+The data is consumed on the first read. Once consumed (or explicitly closed), the body
+behaves as a closed, empty channel.
+-/
+structure Full where
+  private mk ::
+  private state : Mutex (Option ByteArray)
+deriving Nonempty
+
+namespace Full
+
+private def takeChunk : AtomicT (Option ByteArray) Async (Option Chunk) := do
+  match ← get with
+  | none =>
+    pure none
+  | some data =>
+    set (none : Option ByteArray)
+    if data.isEmpty then
+      pure none
+    else
+      pure (some (Chunk.ofByteArray data))
+
+/--
+Creates a `Full` body from a `ByteArray`.
+-/
+def ofByteArray (data : ByteArray) : Async Full := do
+  let state ← Mutex.new (some data)
+  return { state }
+
+/--
+Creates a `Full` body from a `String`.
+-/
+def ofString (data : String) : Async Full := do
+  let state ← Mutex.new (some data.toUTF8)
+  return { state }
+
+/--
+Receives the body data. Returns the full byte array on the first call as a single chunk,
+then `none` on all subsequent calls.
+-/
+def recv (full : Full) : Async (Option Chunk) :=
+  full.state.atomically do
+    takeChunk
+
+/--
+Closes the body, discarding any unconsumed data.
+-/
+def close (full : Full) : Async Unit :=
+  full.state.atomically do
+    set (none : Option ByteArray)
+
+/--
+Returns `true` when the data has been consumed or the body has been closed.
+-/
+def isClosed (full : Full) : Async Bool :=
+  full.state.atomically do
+    return (← get).isNone
+
+/--
+Returns the known size of the remaining data.
+Returns `some (.fixed n)` with the current byte count, or `some (.fixed 0)` if the body has
+already been consumed or closed.
+-/
+def getKnownSize (full : Full) : Async (Option Body.Length) :=
+  full.state.atomically do
+    match ← get with
+    | none => pure (some (.fixed 0))
+    | some data => pure (some (.fixed data.size))
+
+/--
+Selector that immediately resolves to the remaining chunk (or EOF).
+-/
+def recvSelector (full : Full) : Selector (Option Chunk) where
+  tryFn := do
+    let chunk ← full.state.atomically do
+      takeChunk
+    pure (some chunk)
+
+  registerFn waiter := do
+    full.state.atomically do
+      let lose := pure ()
+
+      let win promise := do
+        let chunk ← takeChunk
+        promise.resolve (.ok chunk)
+
+      waiter.race lose win
+
+  unregisterFn := pure ()
+
+end Full
+
+instance : Http.Body Full where
+  recv := Full.recv
+  close := Full.close
+  isClosed := Full.isClosed
+  recvSelector := Full.recvSelector
+  getKnownSize := Full.getKnownSize
+  setKnownSize _ _ := pure ()
+
+instance : Coe Full Any := ⟨Any.ofBody⟩
+
+instance : Coe (Response Full) (Response Any) where
+  coe f := { f with }
+
+instance : Coe (ContextAsync (Response Full)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+instance : Coe (Async (Response Full)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+end Body
+
+namespace Request.Builder
+
+open Internal.IO.Async
+
+/--
+Builds a request body from raw bytes without setting any headers.
+Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
+-/
+def fromBytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) := do
+  return builder.body (← Body.Full.ofByteArray content)
+
+/--
+Builds a request with a binary body.
+Sets `Content-Type: application/octet-stream`.
+Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
+-/
+def bytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
+
+/--
+Builds a request with a text body.
+Sets `Content-Type: text/plain; charset=utf-8`.
+-/
+def text (builder : Builder) (content : String) : Async (Request Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
+
+/--
+Builds a request with a JSON body.
+Sets `Content-Type: application/json`.
+-/
+def json (builder : Builder) (content : String) : Async (Request Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
+
+/--
+Builds a request with an HTML body.
+Sets `Content-Type: text/html; charset=utf-8`.
+-/
+def html (builder : Builder) (content : String) : Async (Request Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
+
+end Request.Builder
+
+namespace Response.Builder
+open Internal.IO.Async
+
+/--
+Builds a response body from raw bytes without setting any headers.
+Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
+-/
+def fromBytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) := do
+  return builder.body (← Body.Full.ofByteArray content)
+
+/--
+Builds a response with a binary body.
+Sets `Content-Type: application/octet-stream`.
+Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
+-/
+def bytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
+
+/--
+Builds a response with a text body.
+Sets `Content-Type: text/plain; charset=utf-8`.
+-/
+def text (builder : Builder) (content : String) : Async (Response Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
+
+/--
+Builds a response with a JSON body.
+Sets `Content-Type: application/json`.
+-/
+def json (builder : Builder) (content : String) : Async (Response Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
+
+/--
+Builds a response with an HTML body.
+Sets `Content-Type: text/html; charset=utf-8`.
+-/
+def html (builder : Builder) (content : String) : Async (Response Body.Full) :=
+  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
+
+end Response.Builder

src/Std/Internal/Http/Data/Body/Length.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 Init.Data.Repr
+
+public section
+
+/-!
+# Body.Length
+
+This module defines the `Length` type, that represents the Content-Length or Transfer-Encoding
+of an HTTP request or response.
+-/
+
+namespace Std.Http.Body
+
+set_option linter.all true
+
+/--
+Size of the body of a response or request.
+-/
+inductive Length
+  /--
+  Indicates that the HTTP message body uses **chunked transfer encoding**.
+  -/
+  | chunked
+
+  /--
+  Indicates that the HTTP message body has a **fixed, known length**, as specified by the
+  `Content-Length` header.
+  -/
+  | fixed (n : Nat)
+deriving Repr, BEq
+
+namespace Length
+
+/--
+Checks if the `Length` is chunked.
+-/
+@[inline]
+def isChunked : Length → Bool
+  | .chunked => true
+  | _ => false
+
+/--
+Checks if the `Length` is a fixed size.
+-/
+@[inline]
+def isFixed : Length → Bool
+  | .fixed _ => true
+  | _ => false
+
+end Length
+
+end Std.Http.Body

src/Std/Internal/Http/Data/Body/Stream.lean

@@ -0,0 +1,650 @@
+/-
+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.Sync
+public import Std.Internal.Async
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Chunk
+public import Std.Internal.Http.Data.Body.Basic
+public import Std.Internal.Http.Data.Body.Any
+public import Init.Data.ByteArray
+
+public section
+
+/-!
+# Body.Stream
+
+This module defines a zero-buffer rendezvous body channel (`Body.Stream`) that supports
+both sending and receiving chunks.
+
+There is no queue and no capacity. A send waits for a receiver and a receive waits for a sender.
+At most one blocked producer and one blocked consumer are supported.
+-/
+
+namespace Std.Http
+
+namespace Body
+
+open Std Internal IO Async
+
+set_option linter.all true
+
+namespace Channel
+
+open Internal.IO.Async in
+private inductive Consumer where
+  | normal (promise : IO.Promise (Option Chunk))
+  | select (finished : Waiter (Option Chunk))
+
+private def Consumer.resolve (c : Consumer) (x : Option Chunk) : BaseIO Bool := do
+  match c with
+  | .normal promise =>
+    promise.resolve x
+    return true
+  | .select waiter =>
+    let lose := return false
+    let win promise := do
+      promise.resolve (.ok x)
+      return true
+    waiter.race lose win
+
+private structure Producer where
+  chunk : Chunk
+
+  /--
+  Resolved with `true` when consumed by a receiver, `false` when the channel closes.
+  -/
+  done : IO.Promise Bool
+
+open Internal.IO.Async in
+private def resolveInterestWaiter (waiter : Waiter Bool) (x : Bool) : BaseIO Bool := do
+  let lose := return false
+  let win promise := do
+    promise.resolve (.ok x)
+    return true
+  waiter.race lose win
+
+private structure State where
+  /--
+  A single blocked producer waiting for a receiver.
+  -/
+  pendingProducer : Option Producer
+
+  /--
+  A single blocked consumer waiting for a producer.
+  -/
+  pendingConsumer : Option Consumer
+
+  /--
+  A waiter for `Stream.interestSelector`.
+  -/
+  interestWaiter : Option (Internal.IO.Async.Waiter Bool)
+
+  /--
+  Whether the channel is closed.
+  -/
+  closed : Bool
+
+  /--
+  Known size of the stream if available.
+  -/
+  knownSize : Option Body.Length
+
+  /--
+  Buffered partial chunk data accumulated from `Stream.send ... (incomplete := true)`.
+  These partial pieces are collapsed and emitted as a single chunk on the next complete send.
+  -/
+  pendingIncompleteChunk : Option Chunk := none
+deriving Nonempty
+
+end Channel
+
+/--
+A zero-buffer rendezvous body channel that supports both sending and receiving chunks.
+-/
+structure Stream where
+  private mk ::
+  private state : Mutex Channel.State
+deriving Nonempty, TypeName
+
+/--
+Creates a rendezvous body stream.
+-/
+def mkStream : Async Stream := do
+  let state ← Mutex.new {
+    pendingProducer := none
+    pendingConsumer := none
+    interestWaiter := none
+    closed := false
+    knownSize := none
+  }
+  return { state }
+
+namespace Channel
+
+private def decreaseKnownSize (knownSize : Option Body.Length) (chunk : Chunk) : Option Body.Length :=
+  match knownSize with
+  | some (.fixed res) => some (Body.Length.fixed (res - chunk.data.size))
+  | _ => knownSize
+
+private def pruneFinishedWaiters [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
+    AtomicT State m Unit := do
+  let st ← get
+
+  let pendingConsumer ←
+    match st.pendingConsumer with
+    | some (.select waiter) =>
+      if ← waiter.checkFinished then
+        pure none
+      else
+        pure st.pendingConsumer
+    | _ =>
+      pure st.pendingConsumer
+
+  let interestWaiter ←
+    match st.interestWaiter with
+    | some waiter =>
+      if ← waiter.checkFinished then
+        pure none
+      else
+        pure st.interestWaiter
+    | none =>
+      pure none
+
+  set { st with pendingConsumer, interestWaiter }
+
+private def signalInterest [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
+    AtomicT State m Unit := do
+  let st ← get
+  if let some waiter := st.interestWaiter then
+    discard <| resolveInterestWaiter waiter true
+    set { st with interestWaiter := none }
+
+private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
+    AtomicT State m Bool := do
+  let st ← get
+  return st.pendingProducer.isSome || st.closed
+
+private def hasInterest' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
+    AtomicT State m Bool := do
+  let st ← get
+  return st.pendingConsumer.isSome
+
+private def tryRecv' [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
+    AtomicT State m (Option Chunk) := do
+  let st ← get
+  if let some producer := st.pendingProducer then
+    set {
+      st with
+      pendingProducer := none
+      knownSize := decreaseKnownSize st.knownSize producer.chunk
+    }
+    discard <| producer.done.resolve true
+    return some producer.chunk
+  else
+    return none
+
+private def close' [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
+    AtomicT State m Unit := do
+  let st ← get
+  if st.closed then
+    return ()
+
+  if let some consumer := st.pendingConsumer then
+    discard <| consumer.resolve none
+
+  if let some waiter := st.interestWaiter then
+    discard <| resolveInterestWaiter waiter false
+
+  if let some producer := st.pendingProducer then
+    discard <| producer.done.resolve false
+
+  set {
+    st with
+    pendingProducer := none
+    pendingConsumer := none
+    interestWaiter := none
+    pendingIncompleteChunk := none
+    closed := true
+  }
+
+end Channel
+
+namespace Stream
+
+/--
+Attempts to receive a chunk from the channel without blocking.
+Returns `some chunk` only when a producer is already waiting.
+-/
+def tryRecv (stream : Stream) : Async (Option Chunk) :=
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    Channel.tryRecv'
+
+private def recv' (stream : Stream) : BaseIO (AsyncTask (Option Chunk)) := do
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+
+    if let some chunk ← Channel.tryRecv' then
+      return AsyncTask.pure (some chunk)
+
+    let st ← get
+    if st.closed then
+      return AsyncTask.pure none
+
+    if st.pendingConsumer.isSome then
+      return Task.pure (.error (IO.Error.userError "only one blocked consumer is allowed"))
+
+    let promise ← IO.Promise.new
+    set { st with pendingConsumer := some (.normal promise) }
+    Channel.signalInterest
+    return promise.result?.map (sync := true) fun
+      | none => .error (IO.Error.userError "the promise linked to the consumer was dropped")
+      | some res => .ok res
+
+/--
+Receives a chunk from the channel. Blocks until a producer sends one.
+Returns `none` if the channel is closed and no producer is waiting.
+-/
+def recv (stream : Stream) : Async (Option Chunk) := do
+  Async.ofAsyncTask (← recv' stream)
+
+/--
+Closes the channel.
+-/
+def close (stream : Stream) : Async Unit :=
+  stream.state.atomically do
+    Channel.close'
+
+/--
+Checks whether the channel is closed.
+-/
+@[always_inline, inline]
+def isClosed (stream : Stream) : Async Bool :=
+  stream.state.atomically do
+    return (← get).closed
+
+/--
+Gets the known size if available.
+-/
+@[always_inline, inline]
+def getKnownSize (stream : Stream) : Async (Option Body.Length) :=
+  stream.state.atomically do
+    return (← get).knownSize
+
+/--
+Sets known size metadata.
+-/
+@[always_inline, inline]
+def setKnownSize (stream : Stream) (size : Option Body.Length) : Async Unit :=
+  stream.state.atomically do
+    modify fun st => { st with knownSize := size }
+
+open Internal.IO.Async in
+
+/--
+Creates a selector that resolves when a producer is waiting (or the channel closes).
+-/
+def recvSelector (stream : Stream) : Selector (Option Chunk) where
+  tryFn := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+      if ← Channel.recvReady' then
+        return some (← Channel.tryRecv')
+      else
+        return none
+
+  registerFn waiter := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+      if ← Channel.recvReady' then
+        let lose := return ()
+        let win promise := do
+          promise.resolve (.ok (← Channel.tryRecv'))
+        waiter.race lose win
+      else
+        let st ← get
+        if st.pendingConsumer.isSome then
+          throw (.userError "only one blocked consumer is allowed")
+
+        set { st with pendingConsumer := some (.select waiter) }
+        Channel.signalInterest
+
+  unregisterFn := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+
+/--
+Iterates over chunks until the channel closes.
+-/
+@[inline]
+protected partial def forIn
+    {β : Type} (stream : Stream) (acc : β)
+    (step : Chunk → β → Async (ForInStep β)) : Async β := do
+
+  let rec @[specialize] loop (stream : Stream) (acc : β) : Async β := do
+    if let some chunk ← stream.recv then
+      match ← step chunk acc with
+      | .done res => return res
+      | .yield res => loop stream res
+    else
+      return acc
+
+  loop stream acc
+
+/--
+Context-aware iteration over chunks until the channel closes.
+-/
+@[inline]
+protected partial def forIn'
+    {β : Type} (stream : Stream) (acc : β)
+    (step : Chunk → β → ContextAsync (ForInStep β)) : ContextAsync β := do
+
+  let rec @[specialize] loop (stream : Stream) (acc : β) : ContextAsync β := do
+    let data ← Selectable.one #[
+      .case stream.recvSelector pure,
+      .case (← ContextAsync.doneSelector) (fun _ => pure none),
+    ]
+
+    if let some chunk := data then
+      match ← step chunk acc with
+      | .done res => return res
+      | .yield res => loop stream res
+    else
+      return acc
+
+  loop stream acc
+
+/--
+Abstracts over how the next chunk is received, allowing `readAll` to work in both `Async`
+(no cancellation) and `ContextAsync` (races with cancellation via `doneSelector`).
+-/
+class NextChunk (m : Type → Type) where
+  /--
+  Receives the next chunk, stopping at EOF or (in `ContextAsync`) when the context is cancelled.
+  -/
+  nextChunk : Stream → m (Option Chunk)
+
+instance : NextChunk Async where
+  nextChunk := Stream.recv
+
+instance : NextChunk ContextAsync where
+  nextChunk stream := do
+    Selectable.one #[
+      .case stream.recvSelector pure,
+      .case (← ContextAsync.doneSelector) (fun _ => pure none),
+    ]
+
+/--
+Reads all remaining chunks and decodes them into `α`.
+
+Works in both `Async` (reads until EOF, no cancellation) and `ContextAsync` (also stops if the
+context is cancelled).
+-/
+partial def readAll
+    [FromByteArray α]
+    [Monad m] [MonadExceptOf IO.Error m] [NextChunk m]
+    (stream : Stream)
+    (maximumSize : Option UInt64 := none) :
+    m α := do
+
+  let rec loop (result : ByteArray) : m ByteArray := do
+    match ← NextChunk.nextChunk stream with
+    | none => return result
+    | some chunk =>
+      let result := result ++ chunk.data
+      if let some max := maximumSize then
+        if result.size.toUInt64 > max then
+          throw (.userError s!"body exceeded maximum size of {max} bytes")
+      loop result
+
+  let result ← loop ByteArray.empty
+
+  match FromByteArray.fromByteArray result with
+  | .ok a => return a
+  | .error msg => throw (.userError msg)
+
+private def collapseForSend
+    (stream : Stream)
+    (chunk : Chunk)
+    (incomplete : Bool) : BaseIO (Except IO.Error (Option Chunk)) := do
+
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    let st ← get
+
+    if st.closed then
+      return .error (.userError "channel closed")
+
+    let merged := match st.pendingIncompleteChunk with
+      | some pending =>
+        {
+          data := pending.data ++ chunk.data
+          extensions := if pending.extensions.isEmpty then chunk.extensions else pending.extensions
+        }
+      | none => chunk
+
+    if incomplete then
+      set { st with pendingIncompleteChunk := some merged }
+      return .ok none
+    else
+      set { st with pendingIncompleteChunk := none }
+      return .ok (some merged)
+
+/--
+Sends a chunk, retrying if a select-mode consumer races and loses. If no consumer is ready,
+installs the chunk as a pending producer and awaits acknowledgement from the receiver.
+-/
+private partial def send' (stream : Stream) (chunk : Chunk) : Async Unit := do
+  let done ← IO.Promise.new
+  let result : Except IO.Error (Option Bool) ← stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    let st ← get
+
+    if st.closed then
+      return .error (IO.Error.userError "channel closed")
+
+    if let some consumer := st.pendingConsumer then
+      let success ← consumer.resolve (some chunk)
+
+      if success then
+        set {
+          st with
+          pendingConsumer := none
+          knownSize := Channel.decreaseKnownSize st.knownSize chunk
+        }
+        return .ok (some true)
+      else
+        set { st with pendingConsumer := none }
+        return .ok (some false)
+    else if st.pendingProducer.isSome then
+      return .error (IO.Error.userError "only one blocked producer is allowed")
+    else
+      set { st with pendingProducer := some { chunk, done } }
+      return .ok none
+
+  match result with
+  | .error err =>
+    throw err
+  | .ok (some true) =>
+    return ()
+  | .ok (some false) =>
+    -- The select-mode consumer raced and lost; recurse to allocate a fresh `done` promise.
+    send' stream chunk
+  | .ok none =>
+    match ← await done.result? with
+    | some true => return ()
+    | _ => throw (IO.Error.userError "channel closed")
+
+/--
+Sends a chunk.
+
+If `incomplete := true`, the chunk is buffered and collapsed with subsequent chunks, and is not
+delivered to the receiver yet.
+If `incomplete := false`, any buffered incomplete pieces are collapsed with this chunk and the
+single merged chunk is sent.
+-/
+def send (stream : Stream) (chunk : Chunk) (incomplete : Bool := false) : Async Unit := do
+  match (← collapseForSend stream chunk incomplete) with
+  | .error err => throw err
+  | .ok none => pure ()
+  | .ok (some toSend) =>
+    if toSend.data.isEmpty ∧ toSend.extensions.isEmpty then
+      return ()
+
+    send' stream toSend
+
+/--
+Returns `true` when a consumer is currently blocked waiting for data.
+-/
+def hasInterest (stream : Stream) : Async Bool :=
+  stream.state.atomically do
+    Channel.pruneFinishedWaiters
+    Channel.hasInterest'
+
+open Internal.IO.Async in
+/--
+Creates a selector that resolves when consumer interest is present.
+Returns `true` when a consumer is waiting, `false` when the channel closes first.
+-/
+def interestSelector (stream : Stream) : Selector Bool where
+  tryFn := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+      let st ← get
+      if st.pendingConsumer.isSome then
+        return some true
+      else if st.closed then
+        return some false
+      else
+        return none
+
+  registerFn waiter := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+      let st ← get
+
+      if st.pendingConsumer.isSome then
+        let lose := return ()
+        let win promise := do
+          promise.resolve (.ok true)
+        waiter.race lose win
+      else if st.closed then
+        let lose := return ()
+        let win promise := do
+          promise.resolve (.ok false)
+        waiter.race lose win
+      else if st.interestWaiter.isSome then
+        throw (.userError "only one blocked interest selector is allowed")
+      else
+        set { st with interestWaiter := some waiter }
+
+  unregisterFn := do
+    stream.state.atomically do
+      Channel.pruneFinishedWaiters
+
+end Stream
+
+/--
+Creates a body from a producer function.
+Returns the stream immediately and runs `gen` in a detached task.
+The channel is always closed when `gen` returns or throws.
+Errors from `gen` are not rethrown here; consumers observe end-of-stream via `recv = none`.
+-/
+def stream (gen : Stream → Async Unit) : Async Stream := do
+  let s ← mkStream
+  background <| do
+    try
+      gen s
+    finally
+      s.close
+  return s
+
+/--
+Creates a body from a fixed byte array.
+-/
+def fromBytes (content : ByteArray) : Async Stream := do
+  stream fun s => do
+    s.setKnownSize (some (.fixed content.size))
+    if content.size > 0 then
+      s.send (Chunk.ofByteArray content)
+
+/--
+Creates an empty `Stream` body channel (already closed, no data).
+
+Prefer `Body.Empty` when you need a concrete zero-cost type. Use this when the calling
+context requires a `Stream` specifically.
+-/
+def empty : Async Stream := do
+  let s ← mkStream
+  s.setKnownSize (some (.fixed 0))
+  s.close
+  return s
+
+instance : ForIn Async Stream Chunk where
+  forIn := Stream.forIn
+
+instance : ForIn ContextAsync Stream Chunk where
+  forIn := Stream.forIn'
+
+instance : Http.Body Stream where
+  recv := Stream.recv
+  close := Stream.close
+  isClosed := Stream.isClosed
+  recvSelector := Stream.recvSelector
+  getKnownSize := Stream.getKnownSize
+  setKnownSize := Stream.setKnownSize
+
+instance : Coe Stream Any := ⟨Any.ofBody⟩
+
+instance : Coe (Response Stream) (Response Any) where
+  coe f := { f with }
+
+instance : Coe (ContextAsync (Response Stream)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+instance : Coe (Async (Response Stream)) (ContextAsync (Response Any)) where
+  coe action := do
+    let response ← action
+    pure (response : Response Any)
+
+end Body
+
+namespace Request.Builder
+
+open Internal.IO.Async
+
+/--
+Builds a request with a streaming body generator.
+-/
+def stream
+    (builder : Builder)
+    (gen : Body.Stream → Async Unit) :
+    Async (Request Body.Stream) := do
+  let s ← Body.stream gen
+  return Request.Builder.body builder s
+
+end Request.Builder
+
+namespace Response.Builder
+open Internal.IO.Async
+
+/--
+Builds a response with a streaming body generator.
+-/
+def stream
+    (builder : Builder)
+    (gen : Body.Stream → Async Unit) :
+    Async (Response Body.Stream) := do
+  let s ← Body.stream gen
+  return Response.Builder.body builder s
+
+end Response.Builder

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
@@ -214,4 +215,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/Request.lean

@@ -124,12 +124,6 @@ def new : Builder := { }
 
 namespace Builder
 
-/--
-Creates a new HTTP request builder with the default head
-(method: GET, version: HTTP/1.1, target: `*`).
--/
-def empty : Builder := { }
-
 /--
 Sets the HTTP method for the request being built.
 -/

src/Std/Internal/Http/Data/Response.lean

@@ -111,7 +111,7 @@ namespace Builder
 /--
 Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).
 -/
-def empty : Builder := { }
+def new : Builder := { }
 
 /--
 Sets the HTTP status code for the response being built.
@@ -173,66 +173,66 @@ end Builder
 Creates a new HTTP Response builder with the 200 status code.
 -/
 def ok : Builder :=
-  .empty |>.status .ok
+  .new |>.status .ok
 
 /--
 Creates a new HTTP Response builder with the provided status.
 -/
 def withStatus (status : Status) : Builder :=
-  .empty |>.status status
+  .new |>.status status
 
 /--
 Creates a new HTTP Response builder with the 404 status code.
 -/
 def notFound : Builder :=
-  .empty |>.status .notFound
+  .new |>.status .notFound
 
 /--
 Creates a new HTTP Response builder with the 500 status code.
 -/
 def internalServerError : Builder :=
-  .empty |>.status .internalServerError
+  .new |>.status .internalServerError
 
 /--
 Creates a new HTTP Response builder with the 400 status code.
 -/
 def badRequest : Builder :=
-  .empty |>.status .badRequest
+  .new |>.status .badRequest
 
 /--
 Creates a new HTTP Response builder with the 201 status code.
 -/
 def created : Builder :=
-  .empty |>.status .created
+  .new |>.status .created
 
 /--
 Creates a new HTTP Response builder with the 202 status code.
 -/
 def accepted : Builder :=
-  .empty |>.status .accepted
+  .new |>.status .accepted
 
 /--
 Creates a new HTTP Response builder with the 401 status code.
 -/
 def unauthorized : Builder :=
-  .empty |>.status .unauthorized
+  .new |>.status .unauthorized
 
 /--
 Creates a new HTTP Response builder with the 403 status code.
 -/
 def forbidden : Builder :=
-  .empty |>.status .forbidden
+  .new |>.status .forbidden
 
 /--
 Creates a new HTTP Response builder with the 409 status code.
 -/
 def conflict : Builder :=
-  .empty |>.status .conflict
+  .new |>.status .conflict
 
 /--
 Creates a new HTTP Response builder with the 503 status code.
 -/
 def serviceUnavailable : Builder :=
-  .empty |>.status .serviceUnavailable
+  .new |>.status .serviceUnavailable
 
 end Response

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

@@ -94,4 +94,3 @@ def parseOrRoot (s : String) : Std.Http.URI.Path :=
   parse? s |>.getD { segments := #[], absolute := true }
 
 end Std.Http.URI.Path
-

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

@@ -51,13 +51,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 (fun b : UInt8 => Internal.Char.isAlphaByte b)
+  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
@@ -67,7 +67,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
 
@@ -81,7 +81,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))
@@ -93,7 +93,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
 
@@ -112,7 +112,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
 
@@ -126,7 +126,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
 
@@ -147,8 +147,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"
@@ -186,7 +186,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
@@ -271,7 +271,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"
@@ -303,7 +303,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,284 @@
+/-
+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
+
+  /--
+  Reserved; not currently entered by the state machine.
+  -/
+  | writingHeaders
+
+  /--
+  Writing the body output (either fixed-length or chunked).
+  -/
+  | writingBody (mode : Body.Length)
+
+  /--
+  Waiting for all buffered output to drain before transitioning to `complete`.
+  -/
+  | shuttingDown
+
+  /--
+  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
+
+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
+    let size := writer.userData.foldl (fun x y => x + y.data.size) 0
+    .fixed size
+  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
+    { writer with userData := writer.userData ++ data }
+  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 }, 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 := #[], 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/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