From a0048bf70324ecb1dd160e0dfc92540440e7dca8 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 17 Mar 2026 09:25:01 -0300 Subject: [PATCH] feat: introduce `Headers` data type for HTTP (#12127) This PR introduces the `Headers` data type, that provides a good and convenient abstraction for parsing, querying, and encoding HTTP/1.1 headers. This contains the same code as #10478, divided into separate pieces to facilitate easier review. The pieces of this feature are: - Core data structures: #12126 - Headers: #12127 - URI: #12128 - Body: #12144 - H1: #12146 - Server: #12151 - Client: --------- Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> --- src/Init/Data/String/Defs.lean | 2 +- src/Init/Data/String/Lemmas/Modify.lean | 10 + src/Init/Data/String/Modify.lean | 2 +- src/Std/Internal/Http/Data.lean | 1 + src/Std/Internal/Http/Data/Chunk.lean | 115 +++++- src/Std/Internal/Http/Data/Headers.lean | 268 ++++++++++++++ src/Std/Internal/Http/Data/Headers/Basic.lean | 217 +++++++++++ src/Std/Internal/Http/Data/Headers/Name.lean | 180 ++++++++++ src/Std/Internal/Http/Data/Headers/Value.lean | 103 ++++++ src/Std/Internal/Http/Data/Request.lean | 47 +++ src/Std/Internal/Http/Data/Response.lean | 42 ++- src/Std/Internal/Http/Internal.lean | 3 + .../Internal/Http/Internal/IndexMultiMap.lean | 281 +++++++++++++++ src/Std/Internal/Http/Internal/LowerCase.lean | 68 ++++ tests/elab/async_http_encode.lean | 203 +++++++++-- tests/elab/async_http_headers.lean | 340 ++++++++++++++++++ 16 files changed, 1841 insertions(+), 41 deletions(-) create mode 100644 src/Std/Internal/Http/Data/Headers.lean create mode 100644 src/Std/Internal/Http/Data/Headers/Basic.lean create mode 100644 src/Std/Internal/Http/Data/Headers/Name.lean create mode 100644 src/Std/Internal/Http/Data/Headers/Value.lean create mode 100644 src/Std/Internal/Http/Internal/IndexMultiMap.lean create mode 100644 src/Std/Internal/Http/Internal/LowerCase.lean create mode 100644 tests/elab/async_http_headers.lean diff --git a/src/Init/Data/String/Defs.lean b/src/Init/Data/String/Defs.lean index be7c1e5bf5..9658817934 100644 --- a/src/Init/Data/String/Defs.lean +++ b/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] diff --git a/src/Init/Data/String/Lemmas/Modify.lean b/src/Init/Data/String/Lemmas/Modify.lean index 526149fb50..028d57b0ac 100644 --- a/src/Init/Data/String/Lemmas/Modify.lean +++ b/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 diff --git a/src/Init/Data/String/Modify.lean b/src/Init/Data/String/Modify.lean index 904e1d39cc..daa94094ee 100644 --- a/src/Init/Data/String/Modify.lean +++ b/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 /-- diff --git a/src/Std/Internal/Http/Data.lean b/src/Std/Internal/Http/Data.lean index 5c0586b828..09658b247a 100644 --- a/src/Std/Internal/Http/Data.lean +++ b/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 diff --git a/src/Std/Internal/Http/Data/Chunk.lean b/src/Std/Internal/Http/Data/Chunk.lean index 33f65c7916..0b380ba4a6 100644 --- a/src/Std/Internal/Http/Data/Chunk.lean +++ b/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 diff --git a/src/Std/Internal/Http/Data/Headers.lean b/src/Std/Internal/Http/Data/Headers.lean new file mode 100644 index 0000000000..0468615cf7 --- /dev/null +++ b/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 diff --git a/src/Std/Internal/Http/Data/Headers/Basic.lean b/src/Std/Internal/Http/Data/Headers/Basic.lean new file mode 100644 index 0000000000..51f7511a42 --- /dev/null +++ b/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 diff --git a/src/Std/Internal/Http/Data/Headers/Name.lean b/src/Std/Internal/Http/Data/Headers/Name.lean new file mode 100644 index 0000000000..0e22c8b80e --- /dev/null +++ b/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 diff --git a/src/Std/Internal/Http/Data/Headers/Value.lean b/src/Std/Internal/Http/Data/Headers/Value.lean new file mode 100644 index 0000000000..3d74baad62 --- /dev/null +++ b/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 diff --git a/src/Std/Internal/Http/Data/Request.lean b/src/Std/Internal/Http/Data/Request.lean index d03ceca092..6ec181d709 100644 --- a/src/Std/Internal/Http/Data/Request.lean +++ b/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. -/ diff --git a/src/Std/Internal/Http/Data/Response.lean b/src/Std/Internal/Http/Data/Response.lean index fbc5b76f01..39f241e080 100644 --- a/src/Std/Internal/Http/Data/Response.lean +++ b/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. -/ diff --git a/src/Std/Internal/Http/Internal.lean b/src/Std/Internal/Http/Internal.lean index 37386a86b4..c56ec7ca2f 100644 --- a/src/Std/Internal/Http/Internal.lean +++ b/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 diff --git a/src/Std/Internal/Http/Internal/IndexMultiMap.lean b/src/Std/Internal/Http/Internal/IndexMultiMap.lean new file mode 100644 index 0000000000..efb67d6a07 --- /dev/null +++ b/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 diff --git a/src/Std/Internal/Http/Internal/LowerCase.lean b/src/Std/Internal/Http/Internal/LowerCase.lean new file mode 100644 index 0000000000..09a072d24f --- /dev/null +++ b/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 diff --git a/tests/elab/async_http_encode.lean b/tests/elab/async_http_encode.lean index a46473409e..b9e4d44810 100644 --- a/tests/elab/async_http_encode.lean +++ b/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) diff --git a/tests/elab/async_http_headers.lean b/tests/elab/async_http_headers.lean new file mode 100644 index 0000000000..9f1ed35d58 --- /dev/null +++ b/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)