Merge branch 'sofia/async-http-uri' into sofia/async-http-body

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

@@ -51,7 +51,7 @@ structure ExtensionName where
   /--
   The proof that it's a valid extension name.
   -/
-  validExtensionName : IsValidExtensionName value := by decide
+  isValidExtensionName : IsValidExtensionName value := by decide
 deriving Repr, DecidableEq, BEq
 
 instance : Hashable ExtensionName where

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

@@ -30,17 +30,6 @@ set_option linter.all true
 `quickCmp` is unavailable here, so this is a simpler implementation of the same comparison.
 -/
 
-private def compareString (s₁ s₂ : String) : Ordering :=
-  let rec go : List Char → List Char → Ordering
-    | [], [] => .eq
-    | [], _ => .lt
-    | _, [] => .gt
-    | c₁ :: cs₁, c₂ :: cs₂ =>
-        match compare c₁.toNat c₂.toNat with
-        | .eq => go cs₁ cs₂
-        | ord => ord
-  go s₁.toList s₂.toList
-
 /--
 An ordering for `Name` keys used by `Extensions`.
 -/
@@ -50,7 +39,7 @@ protected def Extensions.compareName : Name → Name → Ordering
   | _, .anonymous => .gt
   | .str p₁ s₁, .str p₂ s₂ =>
       match Extensions.compareName p₁ p₂ with
-      | .eq => compareString s₁ s₂
+      | .eq => compareOfLessAndEq s₁ s₂
       | ord => ord
   | .str _ _, .num _ _ => .lt
   | .num _ _, .str _ _ => .gt

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

@@ -49,14 +49,14 @@ structure Name where
   value : String
 
   /--
-  The proof that it's a valid header name
+  The proof that it's a valid header name.
   -/
-  validHeaderName : IsValidHeaderName value := by decide
+  isValidHeaderValue : IsValidHeaderName value := by decide
 
   /--
-  The proof that we stored the header name in normal form
+  The proof that we stored the header name in stored as a lower case string.
   -/
-  normalForm : IsLowerCase value := by decide
+  isLowerCase : IsLowerCase value := by decide
 deriving Repr, DecidableEq
 
 namespace Name

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

@@ -55,7 +55,7 @@ structure Value where
   /--
   The proof that it's a valid header value.
   -/
-  validHeaderValue : IsValidHeaderValue value := by decide
+  isValidHeaderValue : IsValidHeaderValue value := by decide
 deriving BEq, DecidableEq, Repr
 
 instance : Hashable Value where

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

@@ -66,7 +66,7 @@ structure Request (t : Type) where
   /--
   The request line information (`method`, `version`, and request-target `uri`).
   -/
-  head : Request.Head
+  line : Request.Head
 
   /--
   The request body content of type t.
@@ -84,9 +84,9 @@ Builds an HTTP Request.
 -/
 structure Request.Builder where
   /--
-  The head of the request.
+  The request-line of an HTTP request.
   -/
-  head : Head := { method := .get, version := .v11, uri := .asteriskForm }
+  line : Head := { method := .get, version := .v11, uri := .asteriskForm }
 
   /--
   Optional dynamic metadata attached to the request.
@@ -134,38 +134,38 @@ def empty : Builder := { }
 Sets the HTTP method for the request being built.
 -/
 def method (builder : Builder) (method : Method) : Builder :=
-  { builder with head := { builder.head with method := method } }
+  { builder with line := { builder.line with method := method } }
 
 /--
 Sets the HTTP version for the request being built.
 -/
 def version (builder : Builder) (version : Version) : Builder :=
-  { builder with head := { builder.head with version := version } }
+  { builder with line := { builder.line with version := version } }
 
 /--
 Sets the request target/URI for the request being built.
 -/
 def uri (builder : Builder) (uri : RequestTarget) : Builder :=
-  { builder with head := { builder.head with uri := uri } }
+  { builder with line := { builder.line with uri := uri } }
 
 /--
 Sets the request target/URI for the request being built
 -/
 def uri! (builder : Builder) (uri : String) : Builder :=
   let uri := RequestTarget.parse! uri
-  { builder with head := { builder.head with uri } }
+  { builder with line := { builder.line with uri } }
 
 /--
 Sets the headers for the request being built
 -/
 def headers (builder : Builder) (headers : Headers) : Builder :=
-  { builder with head := { builder.head with headers } }
+  { 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 head := { builder.head with headers := builder.head.headers.insert key value } }
+  { 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.
@@ -173,7 +173,7 @@ 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 head := { builder.head with headers := builder.head.headers.insert key value } }
+  { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
 
 /--
 Adds a single header to the request being built.
@@ -182,7 +182,7 @@ 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 head := { builder.head with headers := builder.head.headers.insert key 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.
@@ -202,7 +202,7 @@ def extension (builder : Builder) [TypeName α] (data : α) : Builder :=
 Builds and returns the final HTTP Request with the specified body.
 -/
 def body (builder : Builder) (body : t) : Request t :=
-  { head := builder.head, body := body, extensions := builder.extensions }
+  { line := builder.line, body := body, extensions := builder.extensions }
 
 end Builder
 
@@ -248,9 +248,8 @@ def patch (uri : RequestTarget) : Builder :=
 
 /--
 Creates a new HTTP HEAD Request builder with the specified URI.
-Named `head'` to avoid conflict with the `head` field accessor.
 -/
-def head' (uri : RequestTarget) : Builder :=
+def head (uri : RequestTarget) : Builder :=
   new
   |>.method .head
   |>.uri uri

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

@@ -52,7 +52,7 @@ structure Response (t : Type) where
   /--
   The response status-line information.
   -/
-  head : Response.Head := {}
+  line : Response.Head := {}
 
   /--
   The content of the response.
@@ -70,9 +70,9 @@ Builds an HTTP Response.
 -/
 structure Response.Builder where
   /--
-  The response status-line information.
+  The start-line of an HTTP request (method, request-target, and version).
   -/
-  head : Head := {}
+  line : Head := {}
 
   /--
   Optional dynamic metadata attached to the response.
@@ -117,19 +117,19 @@ def empty : Builder := { }
 Sets the HTTP status code for the response being built.
 -/
 def status (builder : Builder) (status : Status) : Builder :=
-  { builder with head := { builder.head with status := status } }
+  { 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 head := { builder.head with headers } }
+  { 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 head := { builder.head with headers := builder.head.headers.insert key value } }
+  { 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.
@@ -137,7 +137,7 @@ Adds a single header to the response being built, panics if the header is invali
 def header! (builder : Builder) (key : String) (value : String) : Builder :=
   let key := Header.Name.ofString! key
   let value := Header.Value.ofString! value
-  { builder with head := { builder.head with headers := builder.head.headers.insert key value } }
+  { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
 
 /--
 Adds a single header to the response being built.
@@ -146,7 +146,7 @@ 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 head := { builder.head with headers := builder.head.headers.insert key 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.
@@ -158,14 +158,14 @@ def extension (builder : Builder) [TypeName α] (data : α) : Builder :=
 Builds and returns the final HTTP Response with the specified body.
 -/
 def body (builder : Builder) (body : t) : Response t :=
-  { head := builder.head, body := body, extensions := builder.extensions }
+  { line := builder.line, body := body, extensions := builder.extensions }
 
 /--
 Builds and returns the final HTTP Response with an empty body (`{}`).
 Requires an `EmptyCollection` instance for the response body type.
 -/
 def build [EmptyCollection t] (builder : Builder) : Response t :=
-  { head := builder.head, body := {}, extensions := builder.extensions }
+  { line := builder.line, body := {}, extensions := builder.extensions }
 
 end Builder
 

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

@@ -39,15 +39,14 @@ abbrev IsValidReasonPhrase (s : String) : Prop :=
 Returns `true` for every status code that has a dedicated named constructor in `Status`.
 Used to ensure `Status.other` is never constructed with a code that already has a name.
 -/
-def isKnownStatusCode : UInt16 → Bool
-  | 100 | 101 | 102 | 103
+def isKnownStatusCode (code: UInt16) : Bool :=
+  code matches 100 | 101 | 102 | 103
   | 200 | 201 | 202 | 203 | 204 | 205 | 206 | 207 | 208 | 226
   | 300 | 301 | 302 | 303 | 304 | 305 | 306 | 307 | 308
   | 400 | 401 | 402 | 403 | 404 | 405 | 406 | 407 | 408 | 409 | 410
   | 411 | 412 | 413 | 414 | 415 | 416 | 417 | 418 | 421 | 422 | 423
   | 424 | 425 | 426 | 428 | 429 | 431 | 451
-  | 500 | 501 | 502 | 503 | 504 | 505 | 506 | 507 | 508 | 510 | 511 => true
-  | _ => false
+  | 500 | 501 | 502 | 503 | 504 | 505 | 506 | 507 | 508 | 510 | 511
 
 /--
 A custom HTTP status with a numeric code and a reason phrase. Used to represent status codes

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

@@ -112,11 +112,9 @@ namespace UserInfo
 Builds a `UserInfo` value from raw strings by applying userinfo percent-encoding.
 -/
 @[inline]
-def ofStrings (username : String) (password : Option String := none) : UserInfo :=
-  {
-    username := EncodedUserInfo.encode username
-    password := EncodedUserInfo.encode <$> password
-  }
+def ofStrings (username : String) (password : Option String := none) : UserInfo where
+  username := EncodedUserInfo.encode username
+  password := EncodedUserInfo.encode <$> password
 
 /--
 Returns the decoded username, or `none` if decoding fails UTF-8 validation.
@@ -227,11 +225,27 @@ instance : ToString Host where
     | .ipv6 addr => s!"[{toString addr}]"
 
 /--
-TCP port number.
-
-Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.3
+Authority port representation, preserving the distinction between:
+* no port separator (`example.com`)
+* empty port (`example.com:`)
+* numeric port (`example.com:443`)
 -/
-abbrev Port := UInt16
+inductive Port where
+  /--
+  No `:` port separator is present (for example, `example.com`).
+  -/
+  | omitted
+
+  /--
+  A `:` port separator is present with no digits after it (for example, `example.com:`).
+  -/
+  | empty
+
+  /--
+  A numeric port value is present (for example, `example.com:443`).
+  -/
+  | value (port : UInt16)
+deriving Inhabited, Repr, DecidableEq
 
 /--
 The authority component of a URI, identifying the network location of the resource.
@@ -250,9 +264,10 @@ structure Authority where
   host : Host
 
   /--
-  Optional port number for connecting to the host.
+  Port component, preserving whether it is omitted (`example.com`),
+  explicitly empty (`example.com:`), or numeric (`example.com:443`).
   -/
-  port : Option Port := none
+  port : Port := .omitted
 deriving Inhabited, Repr
 
 instance : ToString Authority where
@@ -263,8 +278,9 @@ instance : ToString Authority where
       | some ⟨name, none⟩ => s!"{name}@"
     let hostPart := toString auth.host
     let portPart := match auth.port with
-      | none => ""
-      | some p => s!":{p}"
+      | .omitted => ""
+      | .empty => ":"
+      | .value p => s!":{p}"
     s!"{userPart}{hostPart}{portPart}"
 
 /--
@@ -277,7 +293,7 @@ structure Path where
   /--
   The path segments making up the hierarchical structure (each segment is percent-encoded).
   -/
-  segments : Array (EncodedSegment)
+  segments : Array EncodedSegment
 
   /--
   Whether the path is absolute (begins with '/') or relative.
@@ -606,7 +622,7 @@ structure Builder where
   /--
   The port number.
   -/
-  port : Option URI.Port := none
+  port : URI.Port := .omitted
 
   /--
   Path segments (will be encoded when building).
@@ -692,8 +708,8 @@ def setHostIPv6 (b : Builder) (addr : Net.IPv6Addr) : Builder :=
 /--
 Sets the port number.
 -/
-def setPort (b : Builder) (port : Port) : Builder :=
-  { b with port := some port }
+def setPort (b : Builder) (port : UInt16) : Builder :=
+  { b with port := .value port }
 
 /--
 Replaces all path segments. Segments will be automatically percent-encoded when building.

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

@@ -52,10 +52,10 @@ Checks if all characters in a `ByteArray` are allowed in an encoded URI componen
 that only verifies the character set, not full encoding validity.
 -/
 @[inline]
-abbrev isAllowedEncodedChars (rule : UInt8 → Bool) (s : ByteArray) : Prop :=
+abbrev IsAllowedEncodedChars (rule : UInt8 → Bool) (s : ByteArray) : Prop :=
   s.data.all (isEncodedChar rule)
 
-instance : Decidable (isAllowedEncodedChars r s) :=
+instance : Decidable (IsAllowedEncodedChars r s) :=
   inferInstanceAs (Decidable (s.data.all (isEncodedChar r) = true))
 
 /--
@@ -63,10 +63,10 @@ Checks if all characters in a `ByteArray` are allowed in an encoded query parame
 alternative encoding for space (application/x-www-form-urlencoded).
 -/
 @[inline]
-abbrev isAllowedEncodedQueryChars (rule : UInt8 → Bool) (s : ByteArray) : Prop :=
+abbrev IsAllowedEncodedQueryChars (rule : UInt8 → Bool) (s : ByteArray) : Prop :=
   s.data.all (isEncodedQueryChar rule)
 
-instance : Decidable (isAllowedEncodedQueryChars r s) :=
+instance : Decidable (IsAllowedEncodedQueryChars r s) :=
   inferInstanceAs (Decidable (s.data.all (isEncodedQueryChar r) = true))
 
 /--
@@ -118,13 +118,13 @@ def hexDigitToUInt8? (c : UInt8) : Option UInt8 :=
   else
     none
 
-private theorem isAllowedEncodedChars.push {bs : ByteArray} (h : isAllowedEncodedChars r bs) (h₁ : isEncodedChar r c) :
-    isAllowedEncodedChars r (bs.push c) := by
-  simpa [isAllowedEncodedChars, ByteArray.push, Array.all_push, And.intro h h₁]
+private theorem IsAllowedEncodedChars.push {bs : ByteArray} (h : IsAllowedEncodedChars r bs) (h₁ : isEncodedChar r c) :
+    IsAllowedEncodedChars r (bs.push c) := by
+  simpa [IsAllowedEncodedChars, ByteArray.push, Array.all_push, And.intro h h₁]
 
-private theorem isAllowedEncodedQueryChars.push {bs : ByteArray} (h : isAllowedEncodedQueryChars r bs) (h₁ : isEncodedQueryChar r c) :
-    isAllowedEncodedQueryChars r (bs.push c) := by
-  simpa [isAllowedEncodedQueryChars, ByteArray.push, Array.all_push, And.intro h h₁]
+private theorem IsAllowedEncodedQueryChars.push {bs : ByteArray} (h : IsAllowedEncodedQueryChars r bs) (h₁ : isEncodedQueryChar r c) :
+    IsAllowedEncodedQueryChars r (bs.push c) := by
+  simpa [IsAllowedEncodedQueryChars, ByteArray.push, Array.all_push, And.intro h h₁]
 
 private theorem isEncodedChar_isAscii (c : UInt8) (h : isEncodedChar r c) : isAsciiByte c := by
   simp [isEncodedChar, isAsciiByte] at *
@@ -218,7 +218,7 @@ private theorem ByteArray.toList_toByteArray (ba : ByteArray) :
     simp [List.toByteArray_loop_eq, ByteArray.empty]
     decide
 
-theorem ascii_is_valid_utf8 (ba : ByteArray) (s : ba.data.all isAsciiByte) : ByteArray.IsValidUTF8 ba := by
+theorem isValidUTF8_of_isAsciiByte (ba : ByteArray) (s : ba.data.all isAsciiByte) : ByteArray.IsValidUTF8 ba := by
   refine ⟨ba.data.toList.map Char.ofUInt8, ?_⟩
   rw [List.utf8Encode]
   simp only [List.flatMap_map]
@@ -248,7 +248,7 @@ structure EncodedString (r : UInt8 → Bool) where
   /--
   Proof that all characters in the byte array are valid encoded characters.
   -/
-  valid : isAllowedEncodedChars r toByteArray
+  valid : IsAllowedEncodedChars r toByteArray
 
 namespace EncodedString
 
@@ -266,7 +266,7 @@ Appends a single encoded character to an encoded string.
 Requires that the character is not '%' to maintain the percent-encoding invariant.
 -/
 private def push (s : EncodedString r) (c : UInt8) (h : isEncodedChar r c) : EncodedString r :=
-  ⟨s.toByteArray.push c, isAllowedEncodedChars.push s.valid h⟩
+  ⟨s.toByteArray.push c, IsAllowedEncodedChars.push s.valid h⟩
 
 /--
 Converts a byte to its percent-encoded hexadecimal representation (%XX). For example, a space
@@ -288,7 +288,7 @@ private def byteToHex (b : UInt8) (s : EncodedString r) : EncodedString r :=
       let h₀ := hexDigit_isHexDigit (@UInt8.and_lt_add_one b 0xF (by decide))
       isHexDigit_isEncodedChar h₀
 
-    exact isAllowedEncodedChars.push (isAllowedEncodedChars.push (isAllowedEncodedChars.push s.valid h1) h2) h3
+    exact IsAllowedEncodedChars.push (IsAllowedEncodedChars.push (IsAllowedEncodedChars.push s.valid h1) h2) h3
   ⟨ba, valid⟩
 
 /--
@@ -307,7 +307,7 @@ Attempts to create an `EncodedString` from a `ByteArray`. Returns `some` if the
 valid encoded characters and all percent signs are followed by exactly two hex digits, `none` otherwise.
 -/
 def ofByteArray? (ba : ByteArray) : Option (EncodedString r) :=
-  if h : isAllowedEncodedChars r ba then
+  if h : IsAllowedEncodedChars r ba then
     if isValidPercentEncoding ba then some ⟨ba, h⟩ else none
   else none
 
@@ -336,11 +336,11 @@ def ofString! (s : String) : EncodedString r :=
 Creates an `EncodedString` from a `ByteArray` with compile-time proofs.
 Use this when you have proofs that the byte array is valid.
 -/
-def new (ba : ByteArray) (valid : isAllowedEncodedChars r ba) (_validEncoding : isValidPercentEncoding ba) : EncodedString r :=
+def new (ba : ByteArray) (valid : IsAllowedEncodedChars r ba) (_validEncoding : isValidPercentEncoding ba) : EncodedString r :=
   ⟨ba, valid⟩
 
 instance : ToString (EncodedString r) where
-  toString es := ⟨es.toByteArray, ascii_is_valid_utf8 es.toByteArray (all_of_all_of_imp es.valid (fun c h => by simp [isEncodedChar] at h; exact h.left))⟩
+  toString es := ⟨es.toByteArray, isValidUTF8_of_isAsciiByte es.toByteArray (all_of_all_of_imp es.valid (fun c h => by simp [isEncodedChar] at h; exact h.left))⟩
 
 /--
 Decodes an `EncodedString` back to a regular `String`. Converts percent-encoded sequences (e.g., "%20")
@@ -401,7 +401,7 @@ structure EncodedQueryString (r : UInt8 → Bool) where
   /--
   Proof that all characters in the byte array are valid encoded query characters.
   -/
-  valid : isAllowedEncodedQueryChars r toByteArray
+  valid : IsAllowedEncodedQueryChars r toByteArray
 
 namespace EncodedQueryString
 
@@ -418,14 +418,14 @@ instance : Inhabited (EncodedQueryString r) where
 Appends a single encoded query character to an encoded query string.
 -/
 private def push (s : EncodedQueryString r) (c : UInt8) (h : isEncodedQueryChar r c) : EncodedQueryString r :=
-  ⟨s.toByteArray.push c, isAllowedEncodedQueryChars.push s.valid h⟩
+  ⟨s.toByteArray.push c, IsAllowedEncodedQueryChars.push s.valid h⟩
 
 /--
 Attempts to create an `EncodedQueryString` from a `ByteArray`. Returns `some` if the byte array contains
 only valid encoded query characters and all percent signs are followed by exactly two hex digits, `none` otherwise.
 -/
 def ofByteArray? (ba : ByteArray) (r : UInt8 → Bool := isQueryChar) : Option (EncodedQueryString r) :=
-  if h : isAllowedEncodedQueryChars r ba then
+  if h : IsAllowedEncodedQueryChars r ba then
     if isValidPercentEncoding ba then some ⟨ba, h⟩ else none
   else none
 
@@ -454,7 +454,7 @@ def ofString! (s : String) (r : UInt8 → Bool := isQueryChar) : EncodedQueryStr
 Creates an `EncodedQueryString` from a `ByteArray` with compile-time proofs.
 Use this when you have proofs that the byte array is valid.
 -/
-def new (ba : ByteArray) (valid : isAllowedEncodedQueryChars r ba) (_validEncoding : isValidPercentEncoding ba) : EncodedQueryString r :=
+def new (ba : ByteArray) (valid : IsAllowedEncodedQueryChars r ba) (_validEncoding : isValidPercentEncoding ba) : EncodedQueryString r :=
   ⟨ba, valid⟩
 
 /--
@@ -472,7 +472,7 @@ private def byteToHex (b : UInt8) (s : EncodedQueryString r) : EncodedQueryStrin
       isHexDigit_isEncodedQueryChar (hexDigit_isHexDigit (BitVec.toNat_ushiftRight_lt b.toBitVec 4 (by decide)))
     have h3 : isEncodedQueryChar r (hexDigit (b &&& 0xF)) :=
       isHexDigit_isEncodedQueryChar (hexDigit_isHexDigit (@UInt8.and_lt_add_one b 0xF (by decide)))
-    exact isAllowedEncodedQueryChars.push (isAllowedEncodedQueryChars.push (isAllowedEncodedQueryChars.push s.valid h1) h2) h3
+    exact IsAllowedEncodedQueryChars.push (IsAllowedEncodedQueryChars.push (IsAllowedEncodedQueryChars.push s.valid h1) h2) h3
   ⟨ba, valid⟩
 
 /--
@@ -492,7 +492,7 @@ def encode (s : String) (r : UInt8 → Bool := isQueryChar) : EncodedQueryString
 Converts an `EncodedQueryString` to a `String`, given a proof that all characters satisfying `r` are ASCII.
 -/
 def toString (es : EncodedQueryString r) : String :=
-  ⟨es.toByteArray, ascii_is_valid_utf8 es.toByteArray (all_of_all_of_imp es.valid (fun c h => isEncodedQueryChar_isAscii c h))⟩
+  ⟨es.toByteArray, isValidUTF8_of_isAsciiByte es.toByteArray (all_of_all_of_imp es.valid (fun c h => isEncodedQueryChar_isAscii c h))⟩
 
 /--
 Decodes an `EncodedQueryString` back to a regular `String`. Converts percent-encoded sequences and '+'
@@ -649,7 +649,7 @@ end EncodedUserInfo
 /--
 A percent-encoded URI query parameter. Valid characters are `pchar / "/" / "?"` with '+' for spaces.
 -/
-abbrev EncodedQueryParam := EncodedQueryString isQueryChar
+abbrev EncodedQueryParam := EncodedQueryString isQueryDataChar
 
 namespace EncodedQueryParam
 
@@ -657,25 +657,25 @@ namespace EncodedQueryParam
 Encodes a raw string into an encoded query parameter.
 -/
 def encode (s : String) : EncodedQueryParam :=
-  EncodedQueryString.encode (r := isQueryChar) s
+  EncodedQueryString.encode (r := isQueryDataChar) s
 
 /--
 Attempts to create an encoded query parameter from raw bytes.
 -/
 def ofByteArray? (ba : ByteArray) : Option EncodedQueryParam :=
-  EncodedQueryString.ofByteArray? (r := isQueryChar) ba
+  EncodedQueryString.ofByteArray? (r := isQueryDataChar) ba
 
 /--
 Creates an encoded query parameter from raw bytes, panicking on invalid encoding.
 -/
 def ofByteArray! (ba : ByteArray) : EncodedQueryParam :=
-  EncodedQueryString.ofByteArray! (r := isQueryChar) ba
+  EncodedQueryString.ofByteArray! (r := isQueryDataChar) ba
 
 /--
 Attempts to create an encoded query parameter from an encoded string.
 -/
 def fromString? (s : String) : Option EncodedQueryParam :=
-  EncodedQueryString.ofString? (r := isQueryChar) s
+  EncodedQueryString.ofString? (r := isQueryDataChar) s
 
 /--
 Decodes an encoded query parameter back to a UTF-8 string.

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

@@ -65,10 +65,10 @@ private def parseScheme (config : URI.Config) : Parser URI.Scheme := do
   else
     fail "invalid scheme"
 
--- port = *DIGIT
+-- port = 1*DIGIT
 private def parsePortNumber : Parser UInt16 := do
-  let portBytes ← takeWhileUpTo isDigit 5
-  if portBytes.size = 0 then fail "empty port number"
+  let portBytes ← takeWhileUpTo1 isDigit 5
+
   let portStr := String.fromUTF8! portBytes.toByteArray
 
   let some portNum := String.toNat? portStr
@@ -161,18 +161,28 @@ private def parseHost (config : URI.Config) : Parser URI.Host := do
 
 -- authority = [ userinfo "@" ] host [ ":" port ]
 private def parseAuthority (config : URI.Config) : Parser URI.Authority := do
-  let userinfo ← tryOpt do
+  let userInfo ← tryOpt do
     let ui ← parseUserInfo config
     skipByte '@'.toUInt8
     return ui
 
   let host ← parseHost config
 
-  let port ← optional do
-    skipByte ':'.toUInt8
-    parsePortNumber
+  let port : URI.AuthorityPort ←
+    if ← peekIs (· == ':'.toUInt8) then
+      skipByte ':'.toUInt8
+      if (← peekWhen? Internal.Char.isDigit).isSome then
+        pure (.value (← parsePortNumber))
+      else
+        let next ← peek?
+        if next.isNone || next.any (fun c => c = '/'.toUInt8 ∨ c = '?'.toUInt8 ∨ c = '#'.toUInt8) then
+          pure .empty
+        else
+          fail "invalid port number"
+    else
+      pure .omitted
 
-  return { userInfo := userinfo, host := host, port := port }
+  return { userInfo, host, port }
 
 -- segment = *pchar
 private def parseSegment (config : URI.Config) : Parser ByteSlice := do
@@ -388,17 +398,27 @@ where
     let host ← parseHost config
     skipByteChar ':'
     let port ← parsePortNumber
-    return .authorityForm { host, port := some port }
+    return .authorityForm { host, port := .value port }
 
 /--
 Parses an HTTP `Host` header value.
 -/
-public def parseHostHeader (config : URI.Config := {}) : Parser (URI.Host × Option UInt16) := do
+public def parseHostHeader (config : URI.Config := {}) : Parser (URI.Host × URI.Port) := do
   let host ← parseHost config
 
-  let port ← optional do
-    skipByte ':'.toUInt8
-    parsePortNumber
+  let port : URI.AuthorityPort ←
+    if ← peekIs (· == ':'.toUInt8) then
+      skipByte ':'.toUInt8
+      if (← peekWhen? Internal.Char.isDigit).isSome then
+        pure (.value (← parsePortNumber))
+      else
+        let next ← peek?
+        if next.isNone then
+          pure .empty
+        else
+          fail "invalid host header port"
+    else
+      pure .omitted
 
   if ¬(← isEof) then
     fail "invalid host header"

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

@@ -29,6 +29,11 @@ HTTP protocol versions modeled by this library.
 Reference: https://httpwg.org/specs/rfc9110.html#protocol.version
 -/
 inductive Version
+  /--
+  `HTTP/1.0`
+  -/
+  | v10
+
   /--
   `HTTP/1.1`
   -/
@@ -51,6 +56,7 @@ namespace Version
 Converts a pair of `Nat` to the corresponding `Version`.
 -/
 def ofNumber? : Nat → Nat → Option Version
+  | 1, 0 => some .v10
   | 1, 1 => some .v11
   | 2, 0 => some .v20
   | 3, 0 => some .v30
@@ -60,6 +66,7 @@ def ofNumber? : Nat → Nat → Option Version
 Converts `String` to the corresponding `Version`.
 -/
 def ofString? : String → Option Version
+  | "HTTP/1.0" => some .v10
   | "HTTP/1.1" => some .v11
   | "HTTP/2.0" => some .v20
   | "HTTP/3.0" => some .v30
@@ -77,12 +84,14 @@ def ofString! (s : String) : Version :=
 Converts a `Version` to its corresponding major and minor numbers as a pair.
 -/
 def toNumber : Version → (Nat × Nat)
+  | .v10 => (1, 0)
   | .v11 => (1, 1)
   | .v20 => (2, 0)
   | .v30 => (3, 0)
 
 instance : ToString Version where
   toString
+    | .v10 => "HTTP/1.0"
     | .v11 => "HTTP/1.1"
     | .v20 => "HTTP/2.0"
     | .v30 => "HTTP/3.0"

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

@@ -26,7 +26,7 @@ set_option linter.all true
 /--
 Checks if a character is ASCII (Unicode code point < 128).
 -/
-@[expose]
+@[inline, expose]
 def isAscii (c : Char) : Bool :=
   c.toNat < 128
 
@@ -47,7 +47,7 @@ def isAlphaChar (c : Char) : Bool :=
 /--
 Checks if a byte represents an ASCII character (value < 128).
 -/
-@[expose]
+@[inline, expose]
 def isAsciiByte (c : UInt8) : Bool :=
   c < 128
 
@@ -65,195 +65,113 @@ Checks if a byte is an alphabetic character (a-z or A-Z).
 def isAlpha (c : UInt8) : Bool :=
   (c >= 'A'.toUInt8 && c <= 'Z'.toUInt8) || (c >= 'a'.toUInt8 && c <= 'z'.toUInt8)
 
-/--
-Two character predicates are equivalent on ASCII input (`0x00`-`0x7F`).
--/
-abbrev EqOnAscii (x : Char → Bool) (y : Char → Bool) : Prop :=
-  ∀ n < 128, x (Char.ofNat n) ↔ y (Char.ofNat n)
-
 /--
 tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*"
   / "+" / "-" / "." / "^" / "_" / "`" / "|" / "~"
   / DIGIT / ALPHA
   ; Visible token characters used to build `token`.
 -/
+@[inline]
 def tchar (c : Char) : Bool :=
-  "!#$%&'*+-.^_`|~".toList.contains c
-  ∨ isDigitChar c
-  ∨ isAlphaChar c
-
-/--
-Checks if a character is a valid HTTP token character per RFC 9110 §5.6.2.
-
-token = 1*tchar
--/
-def token (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x57ffffffc7fffffe03ff6cfa00000000 c.toNat
-
-theorem token_eq_tchar_on_ascii : EqOnAscii token tchar := by
-  decide
+  (c matches '!' | '#' | '$' | '%' | '&' | '\'' | '*' | '+' | '-' | '.' | '^' | '_' | '`' | '|' | '~') ||
+  isDigitChar c ||
+  isAlphaChar c
 
 /--
 vchar = %x21-7E
 ; Visible (printing) ASCII characters.
 -/
-def vcharSpec (c : Char) : Bool :=
-  c ≥ '!' ∧ c ≤ '~'
-
-/--
-Checks if `c` is a visible (printing) ASCII character.
--/
+@[inline]
 def vchar (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffe00000000 c.toNat
-
-theorem vchar_eq_vcharSpec_on_ascii : EqOnAscii vchar vcharSpec := by
-  decide
+  c ≥ '!' ∧ c ≤ '~'
 
 /--
 qdtext = HTAB / SP / %x21 / %x23-5B / %x5D-7E
 ; ASCII-only variant (no obs-text).
 -/
-def qdtextSpec (c : Char) : Bool :=
-  c = '\t' ∨
-  c = ' ' ∨
-  c = '!' ∨
-  ('#' ≤ c ∧ c ≤ '[') ∨
+@[inline]
+def qdtext (c : Char) : Bool :=
+  (c matches '\t' | ' ' | '!') ||
+  ('#' ≤ c ∧ c ≤ '[') ||
   (']' ≤ c ∧ c ≤ '~')
 
 /--
-Checks if `c` is valid `qdtext` in an HTTP `quoted-string` (ASCII-only).
--/
-def qdtext (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7fffffffeffffffffffffffb00000200 c.toNat
-
-theorem qdtext_eq_qdtextSpec_on_ascii : EqOnAscii qdtext qdtextSpec := by
-  decide
-
-/--
-quoted-pair = "\" ( HTAB / SP / VCHAR )
+quoted-pair = "\\" ( HTAB / SP / VCHAR )
 ; ASCII-only variant (no obs-text).
 -/
-def quotedPairCharSpec (c : Char) : Bool :=
-  c = '\t' ∨ c = ' ' ∨ vchar c
-
-/--
-Checks if `c` is valid after `\` in an HTTP `quoted-pair` (ASCII-only).
--/
+@[inline]
 def quotedPairChar (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
-
-theorem quotedPairChar_eq_quotedPairCharSpec_on_ascii :
-    EqOnAscii quotedPairChar quotedPairCharSpec := by
-  decide
+  (c matches '\t' | ' ') || vchar c
 
 /--
 quoted-string body character class:
 ( qdtext / quoted-pair payload ) in ASCII-only mode.
 -/
-def quotedStringCharSpec (c : Char) : Bool :=
-  qdtext c ∨ quotedPairChar c
-
-/--
-Returns `true` when `c` can be represented inside an HTTP `quoted-string` body:
-either directly as `qdtext` or via `quoted-pair`.
--/
+@[inline]
 def quotedStringChar (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
-
-theorem quotedStringChar_eq_quotedStringCharSpec_on_ascii :
-    EqOnAscii quotedStringChar quotedStringCharSpec := by
-  decide
+  qdtext c || quotedPairChar c
 
 /--
 field-vchar = VCHAR
 ; ASCII-only variant (no obs-text).
 -/
-def fieldVcharSpec (c : Char) : Bool :=
-  vchar c
-
-/--
-Checks if `c` is valid `field-vchar` in ASCII-only mode.
--/
+@[inline]
 def fieldVchar (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffe00000000 c.toNat
-
-theorem fieldVchar_eq_fieldVcharSpec_on_ascii : EqOnAscii fieldVchar fieldVcharSpec := by
-  decide
+  vchar c
 
 /--
 field-content character class:
 field-vchar / SP / HTAB
 ; ASCII-only variant (no obs-text).
 -/
-def fieldContentSpec (c : Char) : Bool :=
-  fieldVchar c ∨ c = ' ' ∨ c = '\t'
-
-/--
-Checks if `c` is valid in the body of an HTTP `field-content` (ASCII-only).
--/
+@[inline]
 def fieldContent (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
-
-theorem fieldContent_eq_fieldContentSpec_on_ascii : EqOnAscii fieldContent fieldContentSpec := by
-  decide
+  fieldVchar c || (c matches ' ' | '\t')
 
 /--
 ctext = HTAB / SP / %x21-27 / %x2A-5B / %x5D-7E
 ; ASCII-only variant (no obs-text).
 -/
-def ctextSpec (c : Char) : Bool :=
-  c = '\t' ∨
-  c = ' ' ∨
-  ('!' ≤ c ∧ c ≤ '\'') ∨
-  ('*' ≤ c ∧ c ≤ '[') ∨
-  (']' ≤ c ∧ c ≤ '~')
-
-/--
-Checks if `c` is valid `ctext` in an HTTP comment (ASCII-only).
--/
+@[inline]
 def ctext (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7fffffffeffffffffffffcff00000200 c.toNat
-
-theorem ctext_eq_ctextSpec_on_ascii : EqOnAscii ctext ctextSpec := by
-  decide
+  (c matches '\t' | ' ') ||
+  ('!' ≤ c ∧ c ≤ '\'') ||
+  ('*' ≤ c ∧ c ≤ '[') ||
+  (']' ≤ c ∧ c ≤ '~')
 
 /--
 etagc = "!" / %x23-7E
 ; ASCII-only variant (no obs-text).
 -/
-def etagcSpec (c : Char) : Bool :=
-  c = '!' ∨ ('#' ≤ c ∧ c ≤ '~')
-
-/--
-Checks if `c` is valid `etagc` inside an `opaque-tag` (ASCII-only).
--/
+@[inline]
 def etagc (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7ffffffffffffffffffffffa00000000 c.toNat
-
-theorem etagc_eq_etagcSpec_on_ascii : EqOnAscii etagc etagcSpec := by
-  decide
+  c = '!' || ('#' ≤ c ∧ c ≤ '~')
 
 /--
 OWS = *( SP / HTAB )  (character class only)
 -/
+@[inline]
 def ows (c : Char) : Bool :=
-  c = ' ' ∨ c = '\t'
+  c matches ' ' | '\t'
 
 /--
 BWS = OWS (character class alias)
 -/
+@[inline]
 def bws (c : Char) : Bool :=
   ows c
 
 /--
 RWS = 1*( SP / HTAB ) (character class is identical to `ows`)
 -/
+@[inline]
 def rws (c : Char) : Bool :=
   ows c
 
 /--
 obs-text = %x80-FF (and higher Unicode scalar values in this library's `Char` model).
 -/
+@[inline]
 def obsText (c : Char) : Bool :=
   0x80 ≤ c.toNat
 
@@ -264,40 +182,22 @@ HTAB / SP / VCHAR
 
 Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase
 -/
-def reasonPhraseCharSpec (c : Char) : Bool :=
-  c = '\t' ∨ c = ' ' ∨ vchar c
-
-/--
-Checks if `c` is valid inside an HTTP `reason-phrase` per RFC 9110 §15.
--/
+@[inline]
 def reasonPhraseChar (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x7fffffffffffffffffffffff00000200 c.toNat
-
-theorem reasonPhraseChar_eq_reasonPhraseCharSpec : EqOnAscii reasonPhraseChar reasonPhraseCharSpec := by
-  decide
+  (c matches '\t' | ' ') || vchar c
 
 /--
-Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F) using a precomputed bitmask.
+Checks if a character is a hexadecimal digit (0-9, a-f, or A-F).
 -/
-def isHexDigitSpec (c : Char) : Bool :=
-  (c ≥ '0' && c ≤ '9') ||
-  (c ≥ 'a' && c ≤ 'f') ||
-  (c ≥ 'A' && c ≤ 'F')
-
-/--
-Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F) using a precomputed bitmask.
--/
-@[expose]
+@[inline, expose]
 def isHexDigit (c : Char) : Bool :=
-  Nat.testBit 0x0000007e0000007e03ff000000000000 c.toNat
-
-theorem isHexDigit_eq_isHexDigitSpec_on_ascii : EqOnAscii isHexDigit isHexDigitSpec := by
-  decide
+  (c matches 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'A' | 'B' | 'C' | 'D' | 'E' | 'F') ||
+  isDigitChar c
 
 /--
 Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F).
 -/
-@[expose]
+@[inline, expose]
 def isHexDigitByte (c : UInt8) : Bool :=
   (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) ||
   (c ≥ 'a'.toUInt8 && c ≤ 'f'.toUInt8) ||
@@ -306,118 +206,54 @@ def isHexDigitByte (c : UInt8) : Bool :=
 /--
 Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z).
 -/
-def isAlphaNumSpec (c : UInt8) : Bool :=
+@[inline, expose]
+def isAlphaNum (c : UInt8) : Bool :=
   (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) ||
   (c ≥ 'a'.toUInt8 && c ≤ 'z'.toUInt8) ||
   (c ≥ 'A'.toUInt8 && c ≤ 'Z'.toUInt8)
 
 /--
-Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z) using a precomputed bitmask.
--/
-@[expose]
-def isAlphaNum (c : UInt8) : Bool :=
-  Nat.testBit 0x7fffffe07fffffe03ff000000000000 c.toNat
-
-theorem isAlphaNum_eq_isAlphaNumSpec_on_ascii :
-    ∀ i : Fin 128, isAlphaNum (UInt8.ofNat i.1) = isAlphaNumSpec (UInt8.ofNat i.1) := by
-  decide
-
-
-/--
-Checks if `c` is valid after `\` in an HTTP `quoted-pair` (ASCII-only).
+Checks whether `c` is an ASCII alphanumeric character.
 -/
 @[inline, expose]
-def isAsciiAlphaNumCharSpec (c : Char) : Bool :=
-  isAscii c && isAlphaNum (UInt8.ofNat c.toNat)
-
-/--
-Checks if `c` is valid after `\` in an HTTP `quoted-pair` (ASCII-only).
--/
 def isAsciiAlphaNumChar (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x07fffffe07fffffe03ff000000000000 c.toNat
-
-theorem isAsciiAlphaNumChar_eq_isAsciiAlphaNumCharSpec_on_ascii :
-    EqOnAscii isAsciiAlphaNumChar isAsciiAlphaNumCharSpec := by
-  decide
-
-/--
-Checks if a character is valid after the first character of a URI scheme.
-Valid characters are ASCII alphanumeric, `+`, `-`, and `.`.
--/
-@[expose]
-def isValidSchemeCharSpec (c : Char) : Bool :=
-  isAsciiAlphaNumCharSpec c || c == '+' || c == '-' || c == '.'
+  isAscii c && (isDigitChar c || isAlphaChar c)
 
 /--
 Checks if a character is valid after the first character of a URI scheme.
 Valid characters are ASCII alphanumeric, `+`, `-`, and `.`.
 -/
+@[inline, expose]
 def isValidSchemeChar (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x07fffffe07fffffe03ff680000000000 c.toNat
-
-theorem isValidSchemeCharChar_eq_isValidSchemeCharCharSpec_on_ascii :
-    EqOnAscii isValidSchemeChar isValidSchemeCharSpec := by
-  decide
+  isAsciiAlphaNumChar c || (c matches '+' | '-' | '.')
 
 /--
 Checks if a character is valid for use in a domain name.
 Valid characters are ASCII alphanumeric, hyphens, and dots.
 -/
-@[expose]
-def isValidDomainNameCharSpec (c : Char) : Bool :=
-  isAsciiAlphaNumCharSpec c || c == '-' || c == '.'
-
-/--
-Checks if a character is valid for use in a domain name.
--/
+@[inline, expose]
 def isValidDomainNameChar (c : Char) : Bool :=
-  isAscii c ∧ Nat.testBit 0x07fffffe07fffffe03ff600000000000 c.toNat
-
-theorem isValidDomainNameChar_eq_isValidDomainNameCharSpec_on_ascii :
-    EqOnAscii isValidDomainNameChar isValidDomainNameCharSpec := by
-  decide
+  isAsciiAlphaNumChar c || (c matches '-' | '.')
 
 /--
 Checks if a byte is an unreserved character according to RFC 3986. Unreserved characters are:
 alphanumeric, hyphen, period, underscore, and tilde.
 -/
-def isUnreservedSpec (c : UInt8) : Bool :=
-  isAlphaNumSpec c ||
-  (c = '-'.toUInt8 || c = '.'.toUInt8 || c = '_'.toUInt8 || c = '~'.toUInt8)
-
-/--
-Checks if a byte is an unreserved character according to RFC 3986 using a precomputed bitmask.
--/
-@[expose]
+@[inline, expose]
 def isUnreserved (c : UInt8) : Bool :=
-  Nat.testBit 0x47fffffe87fffffe03ff600000000000 c.toNat
-
-theorem isUnreserved_eq_isUnreservedSpec_on_ascii :
-    ∀ i : Fin 128, isUnreserved (UInt8.ofNat i.1) = isUnreservedSpec (UInt8.ofNat i.1) := by
-  decide
-
+  isAlphaNum c ||
+  (c = '-'.toUInt8 || c = '.'.toUInt8 || c = '_'.toUInt8 || c = '~'.toUInt8)
 
 /--
 Checks if a byte is a sub-delimiter character according to RFC 3986.
 Sub-delimiters are: `!`, `$`, `&`, `'`, `(`, `)`, `*`, `+`, `,`, `;`, `=`.
 -/
-def isSubDelimsSpec (c : UInt8) : Bool :=
-  c = '!'.toUInt8 || c = '$'.toUInt8 || c = '&'.toUInt8 || c = '\''.toUInt8 ||
+@[inline, expose]
+def isSubDelims (c : UInt8) : Bool :=
+  c = '!'.toUInt8 || c = '$'.toUInt8 || c = '&'.toUInt8 || c = ('\'' : Char).toUInt8 ||
   c = '('.toUInt8 || c = ')'.toUInt8 || c = '*'.toUInt8 || c = '+'.toUInt8 ||
   c = ','.toUInt8 || c = ';'.toUInt8 || c = '='.toUInt8
 
-/--
-Checks if a byte is a sub-delimiter character according to RFC 3986 using a precomputed bitmask.
--/
-@[expose]
-def isSubDelims (c : UInt8) : Bool :=
-  Nat.testBit 0x28001fd200000000 c.toNat
-
-theorem isSubDelims_eq_isSubDelimsSpec_on_ascii :
-    ∀ i : Fin 128, isSubDelims (UInt8.ofNat i.1) = isSubDelimsSpec (UInt8.ofNat i.1) := by
-  decide
-
-
 /--
 Checks if a byte is a valid path character (`pchar`) according to RFC 3986.
 `pchar = unreserved / pct-encoded / sub-delims / ":" / "@"`
@@ -425,57 +261,25 @@ Checks if a byte is a valid path character (`pchar`) according to RFC 3986.
 Note: The percent-encoding (`pct-encoded`) is handled separately by `isEncodedChar`,
 so this predicate only covers the non-percent characters.
 -/
-def isPCharSpec (c : UInt8) : Bool :=
-  isUnreservedSpec c || isSubDelimsSpec c || c = ':'.toUInt8 || c = '@'.toUInt8
-
-/--
-Checks if a byte is a valid path character (`pchar`) according to RFC 3986 using a precomputed bitmask.
--/
-@[expose]
+@[inline, expose]
 def isPChar (c : UInt8) : Bool :=
-  Nat.testBit 0x47fffffe87ffffff2fff7fd200000000 c.toNat
-
-theorem isPChar_eq_isPCharSpec_on_ascii :
-    ∀ i : Fin 128, isPChar (UInt8.ofNat i.1) = isPCharSpec (UInt8.ofNat i.1) := by
-  decide
-
+  isUnreserved c || isSubDelims c || c = ':'.toUInt8 || c = '@'.toUInt8
 
 /--
 Checks if a byte is a valid character in a URI query component according to RFC 3986.
 `query = *( pchar / "/" / "?" )`
 -/
-def isQueryCharSpec (c : UInt8) : Bool :=
-  isPCharSpec c || c = '/'.toUInt8 || c = '?'.toUInt8
-
-/--
-Checks if a byte is a valid character in a URI query component according to RFC 3986 using a precomputed bitmask.
--/
-@[expose]
+@[inline, expose]
 def isQueryChar (c : UInt8) : Bool :=
-  Nat.testBit 0x47fffffe87ffffffafffffd200000000 c.toNat
-
-theorem isQueryChar_eq_isQueryCharSpec_on_ascii :
-    ∀ i : Fin 128, isQueryChar (UInt8.ofNat i.1) = isQueryCharSpec (UInt8.ofNat i.1) := by
-  decide
-
+  isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8
 
 /--
 Checks if a byte is a valid character in a URI fragment component according to RFC 3986.
 `fragment = *( pchar / "/" / "?" )`
 -/
-def isFragmentCharSpec (c : UInt8) : Bool :=
-  isPCharSpec c || c = '/'.toUInt8 || c = '?'.toUInt8
-
-/--
-Checks if a byte is a valid character in a URI fragment component according to RFC 3986 using a precomputed bitmask.
--/
-@[expose]
+@[inline, expose]
 def isFragmentChar (c : UInt8) : Bool :=
-  Nat.testBit 0x47fffffe87ffffffafffffd200000000 c.toNat
-
-theorem isFragmentChar_eq_isFragmentCharSpec_on_ascii :
-    ∀ i : Fin 128, isFragmentChar (UInt8.ofNat i.1) = isFragmentCharSpec (UInt8.ofNat i.1) := by
-  decide
+  isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8
 
 /--
 Checks if a byte is a valid character in a URI userinfo component according to RFC 3986.
@@ -484,19 +288,19 @@ Checks if a byte is a valid character in a URI userinfo component according to R
 Note: It avoids the pct-encoded of the original grammar because it is used with `Encoding.lean`
 that provides it.
 -/
-def isUserInfoCharSpec (c : UInt8) : Bool :=
-  isUnreservedSpec c || isSubDelimsSpec c || c = ':'.toUInt8
+@[inline, expose]
+def isUserInfoChar (c : UInt8) : Bool :=
+  isUnreserved c || isSubDelims c || c = ':'.toUInt8
 
 /--
-Checks if a byte is a valid character in a URI userinfo component according to RFC 3986 using a precomputed bitmask.
+Checks if a byte is a valid character in a URI query component,
+excluding the typical key/value separators `&` and `=`.
+
+Inspired by `query = *( pchar / "/" / "?" )` from RFC 3986,
+but disallows `&` and `=` so they can be treated as structural separators.
 -/
-@[expose]
-def isUserInfoChar (c : UInt8) : Bool :=
-  Nat.testBit 0x47fffffe87fffffe2fff7fd200000000 c.toNat
-
-theorem isUserInfoChar_eq_isUserInfoCharSpec_on_ascii :
-    ∀ i : Fin 128, isUserInfoChar (UInt8.ofNat i.1) = isUserInfoCharSpec (UInt8.ofNat i.1) := by
-  decide
-
+@[inline, expose]
+def isQueryDataChar (c : UInt8) : Bool :=
+  isQueryChar c && c ≠ '&'.toUInt8 && c ≠ '='.toUInt8
 
 end Std.Http.Internal.Char

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

@@ -56,7 +56,7 @@ Returns `none` when any character in `s` cannot be represented by the grammar.
 -/
 @[expose]
 def quoteHttpString? (s : String) : Option String :=
-  if s.all token ∧ ¬s.isEmpty then
+  if s.all tchar ∧ ¬s.isEmpty then
     some s
   else if s.all quotedStringChar then
     some (.append
@@ -101,7 +101,7 @@ def unquoteHttpString? (s : String) : Option String :=
       | .done _ | .invalid => .invalid) .start with
     | .done result => some result
     | _ => none
-  else if s.all Char.token then
+  else if s.all Char.tchar then
     some s
   else
     none
@@ -112,6 +112,6 @@ Checks whether a string is a valid non-empty HTTP token.
 @[expose]
 def isToken (s : String) : Bool :=
   let s := s.toList
-  ¬s.isEmpty ∧ s.all Char.token
+  ¬s.isEmpty ∧ s.all Char.tchar
 
 end Std.Http.Internal

tests/lean/run/async_http_encode.lean

@@ -116,7 +116,7 @@ info: "999 Unknown"
 #guard_msgs in
 #eval encodeStr (Status.other ⟨999, "Unknown", by decide, by decide, by decide⟩)
 
-/-! ## Request.Head encoding -/
+/-! ## Request.line encoding -/
 
 /--
 info: ""
@@ -160,7 +160,7 @@ info: "PUT /resource HTTP/2.0\x0d\nContent-Type: application/json\x0d\n\x0d\n"
     headers := Headers.empty.insert! "content-type" "application/json"
   } : Request.Head)
 
-/-! ## Response.Head encoding -/
+/-! ## Response.line encoding -/
 
 /--
 info: "HTTP/1.1 200 OK\x0d\n\x0d\n"
@@ -222,61 +222,61 @@ info: "a\x0d\n0123456789\x0d\n"
 info: "GET /index.html HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.get (.parse! "/index.html") |>.body ()).head
+#eval encodeStr (Request.get (.parse! "/index.html") |>.body ()).line
 
 /--
 info: "POST /api/data HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.post (.parse! "/api/data") |>.body ()).head
+#eval encodeStr (Request.post (.parse! "/api/data") |>.body ()).line
 
 /--
 info: "PUT /resource HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.put (.parse! "/resource") |>.body ()).head
+#eval encodeStr (Request.put (.parse! "/resource") |>.body ()).line
 
 /--
 info: "DELETE /item HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.delete (.parse! "/item") |>.body ()).head
+#eval encodeStr (Request.delete (.parse! "/item") |>.body ()).line
 
 /--
 info: "PATCH /update HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.patch (.parse! "/update") |>.body ()).head
+#eval encodeStr (Request.patch (.parse! "/update") |>.body ()).line
 
 /--
 info: "HEAD /check HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.head' (.parse! "/check") |>.body ()).head
+#eval encodeStr (Request.head (.parse! "/check") |>.body ()).line
 
 /--
 info: "OPTIONS * HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.options (.parse! "*") |>.body ()).head
+#eval encodeStr (Request.options (.parse! "*") |>.body ()).line
 
 /--
 info: "CONNECT proxy:8080 HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.connect (.parse! "proxy:8080") |>.body ()).head
+#eval encodeStr (Request.connect (.parse! "proxy:8080") |>.body ()).line
 
 /--
 info: "TRACE /debug HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.trace (.parse! "/debug") |>.body ()).head
+#eval encodeStr (Request.trace (.parse! "/debug") |>.body ()).line
 
 /--
 info: "POST /v2 HTTP/2.0\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.new |>.method .post |>.uri (.parse! "/v2") |>.version .v20 |>.body ()).head
+#eval encodeStr (Request.new |>.method .post |>.uri (.parse! "/v2") |>.version .v20 |>.body ()).line
 
 /-! ## Response builder -/
 
@@ -284,67 +284,67 @@ info: "POST /v2 HTTP/2.0\x0d\n\x0d\n"
 info: "HTTP/1.1 200 OK\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.ok |>.body ()).head
+#eval encodeStr (Response.ok |>.body ()).line
 
 /--
 info: "HTTP/1.1 404 Not Found\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.notFound |>.body ()).head
+#eval encodeStr (Response.notFound |>.body ()).line
 
 /--
 info: "HTTP/1.1 500 Internal Server Error\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.internalServerError |>.body ()).head
+#eval encodeStr (Response.internalServerError |>.body ()).line
 
 /--
 info: "HTTP/1.1 400 Bad Request\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.badRequest |>.body ()).head
+#eval encodeStr (Response.badRequest |>.body ()).line
 
 /--
 info: "HTTP/1.1 201 Created\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.created |>.body ()).head
+#eval encodeStr (Response.created |>.body ()).line
 
 /--
 info: "HTTP/1.1 202 Accepted\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.accepted |>.body ()).head
+#eval encodeStr (Response.accepted |>.body ()).line
 
 /--
 info: "HTTP/1.1 401 Unauthorized\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.unauthorized |>.body ()).head
+#eval encodeStr (Response.unauthorized |>.body ()).line
 
 /--
 info: "HTTP/1.1 403 Forbidden\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.forbidden |>.body ()).head
+#eval encodeStr (Response.forbidden |>.body ()).line
 
 /--
 info: "HTTP/1.1 409 Conflict\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.conflict |>.body ()).head
+#eval encodeStr (Response.conflict |>.body ()).line
 
 /--
 info: "HTTP/1.1 503 Service Unavailable\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.serviceUnavailable |>.body ()).head
+#eval encodeStr (Response.serviceUnavailable |>.body ()).line
 
 /--
 info: "HTTP/1.1 418 I'm a teapot\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Response.withStatus .imATeapot |>.body ()).head
+#eval encodeStr (Response.withStatus .imATeapot |>.body ()).line
 
 /-! ## Edge cases: Status encoding -/
 

tests/lean/run/async_http_uri.lean

@@ -212,6 +212,40 @@ info: some " "
 #eval parseCheck "https://user:pass@secure.example.com/private"
 #eval parseCheck "/double//slash//path"
 #eval parseCheck "http://user%40example:pass%3Aword@host.com"
+#eval parseCheck "http://example.com:/"
+#eval parseCheck "http://example.com:/?q=1"
+
+-- `&` in a key must be percent-encoded so toRawString round-trips correctly.
+#guard
+  let query := URI.Query.empty.insert "a&b" "1"
+  query.toRawString == "a%26b=1"
+
+-- `=` in a key must be percent-encoded so re-parsing preserves the key.
+#guard
+  let query := URI.Query.empty.insert "a=b" "1"
+  query.toRawString == "a%3Db=1"
+
+-- `&` in a value must be percent-encoded.
+#guard
+  let query := URI.Query.empty.insert "key" "a&b"
+  query.toRawString == "key=a%26b"
+
+-- `=` in a value is technically safe (parser uses first `=`), but encoding it
+-- is still correct and keeps representation unambiguous.
+#guard
+  let query := URI.Query.empty.insert "key" "a=b"
+  query.toRawString == "key=a%3Db"
+
+-- Round-trip: insert → toRawString → re-parse should preserve the parameter.
+#guard
+  let original := URI.Query.empty.insert "a&b" "c=d"
+  let raw := original.toRawString
+  -- Parse via a synthetic origin-form request target
+  match (URI.Parser.parseRequestTarget <* Std.Internal.Parsec.eof).run
+      s!"/path?{raw}".toUTF8 with
+  | .ok result =>
+      (result.query.get "a&b" == some "c=d")
+  | .error _ => false
 
 #guard
   match (parseRequestTarget <* Std.Internal.Parsec.eof).run "http:80".toUTF8 with
@@ -291,7 +325,7 @@ info: Std.Http.RequestTarget.originForm { segments := #[], absolute := true } no
 
 /--
 info: Std.Http.RequestTarget.authorityForm
-  { userInfo := none, host := Std.Http.URI.Host.name "example.com", port := some 8080 }
+  { userInfo := none, host := Std.Http.URI.Host.name "example.com", port := Std.Http.URI.Port.value 8080 }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -299,7 +333,8 @@ info: Std.Http.RequestTarget.authorityForm
   IO.println (repr result)
 
 /--
-info: Std.Http.RequestTarget.authorityForm { userInfo := none, host := Std.Http.URI.Host.ipv4 192.168.1.1, port := some 3000 }
+info: Std.Http.RequestTarget.authorityForm
+  { userInfo := none, host := Std.Http.URI.Host.ipv4 192.168.1.1, port := Std.Http.URI.Port.value 3000 }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -307,7 +342,8 @@ info: Std.Http.RequestTarget.authorityForm { userInfo := none, host := Std.Http.
   IO.println (repr result)
 
 /--
-info: Std.Http.RequestTarget.authorityForm { userInfo := none, host := Std.Http.URI.Host.ipv6 ::1, port := some 8080 }
+info: Std.Http.RequestTarget.authorityForm
+  { userInfo := none, host := Std.Http.URI.Host.ipv6 ::1, port := Std.Http.URI.Port.value 8080 }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -317,7 +353,9 @@ info: Std.Http.RequestTarget.authorityForm { userInfo := none, host := Std.Http.
 /--
 info: Std.Http.RequestTarget.absoluteForm
   { scheme := "https",
-    authority := some { userInfo := none, host := Std.Http.URI.Host.name "example.com", port := some 8080 },
+    authority := some { userInfo := none,
+                   host := Std.Http.URI.Host.name "example.com",
+                   port := Std.Http.URI.Port.value 8080 },
     path := { segments := #["ata"], absolute := true },
     query := #[],
     fragment := none }
@@ -331,7 +369,9 @@ info: Std.Http.RequestTarget.absoluteForm
 /--
 info: Std.Http.RequestTarget.absoluteForm
   { scheme := "http",
-    authority := some { userInfo := none, host := Std.Http.URI.Host.ipv6 2001:db8::1, port := some 8080 },
+    authority := some { userInfo := none,
+                   host := Std.Http.URI.Host.ipv6 2001:db8::1,
+                   port := Std.Http.URI.Port.value 8080 },
     path := { segments := #["path"], absolute := true },
     query := #[],
     fragment := none }
@@ -347,7 +387,7 @@ info: Std.Http.RequestTarget.absoluteForm
   { scheme := "https",
     authority := some { userInfo := some { username := "user%20b", password := some "pass" },
                    host := Std.Http.URI.Host.name "secure.example.com",
-                   port := none },
+                   port := Std.Http.URI.Port.omitted },
     path := { segments := #["private"], absolute := true },
     query := #[],
     fragment := none }
@@ -847,7 +887,7 @@ info: Std.Http.RequestTarget.originForm { segments := #["caf%C3%A9"], absolute :
 
 /--
 info: Std.Http.RequestTarget.authorityForm
-  { userInfo := none, host := Std.Http.URI.Host.name "proxy.example.com", port := some 3128 }
+  { userInfo := none, host := Std.Http.URI.Host.name "proxy.example.com", port := Std.Http.URI.Port.value 3128 }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -855,7 +895,8 @@ info: Std.Http.RequestTarget.authorityForm
   IO.println (repr result)
 
 /--
-info: Std.Http.RequestTarget.authorityForm { userInfo := none, host := Std.Http.URI.Host.ipv4 127.0.0.1, port := some 8080 }
+info: Std.Http.RequestTarget.authorityForm
+  { userInfo := none, host := Std.Http.URI.Host.ipv4 127.0.0.1, port := Std.Http.URI.Port.value 8080 }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -864,7 +905,7 @@ info: Std.Http.RequestTarget.authorityForm { userInfo := none, host := Std.Http.
 
 /--
 info: Std.Http.RequestTarget.authorityForm
-  { userInfo := none, host := Std.Http.URI.Host.name "1example.com", port := some 8080 }
+  { userInfo := none, host := Std.Http.URI.Host.name "1example.com", port := Std.Http.URI.Port.value 8080 }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -874,7 +915,9 @@ info: Std.Http.RequestTarget.authorityForm
 /--
 info: Std.Http.RequestTarget.absoluteForm
   { scheme := "http",
-    authority := some { userInfo := none, host := Std.Http.URI.Host.name "1example.com", port := none },
+    authority := some { userInfo := none,
+                   host := Std.Http.URI.Host.name "1example.com",
+                   port := Std.Http.URI.Port.omitted },
     path := { segments := #["path"], absolute := true },
     query := #[],
     fragment := none }
@@ -888,7 +931,9 @@ info: Std.Http.RequestTarget.absoluteForm
 /--
 info: Std.Http.RequestTarget.absoluteForm
   { scheme := "http",
-    authority := some { userInfo := none, host := Std.Http.URI.Host.name "123abc.example.com", port := none },
+    authority := some { userInfo := none,
+                   host := Std.Http.URI.Host.name "123abc.example.com",
+                   port := Std.Http.URI.Port.omitted },
     path := { segments := #["page"], absolute := true },
     query := #[],
     fragment := none }