fix: add a bunch of structures

src/Init/Data.lean

@@ -49,5 +49,6 @@ public import Init.Data.Vector
 public import Init.Data.Iterators
 public import Init.Data.Range.Polymorphic
 public import Init.Data.Slice
+public import Init.Data.ByteSlice
 
 public section

src/Init/Data/ByteArray.lean

@@ -1,3 +1,4 @@
+
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

src/Init/Data/ByteArray/Basic.lean

@@ -23,10 +23,18 @@ attribute [extern "lean_byte_array_data"] ByteArray.data
 
 namespace ByteArray
 
-deriving instance BEq for ByteArray
-
 attribute [ext] ByteArray
 
+/--
+Checks whether two `ByteArray` instances have the same length and identical content. Normally used
+via the `==` operator.
+-/
+@[extern "lean_byte_array_beq"]
+protected def beq (a b : @& ByteArray) : Bool :=
+  BEq.beq a.data b.data
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
 instance : DecidableEq ByteArray :=
   fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
 

src/Init/Data/ByteSlice.lean

@@ -0,0 +1,257 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.Array.Basic
+public import Init.Data.Array.DecidableEq
+public import Init.Data.UInt.Basic
+public import all Init.Data.UInt.BasicAux
+public import Init.Data.Option.Basic
+public import Init.Data.ByteArray
+public import Init.Data.Iterators.Basic
+public import Init.Data.Slice.Basic
+
+public section
+
+/--
+A slice of bytes.
+-/
+structure ByteSlice where
+  data : ByteArray
+  start : Nat
+  «end» : Nat
+  valid : start ≤ «end» ∧ «end» ≤ data.size
+
+namespace ByteSlice
+
+/--
+Creates a new `ByteSlice` from a `ByteArray.Iterator`.
+-/
+@[inline]
+def ofIterator (data : ByteArray.Iterator) (size : Nat) (h : data.pos + size ≤ data.array.size) : ByteSlice :=
+  { data := data.array, start := data.pos, «end» := data.pos + size, valid := And.intro (by simp) h }
+
+/--
+Creates a new `ByteSlice` from a `ByteArray`.
+-/
+@[inline]
+def ofByteArray (data : ByteArray) : ByteSlice :=
+  { data, start := 0, «end» := data.size, valid := by simp }
+
+/--
+Creates an empty `ByteSlice`.
+-/
+@[inline]
+def empty : ByteSlice :=
+  { data := ByteArray.empty, start := 0, «end» := 0, valid := by simp }
+
+/--
+Gets the size of the slice.
+-/
+@[inline]
+def size (slice : ByteSlice) : Nat :=
+  slice.«end» - slice.start
+
+/--
+Checks if the slice is empty.
+-/
+@[inline]
+def isEmpty (slice : ByteSlice) : Bool :=
+  slice.size = 0
+
+/--
+Gets a byte at the given index within the slice.
+Returns `none` if the index is out of bounds.
+-/
+@[inline]
+def get (slice : ByteSlice) (i : Nat) (h : i < slice.size := by get_elem_tactic) : UInt8 :=
+  have h_bounds : slice.start + i < slice.data.size := by
+    simp [size] at h
+    have h1 := slice.valid.left
+    have h2 := slice.valid.right
+    have h3 : slice.start + i < slice.«end» := by
+      rw [← Nat.add_sub_cancel' h1]
+      exact Nat.add_lt_add_left h slice.start
+    exact Nat.lt_of_lt_of_le h3 h2
+
+  slice.data.get (slice.start + i) h_bounds
+
+/--
+Gets a byte at the given index within the slice.
+Panics if the index is out of bounds.
+-/
+def get! (slice : ByteSlice) (i : Nat)  : UInt8 :=
+  if h :i < slice.size then
+    slice.get i
+  else
+    panic! "ByteSlice index out of bounds"
+
+/--
+Gets a byte at the given index within the slice.
+Panics if the index is out of bounds.
+-/
+def get? (slice : ByteSlice) (i : Nat) : Option UInt8 :=
+  if h : i < slice.size then
+    some (slice.get i)
+  else
+    none
+
+/--
+Gets a byte at the given index within the slice.
+Panics if the index is out of bounds.
+-/
+@[inline]
+def getD (slice : ByteSlice) (i : Nat) (default : UInt8) : UInt8 :=
+  slice.get? i |>.getD default
+
+/--
+Gets the first byte of the slice.
+Returns `none` if the slice is empty.
+-/
+@[inline]
+def first? (slice : ByteSlice) : Option UInt8 :=
+  slice.get? 0
+
+/--
+Gets the first byte of the slice.
+Returns `none` if the slice is empty.
+-/
+@[inline]
+def nextSlice? (slice : ByteSlice) : Option ByteSlice :=
+  if h : slice.end + 1 ≤ slice.data.size then
+    some { slice with «end» := slice.end + 1, valid := And.intro (Nat.le_trans slice.valid.left (by simp)) h }
+  else
+    none
+
+/--
+Gets the last byte of the slice.
+Returns `none` if the slice is empty.
+-/
+@[inline]
+def last? (slice : ByteSlice) : Option UInt8 :=
+  if slice.isEmpty then none else slice.get? (slice.size - 1)
+
+/--
+Creates a sub-slice from the given start index to the end.
+Returns `none` if the start index is out of bounds.
+-/
+@[inline]
+def drop (slice : ByteSlice) (n : Nat) : ByteSlice :=
+  if h : n <= slice.size then
+    let valid := by
+      simp [size] at h;
+      simp [slice.valid]
+      have h := Nat.add_le_add_left (n := n) h slice.start
+      rw [Nat.add_sub_cancel' slice.valid.left] at h
+      exact h
+    { slice with start := slice.start + n, valid }
+  else
+    { slice with start := slice.end, valid := by simp [slice.valid] }
+
+/--
+Creates a sub-slice with the first `n` elements.
+Returns `none` if `n` is greater than the slice size.
+-/
+@[inline]
+def take (slice : ByteSlice) (n : Nat) : ByteSlice :=
+  if h : n <= slice.size then
+    let newEnd := slice.start + n
+    let valid := by
+      constructor
+      · simp [newEnd]
+      · simp [newEnd]
+        simp [size] at h
+        have h3 : slice.start + n ≤ slice.start + (slice.«end» - slice.start) :=
+          Nat.add_le_add_left h slice.start
+        rw [Nat.add_sub_cancel' slice.valid.left] at h3
+        exact Nat.le_trans h3 slice.valid.right
+    { slice with «end» := newEnd, valid }
+  else
+    slice
+
+/--
+Creates a sub-slice from start index to end index (exclusive).
+Returns the slice unchanged if indices are out of bounds.
+-/
+@[inline]
+def slice (slice : ByteSlice) (start : Nat) (endIdx : Nat) : ByteSlice :=
+  if h1 : start <= endIdx ∧ endIdx <= slice.size then
+    let newStart := slice.start + start
+    let newEnd := slice.start + endIdx
+
+    let valid := by
+      constructor
+      · simp [newStart, newEnd]
+        exact h1.left
+      · simp [newEnd]
+        simp [size] at h1
+        have h4 : slice.start + endIdx ≤ slice.start + (slice.«end» - slice.start) :=
+          Nat.add_le_add_left h1.right slice.start
+        rw [Nat.add_sub_cancel' slice.valid.left] at h4
+        exact Nat.le_trans h4 slice.valid.right
+    { data := slice.data, start := newStart, «end» := newEnd, valid }
+  else
+    slice
+
+/--
+Finds the first occurrence of a byte in the slice.
+Returns the index relative to the slice start, or `none` if not found.
+-/
+def indexOf? (slice : ByteSlice) (byte : UInt8) : Option Nat :=
+  let rec loop (i : Nat) : Option Nat :=
+    if h : i < slice.size then
+      if slice.get i h = byte then
+        some i
+      else
+        loop (i + 1)
+    else
+      none
+  loop 0
+
+/--
+Checks if the slice starts with another slice.
+-/
+def startsWith (slice : ByteSlice) (pref : ByteSlice) : Bool :=
+  if pref.size > slice.size then
+    false
+  else
+    let rec loop (i : Nat) : Bool :=
+      if h : i < pref.size then
+        if h2 : i < slice.size then
+          if slice.get i = pref.get i then
+            loop (i + 1)
+          else
+            false
+        else
+          false
+      else
+        true
+    loop 0
+
+/---
+Checks if the slice contains a specific byte.
+-/
+@[inline]
+def contains (slice : ByteSlice) (byte : UInt8) : Bool :=
+  slice.indexOf? byte |>.isSome
+
+/--
+Converts the slice to a ByteArray by copying.
+-/
+@[inline]
+def toByteArray (slice : ByteSlice) : ByteArray :=
+  slice.data.extract slice.start slice.end
+
+@[extern "lean_byteslice_beq"]
+protected def beq (a b : ByteSlice) : Bool :=
+  BEq.beq a.toByteArray b.toByteArray
+
+instance : BEq ByteSlice where
+  beq := ByteSlice.beq
+
+instance : GetElem ByteSlice Nat UInt8 (fun slice i => i < slice.size) where
+  getElem := fun slice i h => slice.get i h

src/Lean/ErrorExplanation.lean

@@ -89,7 +89,7 @@ where
   upToWs (nonempty : Bool) : Parser String := fun it =>
     let it' := it.find fun c => c.isWhitespace
     if nonempty && it'.pos == it.pos then
-      .error it' "Expected a nonempty string"
+      .error it' (.other "Expected a nonempty string")
     else
       .success it' (it.extract it')
 
@@ -176,7 +176,7 @@ private abbrev ValidationM := Parsec ValidationState
 private def ValidationM.run (p : ValidationM α) (input : String) : Except (Nat × String) α :=
   match p (.ofSource input) with
   | .success _ res => Except.ok res
-  | .error s err  => Except.error (s.getLineNumber, err)
+  | .error s err  => Except.error (s.getLineNumber, toString err)
 
 /--
 Matches `p` as many times as possible, followed by EOF. If `p` cannot be matched prior to the end
@@ -286,7 +286,7 @@ where
   labelingExampleErrors {α} (header : String) (x : ValidationM α) : ValidationM α := fun s =>
     match x s with
     | res@(.success ..) => res
-    | .error s' msg => .error s' s!"Example '{header}' is malformed: {msg}"
+    | .error s' msg => .error s' (.other s!"Example '{header}' is malformed: {msg}")
 
   /--
   If `line` is a level-`level` header and, if `title?` is non-`none`, its title is `title?`,

src/Std/Internal/Async/Basic.lean

@@ -683,10 +683,16 @@ protected partial def forIn
     EAsync ε β := do
   let promise ← IO.Promise.new
 
-  let rec @[specialize] loop (b : β) : EAsync ε (ETask ε Unit) := async (prio := prio) do
+  let rec @[specialize] loop (b : β) : BaseIO Unit := do
     match ← f () b with
-      | ForInStep.done b => promise.resolve (.ok b)
-      | ForInStep.yield b => discard <| (loop b)
+      | .ofTask t => discard <| (IO.bindTask t (fun x =>
+        match x with
+        | .error e => do promise.resolve (.error e); pure (Task.pure (.ok ()))
+        | .ok (.done e) => do promise.resolve (.ok e); pure (Task.pure (.ok ()))
+        | .ok (.yield e) => BaseIO.asTask (prio := prio) (loop e) <&> Task.map .ok))
+      | .pure (.error e) => promise.resolve (.error e)
+      | .pure (.ok (.done e)) => promise.resolve (.ok e)
+      | .pure (.ok (.yield e)) => discard <| BaseIO.asTask (prio := prio) (loop e)
 
   discard <| loop init
 

src/Std/Internal/Http.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+
+namespace Std
+namespace Internal
+namespace Http
+
+/-!
+# Http
+
+The lean API for Http.
+
+# Overview
+
+This module of the standard library defines a lot of concepts related to HTTP protocol
+and the semantics in a Sans/IO format.
+
+# Http 1.1
+
+It's made mainly for Http 1.1 using https://httpwg.org/specs/rfc9112.html as the main
+recomendation.
+
+-/

src/Std/Internal/Http/Buffer.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+
+namespace Std
+namespace Http
+
+set_option linter.all true
+
+/--
+A `Buffer` is a type alias for `ByteArray` that provides a convenient interface for working with binary data.
+-/
+def Buffer := ByteArray
+
+namespace Buffer
+
+/--
+Creates a buffer with minimum size of `1024` if not specified.
+-/
+@[inline]
+def empty (capacity := 1024) : Buffer :=
+  ByteArray.emptyWithCapacity capacity
+
+/--
+Writes a `ByteArray` to the `Buffer`
+-/
+@[inline]
+def write (buffer : Buffer) (data : ByteArray) : Buffer :=
+  buffer.append data
+
+/--
+Writes a `Char` to the `Buffer`
+-/
+@[inline]
+def writeChar (buffer : Buffer) (data : Char) : Buffer :=
+  buffer.push data.toUInt8
+
+/--
+Writes a `String` to the `Buffer`
+-/
+@[inline]
+def writeString (buffer : Buffer) (data : String) : Buffer :=
+  buffer.append data.toUTF8

src/Std/Internal/Http/Connection.lean

@@ -0,0 +1,208 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+import Std.Internal.Async.Select
+import Std.Internal.Async.TCP
+import Std.Internal.Http.V11.Machine
+import Std.Internal.Http.Data.Body
+import Std.Internal.Http.Data.Request
+import Std.Internal.Http.Data.Response
+
+open Std Internal IO Async TCP
+open Std Http V11
+open Std Http Data
+
+namespace Std
+namespace Http
+
+set_option linter.all true
+
+/--
+The connection object that carries a socket and the machine
+-/
+structure Connection where
+  /--
+  The client socket
+  -/
+  socket : Socket.Client
+
+  /--
+  The state machine
+  -/
+  machine : Machine .request
+
+namespace Connection
+
+-- TODO : Guard type for IO.Promise
+-- TODO : Convert all the types of the Async itnerfaces to Async
+-- TODO : Easync.ofTask type is wrong.
+-- TODO : exception on while probasbly creates a promise not resolved error?
+-- TODO : cancelrecv must be fixed
+
+-- Event Handlers
+private def handleEndHeaders
+  (connection : Connection)
+  (fn : Request Body → Async (Response Body))
+  (promise : IO.Ref (ETask IO.Error (Response Body)))
+  (stream : ByteStream)
+  : Async Unit := do
+    if let some (method, uri, version) := connection.machine.inputStatusLine then
+      let res := fn (Request.mk method version uri connection.machine.inputHeaders (.stream stream))
+      promise.set (← res.asTask)
+    else
+      panic! "Invalid State"
+
+private def handleGotData (stream : ByteStream) (final : Bool) (data : ByteSlice) : Async Unit := do
+  await (← stream.data.send data)
+  if final then
+    await (← stream.data.send none)
+
+private def timeoutRecv (socket : Socket.Client) : Async (Option ByteArray) := do
+  let result := Selectable.one #[
+    .case (← Selector.sleep 5000) fun _ => return AsyncTask.pure none,
+    .case (← socket.recvSelector 4096) fun data => return AsyncTask.pure data,
+  ]
+  let result ← result
+  await result
+
+private def handleNeedMoreData (connection : Connection) : Async (Connection × Bool) := do
+  let data ← do
+    try
+      let size := connection.machine.size.getD 4096
+      let some data ← await (← connection.socket.recv? size)
+        | return ({connection with machine := connection.machine.setError .timeout |>.advance}, true)
+      pure (data, false)
+    catch _ =>
+      pure (.empty, true)
+
+  if .empty == data.1 then
+    pure (connection, true)
+  else
+    pure ({ connection with machine := connection.machine.feed data.1 }, false)
+
+private def handleAwaitingAnswer (connection : Connection) (response : Response Body) : Async (Connection × Bool) := do
+  match response.body with
+  | .zero =>
+    pure ({ connection with machine := connection.machine.close }, false)
+  | .bytes bytes =>
+    pure ({ connection with machine := connection.machine.writeData bytes.toByteArray |>.close }, false)
+  | .stream st =>
+    let ba ← await (← st.data.recv)
+    let connection := { connection with machine := { connection.machine with chunkedAnswer := true } }
+    match ba with
+    | some data =>
+      pure ({ connection with machine := connection.machine.writeData data.toByteArray }, false)
+    | none =>
+      pure ({ connection with machine := connection.machine.close }, false)
+
+private def handleReadyToRespond (connection : Connection) (response : Response Body) : Connection :=
+  { connection with machine := connection.machine.answer response }
+
+private def handleClose (stream : ByteStream) : Async Unit := do
+  await (← stream.data.send none)
+
+private def handleNext (stream : ByteStream) : Async Unit := do
+  await (← stream.data.send none)
+
+private def handleFailed (stream : ByteStream) (connection : Connection) : Async Connection := do
+  await (← stream.data.send none)
+  pure { connection with machine := connection.machine.advance }
+
+private def processEvent (connection : Connection)
+  (stream : ByteStream)
+  (fn : Request Body → Async (Response Body))
+  (promise : IO.Ref (ETask IO.Error (Response Body)))
+  : Async (Connection × ByteStream × Bool) := do
+  match connection.machine.event with
+  | some event =>
+    match event with
+    | .chunkExt _ =>
+      pure (connection, stream, false)
+    | .endHeaders _ =>
+      let newStream := { data := (← Channel.new) }
+      handleEndHeaders connection fn promise newStream
+      pure (connection, newStream, false)
+    | .gotData final data =>
+      handleGotData stream final data
+      pure (connection, stream, false)
+    | .needMoreData =>
+      let (newConnection, shouldBreak) ← handleNeedMoreData connection
+      pure (newConnection, stream, shouldBreak)
+    | .awaitingAnswer =>
+      let response ← EAsync.ofETask (← promise.get)
+      let (newConnection, shouldBreak) ← handleAwaitingAnswer connection response
+      pure (newConnection, stream, shouldBreak)
+    | .readyToRespond =>
+      let response ← EAsync.ofETask (← promise.get)
+      let newConnection := handleReadyToRespond connection response
+      pure (newConnection, stream, false)
+    | .next =>
+      handleNext stream
+      pure (connection, stream, false)
+    | .close =>
+      handleClose stream
+      pure (connection, stream, true)
+    | .failed _ =>
+      let newConnection ← handleFailed stream connection
+      pure (newConnection, stream, true)
+  | none =>
+    pure (connection, stream, false)
+
+private def flushConnection (connection : Connection) (force : Bool) : Async Connection := do
+  if connection.machine.needsFlush || force then
+    let machine := connection.machine
+    let (machine, ba) := machine.flush force
+    await (← connection.socket.send ba)
+    pure { connection with machine }
+  else
+    pure connection
+
+private def finalFlush (connection : Connection) : Async Unit := do
+  let machine := connection.machine
+  let (_, ba) := machine.flush true
+  if ba.size > 0 then
+    await (← connection.socket.send ba)
+
+private partial def start (connection : Connection) (fn : Request Body → Async (Response Body)) : Async Unit := do
+  try
+    let mut connection := connection
+    let mut stream : ByteStream := { data := (← Channel.new) }
+
+    let respPromise ← IO.mkRef (← IO.asTask default)
+
+    while true do
+      let (newConnection, newStream, shouldBreak) ←
+        processEvent connection stream fn respPromise
+
+      connection := newConnection
+      stream := newStream
+
+      if shouldBreak then
+        break
+
+      connection := { connection with machine := connection.machine.advance }
+      connection ← flushConnection connection true
+
+    finalFlush connection
+  catch err =>
+    IO.println s!"ERR: {err}"
+
+/--
+
+-/
+def serve (addr : Net.SocketAddress) (fn : Request Body → Async (Response Body)) : Async Unit := do
+  let socket ← Socket.Server.mk
+  socket.bind addr
+  socket.listen 128
+
+  while true do
+    let clientTask ← socket.accept
+    let client ← await clientTask
+    let conn := Connection.mk client {}
+    background .default (start conn fn)
+
+end Connection

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

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+import Std.Sync
+import Std.Internal.Async
+import Std.Internal.Http.Encode
+import Std.Internal.Http.Data.Headers
+import Std.Internal.Http.Data.Method
+import Std.Internal.Http.Data.Version
+
+open Std Internal IO Async
+
+namespace Std
+namespace Http
+namespace Data
+
+structure ByteStream where
+  data : Channel (Option ByteSlice)
+
+inductive Body where
+  | zero
+  | bytes (data : ByteSlice)
+  | stream (channel : ByteStream)
+deriving Inhabited
+
+namespace Body
+
+/--
+Get content length for a body (if known)
+-/
+def getContentLength (body : Body) : Option Nat :=
+  match body with
+  | zero => some 0
+  | .bytes data => some data.size
+  | .stream _ => none
+
+partial def ByteStream.recvString? (body : ByteStream) (buffer : ByteArray) : Async ByteArray := do
+  match (← body.data.recv).get with
+  | some bs => recvString? body (buffer ++ bs.toByteArray)
+  | none => pure buffer
+
+def recvString? (body : Body) : Async String :=
+  match body with
+  | .bytes body => pure (String.fromUTF8! body.toByteArray)
+  | .zero => pure ""
+  | .stream body => String.fromUTF8! <$> ByteStream.recvString? body .empty

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

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+import Std.Data
+import Std.Internal.Http.Encode
+
+open Std
+
+namespace Std
+namespace Http
+namespace Data
+
+/--
+A structure for managing HTTP headers as key-value pairs.
+-/
+structure Headers where
+  data : HashMap String (String × HashSet String)
+deriving Repr, Inhabited
+
+namespace Headers
+
+/--
+Splits a header value on commas, trims whitespace, puts into a HashSet.
+-/
+def splitValues (value : String) : HashSet String :=
+  HashSet.ofList <| value.splitOn "," |>.map String.trim
+
+/--
+Tries to retrieve the header values for the given key, as a HashSet.
+Returns `none` if the header is absent.
+-/
+@[inline]
+def getSingle? (headers : Headers) (name : String) : Option String :=
+  headers.data.get? name.toLower |>.map (List.head! ∘ HashSet.toList ∘ Prod.snd)
+
+/--
+Tries to retrieve the header values for the given key, as a HashSet.
+Returns `none` if the header is absent.
+-/
+@[inline]
+def get? (headers : Headers) (name : String) : Option (HashSet String) :=
+  headers.data.get? name.toLower |>.map Prod.snd
+
+/--
+Like `get?`, but returns an empty HashSet if absent.
+-/
+@[inline]
+def getD (headers : Headers) (name : String) : HashSet String :=
+  headers.get? name |>.getD ∅
+
+/--
+Like `get?`, but panics if absent.
+-/
+@[inline]
+def get! (headers : Headers) (name : String) : HashSet String :=
+  headers.data.get! name.toLower |> Prod.snd
+
+/--
+Inserts a new key-value pair into the headers.
+-/
+@[inline]
+def insert (headers : Headers) (name : String) (value : String) : Headers :=
+  let key := name.toLower
+  let data := headers.data.get? key
+  let words := splitValues value
+  let hm := if let some (name, hm) := data then (name, hm.insertMany words) else (name, words)
+  { data := headers.data.insert key hm }
+
+instance : ToString Headers where
+  toString headers :=
+    let pairs := headers.data.toList.map (fun (_, (k, vs)) => s!"{k}: {String.intercalate ", " vs.toList}")
+    String.intercalate "\r\n" pairs
+
+instance : Encode .v11 Headers where
+  encode buffer := buffer.writeString ∘ toString
+
+/--
+Creates empty headers.
+-/
+def empty : Headers :=
+  { data := HashMap.emptyWithCapacity }
+
+/--
+Creates headers from a list of key-value pairs.
+-/
+def fromList (pairs : List (String × String)) : Headers :=
+  { data := HashMap.ofList (pairs.map (fun (k, v) => (k.toLower, (k, splitValues v)))) }
+
+/--
+Checks if a header with the given name exists.
+-/
+@[inline]
+def contains (headers : Headers) (name : String) : Bool :=
+  headers.data.contains name.toLower
+
+/--
+Removes a header with the given name.
+-/
+@[inline]
+def erase (headers : Headers) (name : String) : Headers :=
+  { data := headers.data.erase name.toLower }
+
+/--
+Gets the number of headers.
+-/
+@[inline]
+def size (headers : Headers) : Nat :=
+  headers.data.size
+
+/--
+Checks if the headers are empty.
+-/
+@[inline]
+def isEmpty (headers : Headers) : Bool :=
+  headers.data.isEmpty
+
+/--
+Merges two headers, with the second taking precedence for duplicate keys.
+-/
+def merge (headers1 headers2 : Headers) : Headers :=
+  { data := headers2.data.fold (fun acc k v => acc.insert k.toLower v) headers1.data }

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

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init.Data
+import Std.Internal.Http.Encode
+
+namespace Std
+namespace Http
+namespace Data
+
+/-
+A method is a verb that describes the action to be performed.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#methods
+-/
+inductive Method where
+  | get
+  | head
+  | post
+  | put
+  | delete
+  | connect
+  | options
+  | trace
+  | patch
+  deriving Repr, Inhabited, BEq
+
+instance : ToString Method where
+  toString
+    | .get => "GET"
+    | .head => "HEAD"
+    | .post => "POST"
+    | .put => "PUT"
+    | .delete => "DELETE"
+    | .connect => "CONNECT"
+    | .options => "OPTIONS"
+    | .trace => "TRACE"
+    | .patch => "PATCH"
+
+instance : Encode .v11 Method where
+  encode buffer := buffer.writeString ∘ toString
+
+namespace Method
+
+/--
+Converts a `String` into a `Method`.
+-/
+def fromString? : String → Option Method
+  | "GET" => some .get
+  | "HEAD" => some .head
+  | "POST" => some .post
+  | "PUT" => some .put
+  | "DELETE" => some .delete
+  | "CONNECT" => some .connect
+  | "OPTIONS" => some .options
+  | "TRACE" => some .trace
+  | "PATCH" => some .patch
+  | _ => none
+
+/--
+Request methods are considered safe if their defined semantics are essentially read-only.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#metho  d.properties
+-/
+def isSafe : Method → Prop
+  | .get | .head | .options | .trace => True
+  | _ => False
+
+/--
+A request method is considered idempotent if the intended effect on the server of multiple
+identical requests with that method is the same as the effect for a single such request.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#idempotent.methods
+-/
+def isIdempotent : Method → Prop
+  | .get | .head | .options | .trace => True
+  | .put | .delete => True
+  | _ => False
+
+/--
+Checks if the given method allows a request body. GET and HEAD methods do not typically allow
+request bodies.
+
+* Reference: https://developer.mozilla.org/en-US/docs/Web/HTTP/Methods
+-/
+def allowsRequestBody : Method → Prop
+  | .get | .head => False
+  | _ => True
+
+end Method
+end Data
+end Http
+end Std

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

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+import Std.Internal.Http.Encode
+import Std.Internal.Http.Data.Headers
+import Std.Internal.Http.Data.Method
+import Std.Internal.Http.Data.Version
+
+namespace Std
+namespace Http
+namespace Data
+
+structure Request (t : Type) where
+  method : Method
+  version : Version
+  uri : String
+  headers : Headers
+  body : t
+
+instance : ToString (Request t) where
+  toString req :=
+    toString req.method ++ " " ++
+    req.uri ++ " " ++
+    toString req.version ++
+    "\r\n" ++
+    toString req.headers ++ "\r\n\r\n"

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

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+import Std.Internal.Http.Encode
+import Std.Internal.Http.Data.Status
+import Std.Internal.Http.Data.Headers
+import Std.Internal.Http.Data.Version
+
+namespace Std
+namespace Http
+namespace Data
+
+structure Response (t : Type) where
+  status : Status
+  version : Version
+  headers : Headers
+  body : t
+deriving Inhabited
+
+instance : ToString (Response t) where
+  toString r :=
+    toString r.version ++ " " ++
+    toString r.status.toCode ++ " " ++
+    toString r.status ++ "\r\n" ++
+    toString r.headers ++ "\r\n\r\n"

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

@@ -0,0 +1,597 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+import Std.Internal.Http.Encode
+
+namespace Std
+namespace Http
+namespace Data
+
+set_option linter.all true
+
+/--
+HTTP Status codes. Status codes are three-digit integer codes that describes the result of a
+HTTP request. In this implementation we do not treat status code as extensible.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+ -/
+inductive Status where
+
+  /--
+  100 Continue
+  -/
+  | «continue»
+
+  /--
+  101 Switching Protocols
+  -/
+  | switchingProtocols
+
+  /--
+  102 Processing
+  -/
+  | processing
+
+  /--
+  103 Early Hints
+  -/
+  | earlyHints
+
+  /--
+  200 OK
+  -/
+  | ok
+
+  /--
+  201 Created
+  -/
+  | created
+
+  /--
+  202 Accepted
+  -/
+  | accepted
+
+  /--
+  203 Non-Authoritative Information
+  -/
+  | nonAuthoritativeInformation
+
+  /--
+  204 No Content
+  -/
+  | noContent
+
+  /--
+  205 Reset Content
+  -/
+  | resetContent
+
+  /--
+  206 Partial Content
+  -/
+  | partialContent
+
+  /--
+  207 Multi-Status
+  -/
+  | multiStatus
+
+  /--
+  208 Already Reported
+  -/
+  | alreadyReported
+
+  /--
+  226 IM Used
+  -/
+  | imUsed
+
+  /--
+  300 Multiple Choices
+  -/
+  | multipleChoices
+
+  /--
+  301 Moved Permanently
+  -/
+  | movedPermanently
+
+  /--
+  302 Found
+  -/
+  | found
+
+  /--
+  303 See Other
+  -/
+  | seeOther
+
+  /--
+  304 Not Modified
+  -/
+  | notModified
+
+  /--
+  305 Use Proxy
+  -/
+  | useProxy
+
+  /--
+  306 Unused
+  -/
+  | unused
+
+  /--
+  307 Temporary Redirect
+  -/
+  | temporaryRedirect
+
+  /--
+  308 Permanent Redirect
+  -/
+  | permanentRedirect
+
+  /--
+  400 Bad Request
+  -/
+  | badRequest
+
+  /--
+  401 Unauthorized
+  -/
+  | unauthorized
+
+  /--
+  402 Payment Required
+  -/
+  | paymentRequired
+
+  /--
+  403 Forbidden
+  -/
+  | forbidden
+
+  /--
+  404 Not Found
+  -/
+  | notFound
+
+  /--
+  405 Method Not Allowed
+  -/
+  | methodNotAllowed
+
+  /--
+  406 Not Acceptable
+  -/
+  | notAcceptable
+
+  /--
+  407 Proxy Authentication Required
+  -/
+  | proxyAuthenticationRequired
+
+  /--
+  408 Request Timeout
+  -/
+  | requestTimeout
+
+  /--
+  409 Conflict
+  -/
+  | conflict
+
+  /--
+  410 Gone
+  -/
+  | gone
+
+  /--
+  411 Length Required
+  -/
+  | lengthRequired
+
+  /--
+  412 Precondition Failed
+  -/
+  | preconditionFailed
+
+  /--
+  413 Payload Too Large
+  -/
+  | payloadTooLarge
+
+  /--
+  414 URI Too Long
+  -/
+  | uriTooLong
+
+  /--
+  415 Unsupported Media Type
+  -/
+  | unsupportedMediaType
+
+  /--
+  416 Range Not Satisfiable
+  -/
+  | rangeNotSatisfiable
+
+  /--
+  417 Expectation Failed
+  -/
+  | expectationFailed
+
+  /--
+  418 I'm a teapot
+  -/
+  | imATeapot
+
+  /--
+  421 Misdirected Request
+  -/
+  | misdirectedRequest
+
+  /--
+  422 Unprocessable Entity
+  -/
+  | unprocessableEntity
+
+  /--
+  423 Locked
+  -/
+  | locked
+
+  /--
+  424 Failed Dependency
+  -/
+  | failedDependency
+
+  /--
+  425 Too Early
+  -/
+  | tooEarly
+
+  /--
+  426 Upgrade Required
+  -/
+  | upgradeRequired
+
+  /--
+  428 Precondition Required
+  -/
+  | preconditionRequired
+
+  /--
+  429 Too Many Requests
+  -/
+  | tooManyRequests
+
+  /--
+  431 Request Header Fields Too Large
+  -/
+  | requestHeaderFieldsTooLarge
+
+  /--
+  451 Unavailable For Legal Reasons
+  -/
+  | unavailableForLegalReasons
+
+  /--
+  500 Internal Server Error
+  -/
+  | internalServerError
+
+  /--
+  501 Not Implemented
+  -/
+  | notImplemented
+
+  /--
+  502 Bad Gateway
+  -/
+  | badGateway
+
+  /--
+  503 Service Unavailable
+  -/
+  | serviceUnavailable
+
+  /--
+  504 Gateway Timeout
+  -/
+  | gatewayTimeout
+
+  /--
+  505 HTTP Version Not Supported
+  -/
+  | httpVersionNotSupported
+
+  /--
+  506 Variant Also Negotiates
+  -/
+  | variantAlsoNegotiates
+
+  /--
+  507 Insufficient Storage
+  -/
+  | insufficientStorage
+
+  /--
+  508 Loop Detected
+  -/
+  | loopDetected
+
+  /--
+  510 Not Extended
+  -/
+  | notExtended
+
+  /--
+  511 Network Authentication Required
+  -/
+  | networkAuthenticationRequired
+deriving Repr, Inhabited
+
+instance : ToString Status where
+  toString
+    | .«continue» => "Continue"
+    | .switchingProtocols => "Switching Protocols"
+    | .processing => "Processing"
+    | .earlyHints => "Early Hints"
+    | .ok => "OK"
+    | .created => "Created"
+    | .accepted => "Accepted"
+    | .nonAuthoritativeInformation => "Non-Authoritative Information"
+    | .noContent => "No Content"
+    | .resetContent => "Reset Content"
+    | .partialContent => "Partial Content"
+    | .multiStatus => "Multi-Status"
+    | .alreadyReported => "Already Reported"
+    | .imUsed => "IM Used"
+    | .multipleChoices => "Multiple Choices"
+    | .movedPermanently => "Moved Permanently"
+    | .found => "Found"
+    | .seeOther => "See Other"
+    | .notModified => "Not Modified"
+    | .useProxy => "Use Proxy"
+    | .unused => "Unused"
+    | .temporaryRedirect => "Temporary Redirect"
+    | .permanentRedirect => "Permanent Redirect"
+    | .badRequest => "Bad Request"
+    | .unauthorized => "Unauthorized"
+    | .paymentRequired => "Payment Required"
+    | .forbidden => "Forbidden"
+    | .notFound => "Not Found"
+    | .methodNotAllowed => "Method Not Allowed"
+    | .notAcceptable => "Not Acceptable"
+    | .proxyAuthenticationRequired => "Proxy Authentication Required"
+    | .requestTimeout => "Request Timeout"
+    | .conflict => "Conflict"
+    | .gone => "Gone"
+    | .lengthRequired => "Length Required"
+    | .preconditionFailed => "Precondition Failed"
+    | .payloadTooLarge => "Request Entity Too Large"
+    | .uriTooLong => "Request URI Too Long"
+    | .unsupportedMediaType => "Unsupported Media Type"
+    | .rangeNotSatisfiable => "Requested Range Not Satisfiable"
+    | .expectationFailed => "Expectation Failed"
+    | .imATeapot => "I'm a teapot"
+    | .misdirectedRequest => "Misdirected Request"
+    | .unprocessableEntity => "Unprocessable Entity"
+    | .locked => "Locked"
+    | .failedDependency => "Failed Dependency"
+    | .tooEarly => "Too Early"
+    | .upgradeRequired => "Upgrade Required"
+    | .preconditionRequired => "Precondition Required"
+    | .tooManyRequests => "Too Many Requests"
+    | .requestHeaderFieldsTooLarge => "Request Header Fields Too Large"
+    | .unavailableForLegalReasons => "Unavailable For Legal Reasons"
+    | .internalServerError => "Internal Server Error"
+    | .notImplemented => "Not Implemented"
+    | .badGateway => "Bad Gateway"
+    | .serviceUnavailable => "Service Unavailable"
+    | .gatewayTimeout => "Gateway Timeout"
+    | .httpVersionNotSupported => "HTTP Version Not Supported"
+    | .variantAlsoNegotiates => "Variant Also Negotiates"
+    | .insufficientStorage => "Insufficient Storage"
+    | .loopDetected => "Loop Detected"
+    | .notExtended => "Not Extended"
+    | .networkAuthenticationRequired => "Network Authentication Required"
+
+namespace Status
+
+/--
+Convert a Status to a numeric code. This is useful for sending the status code in a response.
+-/
+def toCode : Status -> UInt16
+  | «continue» => 100
+  | switchingProtocols => 101
+  | processing => 102
+  | earlyHints => 103
+  | ok => 200
+  | created => 201
+  | accepted => 202
+  | nonAuthoritativeInformation => 203
+  | noContent => 204
+  | resetContent => 205
+  | partialContent => 206
+  | multiStatus => 207
+  | alreadyReported => 208
+  | imUsed => 226
+  | multipleChoices => 300
+  | movedPermanently => 301
+  | found => 302
+  | seeOther => 303
+  | notModified => 304
+  | useProxy => 305
+  | unused => 306
+  | temporaryRedirect => 307
+  | permanentRedirect => 308
+  | badRequest => 400
+  | unauthorized => 401
+  | paymentRequired => 402
+  | forbidden => 403
+  | notFound => 404
+  | methodNotAllowed => 405
+  | notAcceptable => 406
+  | proxyAuthenticationRequired => 407
+  | requestTimeout => 408
+  | conflict => 409
+  | gone => 410
+  | lengthRequired => 411
+  | preconditionFailed => 412
+  | payloadTooLarge => 413
+  | uriTooLong => 414
+  | unsupportedMediaType => 415
+  | rangeNotSatisfiable => 416
+  | expectationFailed => 417
+  | imATeapot => 418
+  | misdirectedRequest => 421
+  | unprocessableEntity => 422
+  | locked => 423
+  | failedDependency => 424
+  | tooEarly => 425
+  | upgradeRequired => 426
+  | preconditionRequired => 428
+  | tooManyRequests => 429
+  | requestHeaderFieldsTooLarge => 431
+  | unavailableForLegalReasons => 451
+  | internalServerError => 500
+  | notImplemented => 501
+  | badGateway => 502
+  | serviceUnavailable => 503
+  | gatewayTimeout => 504
+  | httpVersionNotSupported => 505
+  | variantAlsoNegotiates => 506
+  | insufficientStorage => 507
+  | loopDetected => 508
+  | notExtended => 510
+  | networkAuthenticationRequired => 511
+
+/--
+Converts an `UInt16` to a `Status`.
+-/
+def fromCode? : UInt16 → Option Status
+  | 100 => some «continue»
+  | 101 => some switchingProtocols
+  | 102 => some processing
+  | 103 => some earlyHints
+  | 200 => some ok
+  | 201 => some created
+  | 202 => some accepted
+  | 203 => some nonAuthoritativeInformation
+  | 204 => some noContent
+  | 205 => some resetContent
+  | 206 => some partialContent
+  | 207 => some multiStatus
+  | 208 => some alreadyReported
+  | 226 => some imUsed
+  | 300 => some multipleChoices
+  | 301 => some movedPermanently
+  | 302 => some found
+  | 303 => some seeOther
+  | 304 => some notModified
+  | 305 => some useProxy
+  | 306 => some unused
+  | 307 => some temporaryRedirect
+  | 308 => some permanentRedirect
+  | 400 => some badRequest
+  | 401 => some unauthorized
+  | 402 => some paymentRequired
+  | 403 => some forbidden
+  | 404 => some notFound
+  | 405 => some methodNotAllowed
+  | 406 => some notAcceptable
+  | 407 => some proxyAuthenticationRequired
+  | 408 => some requestTimeout
+  | 409 => some conflict
+  | 410 => some gone
+  | 411 => some lengthRequired
+  | 412 => some preconditionFailed
+  | 413 => some payloadTooLarge
+  | 414 => some uriTooLong
+  | 415 => some unsupportedMediaType
+  | 416 => some rangeNotSatisfiable
+  | 417 => some expectationFailed
+  | 418 => some imATeapot
+  | 421 => some misdirectedRequest
+  | 422 => some unprocessableEntity
+  | 423 => some locked
+  | 424 => some failedDependency
+  | 425 => some tooEarly
+  | 426 => some upgradeRequired
+  | 428 => some preconditionRequired
+  | 429 => some tooManyRequests
+  | 431 => some requestHeaderFieldsTooLarge
+  | 451 => some unavailableForLegalReasons
+  | 500 => some internalServerError
+  | 501 => some notImplemented
+  | 502 => some badGateway
+  | 503 => some serviceUnavailable
+  | 504 => some gatewayTimeout
+  | 505 => some httpVersionNotSupported
+  | 506 => some variantAlsoNegotiates
+  | 507 => some insufficientStorage
+  | 508 => some loopDetected
+  | 510 => some notExtended
+  | 511 => some networkAuthenticationRequired
+  | _   => none
+
+/--
+Checks if the type of the status code is informational, meaning that the request was received
+and the process is continuing.
+-/
+@[inline]
+def isInformational (c : Status) : Prop :=
+  c.toCode < 200
+
+/--
+Checks if the type of the status code is success, meaning that the request was successfully received,
+understood, and accepted.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+@[inline]
+def isSuccess (c : Status) : Prop :=
+  200 ≤ c.toCode ∧ c.toCode < 300
+
+/--
+Checks if the type of the status code is redirection, meaning that further action needs to be taken
+to complete the request.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+@[inline]
+def isRedirection (c : Status) : Prop :=
+  300 ≤ c.toCode ∧ c.toCode < 400
+
+/--
+Checks if the type of the status code is a client error, meaning that the request contains bad syntax
+or cannot be fulfilled.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+@[inline]
+def isClientError (c : Status) : Prop :=
+  400 ≤ c.toCode ∧ c.toCode < 500
+
+/--
+Checks if the type of the status code is a server error, meaning that the server failed to fulfill
+an apparently valid request.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+@[inline]
+def isServerError (c : Status) : Prop :=
+  500 ≤ c.toCode ∧ c.toCode < 600
+
+instance : Encode .v11 Status where
+  encode buffer status := buffer
+    |>.writeString (toString <| toCode status)
+    |>.writeChar ' '
+    |>.writeString (toString status)

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

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+
+namespace Std
+namespace Http
+namespace Data

src/Std/Internal/Http/Data/Version.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
+-/
+prelude
+import Init
+
+namespace Std
+namespace Http
+namespace Data
+
+set_option linter.all true
+
+/--
+The 'Version' structure represents an HTTP version with a major and minor number. It includes
+several standard versions of the HTTP protocol, such as HTTP/1.1, HTTP/2.0, and
+HTTP/3.0.
+
+* Reference: https://httpwg.org/specs/rfc9110.html#protocol.version
+-/
+inductive Version
+
+  /--
+  `HTTP/1.1`
+  -/
+  | v11
+
+  /--
+  `HTTP/2.0`
+  -/
+  | v20
+
+  /--
+  `HTTP/3.0`
+  -/
+  | v30
+
+deriving Repr, Inhabited, BEq, DecidableEq
+
+instance : ToString Version where
+  toString
+    | .v11 => "HTTP/1.1"
+    | .v20 => "HTTP/2.0"
+    | .v30 => "HTTP/3.0"
+
+namespace Version
+
+/--
+Converts a pair of `Nat` to the corresponding `Version`.
+-/
+def fromNumber? : Nat → Nat → Option Version
+  | 1, 1 => some .v11
+  | 2, 0 => some .v20
+  | 3, 0 => some .v30
+  | _, _ => none
+
+/--
+Converts `String` to the corresponding `Version`.
+-/
+def fromString? : String → Option Version
+  | "HTTP/1.1" => some .v11
+  | "HTTP/2.0" => some .v20
+  | "HTTP/3.0" => some .v30
+  | _ => none
+
+/--
+Converts a `Version` to its corresponding major and minor numbers as a pair.
+-/
+def toNumber : Version → (Nat × Nat)
+  | .v11 => (1, 1)
+  | .v20 => (2, 0)
+  | .v30 => (3, 0)

src/Std/Internal/Http/Encode.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+import Std.Internal.Http.Buffer
+import Std.Internal.Http.Data.Version
+
+namespace Std
+namespace Http
+
+set_option linter.all true
+
+/--
+Serializes a type `t` to a `Buffer` containing its canonical HTTP representation
+for protocol version `v`.
+-/
+class Encode (v : Data.Version) (t : Type) where
+
+  /--
+  Encodes a type `t` to a `Buffer`.
+  -/
+  encode : Buffer → t → Buffer
+
+instance : Encode .v11 Data.Version where
+  encode buffer := buffer.writeString ∘ toString

src/Std/Internal/Http/Listener.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+
+namespace Std
+namespace Http
+
+set_option linter.all true

src/Std/Internal/Http/V11/Machine.lean

@@ -0,0 +1,872 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init
+import Std.Internal.Http.Data.Headers
+import Std.Internal.Http.Data.Request
+import Std.Internal.Http.Data.Response
+import Std.Internal.Http.Data.Body
+import Std.Internal.Http.V11.Parser
+
+/-!
+# HTTP/1.1 State Machine
+
+This module implements a streaming HTTP/1.1 state machine that can handle both request and response
+parsing and generation. The machine operates in two modes:
+
+- **Request mode**: Parses incoming HTTP requests and generates responses
+- **Response mode**: Parses incoming HTTP responses (useful for client implementations)
+-/
+
+open Std.Internal.Parsec.ByteArray (Parser)
+
+namespace Std
+namespace Http
+namespace V11
+
+set_option linter.all true
+
+/--
+Connection limits configuration with validation.
+-/
+structure Config where
+  /--
+  Maximum number of requests per connection.
+  -/
+  maxRequests : Nat := 100
+
+  /--
+  Maximum number of headers allowed per request.
+  -/
+  maxHeaders : Nat := 50
+
+  /--
+  Maximum size of a single header value.
+  -/
+  maxHeaderSize : Nat := 8192
+
+  /--
+  Connection timeout in seconds.
+  -/
+  timeoutSeconds : Nat := 10
+
+  /--
+  Whether to enable keep-alive connections by default.
+  -/
+  enableKeepAlive : Bool := true
+
+  /--
+  Whether to enable chunked transfer encoding.
+  -/
+  enableChunked : Bool := true
+
+  /--
+  Size threshold for flushing output buffer.
+  -/
+  highMark : Nat := 4096
+
+/--
+This is the mode that is used by the machine to check the input and output.
+-/
+inductive Mode
+  /--
+  Request mode - machine expects to receive HTTP requests
+  -/
+  | request
+
+  /--
+  Response mode - machine expects to receive HTTP responses
+  -/
+  | response
+
+namespace Mode
+
+/--
+Inverts the mode.
+-/
+def inverse : Mode → Mode
+  | .request => .response
+  | .response => .request
+
+end Mode
+
+/--
+Determines the type of the status line based on the Mode.
+-/
+abbrev StatusLine : Mode → Type
+  | .request => Data.Method × String × Data.Version
+  | .response => Data.Version × Data.Status × String
+
+instance : Repr (StatusLine m) where
+  reprPrec r s :=
+    match m with
+    | .request => reprPrec r s
+    | .response => reprPrec r s
+
+/--
+Determines the type of the status line based on the Mode.
+-/
+abbrev Message (t : Type) : Mode → Type
+  | .request => Data.Request t
+  | .response => Data.Response t
+
+instance : ToString (Message t m) where
+  toString r :=
+    match m with
+    | .request => toString r
+    | .response => toString r
+
+namespace Message
+
+/--
+Extracts headers from a message regardless of mode.
+-/
+def headers (message : Message t mode) : Data.Headers :=
+  match mode with
+  | .request => Data.Request.headers message
+  | .response => Data.Response.headers message
+
+/--
+Adds a header to a message regardless of mode.
+-/
+def addHeader (message : Message t mode) (k : String) (v : String) : Message t mode :=
+  match mode with
+  | .request => { message with headers := message.headers.insert k v }
+  | .response => { message with headers := message.headers.insert k v }
+
+end Message
+
+/--
+Represents the expected size encoding for HTTP message body
+-/
+inductive Size
+  /--
+  Fixed size body with known byte count
+  -/
+  | fixed (n : Nat)
+
+  /--
+  Chunked transfer encoding
+  -/
+  | chunked
+
+deriving Repr, Inhabited
+
+/--
+Specific HTTP processing errors with detailed information.
+-/
+inductive Error where
+  /--
+  Malformed request line or status line.
+  -/
+  | invalidStatusLine
+
+  /--
+  Invalid or malformed header.
+  -/
+  | invalidHeader
+
+  /--
+  Request timeout occurred.
+  -/
+  | timeout
+
+  /--
+  Request entity too large.
+  -/
+  | entityTooLarge
+
+  /--
+  Unsupported HTTP method.
+  -/
+  | unsupportedMethod
+
+  /--
+  Unsupported HTTP version.
+  -/
+  | unsupportedVersion
+
+  /--
+  Invalid chunk encoding.
+  -/
+  | invalidChunk
+
+  /--
+  Bad request
+  -/
+  | badRequest
+  /--
+  Generic error with message.
+  -/
+  | other (message : String)
+deriving Repr, BEq
+
+/--
+Creates appropriate error response based on error type.
+-/
+private def Error.toResponse (error : Error) : Data.Response Data.Body :=
+  let (status, body) := match error with
+    | .badRequest => (Data.Status.badRequest, none)
+    | .invalidStatusLine => (.badRequest, none)
+    | .invalidHeader => (.badRequest, none)
+    | .timeout => (.requestTimeout, none)
+    | .entityTooLarge => (.payloadTooLarge, none)
+    | .unsupportedMethod => (.methodNotAllowed, none)
+    | .unsupportedVersion => (.httpVersionNotSupported, none)
+    | .invalidChunk => (.badRequest, none)
+    | .other msg => (.internalServerError, some msg)
+
+  { status := status,
+    version := .v11,
+    headers := .empty,
+    body := body <&> (Data.Body.bytes ∘ ByteSlice.ofByteArray ∘ String.toUTF8) |>.getD .zero }
+
+/--
+Events that can occur during HTTP message processing.
+-/
+inductive Event (mode : Mode)
+  /--
+  Event received when chunk extension data is encountered in chunked encoding.
+  -/
+  | chunkExt (ext : ByteSlice)
+
+  /--
+  Event received the headers end.
+  -/
+  | endHeaders (size : Size)
+
+  /--
+  Event received when some data arrives from the received thing.
+  -/
+  | gotData (final : Bool) (data : ByteSlice)
+
+  /--
+  Need more data is an event that arrives when the input ended and it requires more
+  data to continue
+  -/
+  | needMoreData
+
+  /--
+  Event received when all request data has been parsed and ready to send response.
+  -/
+  | readyToRespond
+
+  /--
+  Event received when it requires more data to continue
+  -/
+  | awaitingAnswer
+
+  /--
+  Event received when parsing or processing fails with an error message.
+  -/
+  | failed (reason : Error)
+
+  /--
+  Event received when connection should be closed.
+  -/
+  | close
+
+  /--
+  Awaiting the next request
+  -/
+  | next
+deriving Repr, Inhabited
+
+/--
+State of the `Machine`.
+-/
+inductive State : Type
+  /--
+  Initial state waiting for HTTP status line.
+  -/
+  | needStatusLine : State
+
+  /--
+  State waiting for HTTP headers, tracking number of headers parsed.
+  -/
+  | needHeader : Nat → State
+
+  /--
+  State waiting for chunk size in chunked transfer encoding.
+  -/
+  | needChunkedSize : State
+
+  /--
+  State waiting for chunk body data of specified size.
+  -/
+  | needChunkedBody : Nat → State
+
+  /--
+  State waiting for fixed-length body data of specified size.
+  -/
+  | needFixedBody : Nat → State
+
+  /--
+  State when request is fully parsed and ready to generate response.
+  -/
+  | readyToAnswer : State
+
+  /--
+  State when the response can send data.
+  -/
+  | awaitingAnswer
+
+  /--
+  State waiting for connection to close after response sent.
+  -/
+  | awaitingClose : State
+
+  /--
+  Final state when connection is closed.
+  -/
+  | closed
+
+  /--
+  Ready for next request.
+  -/
+  | next
+
+  /--
+  Failed state with error.
+  -/
+  | failed (error : Error)
+deriving Inhabited, Repr, BEq
+
+/--
+The state machine that receives some input bytes and outputs bytes for the HTTP 1.1 protocol.
+-/
+structure Machine (mode : Mode) where
+
+  /--
+  The current state of the machine
+  -/
+  state : State := .needStatusLine
+
+  /--
+  The input status line.
+  -/
+  inputStatusLine : Option (StatusLine mode) := none
+
+  /--
+  The input headers.
+  -/
+  inputHeaders : Data.Headers := .empty
+
+  /--
+  The output status line.
+  -/
+  outputMessage : Option (Message Data.Body mode.inverse) := none
+
+  /--
+  The output headers.
+  -/
+  outputHeaders : Data.Headers := .empty
+
+  /--
+  If the headers has been sent.
+  -/
+  sentOutputHead : Bool := false
+
+  /--
+  This is the buffer that we receive from the user
+  -/
+  inputBuffer : ByteArray.Iterator := (ByteArray.emptyWithCapacity 4096).iter
+
+  /--
+  This is the buffer that we are going to output for the user.
+  -/
+  outputBuffer : ByteArray := .empty
+
+  /--
+  Chunked data to send in the future
+  -/
+  chunkedData : ByteArray := .empty
+
+  /--
+  The event that the machine produced.
+  -/
+  event : Option (Event mode) := some .needMoreData
+
+  /--
+  The minimum size of the body
+  -/
+  size : Option UInt64 := none
+
+  /--
+  Machine configuration.
+  -/
+  config : Config := {}
+
+  /--
+  Amount of requests parsed.
+  -/
+  requestCount : Nat := 0
+
+  /--
+  Whether response uses chunked encoding.
+  -/
+  chunkedAnswer : Bool := false
+
+  /--
+  Whether connection should be kept alive.
+  -/
+  keepAlive : Bool := true
+
+namespace Machine
+
+/--
+Result of parsing operation on input buffer
+-/
+inductive ParseResult (α : Type) where
+  /--
+  Reached end of input buffer without complete parse
+  -/
+  | eof
+
+  /--
+  Successfully parsed value with remaining buffer
+  -/
+  | ok (x : α) (b : ByteArray.Iterator)
+
+  /--
+  Parse failed with error
+  -/
+  | err (err : Error)
+
+/--
+Sets machine to failed state with specific error.
+-/
+def setError (machine : Machine mode) (error : Error) : Machine mode :=
+  { machine with state := .failed error, event := some (.failed error) }
+
+/--
+Sets the event in the machine.
+-/
+private def addEvent (machine : Machine mode) (event : Event mode) : Machine mode :=
+  { machine with event := some event }
+
+/--
+Sets the status in the machine.
+-/
+private def setState (machine : Machine mode) (state : State) : Machine mode :=
+  { machine with state }
+
+/--
+Common parsing wrapper that handles errors and EOF consistently.
+-/
+private def parseWith (machine : Machine mode) (parser : Parser α) : (Machine mode × Option α) :=
+  match parser machine.inputBuffer with
+  | .success buffer reqLine => ({ machine with inputBuffer := buffer }, some reqLine)
+  | .error _ .eof =>  (machine.addEvent .needMoreData, none)
+  | .error _ _ => (machine.setError .badRequest, none)
+
+/--
+Converts raw byte digits to HTTP version.
+-/
+private def parseVersion (major minor : UInt8) : Option Data.Version :=
+  Data.Version.fromNumber? (major.toNat - 48) (minor.toNat - 48)
+
+/--
+Validates that HTTP version is supported by machine configuration.
+-/
+private def validateVersion (version : Data.Version) : Bool :=
+  version == .v11
+
+/--
+Parses HTTP request line into status line format.
+-/
+private def parseRequestStatusLine (raw : Parser.RequestLine) : Option (StatusLine .request) := do
+  let version ← parseVersion raw.major raw.minor
+  guard (validateVersion version)
+  let method ← Data.Method.fromString? =<< String.fromUTF8? raw.method.toByteArray
+  let uri ← String.fromUTF8? raw.uri.toByteArray
+  pure (method, uri, version)
+
+/--
+Parses HTTP response status line into status line format.
+-/
+private def parseResponseStatusLine (raw : Parser.StatusLine) : Option (StatusLine .response) := do
+  let version ← parseVersion raw.major raw.minor
+  guard (validateVersion version)
+  let status ← Data.Status.fromCode? raw.statusCode.toUInt16
+  let reason ← String.fromUTF8? raw.reasonPhrase.toByteArray
+  pure (version, status, reason)
+
+/--
+Common parsing workflow for status lines.
+-/
+private def parseStatusWith
+  (machine : Machine mode)
+  (parser : Parser α)
+  (transform : α → Option (StatusLine mode))
+  : (Machine mode × Option (StatusLine mode)) :=
+    let (machine, result) := parseWith machine parser
+    if let some result := result then
+      (machine, transform result)
+    else
+      (machine, none)
+
+/--
+Parses HTTP status line based on machine mode.
+-/
+private def parseStatusLine (machine : Machine mode) : (Machine mode × Option (StatusLine mode)) :=
+  match mode with
+  | .request => parseStatusWith machine Parser.parseRequestLine parseRequestStatusLine
+  | .response => parseStatusWith machine Parser.parseStatusLine parseResponseStatusLine
+
+/--
+Formats a chunk for chunked transfer encoding.
+-/
+private def formatChunk (data : ByteArray) : ByteArray :=
+  let sizeHex := (Nat.toDigits 16 data.size) |>.toArray |>.map Char.toUInt8 |> ByteArray.mk
+  sizeHex ++ "\r\n".toUTF8 ++ data ++ "\r\n".toUTF8
+
+/--
+Formats the final chunk for chunked transfer encoding.
+-/
+private def formatFinalChunk : ByteArray :=
+  "0\r\n\r\n".toUTF8
+
+/--
+Validates headers and determines body encoding type.
+-/
+private def validateHeaders (mode : Mode) (headers : Data.Headers) : Option Size := do
+  let hostValid : Bool := match mode with
+    | .request => headers.get? "host" |>.isSome
+    | .response => true
+
+  guard hostValid
+
+  match (headers.getSingle? "Content-Length", headers.get? "Transfer-Encoding") with
+  | (some cl, none) => do
+    let num ← cl.toNat?
+    some (.fixed num)
+  | (none, some hs) =>
+    if hs.contains "chunked" then
+      some .chunked
+    else
+      some (.fixed 0)
+  | (none, none) =>
+    some (.fixed 0)
+  | _ => none
+
+/--
+Resets the machine for a new request on the same connection (keep-alive)
+-/
+private def reset (machine : Machine mode) : Machine mode :=
+  { machine with
+    state := .needStatusLine,
+    inputStatusLine := none,
+    inputHeaders := .empty,
+    outputMessage := none,
+    outputHeaders := .empty,
+    sentOutputHead := false,
+    inputBuffer := ByteArray.empty.iter,
+    outputBuffer := .empty,
+    chunkedData := .empty,
+    event := some .needMoreData,
+    requestCount := machine.requestCount + 1 }
+
+/--
+Checks if the machine is in a terminal state that requires flushing.
+-/
+private def isTerminalState (machine : Machine mode) : Bool :=
+  match machine.state with
+  | .closed => true
+  | .failed _ => true
+  | .next => true
+  | _ => false
+/--
+Checks if output buffer exceeds high water mark and needs flushing.
+-/
+def needsFlush (machine : Machine mode) : Bool :=
+  machine.outputBuffer.size >= machine.config.highMark
+  || isTerminalState machine
+
+/--
+Modify message headers based on the given size.
+-/
+private def addSizeHeader (msg : Message t mode) (size : Size) : Message t mode :=
+  match size with
+  | .chunked => msg.addHeader "Transfer-Encoding" "chunked"
+  | .fixed 0 => msg
+  | .fixed n => msg.addHeader "Content-Length" (toString n)
+
+/--
+Modify message headers based on the given size.
+-/
+private def isChunked (size : Size) : Bool :=
+  match size with
+  | .chunked => true
+  | .fixed _ => false
+
+/--
+Adds the message header to the output buffer if not already sent.
+-/
+private def sendOutputHead (machine : Machine mode) (size : Size) : Machine mode :=
+  if machine.sentOutputHead then
+    machine
+  else
+   match machine.outputMessage with
+    | some msg =>
+      let outputMessage := addSizeHeader msg size
+      { machine with
+        outputMessage,
+        outputBuffer := machine.outputBuffer ++ (toString outputMessage).toUTF8,
+        chunkedAnswer := isChunked size,
+        sentOutputHead := true }
+    | none => machine
+
+/--
+Appends data to output buffer based on encoding type.
+-/
+def appendToOutputBuffer (machine : Machine mode) (data : ByteArray) (size : Size) : Machine mode :=
+  let dataToAppend :=
+    match size with
+    | .chunked => formatChunk data
+    | .fixed _ => data
+  { machine with outputBuffer := machine.outputBuffer.append dataToAppend }
+
+/--
+Writes data to the output buffer, ensuring the message head is sent first.
+-/
+def writeToOutputBuffer (machine : Machine mode) (data : ByteArray) (size : Size) : Machine mode :=
+  machine
+  |>.sendOutputHead size
+  |>.appendToOutputBuffer data size
+
+/--
+Checks if chunked data should be flushed based on size and force flag.
+-/
+def shouldFlushChunkedData (machine : Machine mode) (force : Bool) : Bool :=
+  force || machine.chunkedData.size >= machine.config.highMark
+
+/--
+Writes data to the local buffer. Encoding decision is deferred until flush time.
+-/
+def writeData (machine : Machine mode) (data : ByteArray) : Machine mode :=
+  { machine with chunkedData := machine.chunkedData ++ data }
+
+/--
+Flushes the output buffer and returns the data to send.
+-/
+def flush (machine : Machine mode) (final : Bool := false) : Machine mode × ByteArray :=
+  -- Only flush if we hit highMark or it's final
+  if machine.chunkedData.size >= machine.config.highMark || final then
+    let machine :=
+      if !machine.chunkedData.isEmpty then
+        if final then
+          dbg_trace "ha the size {machine.chunkedData.size}"
+          -- Final flush: use Content-Length
+          let size := Size.fixed machine.chunkedData.size
+          let machine := sendOutputHead machine size
+          let machine := appendToOutputBuffer machine machine.chunkedData size
+          { machine with chunkedData := .empty }
+        else
+          -- Non-final flush: use chunked encoding
+          dbg_trace "ha the chunk size {machine.chunkedData.size}"
+          let machine := sendOutputHead machine Size.chunked
+          let machine := appendToOutputBuffer machine machine.chunkedData Size.chunked
+          { machine with chunkedData := .empty }
+      else if final then
+        -- Final flush with no buffered data
+          dbg_trace "ha the none size {machine.chunkedData.size}"
+        let machine := sendOutputHead machine (Size.fixed 0)
+        machine
+      else
+        machine
+
+    -- Add final chunk marker if needed
+    let machine :=
+      if final && machine.sentOutputHead then
+        match machine.outputMessage with
+        | some msg =>
+          if msg.headers.get? "Transfer-Encoding" |>.any (·.contains "chunked") then
+            { machine with outputBuffer := machine.outputBuffer ++ formatFinalChunk }
+          else machine
+        | none => machine
+      else machine
+
+    let data := machine.outputBuffer
+    let machine := { machine with outputBuffer := .empty }
+    (machine, data)
+  else
+    -- Don't flush yet, just return empty
+    (machine, ByteArray.empty)
+
+/--
+Advances the state of the machine by feeding it if with a answer.
+-/
+def answer (machine : Machine mode) (head : Message Data.Body mode.inverse) : Machine mode :=
+  match machine.state with
+  | .readyToAnswer | .failed _ =>
+    let connectionValue := if machine.keepAlive then "keep-alive" else "close"
+
+    let headWithConnection :=
+      if head.headers.contains "Connection"
+        then head
+        else head.addHeader "Connection" connectionValue
+
+    { machine with
+      outputMessage := some headWithConnection,
+      state := .awaitingAnswer }
+  | _ => machine
+
+/--
+Handles machine failure by generating error response.
+-/
+private def handleFailure (machine : Machine mode) (error : Error) : Machine mode :=
+  match mode with
+  | .request =>
+    let errorResponse := error.toResponse
+    let errorResponse := { errorResponse with headers := errorResponse.headers.insert "Connection" "close" }
+    let machine := answer machine errorResponse
+
+    let machine :=
+      match errorResponse.body with
+      | .bytes bodyBytes => writeData machine bodyBytes.toByteArray
+      | .zero => writeData machine .empty
+      | _ => machine
+
+    { machine with state := .closed, event := some .close}
+
+  | .response =>
+    { machine with
+      state := .closed,
+      event := some .close}
+
+/--
+Adds to the input buffer.
+-/
+def feed (machine : Machine mode) (data : ByteArray) : Machine mode :=
+  if machine.inputBuffer.array.size == 0 then
+    { machine with inputBuffer := data.iter }
+  else
+    { machine with inputBuffer := {machine.inputBuffer with array := machine.inputBuffer.array ++ data} }
+
+/--
+Determines keep-alive status from headers and config
+--/
+private def determineKeepAlive (machine : Machine mode) : Bool :=
+  let connectionHeader := machine.inputHeaders.get? "Connection" |>.getD (HashSet.ofList ["keep-alive"])
+  let explicitClose := connectionHeader.contains "close"
+  let explicitKeepAlive := connectionHeader.contains "keep-alive"
+
+  if explicitClose then false
+  else if explicitKeepAlive then true
+  else machine.config.enableKeepAlive && machine.requestCount < machine.config.maxRequests
+
+/--
+Updates machine with keep-alive decision
+--/
+private def updateKeepAlive (machine : Machine mode) : Machine mode :=
+  { machine with keepAlive := determineKeepAlive machine }
+
+/--
+Common state transition helper.
+--/
+private def transitionTo (machine : Machine mode) (newState : State) (event : Option (Event mode) := none) : Machine mode :=
+  { machine with state := newState, event }
+
+/--
+Forces completion of any pending output and transitions to appropriate final state.
+Sends final chunk if using chunked encoding.
+-/
+def close (machine : Machine mode) : Machine mode :=
+  if machine.keepAlive
+    then machine.transitionTo .next (some .next)
+    else machine.transitionTo .closed (some .close)
+
+/--
+Single header validation.
+--/
+private def processHeader (machine : Machine mode) (limit : Nat) (header : Parser.Header) : Machine mode :=
+  if limit > machine.config.maxHeaders then
+    machine.setError .entityTooLarge
+  else
+    { machine with
+    inputHeaders := machine.inputHeaders.insert header.name header.value,
+    state := .needHeader (limit + 1) }
+
+/--
+Header validation with keep-alive consideration.
+--/
+private def processHeaders (machine : Machine mode) : Machine mode :=
+  let machine := updateKeepAlive machine
+  match validateHeaders mode machine.inputHeaders with
+  | none =>
+    machine.setError .badRequest
+  | some (.fixed n) =>
+    machine.transitionTo (.needFixedBody n) (some (.endHeaders (.fixed n)))
+  | some .chunked =>
+    machine.transitionTo .needChunkedSize (some (.endHeaders .chunked))
+
+/--
+Advances the state machine by one step.
+-/
+def advance (machine : Machine mode) : Machine mode :=
+  let machine := { machine with event := none }
+
+  match machine.state with
+  | .needStatusLine =>
+    let (machine, result) := parseStatusLine machine
+    if let some result := result
+      then { machine with inputStatusLine := result, state := .needHeader 0 }
+      else machine
+
+  | .needHeader limit =>
+    let (machine, result) := parseWith machine Parser.parseHeader
+    match result with
+    | some (some header) =>
+      processHeader machine limit header
+    | some none =>
+      processHeaders machine
+    | none =>
+      machine
+
+  | .needChunkedSize =>
+    let (machine, result) := parseWith machine Parser.parseChunkSize
+    match result with
+    | some (size, ext) =>
+      { machine with size := some size.toUInt64, state := .needChunkedBody size, event := ext <&> Event.chunkExt }
+    | none =>
+      machine
+
+  | .needChunkedBody 0 =>
+    { machine with state := .readyToAnswer, event := some (.gotData true .empty) }
+
+  | .needChunkedBody size =>
+    let (machine, result) := parseWith machine (Parser.parseChunkData size)
+    match result with
+    | some data => { machine with size := none, state := .needChunkedSize, event := some (.gotData false data) }
+    | none => machine
+
+  | .needFixedBody size =>
+    let (machine, result) := parseWith machine (Parser.parseFixedBody size)
+    match result with
+    | some data => { machine with size := none, state := .readyToAnswer, event := some (.gotData true data) }
+    | none => machine
+
+  | .failed err =>
+    handleFailure machine err
+
+  | .readyToAnswer =>
+    let buffer : ByteArray := machine.inputBuffer.array.extract machine.inputBuffer.idx machine.inputBuffer.array.size
+    { machine with event := some (.readyToRespond), inputBuffer := buffer.iter }
+
+  | .awaitingAnswer =>
+    { machine with event := some (.awaitingAnswer) }
+
+  | .awaitingClose =>
+    machine
+
+  | .closed =>
+    reset machine
+
+  | .next =>
+    { machine with state := .closed }
+
+end Machine

src/Std/Internal/Http/V11/Parser.lean

@@ -0,0 +1,298 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Init.Data
+import Std.Internal.Parsec
+import Std.Internal.Parsec.ByteArray
+
+open Std Internal Parsec ByteArray
+
+namespace Std
+namespace Http
+namespace V11
+namespace Parser
+
+def failNone (x : Option α) : Parser α :=
+  if let some res := x then
+    pure res
+  else
+    fail "expected value but got none"
+
+deriving instance Repr for ByteArray
+
+instance : Repr ByteSlice where
+  reprPrec x := reprPrec x.toByteArray
+
+instance : Inhabited ByteSlice where
+  default := ⟨.empty, 0, 0, by simp⟩
+
+/--
+Structure representing an HTTP request line
+-/
+structure RequestLine where
+  method : ByteSlice
+  uri : ByteSlice
+  major : UInt8
+  minor : UInt8
+deriving Repr, Inhabited
+
+/--
+Structure representing an HTTP status line
+-/
+structure StatusLine where
+  major : UInt8
+  minor : UInt8
+  statusCode : Nat
+  reasonPhrase : ByteSlice
+deriving Repr
+
+/--
+Structure representing an HTTP header
+-/
+structure Header where
+  name : String
+  value : String
+deriving Repr
+
+/--
+Enumeration for HTTP message types
+-/
+inductive HttpType
+  | request
+  | response
+deriving Inhabited, Repr
+
+/--
+Union type for HTTP start lines (request or response)
+-/
+inductive StartLine : Type
+  | request : RequestLine → StartLine
+  | response : StatusLine → StartLine
+deriving Repr
+
+/--
+Structure representing a complete HTTP message
+-/
+structure HttpMessage where
+  firstLine : StartLine
+  headers : Array Header
+
+/--
+Structure representing a chunked transfer encoding chunk
+-/
+structure Chunk where
+  size : Nat
+  extension : Option ByteSlice
+  data : ByteSlice
+deriving Repr
+
+/--
+Enumeration for different HTTP body types
+-/
+inductive HttpBody
+  | fixed : ByteSlice → HttpBody
+  | chunked : Array Chunk → Array Header → HttpBody
+  | none : HttpBody
+deriving Repr
+
+/--
+Complete HTTP message with body
+-/
+structure CompleteHttpMessage where
+  firstLine : StartLine
+  headers : Array Header
+  body : HttpBody
+deriving Repr
+
+/--
+This function checks if a character is a valid token character according to HTTP spec
+-/
+def isTokenCharacter (c : UInt8) : Bool :=
+  c > 31 && c != '('.toUInt8 && c != ')'.toUInt8 && c != '<'.toUInt8 && c != '>'.toUInt8 &&
+  c != '@'.toUInt8 && c != ','.toUInt8 && c != ';'.toUInt8 && c != ':'.toUInt8 &&
+  c != '"'.toUInt8 && c != '/'.toUInt8 && c != '['.toUInt8 && c != ']'.toUInt8 &&
+  c != '?'.toUInt8 && c != '='.toUInt8 && c != '{'.toUInt8 && c != '}'.toUInt8 && c != ' '.toUInt8
+
+/--
+This function parses CRLF sequence
+-/
+def parseCRLF : Parser Unit :=
+  skipBytes "\r\n".toUTF8
+
+/--
+This function parses a sequence of digits and converts to UInt8
+-/
+def parseDigitAsUInt8 : Parser UInt8 := do
+  let d ← digit
+  return d.toUInt8
+
+/--
+This function parses HTTP version (major.minor)
+-/
+def parseHttpVersion : Parser (UInt8 × UInt8) := do
+  let major ← parseDigitAsUInt8
+  skipByte '.'.toUInt8
+  let minor ← parseDigitAsUInt8
+  return (major, minor)
+
+/--
+This function parses a 3-digit status code
+-/
+def parseStatusCode : Parser Nat := do
+  let d1 ← digit
+  let d2 ← digit
+  let d3 ← digit
+  return (d1.toUInt8 - '0'.toUInt8).toNat * 100 + (d2.toUInt8 - '0'.toUInt8).toNat * 10 + (d3.toUInt8 - '0'.toUInt8).toNat
+
+/--
+This function parses an HTTP request line
+-/
+def parseRequestLine : Parser RequestLine := do
+  let method ← takeWhile isTokenCharacter
+  skipByte ' '.toUInt8
+  let uri ← takeUntil (· == ' '.toUInt8)
+  skipBytes " HTTP/".toUTF8
+  let (major, minor) ← parseHttpVersion
+  parseCRLF
+  return ⟨method, uri, major, minor⟩
+
+/--
+This function parses an HTTP status line
+-/
+def parseStatusLine : Parser StatusLine := do
+  skipBytes "HTTP/".toUTF8
+  let (major, minor) ← parseHttpVersion
+  skipByte ' '.toUInt8
+  let statusCode ← parseStatusCode
+  skipByte ' '.toUInt8
+  let reasonPhrase ← takeUntil (· == '\r'.toUInt8)
+  parseCRLF
+  return ⟨major, minor, statusCode, reasonPhrase⟩
+
+/--
+This function parses a header name-value pair
+-/
+def parseHeaderLine : Parser Header := do
+  let name ← takeUntil (· == ':'.toUInt8)
+  skipByte ':'.toUInt8
+  skipWhile (· == ' '.toUInt8)
+  let value ← takeUntil (· == '\r'.toUInt8)
+  parseCRLF
+  return ⟨← failNone (String.fromUTF8? name.toByteArray), ← failNone (String.fromUTF8? value.toByteArray)⟩
+
+/--
+This function parses a single HTTP header or returns none if end of headers is reached
+-/
+def parseHeader : Parser (Option Header) := do
+  if (← optional parseCRLF).isSome then
+    return none
+  else
+    some <$> parseHeaderLine
+
+/--
+This function parses a hexadecimal digit
+-/
+def parseHexDigit : Parser UInt8 := do
+  let b ← any
+  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 if b ≥ 'a'.toUInt8 && b ≤ 'f'.toUInt8 then return b - 'a'.toUInt8 + 10
+  else fail s!"Invalid hex digit {Char.ofUInt8 b |>.quote}"
+
+/--
+This function parses a hexadecimal number
+-/
+def parseHex : Parser Nat := do
+  let hexDigits ← many1 (attempt parseHexDigit)
+  return (hexDigits.foldl (fun acc cur => acc * 16 + cur.toNat) 0)
+
+/--
+This function parses chunk extensions
+-/
+def parseChunkExt : Parser (Option ByteSlice) := do
+  if (← optional (skipByte ';'.toUInt8)).isSome then
+    some <$> takeUntil (· == '\r'.toUInt8)
+  else
+    return none
+
+/--
+This function parses the size and extension of a chunk
+-/
+def parseChunkSize : Parser (Nat × Option ByteSlice) := do
+  let size ← parseHex
+  let ext ← parseChunkExt
+  parseCRLF
+  return (size, ext)
+
+/--
+This function parses chunk data of a specific size
+-/
+def parseChunkData (size : Nat) : Parser ByteSlice := do
+  let res ← take size
+  parseCRLF
+  return res
+
+/--
+This function parses a trailer header (used after chunked body)
+-/
+def parseTrailerHeader : Parser (Option Header) := parseHeader
+
+/--
+This function parses a fixed-length body
+-/
+def parseFixedBody (size : Nat) : Parser ByteSlice :=
+  take size
+
+/--
+This function parses the first line of an HTTP message (request or response)
+-/
+def parseFirstLine : Parser StartLine := do
+  let peek ← peekWhen? (· == 'H'.toUInt8)
+  if peek.isSome
+    then return .response (← parseStatusLine)
+    else return .request (← parseRequestLine)
+
+/--
+This function parses multiple items until a terminator is found
+-/
+def parseMany {α : Type} (parser : Parser (Option α)) : Parser (Array α) := do
+  let items ← many (parser.bind (fun item => match item with
+    | some x => return x
+    | none => fail "End of items"))
+  return items
+
+/--
+This function parses all HTTP headers until the end marker
+-/
+def parseHeaders : Parser (Array Header) := do
+  let headers ← parseMany parseHeader
+  parseCRLF
+  return headers
+
+/--
+This function parses a single chunk in chunked transfer encoding
+-/
+def parseChunk : Parser (Option Chunk) := do
+  let (size, ext) ← parseChunkSize
+  if size == 0 then
+    return none
+  else
+    let data ← parseChunkData size
+    return some ⟨size, ext, data⟩
+
+/--
+This function parses all chunks in chunked transfer encoding
+-/
+def parseChunks : Parser (Array Chunk) :=
+  parseMany parseChunk
+
+/--
+This function parses trailer headers after chunked body
+-/
+def parseTrailers : Parser (Array Header) := do
+  let trailers ← parseMany parseTrailerHeader
+  parseCRLF
+  return trailers

src/Std/Internal/Parsec/Basic.lean

@@ -1,24 +1,47 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Dany Fabian, Henrik Böving
+Author: Dany Fabian, Henrik Böving, Sofia Rodrigues
 -/
+module
+
 prelude
-import Init.NotationExtra
-import Init.Data.ToString.Macro
+public import Init.NotationExtra
+public import Init.Data.ToString.Macro
 
-namespace Std.Internal
+public section
 
+namespace Std
+namespace Internal
 namespace Parsec
 
+/--
+Error type for the `ParseResult`. It separates `eof` from the rest of the errors in order to
+improve the error handling for this case in parsers that can receive incomplete data and then reparse it.
+-/
+inductive Error where
+  | eof
+  | other (s : String)
+  deriving Repr
+
+instance : ToString Error where
+  toString
+    | .eof => "unexpected end of input"
+    | .other s => s
+
+/--
+The result of parsing some string.
+-/
 inductive ParseResult (α : Type) (ι : Type) where
   | success (pos : ι) (res : α)
-  | error (pos : ι) (err : String)
+  | error (pos : ι) (err : Error)
   deriving Repr
 
 end Parsec
 
-def Parsec (ι : Type) (α : Type) : Type := ι → Parsec.ParseResult α ι
+@[expose]
+def Parsec (ι : Type) (α : Type) : Type :=
+  ι → Parsec.ParseResult α ι
 
 namespace Parsec
 
@@ -34,26 +57,21 @@ variable {α : Type} {ι : Type} {elem : Type} {idx : Type}
 variable [DecidableEq idx] [DecidableEq elem] [Input ι elem idx]
 
 instance : Inhabited (Parsec ι α) where
-  default := fun it => .error it ""
+  default := fun it => ParseResult.error it (.other "")
 
 @[always_inline, inline]
 protected def pure (a : α) : Parsec ι α := fun it =>
   .success it a
 
 @[always_inline, inline]
-def bind {α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) : Parsec ι β := fun it =>
+protected def bind {α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) : Parsec ι β := fun it =>
   match f it with
   | .success rem a => g a rem
   | .error pos msg => .error pos msg
 
-@[always_inline]
-instance : Monad (Parsec ι) where
-  pure := Parsec.pure
-  bind := Parsec.bind
-
 @[always_inline, inline]
 def fail (msg : String) : Parsec ι α := fun it =>
-  .error it msg
+  .error it (.other msg)
 
 @[inline]
 def tryCatch (p : Parsec ι α) (csuccess : α → Parsec ι β) (cerror : Unit → Parsec ι β)
@@ -64,6 +82,11 @@ def tryCatch (p : Parsec ι α) (csuccess : α → Parsec ι β) (cerror : Unit
     -- We assume that it.s never changes as the `Parsec` monad only modifies `it.pos`.
     if Input.pos it = Input.pos rem then cerror () rem else .error rem err
 
+@[always_inline]
+instance : Monad (Parsec ι) where
+  pure := Parsec.pure
+  bind := Parsec.bind
+
 @[always_inline, inline]
 def orElse (p : Parsec ι α) (q : Unit → Parsec ι α) : Parsec ι α :=
   tryCatch p pure q
@@ -79,12 +102,10 @@ instance : Alternative (Parsec ι) where
   failure := fail ""
   orElse := orElse
 
-def expectedEndOfInput := "expected end of input"
-
 @[inline]
 def eof : Parsec ι Unit := fun it =>
   if Input.hasNext it then
-    .error it expectedEndOfInput
+    .error it .eof
   else
     .success it ()
 
@@ -102,8 +123,9 @@ def many (p : Parsec ι α) : Parsec ι <| Array α := manyCore p #[]
 @[inline]
 def many1 (p : Parsec ι α) : Parsec ι <| Array α := do manyCore p #[← p]
 
-def unexpectedEndOfInput := "unexpected end of input"
-
+/--
+Gets the next input element.
+-/
 @[inline]
 def any : Parsec ι elem := fun it =>
   if h : Input.hasNext it then
@@ -111,19 +133,28 @@ def any : Parsec ι elem := fun it =>
     let it' := Input.next' it h
     .success it' c
   else
-    .error it unexpectedEndOfInput
+    .error it .eof
 
+/--
+Checks if the next input element matches some condition.
+-/
 @[inline]
 def satisfy (p : elem → Bool) : Parsec ι elem := attempt do
   let c ← any
   if p c then return c else fail "condition not satisfied"
 
+/--
+Fails if `p` succeeds, otherwise succeeds without consuming input.
+-/
 @[inline]
 def notFollowedBy (p : Parsec ι α) : Parsec ι Unit := fun it =>
   match p it with
-  | .success _ _ => .error it ""
+  | .success _ _ => .error it (.other "")
   | .error _ _ => .success it ()
 
+/--
+Peeks at the next element, returns `some` if exists else `none`, does not consume input.
+-/
 @[inline]
 def peek? : Parsec ι (Option elem) := fun it =>
   if h : Input.hasNext it then
@@ -131,13 +162,32 @@ def peek? : Parsec ι (Option elem) := fun it =>
   else
     .success it none
 
+/--
+Peeks at the next element, returns `some elem` if it satisfies `p`, else `none`. Does not consume input.
+-/
+@[inline]
+def peekWhen? (p : elem → Bool) : Parsec ι (Option elem) := do
+  let some data ← peek?
+    | return none
+
+  if p data then
+    return some data
+  else
+    return none
+
+/--
+Peeks at the next element, errors on EOF, does not consume input.
+-/
 @[inline]
 def peek! : Parsec ι elem := fun it =>
   if h : Input.hasNext it then
     .success it (Input.curr' it h)
   else
-    .error it unexpectedEndOfInput
+    .error it .eof
 
+/--
+Peeks at the next element or returns a default if at EOF, does not consume input.
+-/
 @[inline]
 def peekD (default : elem) : Parsec ι elem := fun it =>
   if h : Input.hasNext it then
@@ -145,23 +195,37 @@ def peekD (default : elem) : Parsec ι elem := fun it =>
   else
     .success it default
 
+/--
+Consumes one element if available, otherwise errors on EOF.
+-/
 @[inline]
 def skip : Parsec ι Unit := fun it =>
   if h : Input.hasNext it then
     .success (Input.next' it h) ()
   else
-    .error it unexpectedEndOfInput
+    .error it .eof
 
+/--
+Parses zero or more chars with `p`, accumulates into a string.
+-/
 @[specialize]
 partial def manyCharsCore (p : Parsec ι Char) (acc : String) : Parsec ι String :=
   tryCatch p (manyCharsCore p <| acc.push ·) (fun _ => pure acc)
 
+/--
+Parses zero or more chars with `p` into a string.
+-/
 @[inline]
-def manyChars (p : Parsec ι Char) : Parsec ι String := manyCharsCore p ""
+def manyChars (p : Parsec ι Char) : Parsec ι String := do
+  manyCharsCore p ""
 
+/--
+Parses one or more chars with `p` into a string, errors if none.
+-/
 @[inline]
-def many1Chars (p : Parsec ι Char) : Parsec ι String := do manyCharsCore p (← p).toString
+def many1Chars (p : Parsec ι Char) : Parsec ι String := do
+  manyCharsCore p (← p).toString
 
 end Parsec
-
-end Std.Internal
+end Internal
+end Std

src/Std/Internal/Parsec/ByteArray.lean

@@ -3,12 +3,18 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-prelude
-import Std.Internal.Parsec.Basic
-import Init.Data.ByteArray.Basic
-import Init.Data.String.Extra
+module
 
-namespace Std.Internal
+prelude
+public import Std.Internal.Parsec.Basic
+public import Init.Data.ByteArray.Basic
+public import Init.Data.String.Extra
+public import Init.Data.ByteSlice
+
+public section
+
+namespace Std
+namespace Internal
 namespace Parsec
 namespace ByteArray
 
@@ -22,29 +28,51 @@ instance : Input ByteArray.Iterator UInt8 Nat where
 
 abbrev Parser (α : Type) : Type := Parsec ByteArray.Iterator α
 
+/--
+Run a `Parser` on a `ByteArray`, returns either the result or an error string with offset.
+-/
 protected def Parser.run (p : Parser α) (arr : ByteArray) : Except String α :=
   match p arr.iter with
   | .success _ res => Except.ok res
-  | .error it err  => Except.error s!"offset {repr it.pos}: {err}"
+  | .error it (.other err)  => Except.error s!"offset {repr it.pos}: {err}"
+  | .error it .eof  => Except.error s!"offset {repr it.pos}: end of file"
 
+/--
+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}'"
 
+/--
+Skip a single byte equal to `b`, fails if different.
+-/
 @[inline]
-def skipByte (b : UInt8) : Parser Unit := pbyte b *> pure ()
+def skipByte (b : UInt8) : Parser Unit :=
+  pbyte b *> pure ()
 
+/--
+Skip a sequence of bytes equal to the given `ByteArray`.
+-/
+@[inline]
 def skipBytes (arr : ByteArray) : Parser Unit := do
   for b in arr do
     skipByte b
 
+/--
+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
   return s
 
+/--
+Skip a string by matching its UTF-8 bytes.
+-/
 @[inline]
-def skipString (s : String) : Parser Unit := pstring s *> pure ()
+def skipString (s : String) : Parser Unit :=
+  pstring s *> pure ()
 
 /--
 Parse a `Char` that can be represented in 1 byte. If `c` uses more than 1 byte it is truncated.
@@ -57,16 +85,27 @@ def pByteChar (c : Char) : Parser Char := attempt do
 Skip a `Char` that can be represented in 1 byte. If `c` uses more than 1 byte it is truncated.
 -/
 @[inline]
-def skipByteChar (c : Char) : Parser Unit := skipByte c.toUInt8
+def skipByteChar (c : Char) : Parser Unit :=
+  skipByte c.toUInt8
 
+/--
+Parse an ASCII digit `0-9` as a `Char`.
+-/
 @[inline]
 def digit : Parser Char := attempt do
   let b ← any
   if '0'.toUInt8 ≤ b ∧ b ≤ '9'.toUInt8 then return Char.ofUInt8 b else fail s!"digit expected"
 
+/--
+Convert a byte representing `'0'..'9'` to a `Nat`.
+-/
 @[inline]
-private def digitToNat (b : UInt8) : Nat := (b - '0'.toUInt8).toNat
+private def digitToNat (b : UInt8) : Nat :=
+  (b - '0'.toUInt8).toNat
 
+/--
+Parse zero or more ASCII digits into a `Nat`, continuing until non-digit or EOF.
+-/
 @[inline]
 private partial def digitsCore (acc : Nat) : Parser Nat := fun it =>
   /-
@@ -88,11 +127,17 @@ where
     else
       (acc, it)
 
+/--
+Parse one or more ASCII digits into a `Nat`.
+-/
 @[inline]
 def digits : Parser Nat := do
   let d ← digit
   digitsCore (digitToNat d.toUInt8)
 
+/--
+Parse a hex digit `0-9`, `a-f`, or `A-F` as a `Char`.
+-/
 @[inline]
 def hexDigit : Parser Char := attempt do
   let b ← any
@@ -100,6 +145,20 @@ def hexDigit : Parser Char := attempt do
    ∨ ('a'.toUInt8 ≤ b ∧ b ≤ 'f'.toUInt8)
    ∨ ('A'.toUInt8 ≤ b ∧ b ≤ 'F'.toUInt8) then return Char.ofUInt8 b else fail s!"hex digit expected"
 
+/--
+Parse an octal digit `0-7` as a `Char`.
+-/
+@[inline]
+def octDigit : Parser Char := attempt do
+  let b ← any
+  if '0'.toUInt8 ≤ b ∧ b ≤ '7'.toUInt8 then
+    return Char.ofUInt8 b
+  else
+    fail s!"octal digit expected"
+
+/--
+Parse an ASCII letter `a-z` or `A-Z` as a `Char`.
+-/
 @[inline]
 def asciiLetter : Parser Char := attempt do
   let b ← any
@@ -118,17 +177,65 @@ private partial def skipWs (it : ByteArray.Iterator) : ByteArray.Iterator :=
   else
    it
 
+/--
+Skip whitespace: tabs, newlines, carriage returns, and spaces.
+-/
 @[inline]
 def ws : Parser Unit := fun it =>
   .success (skipWs it) ()
 
-def take (n : Nat) : Parser ByteArray := fun it =>
-  let subarr := it.array.extract it.idx (it.idx + n)
-  if subarr.size != n then
-    .error it s!"expected: {n} bytes"
+/--
+Parse `n` bytes from the input into a `ByteArray`, errors if not enough bytes.
+-/
+def take (n : Nat) : Parser ByteSlice := fun it =>
+  if h : it.idx + n ≤ it.array.size then
+    let slice := { data := it.array, start := it.idx,  «end» := it.idx + n, valid := ⟨Nat.le_add_right it.idx n, h⟩}
+    .success (it.forward n) slice
   else
-    .success (it.forward n) subarr
+    .error it .eof
+
+/--
+Parses while a predicate is satisfied.
+-/
+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 ((ByteSlice.ofByteArray it.array) |>.drop it.idx |>.take length)
+
+/--
+Parses until a predicate is satisfied (exclusive).
+-/
+@[inline]
+def takeUntil (pred : UInt8 → Bool) : Parser ByteSlice :=
+  takeWhile (fun b => ¬pred b)
+
+/--
+Skips while a predicate is satisfied.
+-/
+@[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) ()
+
+/--
+Skips until a predicate is satisfied.
+-/
+@[inline]
+def skipUntil (pred : UInt8 → Bool) : Parser Unit :=
+  skipWhile (fun b => ¬pred b)
 
 end ByteArray
 end Parsec
-end Std.Internal
+end Internal
+end Std

src/Std/Internal/Parsec/String.lean

@@ -3,8 +3,12 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Dany Fabian, Henrik Böving
 -/
+module
+
 prelude
-import Std.Internal.Parsec.Basic
+public import Std.Internal.Parsec.Basic
+
+public section
 
 namespace Std.Internal
 namespace Parsec
@@ -20,34 +24,55 @@ instance : Input String.Iterator Char String.Pos where
 
 abbrev Parser (α : Type) : Type := Parsec String.Iterator α
 
+/--
+Run a `Parser` on a `String`, returns either the result or an error string with offset.
+-/
 protected def Parser.run (p : Parser α) (s : String) : Except String α :=
   match p s.mkIterator with
   | .success _ res => Except.ok res
-  | .error it err  => Except.error s!"offset {repr it.i.byteIdx}: {err}"
+  | .error it (.other err)  => Except.error s!"offset {repr it.pos}: {err}"
+  | .error it .eof  => Except.error s!"offset {repr it.pos}: end of file"
 
-/-- Parses the given string. -/
+/--
+Parses the given string.
+-/
 def pstring (s : String) : Parser String := fun it =>
   let substr := it.extract (it.forward s.length)
   if substr = s then
     .success (it.forward s.length) substr
   else
-    .error it s!"expected: {s}"
+    .error it (.other s!"expected: {s}")
 
+/--
+Skips the given string.
+-/
 @[inline]
 def skipString (s : String) : Parser Unit := pstring s *> pure ()
 
+/--
+Parses the given char.
+-/
 @[inline]
 def pchar (c : Char) : Parser Char := attempt do
   if (← any) = c then pure c else fail s!"expected: '{c}'"
 
+/--
+Skips the given char.
+-/
 @[inline]
 def skipChar (c : Char) : Parser Unit := pchar c *> pure ()
 
+/--
+Parse an ASCII digit `0-9` as a `Char`.
+-/
 @[inline]
 def digit : Parser Char := attempt do
   let c ← any
   if '0' ≤ c ∧ c ≤ '9' then return c else fail s!"digit expected"
 
+/--
+Convert a byte representing `'0'..'9'` to a `Nat`.
+-/
 @[inline]
 private def digitToNat (b : Char) : Nat := b.toNat - '0'.toNat
 
@@ -72,11 +97,17 @@ where
     else
       (acc, it)
 
+/--
+Parse one or more ASCII digits into a `Nat`.
+-/
 @[inline]
 def digits : Parser Nat := do
   let d ← digit
   digitsCore (digitToNat d)
 
+/--
+Parse a hex digit `0-9`, `a-f`, or `A-F` as a `Char`.
+-/
 @[inline]
 def hexDigit : Parser Char := attempt do
   let c ← any
@@ -84,6 +115,9 @@ def hexDigit : Parser Char := attempt do
    ∨ ('a' ≤ c ∧ c ≤ 'f')
    ∨ ('A' ≤ c ∧ c ≤ 'F') then return c else fail s!"hex digit expected"
 
+/--
+Parse an ASCII letter `a-z` or `A-Z` as a `Char`.
+-/
 @[inline]
 def asciiLetter : Parser Char := attempt do
   let c ← any
@@ -99,14 +133,18 @@ private partial def skipWs (it : String.Iterator) : String.Iterator :=
   else
    it
 
+/--
+Skip whitespace: tabs, newlines, carriage returns, and spaces.
+-/
 @[inline]
 def ws : Parser Unit := fun it =>
   .success (skipWs it) ()
 
+
 def take (n : Nat) : Parser String := fun it =>
   let substr := it.extract (it.forward n)
   if substr.length != n then
-    .error it s!"expected: {n} codepoints"
+    .error it .eof
   else
     .success (it.forward n) substr
 

src/Std/Time/Zoned/Database/TzIf.lean

@@ -174,21 +174,32 @@ structure TZif where
   v2 : Option TZifV2
   deriving Repr, Inhabited
 
-private def toUInt32 (bs : ByteArray) : UInt32 :=
+private def toUInt32 (bs : ByteSlice) : UInt32 :=
   assert! bs.size == 4
   (bs.get! 0).toUInt32 <<< 0x18 |||
   (bs.get! 1).toUInt32 <<< 0x10 |||
   (bs.get! 2).toUInt32 <<< 0x8  |||
   (bs.get! 3).toUInt32
 
-private def toInt32 (bs : ByteArray) : Int32 :=
+private def toUInt64 (bs : ByteSlice) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 0).toUInt64 <<< 0x38 |||
+  (bs.get! 1).toUInt64 <<< 0x30 |||
+  (bs.get! 2).toUInt64 <<< 0x28 |||
+  (bs.get! 3).toUInt64 <<< 0x20 |||
+  (bs.get! 4).toUInt64 <<< 0x18 |||
+  (bs.get! 5).toUInt64 <<< 0x10 |||
+  (bs.get! 6).toUInt64 <<< 0x8  |||
+  (bs.get! 7).toUInt64
+
+private def toInt32 (bs : ByteSlice) : Int32 :=
   let n := toUInt32 bs |>.toNat
   if n < (1 <<< 31)
     then Int.ofNat n
     else Int.negOfNat (UInt32.size - n)
 
-private def toInt64 (bs : ByteArray) : Int64 :=
-  let n := ByteArray.toUInt64BE! bs |>.toNat
+private def toInt64 (bs : ByteSlice) : Int64 :=
+  let n := toUInt64 bs |>.toNat
   if n < (1 <<< 63)
     then Int.ofNat n
     else Int.negOfNat (UInt64.size - n)
@@ -200,7 +211,7 @@ private def manyN (n : Nat) (p : Parser α) : Parser (Array α) := do
     result := result.push x
   return result
 
-private def pu64 : Parser UInt64 := ByteArray.toUInt64LE! <$> take 8
+private def pu64 : Parser UInt64 := toUInt64 <$> take 8
 private def pi64 : Parser Int64 := toInt64 <$> take 8
 private def pu32 : Parser UInt32 := toUInt32 <$> take 4
 private def pi32 : Parser Int32 := toInt32 <$> take 4

src/runtime/object.cpp

@@ -2419,6 +2419,39 @@ extern "C" LEAN_EXPORT obj_res lean_byte_array_mk(obj_arg a) {
     return r;
 }
 
+extern "C" LEAN_EXPORT bool lean_byte_array_beq(obj_arg a, obj_arg b) {
+  size_t size_a = lean_sarray_size(a);
+  size_t size_b = lean_sarray_size(b);
+
+  if (size_a != size_b) {
+    return 0;
+  }
+
+  return memcmp(lean_sarray_cptr(a), lean_sarray_cptr(b), size_a) == 0;
+}
+
+extern "C" LEAN_EXPORT bool lean_byteslice_beq(obj_arg a, obj_arg b) {
+    obj_arg ba_a = lean_ctor_get(a, 0);
+    size_t start_a = lean_unbox(lean_ctor_get(a, 1));
+    size_t end_a   = lean_unbox(lean_ctor_get(a, 2));
+
+    obj_arg ba_b = lean_ctor_get(b, 0);
+    size_t start_b = lean_unbox(lean_ctor_get(b, 1));
+    size_t end_b   = lean_unbox(lean_ctor_get(b, 2));
+
+    size_t size_a = end_a - start_a;
+    size_t size_b = end_b - start_b;
+
+    if (size_a != size_b) {
+        return 0;
+    }
+
+    const uint8_t *ptr_a = lean_sarray_cptr(ba_a) + start_a;
+    const uint8_t *ptr_b = lean_sarray_cptr(ba_b) + start_b;
+
+    return memcmp(ptr_a, ptr_b, size_a) == 0;
+}
+
 extern "C" LEAN_EXPORT obj_res lean_byte_array_data(obj_arg a) {
     usize sz       = lean_sarray_size(a);
     obj_res r      = lean_alloc_array(sz, sz);

src/runtime/uv/tcp.cpp

@@ -27,6 +27,12 @@ typedef struct {
 // =======================================
 // TCP socket object manipulation functions.
 
+extern "C" LEAN_EXPORT lean_obj_res lean_bytearray_to_ascii(obj_arg ba) {
+    char* bastr = (char*)lean_sarray_cptr(ba);
+    int sint = lean_sarray_size(ba);
+    return lean_mk_string_unchecked(bastr, sint, sint);
+}
+
 void lean_uv_tcp_socket_finalizer(void* ptr) {
     lean_uv_tcp_socket_object* tcp_socket = (lean_uv_tcp_socket_object*)ptr;
 
@@ -184,12 +190,11 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
     send_data->data = data;
     send_data->socket = socket;
 
-    // These objects are going to enter the loop and be owned by it
+    event_loop_lock(&global_ev);
+
     lean_inc(promise);
     lean_inc(socket);
 
-    event_loop_lock(&global_ev);
-
     int result = uv_write(write_uv, (uv_stream_t*)tcp_socket->m_uv_tcp, &buf, 1, [](uv_write_t* req, int status) {
         tcp_send_data* tup = (tcp_send_data*) req->data;
 
@@ -376,6 +381,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, ob
     uv_read_stop((uv_stream_t*)tcp_socket->m_uv_tcp);
 
     lean_object* promise = tcp_socket->m_promise_read;
+    lean_promise_resolve(mk_except_ok(lean::mk_option_none()), promise);
     lean_dec(promise);
     tcp_socket->m_promise_read = nullptr;
 
@@ -385,7 +391,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, ob
         tcp_socket->m_byte_array = nullptr;
     }
 
-    lean_dec((lean_object*)tcp_socket);
+    lean_dec(socket);
 
     event_loop_unlock(&global_ev);
     return lean_io_result_mk_ok(lean_box(0));
@@ -481,7 +487,6 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg
     lean_uv_tcp_socket_object* client_socket = lean_to_uv_tcp_socket(client);
 
     int result = uv_accept((uv_stream_t*)tcp_socket->m_uv_tcp, (uv_stream_t*)client_socket->m_uv_tcp);
-
     if (result < 0 && result != UV_EAGAIN) {
         event_loop_unlock(&global_ev);
         lean_dec(client);

src/runtime/uv/tcp.h

@@ -18,6 +18,8 @@ namespace lean {
 static lean_external_class* g_uv_tcp_socket_external_class = NULL;
 void initialize_libuv_tcp_socket();
 
+extern "C" LEAN_EXPORT lean_obj_res lean_bytearray_to_ascii(obj_arg ba);
+
 #ifndef LEAN_EMSCRIPTEN
 
 // Structure for managing a single TCP socket object, including promise handling,