refactor: rename MultiMap to IndexMultiMap

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

src/Init/Data/String/Defs.lean

@@ -230,7 +230,7 @@ Examples:
  * `"empty".isEmpty = false`
  * `" ".isEmpty = false`
 -/
-@[inline] def isEmpty (s : String) : Bool :=
+@[inline, expose] def isEmpty (s : String) : Bool :=
   s.utf8ByteSize == 0
 
 @[export lean_string_isempty]

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

@@ -57,4 +57,14 @@ theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.lengt
 theorem map_eq_empty {f : Char → Char} {s : String} : s.map f = "" ↔ s = "" := by
   simp [← toList_eq_nil_iff]
 
+@[simp]
+theorem map_map {f g : Char → Char} {s : String} : String.map g (String.map f s) = String.map (g ∘ f) s  := by
+  apply String.ext
+  simp [List.map_map]
+
+@[simp]
+theorem map_id {s : String} : String.map id s = s := by
+  apply String.ext
+  simp [List.map_id]
+
 end String

src/Init/Data/String/Modify.lean

@@ -229,7 +229,7 @@ Examples:
 * `"Orange".toLower = "orange"`
 * `"ABc123".toLower = "abc123"`
 -/
-@[inline] def toLower (s : String) : String :=
+@[inline, expose] def toLower (s : String) : String :=
   s.map Char.toLower
 
 /--

src/Std/Internal/Http/Data.lean

@@ -12,6 +12,7 @@ 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
+public import Std.Internal.Http.Data.Headers
 
 /-!
 # HTTP Data Types

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Data.Headers
 public meta import Std.Internal.Http.Internal.String
 
 public section
@@ -20,8 +21,7 @@ Reference: https://www.rfc-editor.org/rfc/rfc9112.html#section-7.1
 -/
 
 namespace Std.Http
-
-open Internal
+open Internal Char
 
 set_option linter.all true
 
@@ -207,3 +207,114 @@ instance : Encode .v11 Chunk where
     buffer.append #[size, exts.toUTF8, "\r\n".toUTF8, chunk.data, "\r\n".toUTF8]
 
 end Chunk
+
+
+/--
+Trailer headers sent after the final chunk in HTTP/1.1 chunked transfer encoding.
+Per RFC 9112 §7.1.2, trailers allow the sender to include additional metadata after
+the message body, such as message integrity checks or digital signatures.
+-/
+structure Trailer where
+  /--
+  The trailer header fields as key-value pairs.
+  -/
+  headers : Headers
+deriving Inhabited
+
+namespace Trailer
+
+/--
+Creates an empty trailer with no headers.
+-/
+def empty : Trailer :=
+  { headers := .empty }
+
+/--
+Inserts a trailer header field.
+-/
+@[inline]
+def insert (trailer : Trailer) (name : Header.Name) (value : Header.Value) : Trailer :=
+  { headers := trailer.headers.insert name value }
+
+/--
+Inserts a trailer header field from string name and value, panicking if either is invalid.
+-/
+@[inline]
+def insert! (trailer : Trailer) (name : String) (value : String) : Trailer :=
+  { headers := trailer.headers.insert! name value }
+
+/--
+Retrieves the first value for the given trailer header name.
+Returns `none` if absent.
+-/
+@[inline]
+def get? (trailer : Trailer) (name : Header.Name) : Option Header.Value :=
+  trailer.headers.get? name
+
+/--
+Retrieves all values for the given trailer header name.
+Returns `none` if absent.
+-/
+@[inline]
+def getAll? (trailer : Trailer) (name : Header.Name) : Option (Array Header.Value) :=
+  trailer.headers.getAll? name
+
+/--
+Checks if a trailer header with the given name exists.
+-/
+@[inline]
+def contains (trailer : Trailer) (name : Header.Name) : Bool :=
+  trailer.headers.contains name
+
+/--
+Removes a trailer header with the given name.
+-/
+@[inline]
+def erase (trailer : Trailer) (name : Header.Name) : Trailer :=
+  { headers := trailer.headers.erase name }
+
+/--
+Gets the number of trailer headers.
+-/
+@[inline]
+def size (trailer : Trailer) : Nat :=
+  trailer.headers.size
+
+/--
+Checks if the trailer has no headers.
+-/
+@[inline]
+def isEmpty (trailer : Trailer) : Bool :=
+  trailer.headers.isEmpty
+
+/--
+Merges two trailers, accumulating values for duplicate keys from both.
+-/
+def merge (t1 t2 : Trailer) : Trailer :=
+  { headers := t1.headers.merge t2.headers }
+
+/--
+Converts the trailer headers to a list of key-value pairs.
+-/
+def toList (trailer : Trailer) : List (Header.Name × Header.Value) :=
+  trailer.headers.toList
+
+/--
+Converts the trailer headers to an array of key-value pairs.
+-/
+def toArray (trailer : Trailer) : Array (Header.Name × Header.Value) :=
+  trailer.headers.toArray
+
+/--
+Folds over all key-value pairs in the trailer headers.
+-/
+def fold (trailer : Trailer) (init : α) (f : α → Header.Name → Header.Value → α) : α :=
+  trailer.headers.fold init f
+
+instance : Encode .v11 Trailer where
+  encode buffer trailer :=
+    buffer.write "0\r\n".toUTF8
+    |> (Encode.encode .v11 · trailer.headers)
+    |>.write  "\r\n".toUTF8
+
+end Trailer

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

@@ -0,0 +1,268 @@
+/-
+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.Headers.Basic
+public import Std.Internal.Http.Data.Headers.Name
+public import Std.Internal.Http.Data.Headers.Value
+
+public section
+
+/-!
+# Headers
+
+This module defines the `Headers` type, which represents a collection of HTTP header name-value pairs.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+open Std Internal
+
+/--
+A structure for managing HTTP headers as key-value pairs.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5
+-/
+structure Headers where
+
+  /--
+  The underlying multimap that stores headers.
+  -/
+  map : IndexMultiMap Header.Name Header.Value
+deriving Inhabited, Repr
+
+instance : Membership Header.Name Headers where
+  mem headers name := name ∈ headers.map
+
+instance (name : Header.Name) (h : Headers) : Decidable (name ∈ h) :=
+  inferInstanceAs (Decidable (name ∈ h.map))
+
+namespace Headers
+
+/--
+Retrieves the first `Header.Value` for the given key.
+-/
+@[inline]
+def get (headers : Headers) (name : Header.Name) (h : name ∈ headers) : Header.Value :=
+  headers.map.get name h
+
+/--
+Retrieves all `Header.Value` entries for the given key.
+-/
+@[inline]
+def getAll (headers : Headers) (name : Header.Name) (h : name ∈ headers) : Array Header.Value :=
+  headers.map.getAll name h
+
+/--
+Like `getAll`, but returns `none` instead of requiring a membership proof.
+Returns `none` if the header is absent.
+-/
+@[inline]
+def getAll? (headers : Headers) (name : Header.Name) : Option (Array Header.Value) :=
+  headers.map.getAll? name
+
+/--
+Retrieves the first `Header.Value` for the given key.
+Returns `none` if the header is absent.
+-/
+@[inline]
+def get? (headers : Headers) (name : Header.Name) : Option Header.Value :=
+  headers.map.get? name
+
+/--
+Checks if the entry is present in the `Headers`.
+-/
+@[inline]
+def hasEntry (headers : Headers) (name : Header.Name) (value : Header.Value) : Bool :=
+  headers.map.hasEntry name value
+
+/--
+Retrieves the last header value for the given key.
+Returns `none` if the header is absent.
+-/
+@[inline]
+def getLast? (headers : Headers) (name : Header.Name) : Option Header.Value :=
+  headers.map.getLast? name
+
+/--
+Like `get?`, but returns a default value if absent.
+-/
+@[inline]
+def getD (headers : Headers) (name : Header.Name) (d : Header.Value) : Header.Value :=
+  headers.map.getD name d
+
+/--
+Like `get?`, but panics if absent.
+-/
+@[inline]
+def get! (headers : Headers) (name : Header.Name) : Header.Value :=
+  headers.map.get! name
+
+/--
+Inserts a new key-value pair into the headers.
+-/
+@[inline]
+def insert (headers : Headers) (key : Header.Name) (value : Header.Value) : Headers :=
+  { map := headers.map.insert key value }
+
+/--
+Adds a header from string name and value, panicking if either is invalid.
+-/
+@[inline]
+def insert! (headers : Headers) (name : String) (value : String) : Headers :=
+  headers.insert (Header.Name.ofString! name) (Header.Value.ofString! value)
+
+/--
+Adds a header from string name and value.
+Returns `none` if either the header name or value is invalid.
+-/
+@[inline]
+def insert? (headers : Headers) (name : String) (value : String) : Option Headers := do
+  let name ← Header.Name.ofString? name
+  let value ← Header.Value.ofString? value
+  pure <| headers.insert name value
+
+/--
+Inserts a new key with an array of values.
+-/
+@[inline]
+def insertMany (headers : Headers) (key : Header.Name) (values : Array Header.Value) : Headers :=
+  { map := headers.map.insertMany key values }
+
+/--
+Creates empty headers.
+-/
+def empty : Headers :=
+  { map := ∅ }
+
+/--
+Creates headers from a list of key-value pairs.
+-/
+def ofList (pairs : List (Header.Name × Header.Value)) : Headers :=
+  { map := IndexMultiMap.ofList pairs }
+
+/--
+Checks if a header with the given name exists.
+-/
+@[inline]
+def contains (headers : Headers) (name : Header.Name) : Bool :=
+  headers.map.contains name
+
+/--
+Removes a header with the given name.
+-/
+@[inline]
+def erase (headers : Headers) (name : Header.Name) : Headers :=
+  { map := headers.map.erase name }
+
+/--
+Gets the number of headers.
+-/
+@[inline]
+def size (headers : Headers) : Nat :=
+  headers.map.size
+
+/--
+Checks if the headers are empty.
+-/
+@[inline]
+def isEmpty (headers : Headers) : Bool :=
+  headers.map.isEmpty
+
+/--
+Merges two headers, accumulating values for duplicate keys from both.
+-/
+def merge (headers1 headers2 : Headers) : Headers :=
+  { map := headers1.map ∪ headers2.map }
+
+/--
+Converts the headers to a list of key-value pairs (flattened). Each header with multiple values produces
+multiple pairs.
+-/
+def toList (headers : Headers) : List (Header.Name × Header.Value) :=
+  headers.map.toList
+
+/--
+Converts the headers to an array of key-value pairs (flattened). Each header with multiple values
+produces multiple pairs.
+-/
+def toArray (headers : Headers) : Array (Header.Name × Header.Value) :=
+  headers.map.toArray
+
+/--
+Folds over all key-value pairs in the headers.
+-/
+def fold (headers : Headers) (init : α) (f : α → Header.Name → Header.Value → α) : α :=
+  headers.map.toArray.foldl (fun acc (k, v) => f acc k v) init
+
+/--
+Maps a function over all header values, producing new headers.
+-/
+def mapValues (headers : Headers) (f : Header.Name → Header.Value → Header.Value) : Headers :=
+  let pairs := headers.map.toArray.map (fun (k, v) => (k, f k v))
+  { map := pairs.foldl (fun acc (k, v) => acc.insert k v) IndexMultiMap.empty }
+
+/--
+Filters and maps over header key-value pairs. Returns only the pairs for which the function returns `some`.
+-/
+def filterMap (headers : Headers) (f : Header.Name → Header.Value → Option Header.Value) : Headers :=
+  let pairs := headers.map.toArray.filterMap (fun (k, v) =>
+    match f k v with
+    | some v' => some (k, v')
+    | none => none)
+  { map := pairs.foldl (fun acc (k, v) => acc.insert k v) IndexMultiMap.empty }
+
+/--
+Filters header key-value pairs, keeping only those that satisfy the predicate.
+-/
+def filter (headers : Headers) (f : Header.Name → Header.Value → Bool) : Headers :=
+  headers.filterMap (fun k v => if f k v then some v else none)
+
+/--
+Updates all the values of a header if it exists.
+-/
+def update (headers : Headers) (name : Header.Name) (f : Header.Value → Header.Value) : Headers :=
+  { map := headers.map.update name f }
+
+/--
+Replaces the last value for the given header name.
+If the header is absent, returns the headers unchanged.
+-/
+@[inline]
+def replaceLast (headers : Headers) (name : Header.Name) (value : Header.Value) : Headers :=
+  { map := headers.map.replaceLast name value }
+
+instance : ToString Headers where
+  toString headers :=
+    let pairs := headers.map.toArray.map (fun (k, v) => s!"{k}: {v}")
+    String.intercalate "\r\n" pairs.toList
+
+instance : Encode .v11 Headers where
+  encode buffer headers :=
+    headers.fold buffer (fun buf name value =>
+      buf.writeString s!"{name}: {value}\r\n")
+
+instance : EmptyCollection Headers :=
+  ⟨Headers.empty⟩
+
+instance : Singleton (Header.Name × Header.Value) Headers :=
+  ⟨fun ⟨a, b⟩ => (∅ : Headers).insert a b⟩
+
+instance : Insert (Header.Name × Header.Value) Headers :=
+  ⟨fun ⟨a, b⟩ s => s.insert a b⟩
+
+instance : Union Headers :=
+  ⟨merge⟩
+
+instance [Monad m] : ForIn m Headers (Header.Name × Header.Value) where
+  forIn headers b f := forIn headers.map.entries b f
+
+end Std.Http.Headers

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

@@ -0,0 +1,217 @@
+/-
+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.Headers.Name
+public import Std.Internal.Http.Data.Headers.Value
+public import Std.Internal.Parsec.Basic
+
+public section
+
+/-!
+# Header Typeclass and Common Headers
+
+This module defines the `Header` typeclass for typed HTTP headers and some common header parsers.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-representation-data-and-met
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+open Internal
+
+/--
+Typeclass for typed HTTP headers that can be parsed from and serialized to header values.
+-/
+class Header (α : Type) where
+
+  /--
+  Parses a header value into the typed representation.
+  -/
+  parse : Header.Value → Option α
+
+  /--
+  Serializes the typed representation back to a name-value pair.
+  -/
+  serialize : α → Header.Name × Header.Value
+
+instance [h : Header α] : Encode .v11 α where
+  encode buffer a :=
+    let (name, value) := h.serialize a
+    buffer.writeString s!"{name}: {value}\r\n"
+
+namespace Header
+
+private def parseTokenList (v : Value) : Option (Array String) := do
+  let rawParts := v.value.split (· == ',')
+  let parts := rawParts.map (·.trimAscii)
+
+  guard (parts.all (¬·.isEmpty))
+
+  return parts.toArray.map (fun s => s.toString.toLower)
+
+/--
+The `Content-Length` header, representing the size of the message body in bytes.
+Parses only valid natural number values.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-8.6-2
+-/
+structure ContentLength where
+
+  /--
+  The content length in bytes.
+  -/
+  length : Nat
+deriving BEq, Repr
+
+namespace ContentLength
+
+/--
+Parses a content length header value.
+-/
+def parse (v : Value) : Option ContentLength :=
+   v.value.toNat?.map (.mk)
+
+/--
+Serializes a content length header back to a name-value pair.
+-/
+def serialize (h : ContentLength) : Name × Value :=
+  (Header.Name.contentLength, Value.ofString! (toString h.length))
+
+instance : Header ContentLength := ⟨parse, serialize⟩
+
+end ContentLength
+
+/--
+Validates the chunked placement rules for the Transfer Encoding header. Returns `false` if the
+encoding list violates the constraints.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9112#section-6.1
+-/
+@[expose]
+def TransferEncoding.Validate (codings : Array String) : Bool :=
+  if codings.isEmpty || codings.any (fun coding => !isToken coding) then
+    false
+  else
+    let chunkedCount := codings.filter (· == "chunked") |>.size
+
+    -- the sender MUST either apply chunked as the final transfer coding
+    let lastIsChunked := codings.back? == some "chunked"
+
+    if chunkedCount > 1 then
+      false
+    else if chunkedCount == 1 && !lastIsChunked then
+      false
+    else
+      true
+
+/--
+The `Transfer-Encoding` header, representing the list of transfer codings applied to the message body.
+
+Validation rules (RFC 9112 Section 6.1):
+- "chunked" may appear at most once.
+- If "chunked" is present, it must be the last encoding in the list.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9112#section-6.1
+-/
+structure TransferEncoding where
+
+  /--
+  The ordered list of transfer codings.
+  -/
+  codings : Array String
+
+  /--
+  Proof that the transfer codings satisfy the chunked placement rules.
+  -/
+  isValid : TransferEncoding.Validate codings = true
+
+deriving Repr
+
+namespace TransferEncoding
+
+/--
+Returns `true` if the transfer encoding ends with chunked.
+-/
+def isChunked (te : TransferEncoding) : Bool :=
+  te.codings.back? == some "chunked"
+
+/--
+Parses a comma-separated list of transfer codings from a header value, validating chunked placement.
+-/
+def parse (v : Value) : Option TransferEncoding := do
+  let codings ← parseTokenList v
+  if h : TransferEncoding.Validate codings then
+    some ⟨codings, h⟩
+  else
+    none
+
+/--
+Serializes a transfer encoding back to a comma-separated header value.
+-/
+def serialize (te : TransferEncoding) : Header.Name × Header.Value :=
+  let value := ",".intercalate (te.codings.toList)
+  (Header.Name.transferEncoding, Value.ofString! value)
+
+instance : Header TransferEncoding := ⟨parse, serialize⟩
+
+end TransferEncoding
+
+/--
+The `Connection` header, represented as a list of connection option tokens.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-connection
+-/
+structure Connection where
+  /--
+  The normalized connection-option tokens.
+  -/
+  tokens : Array String
+
+  /--
+  Proof that all tokens satisfy `isToken`.
+  -/
+  valid : tokens.all isToken = true
+deriving Repr
+
+namespace Connection
+
+/--
+Checks whether a specific token is present in the `Connection` header value.
+-/
+def containsToken (connection : Connection) (token : String) : Bool :=
+  let token := token.trimAscii.toString.toLower
+  connection.tokens.any (· == token)
+
+/--
+Checks whether the `Connection` header requests connection close semantics.
+-/
+def shouldClose (connection : Connection) : Bool :=
+  connection.containsToken "close"
+
+/--
+Parses a `Connection` header value into normalized tokens.
+-/
+def parse (v : Value) : Option Connection := do
+  let tokens ← parseTokenList v
+  if h : tokens.all isToken = true then
+    some ⟨tokens, h⟩
+  else
+    none
+
+/--
+Serializes a `Connection` header back to a comma-separated value.
+-/
+def serialize (connection : Connection) : Header.Name × Header.Value :=
+  let value := ",".intercalate connection.tokens.toList
+  (Header.Name.connection, Value.ofString! value)
+
+instance : Header Connection := ⟨parse, serialize⟩
+
+end Std.Http.Header.Connection

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

@@ -0,0 +1,180 @@
+/-
+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
+
+/-!
+# Header Names
+
+This module defines the `Name` type, which represents validated HTTP header names that conform to
+HTTP standards.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5
+-/
+
+namespace Std.Http.Header
+
+set_option linter.all true
+
+open Internal Char
+
+/--
+Proposition asserting that a string is a valid HTTP header name: all characters are valid token
+characters and the string is non-empty.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-names
+-/
+abbrev IsValidHeaderName (s : String) : Prop :=
+  isToken s
+
+/--
+A validated HTTP header name that ensures all characters conform to HTTP standards. Header names are
+case-insensitive according to HTTP specifications.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-names
+-/
+@[ext]
+structure Name where
+  /--
+  The lowercased normalized header name string.
+  -/
+  value : String
+
+  /--
+  The proof that it's a valid header name.
+  -/
+  isValidHeaderValue : IsValidHeaderName value := by decide
+
+  /--
+  The proof that we stored the header name in stored as a lower case string.
+  -/
+  isLowerCase : IsLowerCase value := by decide
+deriving Repr, DecidableEq
+
+namespace Name
+
+instance : BEq Name where
+  beq a b := a.value = b.value
+
+instance : Hashable Name where
+  hash x := Hashable.hash x.value
+
+theorem Name.beq_eq {x y : Name} : (x == y) = (x.value == y.value) :=
+  rfl
+
+instance : LawfulBEq Name where
+  rfl {x} := by simp [Name.beq_eq]
+  eq_of_beq {x y} := by grind [Name.beq_eq, Name.ext]
+
+instance : LawfulHashable Name := inferInstance
+
+instance : Inhabited Name where
+  default := ⟨"_", by decide, by decide⟩
+
+/--
+Attempts to create a `Name` from a `String`, returning `none` if the string contains invalid
+characters for HTTP header names or is empty.
+-/
+def ofString? (s : String) : Option Name :=
+  let val := s.trimAscii.toString.toLower
+  if h : IsValidHeaderName val ∧ IsLowerCase val then
+    some ⟨val, h.left, h.right⟩
+  else
+    none
+
+/--
+Creates a `Name` from a string, panicking with an error message if the string contains invalid
+characters for HTTP header names or is empty.
+-/
+def ofString! (s : String) : Name :=
+  match ofString? s with
+  | some res => res
+  | none => panic! s!"invalid header name: {s.quote}"
+
+/--
+Converts the header name to title case (e.g., "Content-Type").
+
+Note: some well-known headers have unconventional casing (e.g., "WWW-Authenticate"),
+but since HTTP header names are case-insensitive, this always uses simple capitalization.
+-/
+@[inline]
+def toCanonical (name : Name) : String :=
+  let it := name.value.splitOn "-"
+    |>.map (·.capitalize)
+
+  String.intercalate "-" it
+
+/--
+Performs a case-insensitive comparison between a `Name` and a `String`. Returns `true` if they match.
+-/
+@[expose]
+def is (name : Name) (s : String) : Bool :=
+  name.value == s.toLower
+
+instance : ToString Name where
+  toString name := name.toCanonical
+
+/--
+Standard Content-Type header name
+-/
+def contentType : Header.Name := .mk "content-type"
+
+/--
+Standard Content-Length header name
+-/
+def contentLength : Header.Name := .mk "content-length"
+
+/--
+Standard Host header name
+-/
+def host : Header.Name := .mk "host"
+
+/--
+Standard Authorization header name
+-/
+def authorization : Header.Name := .mk "authorization"
+
+/--
+Standard User-Agent header name
+-/
+def userAgent : Header.Name := .mk "user-agent"
+
+/--
+Standard Accept header name
+-/
+def accept : Header.Name := .mk "accept"
+
+/--
+Standard Connection header name
+-/
+def connection : Header.Name := .mk "connection"
+
+/--
+Standard Transfer-Encoding header name
+-/
+def transferEncoding : Header.Name := .mk "transfer-encoding"
+
+/--
+Standard Server header name
+-/
+def server : Header.Name := .mk "server"
+
+/--
+Standard Date header name
+-/
+def date : Header.Name := .mk "date"
+
+/--
+Standard Expect header name
+-/
+def expect : Header.Name := .mk "expect"
+
+end Std.Http.Header.Name

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

@@ -0,0 +1,103 @@
+/-
+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
+
+/-!
+# Header Values
+
+This module defines the `Value` type, which represents validated HTTP header values that conform to HTTP
+standards.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-values
+-/
+
+namespace Std.Http.Header
+
+set_option linter.all true
+
+open Internal
+
+/--
+Proposition that asserts all characters in a string are valid for HTTP header values,
+and that the first and last characters (if present) are `field-vchar` (not SP/HTAB).
+
+  field-value    = *field-content
+  field-content  = field-vchar
+                   [ 1*( SP / HTAB / field-vchar ) field-vchar ]
+
+Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5.5
+-/
+abbrev IsValidHeaderValue (s : String) : Prop :=
+  let s := s.toList
+
+  s.all Char.fieldContent ∧
+  (s.head?.map Char.fieldVchar |>.getD true) ∧
+  (s.getLast?.map Char.fieldVchar |>.getD true)
+
+/--
+A validated HTTP header value that ensures all characters conform to HTTP standards.
+-/
+structure Value where
+  /--
+  The string data.
+  -/
+  value : String
+
+  /--
+  The proof that it's a valid header value.
+  -/
+  isValidHeaderValue : IsValidHeaderValue value := by decide
+deriving BEq, DecidableEq, Repr
+
+instance : Hashable Value where
+  hash := Hashable.hash ∘ Value.value
+
+instance : Inhabited Value where
+  default := ⟨"", by decide⟩
+
+namespace Value
+
+/--
+Attempts to create a `Value` from a `String`, returning `none` if the string contains invalid characters
+for HTTP header values.
+-/
+@[expose]
+def ofString? (s : String) : Option Value :=
+  -- A field value does not include leading or trailing whitespace.
+  let val := s.trimAscii.toString
+
+  if h : IsValidHeaderValue val then
+    some ⟨val, h⟩
+  else
+    none
+
+/--
+Creates a `Value` from a string, panicking with an error message if the string contains invalid
+characters for HTTP header values.
+-/
+@[expose]
+def ofString! (s : String) : Value :=
+  match ofString? s with
+  | some res => res
+  | none => panic! s!"invalid header value: {s.quote}"
+
+/--
+Performs a case-insensitive comparison between a `Value` and a `String`. Returns `true` if they match.
+-/
+@[expose]
+def is (s : Value) (h : String) : Bool :=
+  s.value.toLower == h.toLower
+
+instance : ToString Value where
+  toString v := v.value
+
+end Std.Http.Header.Value

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

@@ -9,6 +9,7 @@ prelude
 public import Std.Internal.Http.Data.Extensions
 public import Std.Internal.Http.Data.Method
 public import Std.Internal.Http.Data.Version
+public import Std.Internal.Http.Data.Headers
 
 public section
 
@@ -50,6 +51,11 @@ structure Request.Head where
   The raw request-target string (commonly origin-form path/query, `"*"`, or authority-form).
   -/
   uri : String
+
+  /--
+  Collection of HTTP headers for the request (Content-Type, Authorization, etc.).
+  -/
+  headers : Headers := .empty
 deriving Inhabited, Repr
 
 /--
@@ -93,6 +99,8 @@ instance : ToString Head where
     toString req.method ++ " " ++
     toString req.uri ++ " " ++
     toString req.version ++
+    "\r\n" ++
+    toString req.headers ++
     "\r\n"
 
 open Internal in
@@ -103,6 +111,8 @@ instance : Encode .v11 Head where
     let buffer := buffer.writeString req.uri
     let buffer := buffer.writeChar ' '
     let buffer := Encode.encode (v := .v11) buffer req.version
+    let buffer := buffer.writeString "\r\n"
+    let buffer := Encode.encode (v := .v11) buffer req.headers
     buffer.writeString "\r\n"
 
 /--
@@ -137,6 +147,43 @@ 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 } }
 
+/--
+Sets the headers for the request being built.
+-/
+def headers (builder : Builder) (headers : Headers) : Builder :=
+  { builder with line := { builder.line with headers } }
+
+/--
+Adds a single header to the request being built.
+-/
+def header (builder : Builder) (key : Header.Name) (value : Header.Value) : Builder :=
+  { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
+
+/--
+Adds a single header to the request being built, panics if the header is invalid.
+-/
+def header! (builder : Builder) (key : String) (value : String) : Builder :=
+  let key := Header.Name.ofString! key
+  let value := Header.Value.ofString! value
+  { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
+
+/--
+Adds a single header to the request being built.
+Returns `none` if the header name or value is invalid.
+-/
+def header? (builder : Builder) (key : String) (value : String) : Option Builder := do
+  let key ← Header.Name.ofString? key
+  let value ← Header.Value.ofString? value
+  pure <| { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
+
+/--
+Adds a header to the request being built only if the Option Header.Value is some.
+-/
+def headerOpt (builder : Builder) (key : Header.Name) (value : Option Header.Value) : Builder :=
+  match value with
+  | some v => builder.header key v
+  | none => builder
+
 /--
 Inserts a typed extension value into the request being built.
 -/

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

@@ -9,6 +9,7 @@ prelude
 public import Std.Internal.Http.Data.Extensions
 public import Std.Internal.Http.Data.Status
 public import Std.Internal.Http.Data.Version
+public import Std.Internal.Http.Data.Headers
 
 public section
 
@@ -36,6 +37,12 @@ structure Response.Head where
   The HTTP protocol version used in the response, e.g. `HTTP/1.1`.
   -/
   version : Version := .v11
+
+  /--
+  The set of response headers, providing metadata such as `Content-Type`,
+  `Content-Length`, and caching directives.
+  -/
+  headers : Headers := .empty
 deriving Inhabited, Repr
 
 /--
@@ -78,7 +85,9 @@ instance : ToString Head where
   toString r :=
     toString r.version ++ " " ++
     toString r.status.toCode ++ " " ++
-    r.status.reasonPhrase ++ "\r\n"
+    r.status.reasonPhrase ++ "\r\n" ++
+    toString r.headers ++
+    "\r\n"
 
 open Internal in
 instance : Encode .v11 Head where
@@ -88,6 +97,8 @@ instance : Encode .v11 Head where
     let buffer := buffer.writeString (toString r.status.toCode)
     let buffer := buffer.writeChar ' '
     let buffer := buffer.writeString r.status.reasonPhrase
+    let buffer := buffer.writeString "\r\n"
+    let buffer := Encode.encode (v := .v11) buffer r.headers
     buffer.writeString "\r\n"
 
 /--
@@ -108,6 +119,35 @@ 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 } }
 
+/--
+Sets the headers for the response being built.
+-/
+def headers (builder : Builder) (headers : Headers) : Builder :=
+  { builder with line := { builder.line with headers } }
+
+/--
+Adds a single header to the response being built.
+-/
+def header (builder : Builder) (key : Header.Name) (value : Header.Value) : Builder :=
+  { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
+
+/--
+Adds a single header to the response being built, panics if the header is invalid.
+-/
+def header! (builder : Builder) (key : String) (value : String) : Builder :=
+  let key := Header.Name.ofString! key
+  let value := Header.Value.ofString! value
+  { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
+
+/--
+Adds a single header to the response being built.
+Returns `none` if the header name or value is invalid.
+-/
+def header? (builder : Builder) (key : String) (value : String) : Option Builder := do
+  let key ← Header.Name.ofString? key
+  let value ← Header.Value.ofString? value
+  pure <| { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
+
 /--
 Inserts a typed extension value into the response being built.
 -/

src/Std/Internal/Http/Internal.lean

@@ -6,7 +6,10 @@ Authors: Sofia Rodrigues
 module
 
 prelude
+public import Std.Internal.Http.Internal.Char
 public import Std.Internal.Http.Internal.ChunkedBuffer
+public import Std.Internal.Http.Internal.LowerCase
+public import Std.Internal.Http.Internal.IndexMultiMap
 public import Std.Internal.Http.Internal.Encode
 public import Std.Internal.Http.Internal.String
 public import Std.Internal.Http.Internal.Char

src/Std/Internal/Http/Internal/IndexMultiMap.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.Grind
+public import Init.Data.Int.OfNat
+public import Std.Data.HashMap
+
+public section
+
+/-!
+# IndexMultiMap
+
+This module defines a generic `IndexMultiMap` type that maps keys to multiple values.
+The implementation stores entries in a flat array for iteration and an index HashMap
+for fast key lookups. Each key always has at least one associated value.
+-/
+
+namespace Std.Internal
+
+open Std Internal
+
+set_option linter.all true
+
+/--
+A structure for managing ordered key-value pairs where each key can have multiple values.
+-/
+structure IndexMultiMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+
+  /--
+  Flat array of all key-value entries in insertion order.
+  -/
+  entries : Array (α × β)
+
+  /--
+  Maps each key to its indices in `entries`. Each array is non-empty.
+  -/
+  indexes : HashMap α (Array Nat)
+
+  /--
+  Invariant: every key in `indexes` maps to a non-empty array of valid indices into `entries`.
+  -/
+  validity : ∀ k : α, (p : k ∈ indexes) →
+            let idx := (indexes.get k p);
+            idx.size > 0 ∧ (∀ i ∈ idx, i < entries.size)
+
+deriving Repr
+
+instance [BEq α] [Hashable α] [Inhabited α] [Inhabited β] : Inhabited (IndexMultiMap α β) where
+  default := ⟨#[], .emptyWithCapacity, by intro h p; simp at p⟩
+
+namespace IndexMultiMap
+
+variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+
+instance : Membership α (IndexMultiMap α β) where
+  mem map key := key ∈ map.indexes
+
+instance (key : α) (map : IndexMultiMap α β) : Decidable (key ∈ map) :=
+  inferInstanceAs (Decidable (key ∈ map.indexes))
+
+/--
+Retrieves all values for the given key.
+-/
+@[inline]
+def getAll (map : IndexMultiMap α β) (key : α) (h : key ∈ map) : Array β :=
+  let entries := map.indexes.get key h |>.mapFinIdx fun idx _ h₁ =>
+    let proof := map.validity key h |>.right _ (Array.getElem_mem h₁)
+    map.entries[(map.indexes.get key h)[idx]]'proof |>.snd
+
+  entries
+
+/--
+Retrieves the first value for the given key.
+-/
+@[inline]
+def get (map : IndexMultiMap α β) (key : α) (h : key ∈ map) : β :=
+  let ⟨nonEmpty, isIn⟩ := map.validity key h
+  let entry := ((map.indexes.get key h)[0]'nonEmpty)
+
+  let proof := map.validity key h |>.right
+    entry
+    (by simp only [entry, HashMap.get_eq_getElem, Array.getElem_mem])
+
+  map.entries[entry]'proof |>.snd
+
+/--
+Retrieves all values for the given key, or `none` if the key is absent.
+-/
+@[inline]
+def getAll? (map : IndexMultiMap α β) (key : α) : Option (Array β) :=
+  if h : key ∈ map then
+    some (map.getAll key h)
+  else
+    none
+
+/--
+Retrieves the first value for the given key, or `none` if the key is absent.
+-/
+@[inline]
+def get? (map : IndexMultiMap α β) (key : α) : Option β :=
+  if h : key ∈ map then
+    some (map.get key h)
+  else
+    none
+
+/--
+Checks if the key-value pair is present in the map.
+-/
+@[inline]
+def hasEntry (map : IndexMultiMap α β) [BEq β] (key : α) (value : β) : Bool :=
+  map.getAll? key
+  |>.bind (fun arr => arr.find? (· == value))
+  |>.isSome
+
+/--
+Retrieves the last value for the given key.
+Returns `none` if the key is absent.
+-/
+@[inline]
+def getLast? (map : IndexMultiMap α β) (key : α) : Option β :=
+  match map.getAll? key with
+  | none => none
+  | some idxs => idxs.back?
+
+/--
+Like `get?`, but returns a default value if absent.
+-/
+@[inline]
+def getD (map : IndexMultiMap α β) (key : α) (d : β) : β :=
+  map.get? key |>.getD d
+
+/--
+Like `get?`, but panics if absent.
+-/
+@[inline]
+def get! [Inhabited β] (map : IndexMultiMap α β) (key : α) : β :=
+  map.get? key |>.get!
+
+/--
+Inserts a new key-value pair into the map.
+If the key already exists, appends the value to existing values.
+-/
+@[inline]
+def insert [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (value : β) : IndexMultiMap α β :=
+  let i := map.entries.size
+  let entries := map.entries.push (key, value)
+
+  let f := fun
+    | some idxs => some (idxs.push i)
+    | none => some #[i]
+
+  let indexes := map.indexes.alter key f
+
+  { entries, indexes, validity := ?_ }
+where finally
+  have _ := map.validity
+  grind
+
+/--
+Inserts multiple values for a given key, appending to any existing values.
+-/
+@[inline]
+def insertMany [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (values : Array β) : IndexMultiMap α β :=
+  values.foldl (insert · key) map
+
+/--
+Creates an empty multimap.
+-/
+def empty : IndexMultiMap α β :=
+  ⟨#[], .emptyWithCapacity, by intro h p; simp at p⟩
+
+/--
+Creates a multimap from a list of key-value pairs.
+-/
+def ofList [EquivBEq α] [LawfulHashable α] (pairs : List (α × β)) : IndexMultiMap α β :=
+  pairs.foldl (fun acc (k, v) => acc.insert k v) empty
+
+/--
+Checks if a key exists in the map.
+-/
+@[inline]
+def contains (map : IndexMultiMap α β) (key : α) : Bool :=
+  map.indexes.contains key
+
+/--
+Updates all values associated with `key` by applying `f` to each one.
+If the key is absent, returns the map unchanged.
+-/
+@[inline]
+def update [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (f : β → β) : IndexMultiMap α β :=
+  if key ∉ map then
+    map
+  else
+    map.entries.foldl (fun acc (k, v) => acc.insert k (if k == key then f v else v)) empty
+
+/--
+Replaces the last value associated with `key` with `value`.
+If the key is absent, returns the map unchanged.
+-/
+@[inline]
+def replaceLast (map : IndexMultiMap α β) (key : α) (value : β) : IndexMultiMap α β :=
+  if h : key ∈ map then
+    let idxs := map.indexes.get key h
+    let ⟨nonEmpty, isIn⟩ := map.validity key h
+    let lastPos : Fin idxs.size := ⟨idxs.size - 1, Nat.sub_lt nonEmpty (by omega)⟩
+    let lastIdx : Nat := idxs[lastPos]
+    have lastIdxValid : lastIdx < map.entries.size := isIn lastIdx (Array.getElem_mem lastPos.isLt)
+    let entries := map.entries.set (Fin.mk lastIdx lastIdxValid) (key, value)
+    { map with entries, validity := ?_ }
+  else
+    map
+where finally
+  have _ := map.validity
+  grind
+
+/--
+Removes a key and all its values from the map. This function rebuilds the entire
+`entries` array and `indexes` map from scratch by filtering out all pairs whose
+key matches, then re-inserting the survivors.
+-/
+@[inline]
+def erase [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) : IndexMultiMap α β :=
+  if key ∉ map then
+    map
+  else
+    map.entries.filter (fun (k, _) => !(k == key))
+    |>.foldl (fun acc (k, v) => acc.insert k v) empty
+
+/--
+Gets the number of entries in the map.
+-/
+@[inline]
+def size (map : IndexMultiMap α β) : Nat :=
+  map.entries.size
+
+/--
+Checks if the map is empty.
+-/
+@[inline]
+def isEmpty (map : IndexMultiMap α β) : Bool :=
+  map.entries.isEmpty
+
+/--
+Converts the multimap to an array of key-value pairs (flattened).
+-/
+def toArray (map : IndexMultiMap α β) : Array (α × β) :=
+  map.entries
+
+/--
+Converts the multimap to a list of key-value pairs (flattened).
+-/
+def toList (map : IndexMultiMap α β) : List (α × β) :=
+  map.entries.toList
+
+/--
+Merges two multimaps, combining values for shared keys.
+-/
+def merge [EquivBEq α] [LawfulHashable α] (m1 m2 : IndexMultiMap α β) : IndexMultiMap α β :=
+  m2.entries.foldl (fun acc (k, v) => acc.insert k v) m1
+
+instance : EmptyCollection (IndexMultiMap α β) :=
+  ⟨IndexMultiMap.empty⟩
+
+instance [EquivBEq α] [LawfulHashable α] : Singleton (α × β) (IndexMultiMap α β) :=
+  ⟨fun ⟨a, b⟩ => (∅ : IndexMultiMap α β).insert a b⟩
+
+instance [EquivBEq α] [LawfulHashable α] : Insert (α × β) (IndexMultiMap α β) :=
+  ⟨fun ⟨a, b⟩ m => m.insert a b⟩
+
+instance [EquivBEq α] [LawfulHashable α] : Union (IndexMultiMap α β) :=
+  ⟨merge⟩
+
+instance [Monad m] : ForIn m (IndexMultiMap α β) (α × β) where
+  forIn map b f := forIn map.entries b f
+
+end Std.Internal.IndexMultiMap

src/Std/Internal/Http/Internal/LowerCase.lean

@@ -0,0 +1,68 @@
+/-
+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
+import Init.Data.Int.OfNat
+import Init.Data.UInt.Lemmas
+public import Init.Data.String
+
+@[expose]
+public section
+
+/-!
+# LowerCase
+
+This module provides predicates and normalization functions for handling ASCII case-insensitivity.
+It includes proofs of idempotency for lowercase transformations, as well as utilities for validating
+the lowercase state of a String.
+-/
+
+namespace Std.Http.Internal
+
+set_option linter.all true
+
+/--
+Predicate asserting that a string is in lowercase form.
+-/
+@[expose] def IsLowerCase (s : String) : Prop :=
+  s.toLower = s
+
+private theorem Char.toLower_eq_self_iff {c : Char} : c.toLower = c ↔ c.isUpper = false := by
+  simp only [Char.toLower, Char.isUpper]
+  split <;> rename_i h <;> simpa [UInt32.le_iff_toNat_le, Char.ext_iff] using h
+
+private theorem String.toLower_eq_self_iff {s : String} : s.toLower = s ↔ s.toList.any Char.isUpper = false := by
+  simp only [String.toLower, ← String.toList_inj, String.toList_map]
+  rw (occs := [2]) [← List.map_id s.toList]
+  rw [List.map_eq_map_iff]
+  simp [Char.toLower_eq_self_iff]
+
+instance : Decidable (IsLowerCase s) :=
+  decidable_of_decidable_of_iff (p := s.toList.any Char.isUpper = false)
+    (by exact String.toLower_eq_self_iff.symm)
+
+namespace IsLowerCase
+
+private theorem Char.toLower_idempotent (c : Char) : c.toLower.toLower = c.toLower := by
+  grind [Char.toLower]
+
+/--
+Proof that applying `toLower` to any string results in a string that satisfies the `IsLowerCase`
+predicate.
+-/
+theorem isLowerCase_toLower {s : String} : IsLowerCase s.toLower := by
+  unfold IsLowerCase String.toLower
+  rw [String.map_map, Function.comp_def]
+  simp [Char.toLower_idempotent]
+
+theorem isLowerCase_empty : IsLowerCase "" := by
+  simp [IsLowerCase, String.toLower]
+
+end IsLowerCase
+
+end Std.Http.Internal

tests/elab/async_http_encode.lean

@@ -119,48 +119,69 @@ info: "999 Unknown"
 /-! ## Request.line encoding -/
 
 /--
-info: "GET /path HTTP/1.1\x0d\n"
+info: ""
+-/
+#guard_msgs in
+#eval encodeStr Headers.empty
+
+/--
+info: "Content-Type: text/html\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Headers.empty.insert! "content-type" "text/html")
+
+/--
+info: "X-Custom-Header: value\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Headers.empty.insert! "x-custom-header" "value")
+
+
+/--
+info: "GET /path HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ method := .get, version := .v11, uri := "/path" } : Request.Head)
 
 /--
-info: "POST /submit HTTP/1.1\x0d\n"
+info: "POST /submit HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ method := .post, version := .v11, uri := "/submit" } : Request.Head)
 
 /--
-info: "PUT /resource HTTP/2.0\x0d\n"
+info: "PUT /resource HTTP/2.0\x0d\nContent-Type: application/json\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({
     method := .put
     version := .v20
     uri := "/resource"
+    headers := Headers.empty.insert! "content-type" "application/json"
   } : Request.Head)
 
 /-! ## Response.line encoding -/
 
 /--
-info: "HTTP/1.1 200 OK\x0d\n"
+info: "HTTP/1.1 200 OK\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ status := .ok, version := .v11 } : Response.Head)
 
 /--
-info: "HTTP/1.1 404 Not Found\x0d\n"
+info: "HTTP/1.1 404 Not Found\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ status := .notFound, version := .v11 } : Response.Head)
 
 /--
-info: "HTTP/2.0 500 Internal Server Error\x0d\n"
+info: "HTTP/2.0 500 Internal Server Error\x0d\nContent-Type: text/plain\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({
     status := .internalServerError
     version := .v20
+    headers := Headers.empty.insert! "content-type" "text/plain"
   } : Response.Head)
 
 /-! ## Chunk encoding -/
@@ -198,61 +219,61 @@ info: "a\x0d\n0123456789\x0d\n"
 /-! ## Request builder -/
 
 /--
-info: "GET /index.html HTTP/1.1\x0d\n"
+info: "GET /index.html HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.get "/index.html" |>.body ()).line
 
 /--
-info: "POST /api/data HTTP/1.1\x0d\n"
+info: "POST /api/data HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.post "/api/data" |>.body ()).line
 
 /--
-info: "PUT /resource HTTP/1.1\x0d\n"
+info: "PUT /resource HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.put "/resource" |>.body ()).line
 
 /--
-info: "DELETE /item HTTP/1.1\x0d\n"
+info: "DELETE /item HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.delete "/item" |>.body ()).line
 
 /--
-info: "PATCH /update HTTP/1.1\x0d\n"
+info: "PATCH /update HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.patch "/update" |>.body ()).line
 
 /--
-info: "HEAD /check HTTP/1.1\x0d\n"
+info: "HEAD /check HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.head "/check" |>.body ()).line
 
 /--
-info: "OPTIONS * HTTP/1.1\x0d\n"
+info: "OPTIONS * HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.options "*" |>.body ()).line
 
 /--
-info: "CONNECT proxy:8080 HTTP/1.1\x0d\n"
+info: "CONNECT proxy:8080 HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.connect "proxy:8080" |>.body ()).line
 
 /--
-info: "TRACE /debug HTTP/1.1\x0d\n"
+info: "TRACE /debug HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.trace "/debug" |>.body ()).line
 
 /--
-info: "POST /v2 HTTP/2.0\x0d\n"
+info: "POST /v2 HTTP/2.0\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Request.new |>.method .post |>.uri "/v2" |>.version .v20 |>.body ()).line
@@ -260,67 +281,67 @@ info: "POST /v2 HTTP/2.0\x0d\n"
 /-! ## Response builder -/
 
 /--
-info: "HTTP/1.1 200 OK\x0d\n"
+info: "HTTP/1.1 200 OK\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.ok |>.body ()).line
 
 /--
-info: "HTTP/1.1 404 Not Found\x0d\n"
+info: "HTTP/1.1 404 Not Found\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.notFound |>.body ()).line
 
 /--
-info: "HTTP/1.1 500 Internal Server Error\x0d\n"
+info: "HTTP/1.1 500 Internal Server Error\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.internalServerError |>.body ()).line
 
 /--
-info: "HTTP/1.1 400 Bad Request\x0d\n"
+info: "HTTP/1.1 400 Bad Request\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.badRequest |>.body ()).line
 
 /--
-info: "HTTP/1.1 201 Created\x0d\n"
+info: "HTTP/1.1 201 Created\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.created |>.body ()).line
 
 /--
-info: "HTTP/1.1 202 Accepted\x0d\n"
+info: "HTTP/1.1 202 Accepted\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.accepted |>.body ()).line
 
 /--
-info: "HTTP/1.1 401 Unauthorized\x0d\n"
+info: "HTTP/1.1 401 Unauthorized\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.unauthorized |>.body ()).line
 
 /--
-info: "HTTP/1.1 403 Forbidden\x0d\n"
+info: "HTTP/1.1 403 Forbidden\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.forbidden |>.body ()).line
 
 /--
-info: "HTTP/1.1 409 Conflict\x0d\n"
+info: "HTTP/1.1 409 Conflict\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.conflict |>.body ()).line
 
 /--
-info: "HTTP/1.1 503 Service Unavailable\x0d\n"
+info: "HTTP/1.1 503 Service Unavailable\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.serviceUnavailable |>.body ()).line
 
 /--
-info: "HTTP/1.1 418 I'm a teapot\x0d\n"
+info: "HTTP/1.1 418 I'm a teapot\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr (Response.withStatus .imATeapot |>.body ()).line
@@ -440,39 +461,149 @@ 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)
 
+/-! ## Trailer encoding -/
+
+-- Empty trailer: terminal chunk + CRLF
+/--
+info: "0\x0d\n\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr Trailer.empty
+
+-- Trailer with a single header
+/--
+info: "0\x0d\nChecksum: abc123\x0d\n\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Trailer.empty.insert! "checksum" "abc123")
+
+-- Trailer with a single header
+/--
+info: "0\x0d\nChecksum: abc 123\x0d\n\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Trailer.empty.insert! "checksum" "abc 123")
+
+
+-- Trailer with multiple headers
+/--
+info: "0\x0d\nChecksum: abc123\x0d\nExpires: Thu, 01 Dec 2025 16:00:00 GMT\x0d\n\x0d\n"
+-/
+#guard_msgs in
+#eval encodeStr (Trailer.empty.insert! "checksum" "abc123" |>.insert! "expires" "Thu, 01 Dec 2025 16:00:00 GMT")
+
+/-! ## Edge cases: Trailer validation -/
+
+-- Empty header name is rejected
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Name.ofString? "" |>.isNone : Bool)
+
+-- Header name with spaces is rejected
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Name.ofString? "bad name" |>.isNone : Bool)
+
+-- Header name with colon is rejected
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Name.ofString? "bad:name" |>.isNone : Bool)
+
+-- Header name with newline is rejected
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Name.ofString? "bad\nname" |>.isNone : Bool)
+
+-- Header value with newline is rejected
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Value.ofString? "bad\nvalue" |>.isNone : Bool)
+
+-- Header value with null byte is rejected
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Value.ofString? "bad\x00value" |>.isNone : Bool)
+
+-- Header value with carriage return is rejected
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Value.ofString? "bad\rvalue" |>.isNone : Bool)
+
+-- Valid header name succeeds
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Name.ofString? "content-type" |>.isSome : Bool)
+
+-- Valid header value with tab succeeds (tab is allowed per RFC)
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Value.ofString? "value\twith-tab" |>.isSome : Bool)
+
+-- Empty header value is valid
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Value.ofString? "" |>.isSome : Bool)
+
+-- Header value with DEL character (0x7F) is rejected
+/--
+info: true
+-/
+#guard_msgs in
+#eval (Header.Value.ofString? (String.ofList [Char.ofNat 0x7F]) |>.isNone : Bool)
+
 /-! ## Edge cases: Request URI encoding -/
 
 -- URI with query parameters
 /--
-info: "GET /search?q=hello&lang=en HTTP/1.1\x0d\n"
+info: "GET /search?q=hello&lang=en HTTP/1.1\x0d\n\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"
+info: "GET /page#section HTTP/1.1\x0d\n\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"
+info: "GET /path%20with%20spaces HTTP/1.1\x0d\n\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"
+info: "GET /api/v1/users/[id]:action HTTP/1.1\x0d\n\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"
+info: "GET  HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ method := .get, version := .v11, uri := "" } : Request.Head)
@@ -480,25 +611,25 @@ info: "GET  HTTP/1.1\x0d\n"
 /-! ## Edge cases: Response with unusual statuses -/
 
 /--
-info: "HTTP/1.1 100 Continue\x0d\n"
+info: "HTTP/1.1 100 Continue\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ status := .«continue», version := .v11 } : Response.Head)
 
 /--
-info: "HTTP/1.1 204 No Content\x0d\n"
+info: "HTTP/1.1 204 No Content\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ status := .noContent, version := .v11 } : Response.Head)
 
 /--
-info: "HTTP/1.1 301 Moved Permanently\x0d\n"
+info: "HTTP/1.1 301 Moved Permanently\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ status := .movedPermanently, version := .v11 } : Response.Head)
 
 /--
-info: "HTTP/3.0 200 OK\x0d\n"
+info: "HTTP/3.0 200 OK\x0d\n\x0d\n"
 -/
 #guard_msgs in
 #eval encodeStr ({ status := .ok, version := .v30 } : Response.Head)

tests/elab/async_http_headers.lean

@@ -0,0 +1,340 @@
+import Std.Internal.Http.Data.Headers
+
+open Std.Http
+open Std.Http.Header
+
+/-! ## Header.Name tests -/
+
+-- Valid header names
+#guard (Name.ofString? "content-type").isSome
+#guard (Name.ofString? "host").isSome
+#guard (Name.ofString? "x-custom-header").isSome
+#guard (Name.ofString? "accept").isSome
+
+-- Trimming: leading/trailing whitespace is stripped
+#guard (Name.ofString? " content-type ").isSome
+#guard (Name.ofString? " content-type ") == Name.ofString? "content-type"
+#guard (Name.ofString? "  host  ").isSome
+
+-- Invalid header names (empty, spaces, control chars)
+#guard (Name.ofString? "").isNone
+#guard (Name.ofString? "   ").isNone
+#guard (Name.ofString? "invalid header").isNone
+#guard (Name.ofString? "bad\nname").isNone
+#guard (Name.ofString? "bad\x00name").isNone
+#guard (Name.ofString? "bad(name").isNone
+#guard (Name.ofString? "bad)name").isNone
+#guard (Name.ofString? "bad,name").isNone
+#guard (Name.ofString? "bad;name").isNone
+#guard (Name.ofString? "bad[name").isNone
+#guard (Name.ofString? "bad]name").isNone
+#guard (Name.ofString? "bad{name").isNone
+#guard (Name.ofString? "bad}name").isNone
+#guard (Name.ofString? "bad\"name").isNone
+
+-- Case normalization
+/--
+info: "content-type"
+-/
+#guard_msgs in
+#eval (Name.ofString! "Content-Type").value
+
+/--
+info: "content-type"
+-/
+#guard_msgs in
+#eval (Name.ofString! "CONTENT-TYPE").value
+
+-- Canonical form
+/--
+info: "Content-Type"
+-/
+#guard_msgs in
+#eval toString (Name.ofString! "content-type")
+
+/--
+info: "X-Custom-Header"
+-/
+#guard_msgs in
+#eval toString (Name.ofString! "x-custom-header")
+
+/--
+info: "Host"
+-/
+#guard_msgs in
+#eval toString (Name.ofString! "host")
+
+-- Name.is case-insensitive comparison
+#guard (Name.ofString! "content-type").is "Content-Type"
+#guard (Name.ofString! "content-type").is "CONTENT-TYPE"
+#guard (Name.ofString! "content-type").is "content-type"
+#guard !(Name.ofString! "content-type").is "host"
+
+-- Predefined names
+#guard Name.contentType.value == "content-type"
+#guard Name.contentLength.value == "content-length"
+#guard Name.host.value == "host"
+#guard Name.authorization.value == "authorization"
+#guard Name.userAgent.value == "user-agent"
+#guard Name.accept.value == "accept"
+#guard Name.connection.value == "connection"
+#guard Name.transferEncoding.value == "transfer-encoding"
+#guard Name.server.value == "server"
+
+-- Name equality
+#guard Name.ofString! "content-type" == Name.ofString! "Content-Type"
+#guard Name.ofString! "HOST" == Name.ofString! "host"
+#guard !(Name.ofString! "content-type" == Name.ofString! "host")
+
+/-! ## Header.Value tests -/
+
+-- Trimming: leading/trailing whitespace is stripped
+#guard (Value.ofString? " text/html ") == Value.ofString? "text/html"
+#guard (Value.ofString? "  value  ") == Value.ofString? "value"
+
+-- Valid header values (printable ASCII, tab, space)
+#guard (Value.ofString? "text/html").isSome
+#guard (Value.ofString? "application/json; charset=utf-8").isSome
+#guard (Value.ofString? "").isSome
+#guard (Value.ofString? "value with spaces").isSome
+#guard (Value.ofString? "value\twith\ttabs").isSome
+
+-- Invalid header values (control characters except tab)
+#guard (Value.ofString? "bad\x00value").isNone
+#guard (Value.ofString? "bad\nvalue").isNone
+#guard (Value.ofString? "bad\rvalue").isNone
+
+-- Value.is case-insensitive comparison
+#guard (Value.ofString! "text/html").is "TEXT/HTML"
+#guard (Value.ofString! "text/html").is "text/html"
+#guard !(Value.ofString! "text/html").is "application/json"
+
+-- Value toString
+/--
+info: "text/html"
+-/
+#guard_msgs in
+#eval toString (Value.ofString! "text/html")
+
+/-! ## Headers collection tests -/
+
+-- Empty headers
+#guard Headers.empty.isEmpty
+#guard Headers.empty.size == 0
+
+-- Add and retrieve
+#guard (Headers.empty.insert! "content-type" "text/html").size == 1
+#guard !(Headers.empty.insert! "content-type" "text/html").isEmpty
+#guard (Headers.empty.insert! "content-type" "text/html").contains (Name.ofString! "content-type")
+#guard (Headers.empty.insert? "content-type" "text/html").isSome
+#guard (Headers.empty.insert? "bad header name" "text/html").isNone
+#guard (Headers.empty.insert? "content-type" "bad\nvalue").isNone
+
+-- get? retrieves the value
+/--
+info: "text/html"
+-/
+#guard_msgs in
+#eval do
+  let h := Headers.empty.insert! "content-type" "text/html"
+  return (h.get? (Name.ofString! "content-type")).get!.value
+
+-- get? returns none for missing headers
+#guard (Headers.empty.get? (Name.ofString! "content-type")).isNone
+
+-- Multiple headers
+#guard
+  let h := Headers.empty
+    |>.insert! "content-type" "text/html"
+    |>.insert! "host" "example.com"
+    |>.insert! "accept" "application/json"
+  h.size == 3
+
+#guard
+  let h := Headers.empty.insert! "host" "example.com"
+  h.contains (Name.ofString! "host") && !h.contains (Name.ofString! "accept")
+
+#guard
+  let h := Headers.empty
+    |>.insert! "content-type" "text/html"
+    |>.insert! "host" "example.com"
+  let h' := h.erase (Name.ofString! "content-type")
+  !h'.contains (Name.ofString! "content-type") && h'.contains (Name.ofString! "host")
+
+#guard
+  let h := Headers.empty
+    |>.insert! "content-type" "text/html"
+    |>.insert! "host" "example.com"
+  (h.erase (Name.ofString! "content-type")).size == 1
+
+-- hasEntry
+#guard
+  let h := Headers.empty.insert! "content-type" "text/html"
+  h.hasEntry (Name.ofString! "content-type") (Value.ofString! "text/html")
+
+#guard
+  let h := Headers.empty.insert! "content-type" "text/html"
+  !h.hasEntry (Name.ofString! "content-type") (Value.ofString! "application/json")
+
+-- update existing
+/--
+info: "TEXT/HTML"
+-/
+#guard_msgs in
+#eval do
+  let h := Headers.empty.insert! "content-type" "text/html"
+  let h' := h.update (Name.ofString! "content-type") (fun v => Value.ofString! v.value.toUpper)
+  return (h'.get? (Name.ofString! "content-type")).get!.value
+
+-- ofList
+#guard
+  let h := Headers.ofList [
+    (Name.ofString! "host", Value.ofString! "example.com"),
+    (Name.ofString! "accept", Value.ofString! "*/*")
+  ]
+  h.size == 2 && h.contains (Name.ofString! "host")
+
+-- merge
+#guard
+  let h1 := Headers.empty.insert! "content-type" "text/html"
+  let h2 := Headers.empty.insert! "host" "example.com"
+  let merged := h1.merge h2
+  merged.contains (Name.ofString! "content-type") && merged.contains (Name.ofString! "host")
+
+-- filter
+#guard
+  let h := Headers.empty
+    |>.insert! "content-type" "text/html"
+    |>.insert! "host" "example.com"
+    |>.insert! "accept" "application/json"
+  let filtered := h.filter (fun name _ => name.is "host")
+  filtered.size == 1 && filtered.contains (Name.ofString! "host")
+
+-- fold
+/--
+info: 3
+-/
+#guard_msgs in
+#eval do
+  let h := Headers.empty
+    |>.insert! "a" "1"
+    |>.insert! "b" "2"
+    |>.insert! "c" "3"
+  return h.fold 0 (fun acc _ _ => acc + 1)
+
+-- getD with default
+/--
+info: "fallback"
+-/
+#guard_msgs in
+#eval do
+  let h := Headers.empty
+  return (h.getD (Name.ofString! "missing") (Value.ofString! "fallback")).value
+
+-- mapValues
+/--
+info: "TEXT/HTML"
+-/
+#guard_msgs in
+#eval do
+  let h := Headers.empty.insert! "content-type" "text/html"
+  let h' := h.mapValues (fun _ v => Value.ofString! v.value.toUpper)
+  return (h'.get? (Name.ofString! "content-type")).get!.value
+
+-- toArray preserves insertion order
+#guard
+  let h := Headers.empty
+    |>.insert! "content-type" "text/html"
+    |>.insert! "host" "example.com"
+    |>.insert! "accept" "application/json"
+  h.toArray.map (fun (n, v) => (n.value, v.value)) ==
+    #[("content-type", "text/html"), ("host", "example.com"), ("accept", "application/json")]
+
+-- toArray with duplicate keys: both values appear in insertion order
+#guard
+  let h := Headers.empty
+    |>.insert! "accept" "text/html"
+    |>.insert! "accept" "application/json"
+  h.toArray.map (fun (n, v) => (n.value, v.value)) ==
+    #[("accept", "text/html"), ("accept", "application/json")]
+
+-- toArray after erase preserves remaining insertion order
+#guard
+  let h := Headers.empty
+    |>.insert! "content-type" "text/html"
+    |>.insert! "host" "example.com"
+    |>.insert! "accept" "application/json"
+  (h.erase (Name.ofString! "host")).toArray.map (fun (n, v) => (n.value, v.value)) ==
+    #[("content-type", "text/html"), ("accept", "application/json")]
+
+/-! ## Header typeclass tests -/
+
+-- ContentLength parse
+#guard
+  match Header.ContentLength.parse (Value.ofString! "42") with
+  | some cl => cl.length == 42
+  | none => false
+
+#guard
+  match Header.ContentLength.parse (Value.ofString! "0") with
+  | some cl => cl.length == 0
+  | none => false
+
+#guard (Header.ContentLength.parse =<< (Value.ofString! "abc")).isNone
+#guard (Header.ContentLength.parse =<< (Value.ofString? "")).isNone
+
+/--
+info: ("content-length", "42")
+-/
+#guard_msgs in
+#eval do
+  let (name, value) := Header.ContentLength.serialize ⟨42⟩
+  return (name.value, value.value)
+
+#guard
+  match Header.TransferEncoding.parse (Value.ofString! "chunked") with
+  | some te => te.isChunked
+  | none => false
+
+#guard
+  match Header.TransferEncoding.parse (Value.ofString! "gzip, chunked") with
+  | some te => te.isChunked && te.codings.size == 2
+  | none => false
+
+#guard
+  match Header.TransferEncoding.parse (Value.ofString! "gzip") with
+  | some te => !te.isChunked
+  | none => false
+
+#guard (Header.TransferEncoding.parse =<< (Value.ofString? "chunked, gzip")).isNone
+#guard (Header.TransferEncoding.parse =<< (Value.ofString? "chunked, chunked")).isNone
+#guard (Header.TransferEncoding.parse =<< (Value.ofString? "")).isNone
+#guard (Header.TransferEncoding.parse =<< (Value.ofString? ",")).isNone
+#guard (Header.TransferEncoding.parse =<< (Value.ofString? " , , ")).isNone
+#guard (Header.TransferEncoding.parse =<< (Value.ofString? "g zip")).isNone
+#guard (Header.TransferEncoding.parse =<< (Value.ofString? "\"chunked\"")).isNone
+
+/--
+info: ("transfer-encoding", "gzip,chunked")
+-/
+#guard_msgs in
+#eval do
+  let te : Header.TransferEncoding := ⟨#["gzip", "chunked"], by native_decide⟩
+  let (name, value) := Header.TransferEncoding.serialize te
+  return (name.value, value.value)
+
+#guard
+  match Header.Connection.parse (Value.ofString! "keep-alive, Close") with
+  | some c => c.containsToken "close" && c.shouldClose
+  | none => false
+
+#guard (Header.Connection.parse =<< (Value.ofString? "keep alive")).isNone
+
+/--
+info: ("connection", "keep-alive,close")
+-/
+#guard_msgs in
+#eval do
+  let c : Header.Connection := ⟨#["keep-alive", "close"], by native_decide⟩
+  let (name, value) := Header.Connection.serialize c
+  return (name.value, value.value)