refactor: change Char.isDigit and Char.isAlpha

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

src/Std/Internal.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Internal.Async
+public import Std.Internal.Http
 public import Std.Internal.Parsec
 public import Std.Internal.UV
 

src/Std/Internal/Http.lean

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

src/Std/Internal/Http/Data.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Data.Method
+public import Std.Internal.Http.Data.Version
+public import Std.Internal.Http.Data.Request
+public import Std.Internal.Http.Data.Response
+public import Std.Internal.Http.Data.Status
+public import Std.Internal.Http.Data.Chunk
+
+/-!
+# HTTP Data Types
+
+This module re-exports all HTTP data types including request/response structures,
+methods, status codes, chunks, and extension metadata.
+-/

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

@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Internal
+public meta import Std.Internal.Http.Internal.String
+
+public section
+
+/-!
+# Chunk
+
+This module defines the `Chunk` type, which represents a chunk of data from a request or response.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9112.html#section-7.1
+-/
+
+namespace Std.Http
+
+open Internal
+
+set_option linter.all true
+
+namespace Chunk
+
+/--
+A proposition stating that `s` is a valid chunk-extension name: every character in `s` is an
+HTTP token character and `s` is non-empty.
+
+Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
+-/
+abbrev IsValidExtensionName (s : String) : Prop :=
+  isToken s
+
+/--
+A validated chunk extension name that ensures all characters conform to HTTP standards
+per RFC 9112 §7.1.1. Extension names appear in chunked transfer encoding as key-value metadata.
+
+Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
+-/
+structure ExtensionName where
+  /--
+  The extension name string.
+  -/
+  value : String
+
+  /--
+  The proof that it's a valid extension name.
+  -/
+  isValidExtensionName : IsValidExtensionName value := by decide
+deriving Repr, DecidableEq, BEq
+
+instance : Hashable ExtensionName where
+  hash x := Hashable.hash x.value
+
+instance : Inhabited ExtensionName where
+  default := ⟨"_", by decide⟩
+
+instance : ToString ExtensionName where
+  toString name := name.value
+
+namespace ExtensionName
+
+/--
+Attempts to create an `ExtensionName` from a `String`, returning `none` if the string contains
+invalid characters or is empty.
+-/
+def ofString? (s : String) : Option ExtensionName :=
+  if h : IsValidExtensionName s then
+    some ⟨s, h⟩
+  else
+    none
+
+/--
+Creates an `ExtensionName` from a string, panicking with an error message if the string contains
+invalid characters or is empty.
+-/
+def ofString! (s : String) : ExtensionName :=
+  match ofString? s with
+  | some res => res
+  | none => panic! ("invalid extension name: " ++ s.quote)
+
+end ExtensionName
+
+/--
+A proposition asserting that `s` is a valid extension value, meaning it can be correctly encoded and
+decoded as either a token or a quoted-string.
+
+Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
+-/
+abbrev IsValidExtensionValue (s : String) : Prop :=
+  (quoteHttpString? s).isSome
+
+/--
+A validated chunk extension value that ensures all characters conform to HTTP standards per RFC 9112 §7.1.1.
+Extension values appear in chunked transfer encoding as metadata associated with extension names.
+
+Note: UTF-8 encoding is not supported. The quoting mechanism is strict and only permits escaping
+specific values. Additionally, the library does not support obs-text, which means certain UTF-8
+characters or values outside of token, qdtext, and the limited set of escapable characters cannot be
+encoded.
+
+Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
+-/
+structure ExtensionValue where
+  /--
+  The extension value string.
+  -/
+  value : String
+
+  /--
+  The proof that it's a valid extension value.
+  -/
+  validExtensionValue : IsValidExtensionValue value := by decide
+deriving Repr, DecidableEq, BEq
+
+namespace ExtensionValue
+
+instance : Inhabited ExtensionValue where
+  default := ⟨"", by native_decide⟩
+
+instance : ToString ExtensionValue where
+  toString v := v.value
+
+/--
+Quotes an extension value if it contains non-token characters, otherwise returns it as-is.
+
+-/
+def quote (s : ExtensionValue) : String :=
+  quoteHttpString? s.value |>.get s.validExtensionValue
+
+/--
+Attempts to create an `ExtensionValue` from a `String`, returning `none` if the string contains
+characters that cannot be encoded as an HTTP quoted-string.
+-/
+def ofString? (s : String) : Option ExtensionValue :=
+  if h : (quoteHttpString? s).isSome then
+    some ⟨s, h⟩
+  else
+    none
+
+/--
+Creates an `ExtensionValue` from a string, panicking with an error message if the string contains
+characters that cannot be encoded as an HTTP quoted-string.
+-/
+def ofString! (s : String) : ExtensionValue :=
+  match ofString? s with
+  | some res => res
+  | none => panic! ("invalid extension value: " ++ s.quote)
+
+end Chunk.ExtensionValue
+
+/--
+Represents a chunk of data with optional extensions (key-value pairs).
+
+Reference: https://httpwg.org/specs/rfc9112.html#rfc.section.7.1
+-/
+structure Chunk where
+
+  /--
+  The byte data contained in this chunk.
+  -/
+  data : ByteArray
+
+  /--
+  Optional metadata associated with this chunk as key-value pairs. Keys are validated
+  `Chunk.ExtensionName` values, values are optional strings.
+  -/
+  extensions : Array (Chunk.ExtensionName × Option Chunk.ExtensionValue) := #[]
+deriving Inhabited
+
+namespace Chunk
+
+/--
+An empty chunk with no data and no extensions.
+-/
+def empty : Chunk :=
+  { data := .empty, extensions := #[] }
+
+/--
+Creates a simple chunk without extensions.
+-/
+def ofByteArray (data : ByteArray) : Chunk :=
+  { data := data, extensions := #[] }
+
+/--
+Adds an extension to a chunk.
+-/
+def insertExtension (chunk : Chunk) (key : Chunk.ExtensionName) (value : ExtensionValue) : Chunk :=
+  { chunk with extensions := chunk.extensions.push (key, some value) }
+
+/--
+Interprets the chunk data as a UTF-8 encoded string.
+-/
+def toString? (chunk : Chunk) : Option String :=
+  String.fromUTF8? chunk.data
+
+instance : Encode .v11 Chunk where
+  encode buffer chunk :=
+    let chunkLen := chunk.data.size
+    let exts := chunk.extensions.foldl (fun acc (name, value)  =>
+      acc ++ ";" ++ name.value ++ (value.elim "" (fun x => "=" ++ x.quote))) ""
+    let size := Nat.toDigits 16 chunkLen |>.toArray |>.map Char.toUInt8 |> ByteArray.mk
+    buffer.append #[size, exts.toUTF8, "\r\n".toUTF8, chunk.data, "\r\n".toUTF8]
+
+end Chunk

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

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Init.Dynamic
+public import Init.Data.String
+public import Std.Data.TreeMap
+
+open Lean
+
+public section
+
+/-!
+# Extensions
+
+This module provides the `Extensions` type, a dynamically-typed map for storing metadata on HTTP
+requests and responses. It can be used by parsers, middleware, or other processing stages
+to attach arbitrary typed data.
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+/-
+`quickCmp` is unavailable here, so this is a simpler implementation of the same comparison.
+-/
+
+/--
+An ordering for `Name` keys used by `Extensions`.
+-/
+protected def Extensions.compareName : Name → Name → Ordering
+  | .anonymous, .anonymous => .eq
+  | .anonymous, _ => .lt
+  | _, .anonymous => .gt
+  | .str p₁ s₁, .str p₂ s₂ =>
+    match Extensions.compareName p₁ p₂ with
+    | .eq => compareOfLessAndEq s₁ s₂
+    | ord => ord
+  | .str _ _, .num _ _ => .lt
+  | .num _ _, .str _ _ => .gt
+  | .num p₁ n₁, .num p₂ n₂ =>
+    match Extensions.compareName p₁ p₂ with
+    | .eq => compare n₁ n₂
+    | ord => ord
+
+/--
+A dynamically typed map for optional metadata that can be attached to HTTP requests and responses.
+Extensions allow storing arbitrary typed data keyed by type name, useful for metadata such as socket
+information or custom processing data.
+-/
+structure Extensions where
+  private mk ::
+
+  /--
+  The underlying tree map storing dynamic values keyed by their type name.
+  -/
+  private data : TreeMap Name Dynamic Extensions.compareName := .empty
+deriving Inhabited
+
+namespace Extensions
+
+/--
+An empty extensions map with no data.
+-/
+def empty : Extensions :=
+  ⟨.empty⟩
+
+/--
+Retrieves a value of type `α` from the extensions, if present.
+-/
+@[inline]
+def get (x : Extensions) (α : Type) [TypeName α] : Option α := do
+  let dyn ← x.data.get? (TypeName.typeName α)
+  dyn.get? α
+
+/--
+Inserts a value into the extensions, keyed by its type name. If a value of the same type already
+exists, it is replaced.
+-/
+@[inline]
+def insert (x : Extensions) [TypeName α] (data : α) : Extensions :=
+  let dyn := Dynamic.mk data
+  ⟨x.data.insert dyn.typeName dyn⟩
+
+/--
+Removes the value of type `α` from the extensions.
+-/
+@[inline]
+def remove (x : Extensions) (α : Type) [TypeName α] : Extensions :=
+  ⟨x.data.erase (TypeName.typeName α)⟩
+
+/--
+Checks whether the extensions contain a value of type `α`.
+-/
+@[inline]
+def contains (x : Extensions) (α : Type) [TypeName α] : Bool :=
+  x.data.contains (TypeName.typeName α)
+
+end Std.Http.Extensions

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

@@ -0,0 +1,385 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Init.Data.ToString
+public import Std.Internal.Http.Internal
+
+public section
+
+/-!
+# Method
+
+This module provides the `Method` type that represents HTTP request methods. It defines all
+IANA-registered HTTP methods as distinct constructors, including standard methods (e.g. `GET`,
+`POST`, `PUT`, `DELETE`) and extension methods from WebDAV, CalDAV, and other specifications.
+Unrecognized method strings produce `none` from `ofString?`.
+
+References:
+* https://httpwg.org/specs/rfc9112.html#request.method
+* https://httpwg.org/specs/rfc9110.html#method.overview
+* https://www.iana.org/assignments/http-methods/http-methods.xhtml
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+open Internal
+
+/--
+A method is a verb that describes the action to be performed.
+
+Covers all methods in the IANA HTTP Method Registry.
+
+* Reference: https://www.iana.org/assignments/http-methods/http-methods.xhtml
+-/
+inductive Method where
+  /--
+  Access control list for a resource.
+  Source: https://www.rfc-editor.org/rfc/rfc3744#section-8.1
+  -/
+  | acl
+
+  /--
+  Apply a label to a version-controlled resource baseline.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-12.6
+  -/
+  | baselineControl
+
+  /--
+  Bind a resource to an additional URI path.
+  Source: https://www.rfc-editor.org/rfc/rfc5842#section-4
+  -/
+  | bind
+
+  /--
+  Check in a checked-out version-controlled resource.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-9.4
+  -/
+  | checkin
+
+  /--
+  Check out a version-controlled resource for modification.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-8.8
+  -/
+  | checkout
+
+  /--
+  Establish a tunnel to a server (often for TLS).
+  Source: https://httpwg.org/specs/rfc9110.html#section-9.3.6
+  -/
+  | connect
+
+  /--
+  Copy a resource to a new URI.
+  Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.8
+  -/
+  | copy
+
+  /--
+  Remove a resource.
+  Source: https://httpwg.org/specs/rfc9110.html#section-9.3.5
+  -/
+  | delete
+
+  /--
+  Retrieve a resource.
+  Source: https://httpwg.org/specs/rfc9110.html#section-9.3.1
+  -/
+  | get
+
+  /--
+  Retrieve headers for a resource, without the body.
+  Source: https://httpwg.org/specs/rfc9110.html#section-9.3.2
+  -/
+  | head
+
+  /--
+  Apply a label to a version history.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-8.2
+  -/
+  | label
+
+  /--
+  Create a link relationship between resources.
+  Source: https://www.rfc-editor.org/rfc/rfc2068#section-19.6.1.2
+  -/
+  | link
+
+  /--
+  Lock a resource to prevent concurrent modifications.
+  Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.10
+  -/
+  | lock
+
+  /--
+  Merge a version-controlled resource.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-11.2
+  -/
+  | merge
+
+  /--
+  Create a new activity resource.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-13.5
+  -/
+  | mkactivity
+
+  /--
+  Create a calendar collection.
+  Source: https://www.rfc-editor.org/rfc/rfc4791#section-5.3.1
+  -/
+  | mkcalendar
+
+  /--
+  Create a collection resource (WebDAV directory).
+  Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.3
+  -/
+  | mkcol
+
+  /--
+  Create a redirect reference resource.
+  Source: https://www.rfc-editor.org/rfc/rfc4437#section-6
+  -/
+  | mkredirectref
+
+  /--
+  Create a workspace resource.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-6.3
+  -/
+  | mkworkspace
+
+  /--
+  Move a resource to a new URI.
+  Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.9
+  -/
+  | move
+
+  /--
+  Describe communication options for a resource.
+  Source: https://httpwg.org/specs/rfc9110.html#section-9.3.7
+  -/
+  | options
+
+  /--
+  Reorder members of a collection.
+  Source: https://www.rfc-editor.org/rfc/rfc3648#section-7
+  -/
+  | orderpatch
+
+  /--
+  Apply partial modifications to a resource.
+  Source: https://www.rfc-editor.org/rfc/rfc5789#section-2
+  -/
+  | patch
+
+  /--
+  Submit data to be processed (e.g., form submission).
+  Source: https://httpwg.org/specs/rfc9110.html#section-9.3.3
+  -/
+  | post
+
+  /--
+  HTTP/2 connection preface (not used in application code).
+  Source: https://www.rfc-editor.org/rfc/rfc9113#section-3.4
+  -/
+  | pri
+
+  /--
+  Retrieve properties of a resource (WebDAV).
+  Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.1
+  -/
+  | propfind
+
+  /--
+  Set or remove properties on a resource (WebDAV).
+  Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.2
+  -/
+  | proppatch
+
+  /--
+  Replace a resource with new data.
+  Source: https://httpwg.org/specs/rfc9110.html#section-9.3.4
+  -/
+  | put
+
+  /--
+  Perform a safe query with a request body.
+  Source: https://www.ietf.org/archive/id/draft-ietf-httpbis-safe-method-w-body-14.html#section-2
+  -/
+  | query
+
+  /--
+  Rebind a resource to a new URI path.
+  Source: https://www.rfc-editor.org/rfc/rfc5842#section-6
+  -/
+  | rebind
+
+  /--
+  Retrieve a report on a resource.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-3.6
+  -/
+  | report
+
+  /--
+  Search a resource.
+  Source: https://www.rfc-editor.org/rfc/rfc5323#section-2
+  -/
+  | search
+
+  /--
+  Perform a message loop-back test.
+  Source: https://httpwg.org/specs/rfc9110.html#section-9.3.8
+  -/
+  | trace
+
+  /--
+  Remove a URI binding from a resource.
+  Source: https://www.rfc-editor.org/rfc/rfc5842#section-5
+  -/
+  | unbind
+
+  /--
+  Undo a previous checkout of a version-controlled resource.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-4.5
+  -/
+  | uncheckout
+
+  /--
+  Remove a link relationship between resources.
+  Source: https://www.rfc-editor.org/rfc/rfc2068#section-19.6.1.3
+  -/
+  | unlink
+
+  /--
+  Unlock a resource.
+  Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.11
+  -/
+  | unlock
+
+  /--
+  Update a version-controlled resource.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-7.1
+  -/
+  | update
+
+  /--
+  Update a redirect reference resource.
+  Source: https://www.rfc-editor.org/rfc/rfc4437#section-7
+  -/
+  | updateredirectref
+
+  /--
+  Put a resource under version control.
+  Source: https://www.rfc-editor.org/rfc/rfc3253#section-3.5
+  -/
+  | versionControl
+deriving Repr, Inhabited, BEq, DecidableEq
+
+namespace Method
+
+/--
+Converts a `String` into a `Method`. Returns `none` for unrecognized method strings.
+-/
+def ofString? : String → Option Method
+  | "ACL" => some .acl
+  | "BASELINE-CONTROL" => some .baselineControl
+  | "BIND" => some .bind
+  | "CHECKIN" => some .checkin
+  | "CHECKOUT" => some .checkout
+  | "CONNECT" => some .connect
+  | "COPY" => some .copy
+  | "DELETE" => some .delete
+  | "GET" => some .get
+  | "HEAD" => some .head
+  | "LABEL" => some .label
+  | "LINK" => some .link
+  | "LOCK" => some .lock
+  | "MERGE" => some .merge
+  | "MKACTIVITY" => some .mkactivity
+  | "MKCALENDAR" => some .mkcalendar
+  | "MKCOL" => some .mkcol
+  | "MKREDIRECTREF" => some .mkredirectref
+  | "MKWORKSPACE" => some .mkworkspace
+  | "MOVE" => some .move
+  | "OPTIONS" => some .options
+  | "ORDERPATCH" => some .orderpatch
+  | "PATCH" => some .patch
+  | "POST" => some .post
+  | "PRI" => some .pri
+  | "PROPFIND" => some .propfind
+  | "PROPPATCH" => some .proppatch
+  | "PUT" => some .put
+  | "QUERY" => some .query
+  | "REBIND" => some .rebind
+  | "REPORT" => some .report
+  | "SEARCH" => some .search
+  | "TRACE" => some .trace
+  | "UNBIND" => some .unbind
+  | "UNCHECKOUT" => some .uncheckout
+  | "UNLINK" => some .unlink
+  | "UNLOCK" => some .unlock
+  | "UPDATE" => some .update
+  | "UPDATEREDIRECTREF" => some .updateredirectref
+  | "VERSION-CONTROL" => some .versionControl
+  | _ => none
+
+/--
+Converts a `String` into a `Method`, panicking if unrecognized.
+-/
+def ofString! (s : String) : Method :=
+  match ofString? s with
+  | some m => m
+  | none => panic! s!"invalid HTTP method: {s.quote}"
+
+instance : ToString Method where
+  toString
+    | .acl => "ACL"
+    | .baselineControl => "BASELINE-CONTROL"
+    | .bind => "BIND"
+    | .checkin => "CHECKIN"
+    | .checkout => "CHECKOUT"
+    | .connect => "CONNECT"
+    | .copy => "COPY"
+    | .delete => "DELETE"
+    | .get => "GET"
+    | .head => "HEAD"
+    | .label => "LABEL"
+    | .link => "LINK"
+    | .lock => "LOCK"
+    | .merge => "MERGE"
+    | .mkactivity => "MKACTIVITY"
+    | .mkcalendar => "MKCALENDAR"
+    | .mkcol => "MKCOL"
+    | .mkredirectref => "MKREDIRECTREF"
+    | .mkworkspace => "MKWORKSPACE"
+    | .move => "MOVE"
+    | .options => "OPTIONS"
+    | .orderpatch => "ORDERPATCH"
+    | .patch => "PATCH"
+    | .post => "POST"
+    | .pri => "PRI"
+    | .propfind => "PROPFIND"
+    | .proppatch => "PROPPATCH"
+    | .put => "PUT"
+    | .query => "QUERY"
+    | .rebind => "REBIND"
+    | .report => "REPORT"
+    | .search => "SEARCH"
+    | .trace => "TRACE"
+    | .unbind => "UNBIND"
+    | .uncheckout => "UNCHECKOUT"
+    | .unlink => "UNLINK"
+    | .unlock => "UNLOCK"
+    | .update => "UPDATE"
+    | .updateredirectref => "UPDATEREDIRECTREF"
+    | .versionControl => "VERSION-CONTROL"
+
+instance : Encode .v11 Method where
+  encode buffer := buffer.writeString ∘ toString
+
+end Std.Http.Method

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

@@ -0,0 +1,228 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Data.Extensions
+public import Std.Internal.Http.Data.Method
+public import Std.Internal.Http.Data.Version
+
+public section
+
+/-!
+# Request
+
+This module provides the `Request` type, which represents an HTTP request. It also defines ways
+to build a `Request` using functions that make it easier.
+
+References:
+* https://httpwg.org/specs/rfc9112.html#request.line
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+/--
+The main parts of a request containing the HTTP method, version, and request target URI.
+
+Reference: https://httpwg.org/specs/rfc9112.html#request.line
+-/
+structure Request.Head where
+  /--
+  The HTTP method (GET, POST, PUT, DELETE, etc.) for the request
+
+  Reference: https://httpwg.org/specs/rfc9112.html#rfc.section.3.1
+  -/
+  method : Method
+
+  /--
+  The HTTP protocol version for the request (e.g. HTTP/1.1, HTTP/2.0, HTTP/3.0).
+
+  Reference: https://httpwg.org/specs/rfc9112.html#http.version
+  -/
+  version : Version
+
+  /--
+  The raw request-target string (commonly origin-form path/query, `"*"`, or authority-form).
+  -/
+  uri : String
+deriving Inhabited, Repr
+
+/--
+HTTP request structure parameterized by body type.
+-/
+structure Request (t : Type) where
+  /--
+  The request line information (`method`, `version`, and request-target `uri`).
+  -/
+  line : Request.Head
+
+  /--
+  The request body content of type t.
+  -/
+  body : t
+
+  /--
+  Optional dynamic metadata attached to the request.
+  -/
+  extensions : Extensions := .empty
+deriving Inhabited
+
+/--
+Builds an HTTP Request.
+-/
+structure Request.Builder where
+  /--
+  The request-line of an HTTP request.
+  -/
+  line : Head := { method := .get, version := .v11, uri := "*" }
+
+  /--
+  Optional dynamic metadata attached to the request.
+  -/
+  extensions : Extensions := .empty
+
+namespace Request
+
+instance : ToString Head where
+  toString req :=
+    toString req.method ++ " " ++
+    toString req.uri ++ " " ++
+    toString req.version ++
+    "\r\n"
+
+open Internal in
+instance : Encode .v11 Head where
+  encode buffer req :=
+    let buffer := Encode.encode (v := .v11) buffer req.method
+    let buffer := buffer.writeChar ' '
+    let buffer := buffer.writeString req.uri
+    let buffer := buffer.writeChar ' '
+    let buffer := Encode.encode (v := .v11) buffer req.version
+    buffer.writeString "\r\n"
+
+/--
+Creates a new HTTP request builder with the default head
+(method: GET, version: HTTP/1.1, target: `*`).
+-/
+def new : Builder := { }
+
+namespace Builder
+
+/--
+Creates a new HTTP request builder with the default head
+(method: GET, version: HTTP/1.1, target: `*`).
+-/
+def empty : Builder := { }
+
+/--
+Sets the HTTP method for the request being built.
+-/
+def method (builder : Builder) (method : Method) : Builder :=
+  { builder with line := { builder.line with method := method } }
+
+/--
+Sets the HTTP version for the request being built.
+-/
+def version (builder : Builder) (version : Version) : Builder :=
+  { builder with line := { builder.line with version := version } }
+
+/--
+Sets the request target/URI for the request being built.
+-/
+def uri (builder : Builder) (uri : String) : Builder :=
+  { builder with line := { builder.line with uri := uri } }
+
+/--
+Inserts a typed extension value into the request being built.
+-/
+def extension (builder : Builder) [TypeName α] (data : α) : Builder :=
+  { builder with extensions := builder.extensions.insert data }
+
+/--
+Builds and returns the final HTTP Request with the specified body.
+-/
+def body (builder : Builder) (body : t) : Request t :=
+  { line := builder.line, body := body, extensions := builder.extensions }
+
+end Builder
+
+/--
+Creates a new HTTP GET Request with the specified URI.
+-/
+def get (uri : String) : Builder :=
+  new
+  |>.method .get
+  |>.uri uri
+
+/--
+Creates a new HTTP POST Request builder with the specified URI.
+-/
+def post (uri : String) : Builder :=
+  new
+  |>.method .post
+  |>.uri uri
+
+/--
+Creates a new HTTP PUT Request builder with the specified URI.
+-/
+def put (uri : String) : Builder :=
+  new
+  |>.method .put
+  |>.uri uri
+
+/--
+Creates a new HTTP DELETE Request builder with the specified URI.
+-/
+def delete (uri : String) : Builder :=
+  new
+  |>.method .delete
+  |>.uri uri
+
+/--
+Creates a new HTTP PATCH Request builder with the specified URI.
+-/
+def patch (uri : String) : Builder :=
+  new
+  |>.method .patch
+  |>.uri uri
+
+/--
+Creates a new HTTP HEAD Request builder with the specified URI.
+-/
+def head (uri : String) : Builder :=
+  new
+  |>.method .head
+  |>.uri uri
+
+/--
+Creates a new HTTP OPTIONS Request builder with the specified URI.
+Use `Request.options "*"` for server-wide OPTIONS.
+-/
+def options (uri : String) : Builder :=
+  new
+  |>.method .options
+  |>.uri uri
+
+/--
+Creates a new HTTP CONNECT Request builder with the specified URI.
+Typically used with authority-form URIs such as `"example.com:443"` for tunneling.
+-/
+def connect (uri : String) : Builder :=
+  new
+  |>.method .connect
+  |>.uri uri
+
+/--
+Creates a new HTTP TRACE Request builder with the specified URI.
+-/
+def trace (uri : String) : Builder :=
+  new
+  |>.method .trace
+  |>.uri uri
+
+end Std.Http.Request

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

@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Data.Extensions
+public import Std.Internal.Http.Data.Status
+public import Std.Internal.Http.Data.Version
+
+public section
+
+/-!
+# Response
+
+This module provides the `Response` type, which represents an HTTP response. It also defines
+builder functions for constructing responses and selecting common HTTP status codes.
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+/--
+The main parts of a response.
+-/
+structure Response.Head where
+  /--
+  The HTTP status for the response.
+  -/
+  status : Status := .ok
+
+  /--
+  The HTTP protocol version used in the response, e.g. `HTTP/1.1`.
+  -/
+  version : Version := .v11
+deriving Inhabited, Repr
+
+/--
+HTTP response structure parameterized by body type.
+-/
+structure Response (t : Type) where
+  /--
+  The response status-line information.
+  -/
+  line : Response.Head := {}
+
+  /--
+  The content of the response.
+  -/
+  body : t
+
+  /--
+  Optional dynamic metadata attached to the response.
+  -/
+  extensions : Extensions := .empty
+deriving Inhabited
+
+/--
+Builds an HTTP Response.
+-/
+structure Response.Builder where
+  /--
+  The response status-line information.
+  -/
+  line : Head := {}
+
+  /--
+  Optional dynamic metadata attached to the response.
+  -/
+  extensions : Extensions := .empty
+
+namespace Response
+
+instance : ToString Head where
+  toString r :=
+    toString r.version ++ " " ++
+    toString r.status.toCode ++ " " ++
+    r.status.reasonPhrase ++ "\r\n"
+
+open Internal in
+instance : Encode .v11 Head where
+  encode buffer r :=
+    let buffer := Encode.encode (v := .v11) buffer r.version
+    let buffer := buffer.writeChar ' '
+    let buffer := buffer.writeString (toString r.status.toCode)
+    let buffer := buffer.writeChar ' '
+    let buffer := buffer.writeString r.status.reasonPhrase
+    buffer.writeString "\r\n"
+
+/--
+Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).
+-/
+def new : Builder := { }
+
+namespace Builder
+
+/--
+Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).
+-/
+def empty : Builder := { }
+
+/--
+Sets the HTTP status code for the response being built.
+-/
+def status (builder : Builder) (status : Status) : Builder :=
+  { builder with line := { builder.line with status := status } }
+
+/--
+Inserts a typed extension value into the response being built.
+-/
+def extension (builder : Builder) [TypeName α] (data : α) : Builder :=
+  { builder with extensions := builder.extensions.insert data }
+
+/--
+Builds and returns the final HTTP Response with the specified body.
+-/
+def body (builder : Builder) (body : t) : Response t :=
+  { line := builder.line, body := body, extensions := builder.extensions }
+
+/--
+Builds and returns the final HTTP Response with an empty body (`{}`).
+Requires an `EmptyCollection` instance for the response body type.
+-/
+def build [EmptyCollection t] (builder : Builder) : Response t :=
+  { line := builder.line, body := {}, extensions := builder.extensions }
+
+end Builder
+
+/--
+Creates a new HTTP Response builder with the 200 status code.
+-/
+def ok : Builder :=
+  .empty |>.status .ok
+
+/--
+Creates a new HTTP Response builder with the provided status.
+-/
+def withStatus (status : Status) : Builder :=
+  .empty |>.status status
+
+/--
+Creates a new HTTP Response builder with the 404 status code.
+-/
+def notFound : Builder :=
+  .empty |>.status .notFound
+
+/--
+Creates a new HTTP Response builder with the 500 status code.
+-/
+def internalServerError : Builder :=
+  .empty |>.status .internalServerError
+
+/--
+Creates a new HTTP Response builder with the 400 status code.
+-/
+def badRequest : Builder :=
+  .empty |>.status .badRequest
+
+/--
+Creates a new HTTP Response builder with the 201 status code.
+-/
+def created : Builder :=
+  .empty |>.status .created
+
+/--
+Creates a new HTTP Response builder with the 202 status code.
+-/
+def accepted : Builder :=
+  .empty |>.status .accepted
+
+/--
+Creates a new HTTP Response builder with the 401 status code.
+-/
+def unauthorized : Builder :=
+  .empty |>.status .unauthorized
+
+/--
+Creates a new HTTP Response builder with the 403 status code.
+-/
+def forbidden : Builder :=
+  .empty |>.status .forbidden
+
+/--
+Creates a new HTTP Response builder with the 409 status code.
+-/
+def conflict : Builder :=
+  .empty |>.status .conflict
+
+/--
+Creates a new HTTP Response builder with the 503 status code.
+-/
+def serviceUnavailable : Builder :=
+  .empty |>.status .serviceUnavailable
+
+end Response

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

@@ -0,0 +1,722 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Internal
+
+public section
+
+/-!
+# Status
+
+This module defines the `Status` type, a representation of HTTP status codes. Status codes are
+three-digit integer codes that describe the result of an HTTP request. This implementation
+includes common named statuses and supports custom codes through `Status.other`.
+
+Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+open Internal
+
+/--
+A proposition stating that `s` is a valid HTTP reason phrase: every character passes
+`Char.reasonPhraseChar` per RFC 9110 §15.
+
+Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase
+-/
+abbrev IsValidReasonPhrase (s : String) : Prop :=
+  s.toList.all Char.reasonPhraseChar
+
+/--
+Returns `true` for every status code that has a dedicated named constructor in `Status`.
+Used to ensure `Status.other` is never constructed with a code that already has a name.
+-/
+def isKnownStatusCode (code: UInt16) : Bool :=
+  code matches 100 | 101 | 102 | 103
+  | 200 | 201 | 202 | 203 | 204 | 205 | 206 | 207 | 208 | 226
+  | 300 | 301 | 302 | 303 | 304 | 305 | 306 | 307 | 308
+  | 400 | 401 | 402 | 403 | 404 | 405 | 406 | 407 | 408 | 409 | 410
+  | 411 | 412 | 413 | 414 | 415 | 416 | 417 | 418 | 421 | 422 | 423
+  | 424 | 425 | 426 | 428 | 429 | 431 | 451
+  | 500 | 501 | 502 | 503 | 504 | 505 | 506 | 507 | 508 | 510 | 511
+
+/--
+A custom HTTP status with a numeric code and a reason phrase. Used to represent status codes
+not enumerated as dedicated constructors in `Status`. The code must be in the range 100–999
+(a three-digit integer per RFC 9112 §4) and must not correspond to any named constructor.
+
+Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+structure CustomStatus where
+
+  /--
+  The numeric status code.
+  -/
+  code : UInt16
+
+  /--
+  The reason phrase associated with the status code.
+  -/
+  phrase : String
+
+  /--
+  Proof that the reason phrase contains only valid characters.
+  -/
+  validReasonPhrase : IsValidReasonPhrase phrase := by decide
+
+  /--
+  Proof that the code is a valid HTTP status code (100–999), i.e. a three-digit integer
+  as required by RFC 9112 §4.
+  -/
+  validCode : 100 ≤ code ∧ code ≤ 999 := by decide
+
+  /--
+  Proof that the code does not clash with any named `Status` constructor.
+  -/
+  validUnknown : ¬isKnownStatusCode code := by decide
+deriving Repr, BEq
+
+instance : Inhabited CustomStatus where
+  default := ⟨209, "Unknown", by decide, by decide, by decide⟩
+
+instance : ToString CustomStatus where
+  toString s := s.phrase
+
+namespace CustomStatus
+
+/--
+Attempts to create a `CustomStatus` from a numeric code and a reason phrase string, returning
+`none` if the phrase contains invalid characters.
+-/
+def ofCodeAndPhrase? (code : UInt16) (phrase : String) : Option CustomStatus :=
+  if h : IsValidReasonPhrase phrase ∧ (100 ≤ code ∧ code ≤ 999) ∧ ¬isKnownStatusCode code then
+    some ⟨code, phrase, h.left, h.right.left, h.right.right⟩
+  else
+    none
+
+end CustomStatus
+
+/--
+HTTP Status codes. Status codes are three-digit integer codes that describe the result of an
+HTTP request. This implementation includes common named statuses and supports custom codes through
+`Status.other`.
+
+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
+
+  /--
+  A custom status code not covered by the standard constructors above.
+  -/
+  | other (status : CustomStatus)
+deriving Repr, Inhabited, BEq
+
+namespace Status
+
+/--
+Converts 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
+  | other c => c.code
+
+/--
+Converts a `UInt16` to `Status`.
+-/
+def ofCode (reasonPhrase : Option { x : String // IsValidReasonPhrase x }) (code: UInt16) : Option Status :=
+  match h : code with
+  | 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
+  | n =>
+    let ph := reasonPhrase.getD ⟨"Unknown", by decide⟩
+
+    if h : (100 ≤ n ∧ n ≤ 999) ∧ ¬isKnownStatusCode n then
+      some <| .other ⟨n, ph.val, ph.property, h.left, h.right⟩
+    else
+      none
+
+/--
+Checks if the type of the status code is informational, meaning that the request was received
+and the process is continuing.
+
+Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+@[inline]
+def isInformational (c : Status) : Bool :=
+  100 ≤ c.toCode ∧ c.toCode < 200
+
+/--
+Checks if the status code is a success status, meaning that the request was successfully received,
+understood, and accepted.
+
+Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+@[inline]
+def isSuccess (c : Status) : Bool :=
+  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) : Bool :=
+  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) : Bool :=
+  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) : Bool :=
+  500 ≤ c.toCode ∧ c.toCode < 600
+
+/--
+Checks if the status code indicates an error (either client error 4xx or server error 5xx).
+
+Reference: https://httpwg.org/specs/rfc9110.html#status.codes
+-/
+@[inline]
+def isError (c : Status) : Bool :=
+  c.isClientError ∨ c.isServerError
+
+/--
+Returns the standard reason phrase for an HTTP status code as defined in RFC 9110.
+For known status codes this returns the canonical phrase (e.g., "OK" for 200).
+For unknown codes (`other n s`), returns the caller-supplied reason phrase `s`.
+-/
+def reasonPhrase : Status → String
+  | .«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 => "Payload Too Large"
+  | .uriTooLong => "URI Too Long"
+  | .unsupportedMediaType => "Unsupported Media Type"
+  | .rangeNotSatisfiable => "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"
+  | .other c => c.phrase
+
+instance : ToString Status where
+  toString := reasonPhrase
+
+instance : Encode .v11 Status where
+  encode buffer status := buffer
+    |>.writeString (toString <| toCode status)
+    |>.writeChar ' '
+    |>.writeString status.reasonPhrase
+
+end Std.Http.Status

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

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+import Init.Data.ToString
+public import Init.Data.String
+
+public section
+
+/-!
+# Version
+
+This module defines `Version`, the set of HTTP protocol versions modeled by this library.
+
+Reference: https://httpwg.org/specs/rfc9110.html#protocol.version
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+/--
+HTTP protocol versions modeled by this library.
+
+Reference: https://httpwg.org/specs/rfc9110.html#protocol.version
+-/
+inductive Version
+  /--
+  `HTTP/1.0`
+  -/
+  | v10
+
+  /--
+  `HTTP/1.1`
+  -/
+  | v11
+
+  /--
+  `HTTP/2.0`
+  -/
+  | v20
+
+  /--
+  `HTTP/3.0`
+  -/
+  | v30
+deriving Repr, Inhabited, BEq, DecidableEq
+
+namespace Version
+
+/--
+Converts a pair of `Nat` to the corresponding `Version`.
+-/
+def ofNumber? : Nat → Nat → Option Version
+  | 1, 0 => some .v10
+  | 1, 1 => some .v11
+  | 2, 0 => some .v20
+  | 3, 0 => some .v30
+  | _, _ => none
+
+/--
+Converts `String` to the corresponding `Version`.
+-/
+def ofString? : String → Option Version
+  | "HTTP/1.0" => some .v10
+  | "HTTP/1.1" => some .v11
+  | "HTTP/2.0" => some .v20
+  | "HTTP/3.0" => some .v30
+  | _ => none
+
+/--
+Converts `String` to the corresponding `Version`, panics if invalid.
+-/
+def ofString! (s : String) : Version :=
+  match ofString? s with
+  | some v => v
+  | none => panic! s!"invalid HTTP version: {s.quote}"
+
+/--
+Converts a `Version` to its corresponding major and minor numbers as a pair.
+-/
+def toNumber : Version → (Nat × Nat)
+  | .v10 => (1, 0)
+  | .v11 => (1, 1)
+  | .v20 => (2, 0)
+  | .v30 => (3, 0)
+
+instance : ToString Version where
+  toString
+    | .v10 => "HTTP/1.0"
+    | .v11 => "HTTP/1.1"
+    | .v20 => "HTTP/2.0"
+    | .v30 => "HTTP/3.0"
+
+end Std.Http.Version

src/Std/Internal/Http/Internal.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Internal.ChunkedBuffer
+public import Std.Internal.Http.Internal.Encode
+public import Std.Internal.Http.Internal.String
+public import Std.Internal.Http.Internal.Char
+
+/-!
+# HTTP Internal Utilities
+
+This module re-exports internal utilities used by the HTTP library including
+data structures, encoding functions, and buffer management.
+-/

src/Std/Internal/Http/Internal/Char.lean

@@ -0,0 +1,281 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Init.Data.String
+
+@[expose]
+public section
+
+/-!
+# HTTP Character Predicates
+
+This module provides shared character validation predicates used across the HTTP library.
+All predicates in this module are ASCII-only by design (`isAscii c` where applicable), and
+intentionally exclude `obs-text` and all non-ASCII code points.
+-/
+
+namespace Std.Http.Internal.Char
+
+set_option linter.all true
+
+/--
+Checks if a character is ASCII (Unicode code point < 128).
+-/
+@[inline, expose]
+def isAscii (c : Char) : Bool :=
+  c.toNat < 128
+
+/--
+Checks if a byte represents an ASCII character (value < 128).
+-/
+@[inline, expose]
+def isAsciiByte (c : UInt8) : Bool :=
+  c < 128
+
+/--
+Checks if a byte is a decimal digit (0-9).
+-/
+@[inline, expose]
+def isDigitByte (c : UInt8) : Bool :=
+  c >= '0'.toUInt8 && c <= '9'.toUInt8
+
+/--
+Checks if a byte is an alphabetic character (a-z or A-Z).
+-/
+@[inline, expose]
+def isAlphaByte (c : UInt8) : Bool :=
+  (c >= 'A'.toUInt8 && c <= 'Z'.toUInt8) || (c >= 'a'.toUInt8 && c <= 'z'.toUInt8)
+
+/--
+tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*"
+  / "+" / "-" / "." / "^" / "_" / "`" / "|" / "~"
+  / DIGIT / ALPHA
+  ; Visible token characters used to build `token`.
+-/
+@[inline]
+def tchar (c : Char) : Bool :=
+  (c matches '!' | '#' | '$' | '%' | '&' | '\'' | '*' | '+' | '-' | '.' | '^' | '_' | '`' | '|' | '~') ||
+  Char.isDigit c ||
+  Char.isAlpha c
+
+/--
+vchar = %x21-7E
+; Visible (printing) ASCII characters.
+-/
+@[inline]
+def vchar (c : Char) : Bool :=
+  c ≥ '!' ∧ c ≤ '~'
+
+/--
+qdtext = HTAB / SP / %x21 / %x23-5B / %x5D-7E
+; ASCII-only variant (no obs-text).
+-/
+@[inline]
+def qdtext (c : Char) : Bool :=
+  (c matches '\t' | ' ' | '!') ||
+  ('#' ≤ c ∧ c ≤ '[') ||
+  (']' ≤ c ∧ c ≤ '~')
+
+/--
+quoted-pair = "\\" ( HTAB / SP / VCHAR )
+; ASCII-only variant (no obs-text).
+-/
+@[inline]
+def quotedPairChar (c : Char) : Bool :=
+  (c matches '\t' | ' ') || vchar c
+
+/--
+quoted-string body character class:
+( qdtext / quoted-pair payload ) in ASCII-only mode.
+-/
+@[inline]
+def quotedStringChar (c : Char) : Bool :=
+  qdtext c || quotedPairChar c
+
+/--
+field-vchar = VCHAR
+; ASCII-only variant (no obs-text).
+-/
+@[inline]
+def fieldVchar (c : Char) : Bool :=
+  vchar c
+
+/--
+field-content character class:
+field-vchar / SP / HTAB
+; ASCII-only variant (no obs-text).
+-/
+@[inline]
+def fieldContent (c : Char) : Bool :=
+  fieldVchar c || (c matches ' ' | '\t')
+
+/--
+ctext = HTAB / SP / %x21-27 / %x2A-5B / %x5D-7E
+; ASCII-only variant (no obs-text).
+-/
+@[inline]
+def ctext (c : Char) : Bool :=
+  (c matches '\t' | ' ') ||
+  ('!' ≤ c ∧ c ≤ '\'') ||
+  ('*' ≤ c ∧ c ≤ '[') ||
+  (']' ≤ c ∧ c ≤ '~')
+
+/--
+etagc = "!" / %x23-7E
+; ASCII-only variant (no obs-text).
+-/
+@[inline]
+def etagc (c : Char) : Bool :=
+  c = '!' || ('#' ≤ c ∧ c ≤ '~')
+
+/--
+OWS = *( SP / HTAB )  (character class only)
+-/
+@[inline]
+def ows (c : Char) : Bool :=
+  c matches ' ' | '\t'
+
+/--
+BWS = OWS (character class alias)
+-/
+@[inline]
+def bws (c : Char) : Bool :=
+  ows c
+
+/--
+RWS = 1*( SP / HTAB ) (character class is identical to `ows`)
+-/
+@[inline]
+def rws (c : Char) : Bool :=
+  ows c
+
+/--
+obs-text = %x80-FF (and higher Unicode scalar values in this library's `Char` model).
+-/
+@[inline]
+def obsText (c : Char) : Bool :=
+  0x80 ≤ c.toNat
+
+/--
+reason-phrase character class:
+HTAB / SP / VCHAR
+; ASCII-only variant (no obs-text).
+
+Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase
+-/
+@[inline]
+def reasonPhraseChar (c : Char) : Bool :=
+  (c matches '\t' | ' ') || vchar c
+
+/--
+Checks if a character is a hexadecimal digit (0-9, a-f, or A-F).
+-/
+@[inline, expose]
+def isHexDigit (c : Char) : Bool :=
+  (c matches 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'A' | 'B' | 'C' | 'D' | 'E' | 'F') ||
+  Char.isDigit c
+
+/--
+Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F).
+-/
+@[inline, expose]
+def isHexDigitByte (c : UInt8) : Bool :=
+  (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) ||
+  (c ≥ 'a'.toUInt8 && c ≤ 'f'.toUInt8) ||
+  (c ≥ 'A'.toUInt8 && c ≤ 'F'.toUInt8)
+
+/--
+Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z).
+-/
+@[inline, expose]
+def isAlphaNum (c : UInt8) : Bool :=
+  (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) ||
+  (c ≥ 'a'.toUInt8 && c ≤ 'z'.toUInt8) ||
+  (c ≥ 'A'.toUInt8 && c ≤ 'Z'.toUInt8)
+
+/--
+Checks whether `c` is an ASCII alphanumeric character.
+-/
+@[inline, expose]
+def isAsciiAlphaNumChar (c : Char) : Bool :=
+  isAscii c && (Char.isDigit c || Char.isAlpha c)
+
+/--
+Checks if a character is valid after the first character of a URI scheme.
+Valid characters are ASCII alphanumeric, `+`, `-`, and `.`.
+-/
+@[inline, expose]
+def isValidSchemeChar (c : Char) : Bool :=
+  isAsciiAlphaNumChar c || (c matches '+' | '-' | '.')
+
+/--
+Checks if a character is valid for use in a domain name.
+Valid characters are ASCII alphanumeric, hyphens, and dots.
+-/
+@[inline, expose]
+def isValidDomainNameChar (c : Char) : Bool :=
+  isAsciiAlphaNumChar c || (c matches '-' | '.')
+
+/--
+Checks if a byte is an unreserved character according to RFC 3986. Unreserved characters are:
+alphanumeric, hyphen, period, underscore, and tilde.
+-/
+@[inline, expose]
+def isUnreserved (c : UInt8) : Bool :=
+  isAlphaNum c ||
+  (c = '-'.toUInt8 || c = '.'.toUInt8 || c = '_'.toUInt8 || c = '~'.toUInt8)
+
+/--
+Checks if a byte is a sub-delimiter character according to RFC 3986.
+Sub-delimiters are: `!`, `$`, `&`, `'`, `(`, `)`, `*`, `+`, `,`, `;`, `=`.
+-/
+@[inline, expose]
+def isSubDelims (c : UInt8) : Bool :=
+  c = '!'.toUInt8 || c = '$'.toUInt8 || c = '&'.toUInt8 || c = ('\'' : Char).toUInt8 ||
+  c = '('.toUInt8 || c = ')'.toUInt8 || c = '*'.toUInt8 || c = '+'.toUInt8 ||
+  c = ','.toUInt8 || c = ';'.toUInt8 || c = '='.toUInt8
+
+/--
+Checks if a byte is a valid path character (`pchar`) according to RFC 3986.
+`pchar = unreserved / pct-encoded / sub-delims / ":" / "@"`
+
+Note: The percent-encoding (`pct-encoded`) is handled separately by `isEncodedChar`,
+so this predicate only covers the non-percent characters.
+-/
+@[inline, expose]
+def isPChar (c : UInt8) : Bool :=
+  isUnreserved c || isSubDelims c || c = ':'.toUInt8 || c = '@'.toUInt8
+
+/--
+Checks if a byte is a valid character in a URI query component according to RFC 3986.
+`query = *( pchar / "/" / "?" )`
+-/
+@[inline, expose]
+def isQueryChar (c : UInt8) : Bool :=
+  isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8
+
+/--
+Checks if a byte is a valid character in a URI fragment component according to RFC 3986.
+`fragment = *( pchar / "/" / "?" )`
+-/
+@[inline, expose]
+def isFragmentChar (c : UInt8) : Bool :=
+  isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8
+
+/--
+Checks if a byte is a valid character in a URI userinfo component according to RFC 3986.
+`userinfo = *( unreserved/ sub-delims / ":" )`
+
+Note: It avoids the pct-encoded of the original grammar because it is used with `Encoding.lean`
+that provides it.
+-/
+@[inline, expose]
+def isUserInfoChar (c : UInt8) : Bool :=
+  isUnreserved c || isSubDelims c || c = ':'.toUInt8
+
+end Std.Http.Internal.Char

src/Std/Internal/Http/Internal/ChunkedBuffer.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+import Init.Data.ToString
+import Init.Data.Array.Lemmas
+public import Init.Data.String
+public import Init.Data.ByteArray
+
+public section
+
+/-!
+# ChunkedBuffer
+
+This module provides an efficient way to concatenate multiple `ByteArray`s by deferring the actual
+concatenation until necessary. This is particularly useful in HTTP response building and streaming
+scenarios where data is accumulated incrementally.
+-/
+
+namespace Std.Http.Internal
+
+set_option linter.all true
+
+/--
+A structure that accumulates multiple `ByteArray`s efficiently by tracking them in an array and
+maintaining the total size. This allows building large buffers without repeated allocations and copies.
+-/
+structure ChunkedBuffer where
+  /--
+  The accumulated byte arrays.
+  -/
+  data : Array ByteArray
+
+  /--
+  The total size in bytes of all accumulated arrays
+  -/
+  size : Nat
+
+namespace ChunkedBuffer
+
+/--
+An empty `ChunkedBuffer`.
+-/
+@[inline]
+def empty : ChunkedBuffer :=
+  { data := #[], size := 0 }
+
+/--
+Append a single `ByteArray` to the `ChunkedBuffer`.
+-/
+@[inline]
+def push (c : ChunkedBuffer) (b : ByteArray) : ChunkedBuffer :=
+  { data := c.data.push b, size := c.size + b.size }
+
+/--
+Writes a `ByteArray` to the `ChunkedBuffer`.
+-/
+@[inline]
+def write (buffer : ChunkedBuffer) (data : ByteArray) : ChunkedBuffer :=
+  buffer.push data
+
+/--
+Writes a `ChunkedBuffer` to the `ChunkedBuffer`.
+-/
+@[inline]
+def append (buffer : ChunkedBuffer) (data : ChunkedBuffer) : ChunkedBuffer :=
+  { data := buffer.data ++ data.data, size := buffer.size + data.size }
+
+/--
+Writes a `Char` to the `ChunkedBuffer`. Only the low byte is written (`Char.toUInt8`),
+so this is only correct for ASCII characters.
+-/
+@[inline]
+def writeChar (buffer : ChunkedBuffer) (data : Char) : ChunkedBuffer :=
+  buffer.push (ByteArray.mk #[data.toUInt8])
+
+/--
+Writes a `String` to the `ChunkedBuffer`.
+-/
+@[inline]
+def writeString (buffer : ChunkedBuffer) (data : String) : ChunkedBuffer :=
+  buffer.push data.toUTF8
+
+/--
+Turn the combined structure into a single contiguous ByteArray.
+-/
+@[inline]
+def toByteArray (cb : ChunkedBuffer) : ByteArray :=
+  if h : 1 = cb.data.size then
+    cb.data[0]'(Nat.le_of_eq h)
+  else
+    cb.data.foldl (· ++ ·) (.emptyWithCapacity cb.size)
+
+/--
+Build from a ByteArray directly.
+-/
+@[inline]
+def ofByteArray (bs : ByteArray) : ChunkedBuffer :=
+  { data := #[bs], size := bs.size }
+
+/--
+Build from an array of ByteArrays directly.
+-/
+@[inline]
+def ofArray (bs : Array ByteArray) : ChunkedBuffer :=
+  { data := bs, size := bs.foldl (· + ·.size) 0 }
+
+/--
+Checks whether the buffer is empty.
+-/
+@[inline]
+def isEmpty (bb : ChunkedBuffer) : Bool :=
+  bb.size = 0
+
+instance : Inhabited ChunkedBuffer := ⟨empty⟩
+
+instance : EmptyCollection ChunkedBuffer where
+  emptyCollection := empty
+
+instance : Coe ByteArray ChunkedBuffer where
+  coe := ofByteArray
+
+instance : Coe (Array ByteArray) ChunkedBuffer where
+  coe := ofArray
+
+end Std.Http.Internal.ChunkedBuffer

src/Std/Internal/Http/Internal/Encode.lean

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

src/Std/Internal/Http/Internal/String.lean

@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+import Init.Grind
+public import Init.Data.String
+public import Std.Internal.Http.Internal.Char
+
+public section
+
+
+/-!
+# Internal String Helpers
+
+Shared string utilities for HTTP: token validation and quoted-string encoding/decoding for header
+parameter values and chunk extensions.
+-/
+
+namespace Std.Http.Internal
+
+open Char
+
+set_option linter.all true
+
+/--
+Core character quoting used by `String.quote`.
+
+In string context (`inString := true`), this emits:
+- `qdtext` characters directly
+- `"` and `\\` as `quoted-pair`
+and panics for characters outside the grammar.
+-/
+def quoteCore (c : Char) (inString : Bool := false) : String :=
+  if inString then
+    if qdtext c then
+      .singleton c
+    else if c = '\\' || c = '\"' then
+      .append "\\" (.singleton c)
+    else
+      panic! "invalid HTTP quoted-string content"
+  else
+    if quotedPairChar c then
+      .singleton c
+    else
+      panic! "invalid HTTP quoted-pair content"
+
+/--
+Attempts to quote `s` as an HTTP `quoted-string`:
+`DQUOTE *( qdtext / quoted-pair ) DQUOTE`.
+
+Returns `none` when any character in `s` cannot be represented by the grammar.
+-/
+@[expose]
+def quoteHttpString? (s : String) : Option String :=
+  if s.all tchar ∧ ¬s.isEmpty then
+    some s
+  else if s.all quotedStringChar then
+    some (.append
+      (.foldl (fun acc c =>
+        .append acc (quoteCore c (inString := true))) "\"" s)
+      "\"")
+  else
+    none
+
+/--
+Quotes `s` as an HTTP `quoted-string`, panicking if `s` contains characters that cannot be
+represented by `qdtext`/`quoted-pair`.
+-/
+def quoteHttpString! (s : String) : String :=
+  match quoteHttpString? s with
+  | some res => res
+  | none => panic! "invalid HTTP quoted-string content"
+
+private inductive UnquoteState where
+  | start
+  | valid (escaped : Bool) (acc : String)
+  | done (result : String)
+  | invalid
+
+/--
+Parses an HTTP `quoted-string`, returning the unescaped content when valid.
+-/
+def unquoteHttpString? (s : String) : Option String :=
+  if s.startsWith '"' then
+    match s.foldl (fun (st : UnquoteState) c =>
+      match st with
+      | .start =>
+          if c == '"' then .valid false "" else .invalid
+      | .valid false acc =>
+          if c == '\\' then .valid true acc
+          else if c == '"' then .done acc
+          else if qdtext c then .valid false (acc.push c)
+          else .invalid
+      | .valid true acc =>
+          if quotedPairChar c then .valid false (acc.push c)
+          else .invalid
+      | .done _ | .invalid => .invalid) .start with
+    | .done result => some result
+    | _ => none
+  else if s.all Char.tchar then
+    some s
+  else
+    none
+
+/--
+Checks whether a string is a valid non-empty HTTP token.
+-/
+@[expose]
+def isToken (s : String) : Bool :=
+  let s := s.toList
+  ¬s.isEmpty ∧ s.all Char.tchar
+
+end Std.Http.Internal

tests/lean/run/async_http_encode.lean

@@ -0,0 +1,504 @@
+import Std.Internal.Http.Data.Chunk
+import Std.Internal.Http.Data.Request
+import Std.Internal.Http.Data.Response
+
+open Std.Http
+open Std.Http.Internal
+
+private def encodeStr [Encode .v11 t] (v : t) : String :=
+  String.fromUTF8! (Encode.encode (v := .v11) ChunkedBuffer.empty v).toByteArray
+
+/-! ## Version encoding -/
+
+/--
+info: "HTTP/1.1"
+-/
+#guard_msgs in
+#eval encodeStr Version.v11
+
+/--
+info: "HTTP/2.0"
+-/
+#guard_msgs in
+#eval encodeStr Version.v20
+
+/--
+info: "HTTP/3.0"
+-/
+#guard_msgs in
+#eval encodeStr Version.v30
+
+/-! ## Method encoding -/
+
+/--
+info: "GET"
+-/
+#guard_msgs in
+#eval encodeStr Method.get
+
+/--
+info: "HEAD"
+-/
+#guard_msgs in
+#eval encodeStr Method.head
+
+/--
+info: "POST"
+-/
+#guard_msgs in
+#eval encodeStr Method.post
+
+/--
+info: "PUT"
+-/
+#guard_msgs in
+#eval encodeStr Method.put
+
+/--
+info: "DELETE"
+-/
+#guard_msgs in
+#eval encodeStr Method.delete
+
+/--
+info: "CONNECT"
+-/
+#guard_msgs in
+#eval encodeStr Method.connect
+
+/--
+info: "OPTIONS"
+-/
+#guard_msgs in
+#eval encodeStr Method.options
+
+/--
+info: "TRACE"
+-/
+#guard_msgs in
+#eval encodeStr Method.trace
+
+/--
+info: "PATCH"
+-/
+#guard_msgs in
+#eval encodeStr Method.patch
+
+/-! ## Status encoding -/
+
+/--
+info: "200 OK"
+-/
+#guard_msgs in
+#eval encodeStr Status.ok
+
+/--
+info: "201 Created"
+-/
+#guard_msgs in
+#eval encodeStr Status.created
+
+/--
+info: "404 Not Found"
+-/
+#guard_msgs in
+#eval encodeStr Status.notFound
+
+/--
+info: "500 Internal Server Error"
+-/
+#guard_msgs in
+#eval encodeStr Status.internalServerError
+
+/--
+info: "999 Unknown"
+-/
+#guard_msgs in
+#eval encodeStr (Status.other ⟨999, "Unknown", by decide, by decide, by decide⟩)
+
+/-! ## Request.line encoding -/
+
+/--
+info: "GET /path HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ method := .get, version := .v11, uri := "/path" } : Request.Head)
+
+/--
+info: "POST /submit HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ method := .post, version := .v11, uri := "/submit" } : Request.Head)
+
+/--
+info: "PUT /resource HTTP/2.0\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({
+    method := .put
+    version := .v20
+    uri := "/resource"
+  } : Request.Head)
+
+/-! ## Response.line encoding -/
+
+/--
+info: "HTTP/1.1 200 OK\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ status := .ok, version := .v11 } : Response.Head)
+
+/--
+info: "HTTP/1.1 404 Not Found\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ status := .notFound, version := .v11 } : Response.Head)
+
+/--
+info: "HTTP/2.0 500 Internal Server Error\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({
+    status := .internalServerError
+    version := .v20
+  } : Response.Head)
+
+/-! ## Chunk encoding -/
+
+/--
+info: "5\x0d\nhello\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "hello".toUTF8)
+
+/--
+info: "0\x0d\n\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr Chunk.empty
+
+/--
+info: "3;lang=en\x0d\nabc\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "lang") (.ofString! "en"))
+
+/--
+info: "3;lang=\"en \\\" u\";type=text\x0d\nabc\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "lang") (.ofString! "en \" u") |>.insertExtension (Chunk.ExtensionName.mk "type") (.ofString! "text"))
+
+/--
+info: "a\x0d\n0123456789\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "0123456789".toUTF8)
+
+/-! ## Request builder -/
+
+/--
+info: "GET /index.html HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.get "/index.html" |>.body ()).line
+
+/--
+info: "POST /api/data HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.post "/api/data" |>.body ()).line
+
+/--
+info: "PUT /resource HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.put "/resource" |>.body ()).line
+
+/--
+info: "DELETE /item HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.delete "/item" |>.body ()).line
+
+/--
+info: "PATCH /update HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.patch "/update" |>.body ()).line
+
+/--
+info: "HEAD /check HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.head "/check" |>.body ()).line
+
+/--
+info: "OPTIONS * HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.options "*" |>.body ()).line
+
+/--
+info: "CONNECT proxy:8080 HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.connect "proxy:8080" |>.body ()).line
+
+/--
+info: "TRACE /debug HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.trace "/debug" |>.body ()).line
+
+/--
+info: "POST /v2 HTTP/2.0\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Request.new |>.method .post |>.uri "/v2" |>.version .v20 |>.body ()).line
+
+/-! ## Response builder -/
+
+/--
+info: "HTTP/1.1 200 OK\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.ok |>.body ()).line
+
+/--
+info: "HTTP/1.1 404 Not Found\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.notFound |>.body ()).line
+
+/--
+info: "HTTP/1.1 500 Internal Server Error\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.internalServerError |>.body ()).line
+
+/--
+info: "HTTP/1.1 400 Bad Request\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.badRequest |>.body ()).line
+
+/--
+info: "HTTP/1.1 201 Created\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.created |>.body ()).line
+
+/--
+info: "HTTP/1.1 202 Accepted\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.accepted |>.body ()).line
+
+/--
+info: "HTTP/1.1 401 Unauthorized\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.unauthorized |>.body ()).line
+
+/--
+info: "HTTP/1.1 403 Forbidden\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.forbidden |>.body ()).line
+
+/--
+info: "HTTP/1.1 409 Conflict\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.conflict |>.body ()).line
+
+/--
+info: "HTTP/1.1 503 Service Unavailable\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.serviceUnavailable |>.body ()).line
+
+/--
+info: "HTTP/1.1 418 I'm a teapot\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Response.withStatus .imATeapot |>.body ()).line
+
+/-! ## Edge cases: Status encoding -/
+
+-- Status.other 0: minimum possible value
+/--
+info: "999 Unknown"
+-/
+#guard_msgs in
+#eval encodeStr (Status.other ⟨999, "Unknown", by decide, by decide, by decide⟩)
+
+-- Status.other that overlaps with a named status (100 = Continue)
+/--
+info: "888 Unknown"
+-/
+#guard_msgs in
+#eval encodeStr (Status.other ⟨888, "Unknown", by decide, by decide, by decide⟩)
+
+-- Status.other max UInt16
+/--
+info: "999 Unknown"
+-/
+#guard_msgs in
+#eval encodeStr (Status.other ⟨999, "Unknown", by decide, by decide, by decide⟩)
+
+-- Non-standard status code in the middle
+/--
+info: "299 Unknown"
+-/
+#guard_msgs in
+#eval encodeStr (Status.other ⟨299, "Unknown", by decide, by decide, by decide⟩)
+
+/-! ## Edge cases: Chunk size hex encoding -/
+
+-- Size 16 → hex "10" (first two-digit hex)
+/--
+info: "10\x0d\n0123456789abcdef\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "0123456789abcdef".toUTF8)
+
+-- Size 255 → hex "ff": verify prefix
+/--
+info: true
+-/
+#guard_msgs in
+#eval do
+  let data := ByteArray.mk (Array.replicate 255 (0x41 : UInt8))
+  return encodeStr (Chunk.ofByteArray data) |>.startsWith "ff\r\n"
+
+-- Size 256 → hex "100" (first three-digit hex): verify prefix
+/--
+info: true
+-/
+#guard_msgs in
+#eval do
+  let data := ByteArray.mk (Array.replicate 256 (0x41 : UInt8))
+  return encodeStr (Chunk.ofByteArray data) |>.startsWith "100\r\n"
+
+-- Size 15 → hex "f" (largest single hex digit)
+/--
+info: "f\x0d\n0123456789abcde\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "0123456789abcde".toUTF8)
+
+-- Chunk.ofByteArray with empty data (same as Chunk.empty)
+/--
+info: "0\x0d\n\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray ByteArray.empty)
+
+/-! ## Edge cases: Chunk extensions -/
+
+-- Extension with no value (None case) via direct struct construction
+/--
+info: "3;marker\x0d\nabc\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ data := "abc".toUTF8, extensions := #[(Chunk.ExtensionName.mk "marker", none)] } : Chunk)
+
+-- Extension with empty string value (not quoted since "".any returns false)
+/--
+info: "3;key=\"\"\x0d\nabc\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "key") (.ofString! ""))
+
+-- Extension value that is all token chars (no quoting needed)
+/--
+info: "3;key=abc123\x0d\nabc\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "key") (.ofString! "abc123"))
+
+-- Extension value with space (must be quoted)
+/--
+info: "3;key=\"hello world\"\x0d\nabc\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "key") (.ofString! "hello world"))
+
+-- Extension value with backslash (must be escaped)
+/--
+info: "3;key=\"a\\\\b\"\x0d\nabc\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Chunk.ofByteArray "abc".toUTF8 |>.insertExtension (Chunk.ExtensionName.mk "key") (.ofString! "a\\b"))
+
+-- Multiple extensions with no value and with value
+/--
+info: "3;a;b=1\x0d\nabc\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ data := "abc".toUTF8, extensions := #[(Chunk.ExtensionName.mk "a", none), (Chunk.ExtensionName.mk "b", some (.ofString! "1"))] } : Chunk)
+
+/-! ## Edge cases: Request URI encoding -/
+
+-- URI with query parameters
+/--
+info: "GET /search?q=hello&lang=en HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ method := .get, version := .v11, uri := "/search?q=hello&lang=en" } : Request.Head)
+
+-- URI with fragment
+/--
+info: "GET /page#section HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ method := .get, version := .v11, uri := "/page#section" } : Request.Head)
+
+-- URI with percent-encoded characters
+/--
+info: "GET /path%20with%20spaces HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ method := .get, version := .v11, uri := "/path%20with%20spaces" } : Request.Head)
+
+-- URI with special characters (brackets, colons)
+/--
+info: "GET /api/v1/users/[id]:action HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ method := .get, version := .v11, uri := "/api/v1/users/[id]:action" } : Request.Head)
+
+-- Empty URI
+/--
+info: "GET  HTTP/1.1\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ method := .get, version := .v11, uri := "" } : Request.Head)
+
+/-! ## Edge cases: Response with unusual statuses -/
+
+/--
+info: "HTTP/1.1 100 Continue\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ status := .«continue», version := .v11 } : Response.Head)
+
+/--
+info: "HTTP/1.1 204 No Content\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ status := .noContent, version := .v11 } : Response.Head)
+
+/--
+info: "HTTP/1.1 301 Moved Permanently\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ status := .movedPermanently, version := .v11 } : Response.Head)
+
+/--
+info: "HTTP/3.0 200 OK\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr ({ status := .ok, version := .v30 } : Response.Head)

tests/lean/run/async_http_string_quoting.lean

@@ -0,0 +1,85 @@
+import Std.Internal.Http.Internal.String
+import Std.Internal.Http.Internal.Char
+
+open Std.Http.Internal
+
+private def c (n : Nat) : Char := Char.ofNat n
+
+#guard Std.Http.Internal.Char.qdtext (c 0x08) = false
+#guard Std.Http.Internal.Char.qdtext (c 0x09) = true
+#guard Std.Http.Internal.Char.qdtext (c 0x0a) = false
+#guard Std.Http.Internal.Char.qdtext (c 0x1f) = false
+#guard Std.Http.Internal.Char.qdtext (c 0x20) = true
+#guard Std.Http.Internal.Char.qdtext (c 0x21) = true
+#guard Std.Http.Internal.Char.qdtext (c 0x22) = false
+#guard Std.Http.Internal.Char.qdtext (c 0x23) = true
+#guard Std.Http.Internal.Char.qdtext (c 0x5b) = true
+#guard Std.Http.Internal.Char.qdtext (c 0x5c) = false
+#guard Std.Http.Internal.Char.qdtext (c 0x5d) = true
+#guard Std.Http.Internal.Char.qdtext (c 0x7e) = true
+#guard Std.Http.Internal.Char.qdtext (c 0x7f) = false
+
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x08) = false
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x09) = true
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x1f) = false
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x20) = true
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x21) = true
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x22) = true
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x5c) = true
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x7e) = true
+#guard Std.Http.Internal.Char.quotedPairChar (c 0x7f) = false
+
+#guard Std.Http.Internal.Char.quotedStringChar (c 0x09) = true
+#guard Std.Http.Internal.Char.quotedStringChar (c 0x20) = true
+#guard Std.Http.Internal.Char.quotedStringChar (c 0x22) = true
+#guard Std.Http.Internal.Char.quotedStringChar (c 0x5c) = true
+#guard Std.Http.Internal.Char.quotedStringChar (c 0x0a) = false
+#guard Std.Http.Internal.Char.quotedStringChar (c 0x0d) = false
+#guard Std.Http.Internal.Char.quotedStringChar (c 0x7f) = false
+
+#guard quoteHttpString? "token" = some "token"
+#guard quoteHttpString? "a\t " = some "\"a\t \""
+#guard quoteHttpString? "atabpo\n\t " = none
+#guard quoteHttpString? "" = some "\"\""
+#guard quoteHttpString? "\"" = some "\"\\\"\""
+#guard quoteHttpString? "\\" = some "\"\\\\\""
+#guard quoteHttpString? "\"\\\"" = some "\"\\\"\\\\\\\"\""
+#guard quoteHttpString? "abc\rdef" = none
+#guard quoteHttpString? "abc\ndef" = none
+#guard quoteHttpString? "abc\u0000def" = none
+
+#guard unquoteHttpString? "\"token\"" = some "token"
+#guard unquoteHttpString? "\"a\\\\\\\"b\"" = some "a\\\"b"
+#guard unquoteHttpString? "\"line1\nline2\"" = none
+#guard unquoteHttpString? "\"\"" = some ""
+#guard unquoteHttpString? "\"\\\\\"" = some "\\"
+#guard unquoteHttpString? "\"\\\"\"" = some "\""
+#guard unquoteHttpString? "\"a\\tb\"" = some "atb"
+#guard unquoteHttpString? "\"a\tb\"" = some "a\tb"
+#guard unquoteHttpString? "token" = some "token"
+#guard unquoteHttpString? "\"" = none
+#guard unquoteHttpString? "\"abc" = none
+#guard unquoteHttpString? "\"abc\\\"" = none
+#guard unquoteHttpString? "\"abc\\\n\"" = none
+#guard unquoteHttpString? "\"abc\r\"" = none
+
+private def isQuotedString (s : String) : Bool :=
+  s.startsWith '"' && (unquoteHttpString? s).isSome
+
+#guard isQuotedString "\"abc\"" = true
+#guard isQuotedString "\"ab\\\\\\\"c\"" = true
+#guard isQuotedString "\"ab\nc\"" = false
+#guard isQuotedString "\"\"" = true
+#guard isQuotedString "\"\\\"\"" = true
+#guard isQuotedString "\"\\\\\"" = true
+#guard isQuotedString "abc" = false
+#guard isQuotedString "\"" = false
+#guard isQuotedString "\"abc" = false
+#guard isQuotedString "\"abc\\\"" = false
+
+#guard unquoteHttpString? (quoteHttpString! "abc\t ") = some "abc\t "
+#guard unquoteHttpString? (quoteHttpString! "a\\\"b") = some "a\\\"b"
+#guard unquoteHttpString? (quoteHttpString! "") = some ""
+#guard unquoteHttpString? (quoteHttpString! "\"") = some "\""
+#guard unquoteHttpString? (quoteHttpString! "\\") = some "\\"
+#guard unquoteHttpString? (quoteHttpString! " !#$%&'()*+,-./:;<=>?@[\\]^_`{|}~") = some " !#$%&'()*+,-./:;<=>?@[\\]^_`{|}~"