perf: specialize qsort properly onto the lt function

This PR adds the option `LEAN_MI_SECURE` to our CMake build. It can be
configured with values `0`
through `4`. Every increment enables additional memory safety
mitigations in mimalloc, at the cost
of 2%-20% instruction count, depending on the benchmark. The option is
disabled by default in our
release builds as most of our users do not use the Lean runtime in
security sensitive situations.
Distributors and organization deploying production Lean code should
consider enabling the option as
a hardening measure. The effects of the various levels can be found at
https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60.

CMakeLists.txt

@@ -129,6 +129,7 @@ if(USE_MIMALLOC)
     # cadical, it might be worth reorganizing the directory structure.
     SOURCE_DIR
     "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
+    EXCLUDE_FROM_ALL
   )
   FetchContent_MakeAvailable(mimalloc)
 endif()

src/CMakeLists.txt

@@ -110,6 +110,7 @@ option(RUNTIME_STATS "RUNTIME_STATS" OFF)
 option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
 option(USE_GMP "USE_GMP" ON)
 option(USE_MIMALLOC "use mimalloc" ON)
+set(LEAN_MI_SECURE 0 CACHE STRING "Configure mimalloc memory safety mitigations (https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60)")
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)

src/Init/Data/Array/QSort/Basic.lean

@@ -33,6 +33,7 @@ if necessary so that the middle (pivot) element is at index `hi`.
 We then iterate from `k = lo` to `k = hi`, with a pointer `i` starting at `lo`, and
 swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
 -/
+@[inline]
 def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w : lo ≤ hi := by omega)
     (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m ≤ hi} × Vector α n :=
   let mid := (lo + hi) / 2
@@ -44,7 +45,7 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w
   -- elements in `[i, k)` are greater than or equal to `pivot`,
   -- elements in `[k, hi)` are unexamined,
   -- while `as[hi]` is (by definition) the pivot.
-  let rec loop (as : Vector α n) (i k : Nat)
+  let rec @[specialize] loop (as : Vector α n) (i k : Nat)
       (ilo : lo ≤ i := by omega) (ik : i ≤ k := by omega) (w : k ≤ hi := by omega) :=
     if h : k < hi then
       if lt as[k] pivot then

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Basic.lean

@@ -909,7 +909,7 @@ theorem Slice.Pos.skipWhile_copy {ρ : Type} {pat : ρ} [ForwardPattern pat] [Pa
   simp
 
 @[simp]
-theorem Pos.skipWhile_le {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
+theorem Pos.le_skipWhile {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
     [LawfulForwardPatternModel pat] {s : String} {pos : s.Pos} : pos ≤ pos.skipWhile pat := by
   simp [skipWhile_eq_skipWhile_toSlice, Pos.le_ofToSlice_iff]
 

src/Lean/Elab/BuiltinDo/For.lean

@@ -153,6 +153,9 @@ open Lean.Meta
 
   let body ←
     withLocalDeclsD xh fun xh => do
+    Term.addLocalVarInfo x xh[0]!
+    if let some h := h? then
+      Term.addLocalVarInfo h xh[1]!
     withLocalDecl s .default σ (kind := .implDetail) fun loopS => do
     mkLambdaFVars (xh.push loopS) <| ← do
     bindMutVarsFromTuple loopMutVarNames loopS.fvarId! do

src/Lean/Elab/Deriving/Inhabited.lean

@@ -89,7 +89,7 @@ where
       let val ←
         if isStructure (← getEnv) inductiveTypeName then
           withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using structure instance elaborator") do
-            let stx ← `(structInst| {..})
+            let stx ← `(structInstDefault| struct_inst_default%)
             withoutErrToSorry <| elabTermAndSynthesize stx type
         else
           withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using constructor `{.ofConstName ctorName}`") do

src/Lean/Elab/Do/Basic.lean

@@ -384,6 +384,7 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
   let k := dec.k
   -- The .ofBinderName below is mainly to interpret `__do_lift` binders as implementation details.
   let declKind := .ofBinderName x
+  let kResultTy ← mkFreshResultType `kResultTy
   withLocalDecl x .default eResultTy (kind := declKind) fun xFVar => do
     let body ← k
     let body' := body.consumeMData
@@ -411,7 +412,6 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
         -- else -- would be too aggressive
         --   return ← mapLetDecl (nondep := true) (kind := declKind) x eResultTy eRes fun _ => k ref
 
-    let kResultTy ← mkFreshResultType `kResultTy
     let body ← Term.ensureHasType (← mkMonadicType kResultTy) body
     let k ← mkLambdaFVars #[xFVar] body
     mkBindApp eResultTy kResultTy e k
@@ -545,7 +545,10 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
-  discard <| joinRhsMVar.mvarId!.checkedAssign joinRhs
+  unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
+    joinRhsMVar.mvarId!.withContext do
+      throwError "Bug in a `do` elaborator. Failed to assign join point RHS{indentExpr joinRhs}\n\
+        to metavariable\n{joinRhsMVar.mvarId!}"
 
   let body ← body?.getDM do
     -- Here we unconditionally add a pending MVar.

src/Lean/Elab/StructInst.lean

@@ -150,6 +150,8 @@ structure SourcesView where
   explicit : Array ExplicitSourceView
   /-- The syntax for a trailing `..`. This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications. -/
   implicit : Option Syntax
+  /-- Use `Inhabited` instances inherited from parent structures, and use `default` instances for missing fields. -/
+  useInhabited : Bool
   deriving Inhabited
 
 /--
@@ -179,7 +181,7 @@ private def getStructSources (structStx : Syntax) : TermElabM SourcesView :=
         let structName ← getStructureName srcType
         return { stx, fvar := src, structName }
     let implicit := if implicitSource[0].isNone then none else implicitSource
-    return { explicit, implicit }
+    return { explicit, implicit, useInhabited := false }
 
 /--
 We say a structure instance notation is a "modifyOp" if it contains only a single array update.
@@ -579,6 +581,9 @@ private structure StructInstContext where
   /-- If true, then try using default values or autoParams for missing fields.
   (Considered after `useParentInstanceFields`.) -/
   useDefaults : Bool
+  /-- If true, then tries `Inhabited` instances as an alternative to parent instances,
+  and when default values are missing. -/
+  useInhabited : Bool
   /-- If true, then missing fields after default value synthesis remain as metavariables rather than yielding an error.
   Only applies if `useDefaults` is true. -/
   unsynthesizedAsMVars : Bool
@@ -735,14 +740,27 @@ The arguments for the `_default` auxiliary function are provided by `fieldMap`.
 After default values are resolved, then the one that is added to the environment
 as an `_inherited_default` auxiliary function is normalized; we don't do those normalizations here.
 -/
-private partial def getFieldDefaultValue? (fieldName : Name) : StructInstM (NameSet × Option Expr) := do
+private def getFieldDefaultValue? (fieldName : Name) : StructInstM (Option (NameSet × Expr)) := do
   let some defFn := getEffectiveDefaultFnForField? (← getEnv) (← read).structName fieldName
-    | return ({}, none)
+    | return none
   let fieldMap := (← get).fieldMap
   let some (fields, val) ← instantiateStructDefaultValueFn? defFn (← read).levels (← read).params (pure ∘ fieldMap.find?)
     | logError m!"default value for field `{fieldName}` of structure `{.ofConstName (← read).structName}` could not be instantiated, ignoring"
-      return ({}, none)
-  return (fields, val)
+      return none
+  return some (fields, val)
+
+/--
+If `useInhabited` is enabled, tries synthesizing an `Inhabited` instance for the field.
+-/
+private def getFieldDefaultValueUsingInhabited (fieldType : Expr) : StructInstM (Option (NameSet × Expr)) := do
+  if (← read).useInhabited then
+    try
+      let val ← mkDefault fieldType
+      return some ({}, val)
+    catch _ =>
+      return none
+  else
+    return none
 
 /--
 Auxiliary type for `synthDefaultFields`
@@ -751,8 +769,16 @@ private structure PendingField where
   fieldName : Name
   fieldType : Expr
   required : Bool
-  deps : NameSet
-  val? : Option Expr
+  /-- If present, field dependencies and the default value. -/
+  val? : Option (NameSet × Expr)
+
+private def PendingField.isReady (pendingField : PendingField) (hasDep : Name → Bool) : Bool :=
+  pendingField.val?.any fun (deps, _) => deps.all hasDep
+
+private def PendingField.val! (pendingField : PendingField) : Expr :=
+  match pendingField.val? with
+  | some (_, val) => val
+  | none          => panic! "PendingField has no value"
 
 private def registerFieldMVarError (e : Expr) (ref : Syntax) (fieldName : Name) : StructInstM Unit :=
   registerCustomErrorIfMVar e ref m!"Cannot synthesize placeholder for field `{fieldName}`"
@@ -786,12 +812,15 @@ private def synthOptParamFields : StructInstM Unit := do
   -- Process default values for pending optParam fields.
   let mut pendingFields : Array PendingField ← optParamFields.filterMapM fun (fieldName, fieldType, required) => do
     if required || (← isFieldNotSolved? fieldName).isSome then
-      let (deps, val?) ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure ({}, none)
-      if let some val := val? then
-        trace[Elab.struct] "default value for {fieldName}:{indentExpr val}"
-      else
-        trace[Elab.struct] "no default value for {fieldName}"
-      pure <| some { fieldName, fieldType, required, deps, val? }
+      let val? ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure none
+      let val? ← pure val? <||> if (← read).useInhabited then getFieldDefaultValueUsingInhabited fieldType else pure none
+      trace[Elab.struct]
+        if let some (deps, val) := val? then
+          m!"default value for {fieldName}:{inlineExpr val}" ++
+          if deps.isEmpty then m!"" else m!"(depends on fields {deps.toArray})"
+        else
+          m!"no default value for {fieldName}"
+      pure <| some { fieldName, fieldType, required, val? }
     else
       pure none
   -- We then iteratively look for pending fields that do not depend on unsolved-for fields.
@@ -799,12 +828,11 @@ private def synthOptParamFields : StructInstM Unit := do
   -- so we need to keep trying until no more progress is made.
   let mut pendingSet : NameSet := pendingFields.foldl (init := {}) fun set pending => set.insert pending.fieldName
   while !pendingSet.isEmpty do
-    let selectedFields := pendingFields.filter fun pendingField =>
-      pendingField.val?.isSome && pendingField.deps.all (fun dep => !pendingSet.contains dep)
+    let selectedFields := pendingFields.filter (·.isReady (!pendingSet.contains ·))
     let mut toRemove : Array Name := #[]
     let mut assignErrors : Array MessageData := #[]
     for selected in selectedFields do
-      let some selectedVal := selected.val? | unreachable!
+      let selectedVal := selected.val!
       if let some mvarId ← isFieldNotSolved? selected.fieldName then
         let fieldType := selected.fieldType
         let selectedType ← inferType selectedVal
@@ -1084,6 +1112,7 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
         addStructFieldAux fieldName mvar
         return ← loop
   -- Default case: natural metavariable, register it for optParams
+  let fieldType := fieldType.consumeTypeAnnotations
   discard <| addStructFieldMVar fieldName fieldType
   modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
   loop
@@ -1111,29 +1140,44 @@ private partial def loop : StructInstM Expr := withViewRef do
 For each parent class, see if it can be used to synthesize the fields that haven't been provided.
 -/
 private partial def addParentInstanceFields : StructInstM Unit := do
-  let env ← getEnv
   let structName := (← read).structName
-  let fieldNames := getStructureFieldsFlattened env structName (includeSubobjectFields := false)
+  let fieldNames := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false)
   let fieldViews := (← read).fieldViews
   if fieldNames.all fieldViews.contains then
     -- Every field is accounted for already
     return
 
-  -- We look at class parents in resolution order
+  -- We look at parents in resolution order
   let parents ← getAllParentStructures structName
-  let classParents := parents.filter (isClass env)
-  if classParents.isEmpty then return
+  let env ← getEnv
+  let parentsToVisit := if (← read).useInhabited then parents else parents.filter (isClass env)
+  if parentsToVisit.isEmpty then return
 
   let allowedFields := fieldNames.filter (!fieldViews.contains ·)
   let mut remainingFields := allowedFields
 
   -- Worklist of parent/fields pairs. If fields is empty, then it will be computed later.
-  let mut worklist : List (Name × Array Name) := classParents |>.map (·, #[]) |>.toList
+  let mut worklist : List (Name × Array Name) := parentsToVisit |>.map (·, #[]) |>.toList
   let mut deferred : List (Name × Array Name) := []
 
+  let trySynthParent (parentName : Name) (parentTy : Expr) : StructInstM (LOption Expr) := do
+    if isClass (← getEnv) parentName then
+      match ← trySynthInstance parentTy with
+      | .none => pure ()
+      | r     => return r
+    if (← read).useInhabited then
+      let u ← getLevel parentTy
+      let cls := Expr.app (Expr.const ``Inhabited [u]) parentTy
+      match ← trySynthInstance cls with
+      | .none      => pure ()
+      | .undef     => return .undef
+      | .some inst => return .some <| mkApp2 (Expr.const ``Inhabited.default [u]) parentTy inst
+    return .none
+
   while !worklist.isEmpty do
     let (parentName, parentFields) :: worklist' := worklist | unreachable!
     worklist := worklist'
+    let env ← getEnv
     let parentFields := if parentFields.isEmpty then getStructureFieldsFlattened env parentName (includeSubobjectFields := false) else parentFields
     -- We only try synthesizing if the parent contains one of the remaining fields
     -- and if every parent field is an allowed field.
@@ -1145,7 +1189,7 @@ private partial def addParentInstanceFields : StructInstM Unit := do
         trace[Elab.struct] "could not calculate type for parent `{.ofConstName parentName}`"
         deferred := (parentName, parentFields) :: deferred
       | some (parentTy, _) =>
-        match ← trySynthInstance parentTy with
+        match ← trySynthParent parentName parentTy with
         | .none => trace[Elab.struct] "failed to synthesize instance for parent {parentTy}"
         | .undef =>
           trace[Elab.struct] "instance synthesis stuck for parent {parentTy}"
@@ -1199,17 +1243,19 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
   let fields ← addSourceFields structName s.sources.explicit fields
   trace[Elab.struct] "expanded fields:\n{MessageData.joinSep (fields.toList.map (fun (_, field) => m!"- {MessageData.nestD (toMessageData field)}")) "\n"}"
   let ellipsis := s.sources.implicit.isSome
+  let useInhabited := s.sources.useInhabited
   let (val, _) ← main
     |>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn
              -- See the note in `ElabAppArgs.processExplicitArg`
              -- For structure instances though, there's a sense in which app-style ellipsis mode is always enabled,
              -- so we do not specifically check for it to disable defaults.
              -- An effect of this is that if a user forgets `..` they'll be reminded with a "Fields missing" error.
-             useDefaults := !(← readThe Term.Context).inPattern
+             useDefaults := !(← readThe Term.Context).inPattern || useInhabited
              -- Similarly, for patterns we disable using parent instances to fill in fields
-             useParentInstanceFields := !(← readThe Term.Context).inPattern
+             useParentInstanceFields := !(← readThe Term.Context).inPattern || useInhabited
              -- In ellipsis mode, unsynthesized missing fields become metavariables, rather than being an error
              unsynthesizedAsMVars := ellipsis
+             useInhabited := useInhabited
      }
     |>.run { type := ctorFnType }
   return val
@@ -1333,6 +1379,15 @@ where
       trace[Elab.struct] "result:{indentExpr r}"
       return r
 
+@[builtin_term_elab structInstDefault] def elabStructInstDefault : TermElab := fun stx expectedType? => do
+  let sourcesView : SourcesView := { explicit := #[], implicit := none, useInhabited := true }
+  let (structName, structType?) ← getStructName expectedType? sourcesView
+  withTraceNode `Elab.struct (fun _ => return m!"elaborating default value for `{structName}`") do
+    let struct : StructInstView := { ref := stx, fields := #[], sources := sourcesView }
+    let r ← withSynthesize (postpone := .yes) <| elabStructInstView struct structName structType?
+    trace[Elab.struct] "result:{indentExpr r}"
+    return r
+
 builtin_initialize
   registerTraceClass `Elab.struct
   registerTraceClass `Elab.struct.modifyOp

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

@@ -50,6 +50,18 @@ register_builtin_option debug.tactic.simp.checkDefEqAttr : Bool := {
     of the `defeq` attribute, and warn if it was. Note that this is a costly check."
 }
 
+register_builtin_option warning.simp.varHead : Bool := {
+  defValue := false
+  descr := "If true, warns when the head symbol of the left-hand side of a `@[simp]` theorem \
+    is a variable. Such lemmas are tried on every simp step, which can be slow."
+}
+
+register_builtin_option warning.simp.otherHead : Bool := {
+  defValue := true
+  descr := "If true, warns when the left-hand side of a `@[simp]` theorem is headed by a \
+    `.other` key in the discrimination tree (e.g. a lambda expression). Such lemmas can cause slowdowns."
+}
+
 /--
 An `Origin` is an identifier for simp theorems which indicates roughly
 what action the user took which lead to this theorem existing in the simp set.
@@ -359,12 +371,27 @@ private def checkTypeIsProp (type : Expr) : MetaM Unit :=
   unless (← isProp type) do
     throwError "Invalid simp theorem: Expected a proposition, but found{indentExpr type}"
 
-private def mkSimpTheoremKeys (type : Expr) (noIndexAtArgs : Bool) : MetaM (Array SimpTheoremKey × Bool) := do
+private def mkSimpTheoremKeys (type : Expr) (noIndexAtArgs : Bool) (checkLhs : Bool := false) : MetaM (Array SimpTheoremKey × Bool) := do
   withNewMCtxDepth do
     let (_, _, type) ← forallMetaTelescopeReducing type
     let type ← whnfR type
     match type.eq? with
-    | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
+    | some (_, lhs, rhs) =>
+      let keys ← DiscrTree.mkPath lhs noIndexAtArgs
+      if checkLhs then
+        if warning.simp.varHead.get (← getOptions) && keys[0]? == some .star then
+          logWarning m!"Left-hand side of simp theorem has a variable as head symbol. \
+            This means the theorem will be tried on every simp step, which can be expensive. \
+            This may be acceptable for `local` or `scoped` simp lemmas.\n\
+            Use `set_option warning.simp.varHead false` to disable this warning."
+        if warning.simp.otherHead.get (← getOptions) && keys[0]? == some .other then
+          logWarning m!"Left-hand side of simp theorem is headed by a `.other` key in the \
+            discrimination tree (e.g. because it is a lambda expression). \
+            This theorem will be tried against all expressions that also have a `.other` key as head, \
+            which can cause slowdowns. \
+            This may be acceptable for `local` or `scoped` simp lemmas.\n\
+            Use `set_option warning.simp.otherHead false` to disable this warning."
+      pure (keys, ← isPerm lhs rhs)
     | none => throwError "Unexpected kind of simp theorem{indentExpr type}"
 
 register_builtin_option simp.rfl.checkTransparency: Bool := {
@@ -373,10 +400,10 @@ register_builtin_option simp.rfl.checkTransparency: Bool := {
 }
 
 private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr)
-    (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
+    (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) (checkLhs : Bool := false): MetaM SimpTheorem := do
   assert! origin != .fvar ⟨.anonymous⟩
   let type ← instantiateMVars (← inferType e)
-  let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs
+  let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs checkLhs
   let rfl ← isRflProof proof
   if rfl && simp.rfl.checkTransparency.get (← getOptions) then
     forallTelescopeReducing type fun _ type => do
@@ -399,7 +426,7 @@ Creates a `SimpTheorem` from a global theorem.
 Because some theorems lead to multiple `SimpTheorems` (in particular conjunctions), returns an array.
 -/
 def mkSimpTheoremFromConst (declName : Name) (post := true) (inv := false)
-    (prio : Nat := eval_prio default) : MetaM (Array SimpTheorem) := do
+    (prio : Nat := eval_prio default) (checkLhs : Bool := false) : MetaM (Array SimpTheorem) := do
   let cinfo ← getConstVal declName
   let us := cinfo.levelParams.map mkLevelParam
   let origin := .decl declName post inv
@@ -413,10 +440,10 @@ def mkSimpTheoremFromConst (declName : Name) (post := true) (inv := false)
         let auxName ← mkAuxLemma (kind? := `_simp) cinfo.levelParams type val (inferRfl := true)
           (forceExpose := true)  -- These kinds of theorems are small and `to_additive` may need to
                                  -- unfold them.
-        r := r.push <| (← do mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false))
+        r := r.push <| (← do mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false) (checkLhs := checkLhs))
       return r
     else
-      return #[← withoutExporting do mkSimpTheoremCore origin (mkConst declName us) #[] (mkConst declName) post prio (noIndexAtArgs := false)]
+      return #[← withoutExporting do mkSimpTheoremCore origin (mkConst declName us) #[] (mkConst declName) post prio (noIndexAtArgs := false) (checkLhs := checkLhs)]
 
 def SimpTheorem.getValue (simpThm : SimpTheorem) : MetaM Expr := do
   if simpThm.proof.isConst && simpThm.levelParams.isEmpty then
@@ -670,7 +697,7 @@ def SimpExtension.getTheorems (ext : SimpExtension) : CoreM SimpTheorems :=
 Adds a simp theorem to a simp extension
 -/
 def addSimpTheorem (ext : SimpExtension) (declName : Name) (post : Bool) (inv : Bool) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
-  let simpThms ← withExporting (isExporting := attrKind != .local && !isPrivateName declName) do mkSimpTheoremFromConst declName post inv prio
+  let simpThms ← withExporting (isExporting := attrKind != .local && !isPrivateName declName) do mkSimpTheoremFromConst declName post inv prio (checkLhs := true)
   for simpThm in simpThms do
     ext.add (SimpEntry.thm simpThm) attrKind
 

src/Lean/Parser/Term.lean

@@ -354,6 +354,13 @@ def structInstFieldDef := leading_parser
 def structInstFieldEqns := leading_parser
   optional "private" >> matchAlts
 
+/--
+Synthesizes a default value for a structure, making use of `Inhabited` instances for
+missing fields, as well as `Inhabited` instances for parent structures.
+-/
+@[builtin_term_parser] def structInstDefault := leading_parser
+  "struct_inst_default%"
+
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
 def funStrictImplicitBinder :=

src/Std/Internal/Http.lean

@@ -7,3 +7,4 @@ module
 
 prelude
 public import Std.Internal.Http.Data
+public import Std.Internal.Http.Protocol.H1

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

@@ -6,6 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
+public import Std.Internal.Http.Data.URI
 public import Std.Internal.Http.Data.Headers.Name
 public import Std.Internal.Http.Data.Headers.Value
 public import Std.Internal.Parsec.Basic
@@ -215,4 +216,89 @@ 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
+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 ⟨⟩
+  else
+    none
+
+/--
+Serializes an `Expect` header.
+-/
+def serialize (_ : Expect) : Header.Name × Header.Value :=
+  (Header.Name.expect, Value.ofString! "100-continue")
+
+instance : Header Expect := ⟨parse, serialize⟩
+
+end Expect
+
+end Std.Http.Header

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

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

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

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

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

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

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

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Time
+public import Std.Internal.Http.Data
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Protocol.H1.Parser
+public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Internal.Http.Protocol.H1.Error
+
+public section
+
+/-!
+# HTTP/1.1 Events
+
+This module defines the events that can occur during HTTP/1.1 message processing,
+including header completion and control/error signals.
+-/
+
+namespace Std.Http.Protocol.H1
+
+set_option linter.all true
+
+/--
+Events emitted during HTTP message processing.
+-/
+inductive Event (dir : Direction)
+  /--
+  Indicates that all headers have been successfully parsed.
+  -/
+  | endHeaders (head : Message.Head dir)
+
+  /--
+  Signals that additional input data is required to continue processing.
+  -/
+  | needMoreData (size : Option Nat)
+
+  /--
+  Indicates a failure during parsing or processing.
+  -/
+  | failed (err : Error)
+
+  /--
+  Requests that the connection be closed.
+  -/
+  | close
+
+  /--
+  The body should be closed.
+  -/
+  | closeBody
+
+  /--
+  Indicates that a response is required.
+  -/
+  | needAnswer
+
+  /--
+  Indicates readiness to process the next message.
+  -/
+  | next
+
+  /--
+  Signals that an `Expect: 100-continue` decision is pending.
+  -/
+  | «continue»
+deriving Inhabited, Repr

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

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

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

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

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

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

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

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

src/Std/Internal/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/include/lean/lean.h

@@ -325,6 +325,55 @@ LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_unreachable(void);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_rc_overflow(void);
+LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_overflow(void);
+
+static inline bool lean_usize_mul_would_overflow(size_t a, size_t b) {
+#if defined(__GNUC__) || defined(__clang__)
+    size_t r;
+    return __builtin_mul_overflow(a, b, &r);
+#else
+    return a != 0 && b > SIZE_MAX / a;
+#endif
+}
+
+static inline bool lean_usize_add_would_overflow(size_t a, size_t b) {
+#if defined(__GNUC__) || defined(__clang__)
+    size_t r;
+    return __builtin_add_overflow(a, b, &r);
+#else
+    return a > SIZE_MAX - b;
+#endif
+}
+
+static inline size_t lean_usize_mul_checked(size_t a, size_t b) {
+#if defined(__GNUC__) || defined(__clang__)
+    size_t r;
+    if (LEAN_UNLIKELY(__builtin_mul_overflow(a, b, &r))) {
+        lean_internal_panic_overflow();
+    }
+    return r;
+#else
+    if (a != 0 && b > SIZE_MAX / a) {
+        lean_internal_panic_overflow();
+    }
+    return a * b;
+#endif
+}
+
+static inline size_t lean_usize_add_checked(size_t a, size_t b) {
+#if defined(__GNUC__) || defined(__clang__)
+    size_t r;
+    if (LEAN_UNLIKELY(__builtin_add_overflow(a, b, &r))) {
+        lean_internal_panic_overflow();
+    }
+    return r;
+#else
+    if (a > SIZE_MAX - b) {
+        lean_internal_panic_overflow();
+    }
+    return a + b;
+#endif
+}
 
 static inline size_t lean_align(size_t v, size_t a) {
     return (v / a)*a + a * (v % a != 0);
@@ -617,7 +666,7 @@ static inline uint8_t * lean_ctor_scalar_cptr(lean_object * o) {
 
 static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
     assert(tag <= LeanMaxCtorTag && num_objs < LEAN_MAX_CTOR_FIELDS && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE);
-    lean_object * o = lean_alloc_ctor_memory(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
+    lean_object * o = lean_alloc_ctor_memory(lean_usize_add_checked(lean_usize_add_checked(sizeof(lean_ctor_object), lean_usize_mul_checked(sizeof(void*), num_objs)), scalar_sz));
     lean_set_st_header(o, tag, num_objs);
     return o;
 }
@@ -727,7 +776,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea
 static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) {
     assert(arity > 0);
     assert(num_fixed < arity);
-    lean_closure_object * o = (lean_closure_object*)lean_alloc_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
+    lean_closure_object * o = (lean_closure_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_closure_object), lean_usize_mul_checked(sizeof(void*), num_fixed)));
     lean_set_st_header((lean_object*)o, LeanClosure, 0);
     o->m_fun = fun;
     o->m_arity = arity;
@@ -773,7 +822,7 @@ LEAN_EXPORT lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object**
 
 /* Arrays of objects (low level API) */
 static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {
-    lean_array_object * o = (lean_array_object*)lean_alloc_object(sizeof(lean_array_object) + sizeof(void*)*capacity);
+    lean_array_object * o = (lean_array_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), capacity)));
     lean_set_st_header((lean_object*)o, LeanArray, 0);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -950,8 +999,18 @@ LEAN_EXPORT lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
 
 /* Array of scalars */
 
+static inline bool lean_alloc_sarray_would_overflow(unsigned elem_size, size_t capacity) {
+    if (lean_usize_mul_would_overflow(elem_size, capacity)) {
+        return true;
+    }
+    if (lean_usize_add_would_overflow(sizeof(lean_sarray_object), elem_size * capacity)) {
+        return true;
+    }
+    return false;
+}
+
 static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) {
-    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity);
+    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_size, capacity)));
     lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -1113,7 +1172,7 @@ static inline lean_obj_res lean_float_array_set(lean_obj_arg a, b_lean_obj_arg i
 /* Strings */
 
 static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_t len) {
-    lean_string_object * o = (lean_string_object*)lean_alloc_object(sizeof(lean_string_object) + capacity);
+    lean_string_object * o = (lean_string_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_string_object), capacity));
     lean_set_st_header((lean_object*)o, LeanString, 0);
     o->m_size = size;
     o->m_capacity = capacity;

src/runtime/CMakeLists.txt

@@ -39,7 +39,7 @@ if(USE_MIMALLOC)
   # Lean code includes it as `lean/mimalloc.h` but for compiling `static.c` itself, add original dir
   include_directories(${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/include)
   # make all symbols visible, always build with optimizations as otherwise Lean becomes too slow
-  set(MIMALLOC_FLAGS "-DMI_SHARED_LIB -DMI_SHARED_LIB_EXPORT -O3 -DNDEBUG -DMI_WIN_NOREDIRECT -Wno-unused-function")
+  set(MIMALLOC_FLAGS "-DMI_SHARED_LIB -DMI_SHARED_LIB_EXPORT -O3 -DNDEBUG -DMI_WIN_NOREDIRECT -DMI_SECURE=${LEAN_MI_SECURE} -Wno-unused-function")
   if(CMAKE_CXX_COMPILER_ID MATCHES "AppleClang|Clang")
     string(APPEND MIMALLOC_FLAGS " -Wno-deprecated")
   endif()

src/runtime/compact.cpp

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

src/runtime/io.cpp

@@ -583,6 +583,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h) {
 /* Handle.read : (@& Handle) → USize → IO ByteArray */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes) {
     FILE * fp = io_get_handle(h);
+    if (lean_alloc_sarray_would_overflow(1, nbytes)) {
+        return io_result_mk_error(decode_io_error(ENOMEM, NULL));
+    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     if (nbytes == 0) {
         // std::fread doesn't handle 0 reads well, see https://github.com/leanprover/lean4/issues/12138
@@ -865,6 +868,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes) {
     }
 #endif
 
+    if (lean_alloc_sarray_would_overflow(1, nbytes)) {
+        return io_result_mk_error(decode_io_error(ENOMEM, NULL));
+    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     size_t remain = nbytes;
     uint8_t *dst = lean_sarray_cptr(res);

src/runtime/mpz.cpp

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

src/runtime/object.cpp

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

src/runtime/uv/tcp.cpp

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

src/runtime/uv/udp.cpp

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