Merge branch 'master' of https://github.com/leanprover/lean4 into sofia/async-http-uri

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

src/Std/Internal/Http/Data.lean

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

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

@@ -10,6 +10,7 @@ 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 import Std.Internal.Http.Data.URI
 
 public section
 
@@ -50,7 +51,7 @@ structure Request.Head where
   /--
   The raw request-target string (commonly origin-form path/query, `"*"`, or authority-form).
   -/
-  uri : String
+  uri : RequestTarget := .asteriskForm
 
   /--
   Collection of HTTP headers for the request (Content-Type, Authorization, etc.).
@@ -85,7 +86,7 @@ structure Request.Builder where
   /--
   The request-line of an HTTP request.
   -/
-  line : Head := { method := .get, version := .v11, uri := "*" }
+  line : Head := { method := .get, version := .v11, uri := .asteriskForm }
 
   /--
   Optional dynamic metadata attached to the request.
@@ -108,7 +109,7 @@ instance : Encode .v11 Head where
   encode buffer req :=
     let buffer := Encode.encode (v := .v11) buffer req.method
     let buffer := buffer.writeChar ' '
-    let buffer := buffer.writeString req.uri
+    let buffer := Encode.encode (v := .v11) buffer req.uri
     let buffer := buffer.writeChar ' '
     let buffer := Encode.encode (v := .v11) buffer req.version
     let buffer := buffer.writeString "\r\n"
@@ -144,11 +145,18 @@ def version (builder : Builder) (version : Version) : Builder :=
 /--
 Sets the request target/URI for the request being built.
 -/
-def uri (builder : Builder) (uri : String) : Builder :=
+def uri (builder : Builder) (uri : RequestTarget) : Builder :=
   { builder with line := { builder.line with uri := uri } }
 
 /--
-Sets the headers for the request being built.
+Sets the request target/URI for the request being built
+-/
+def uri! (builder : Builder) (uri : String) : Builder :=
+  let uri := RequestTarget.parse! 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 line := { builder.line with headers } }
@@ -201,7 +209,7 @@ end Builder
 /--
 Creates a new HTTP GET Request with the specified URI.
 -/
-def get (uri : String) : Builder :=
+def get (uri : RequestTarget) : Builder :=
   new
   |>.method .get
   |>.uri uri
@@ -209,7 +217,7 @@ def get (uri : String) : Builder :=
 /--
 Creates a new HTTP POST Request builder with the specified URI.
 -/
-def post (uri : String) : Builder :=
+def post (uri : RequestTarget) : Builder :=
   new
   |>.method .post
   |>.uri uri
@@ -217,7 +225,7 @@ def post (uri : String) : Builder :=
 /--
 Creates a new HTTP PUT Request builder with the specified URI.
 -/
-def put (uri : String) : Builder :=
+def put (uri : RequestTarget) : Builder :=
   new
   |>.method .put
   |>.uri uri
@@ -225,7 +233,7 @@ def put (uri : String) : Builder :=
 /--
 Creates a new HTTP DELETE Request builder with the specified URI.
 -/
-def delete (uri : String) : Builder :=
+def delete (uri : RequestTarget) : Builder :=
   new
   |>.method .delete
   |>.uri uri
@@ -233,7 +241,7 @@ def delete (uri : String) : Builder :=
 /--
 Creates a new HTTP PATCH Request builder with the specified URI.
 -/
-def patch (uri : String) : Builder :=
+def patch (uri : RequestTarget) : Builder :=
   new
   |>.method .patch
   |>.uri uri
@@ -241,25 +249,25 @@ def patch (uri : String) : Builder :=
 /--
 Creates a new HTTP HEAD Request builder with the specified URI.
 -/
-def head (uri : String) : Builder :=
+def head (uri : RequestTarget) : Builder :=
   new
   |>.method .head
   |>.uri uri
 
 /--
 Creates a new HTTP OPTIONS Request builder with the specified URI.
-Use `Request.options "*"` for server-wide OPTIONS.
+Use `Request.options (RequestTarget.asteriskForm)` for server-wide OPTIONS.
 -/
-def options (uri : String) : Builder :=
+def options (uri : RequestTarget) : Builder :=
   new
   |>.method .options
   |>.uri uri
 
 /--
 Creates a new HTTP CONNECT Request builder with the specified URI.
-Typically used with authority-form URIs such as `"example.com:443"` for tunneling.
+Typically used with `RequestTarget.authorityForm` for tunneling.
 -/
-def connect (uri : String) : Builder :=
+def connect (uri : RequestTarget) : Builder :=
   new
   |>.method .connect
   |>.uri uri
@@ -267,7 +275,7 @@ def connect (uri : String) : Builder :=
 /--
 Creates a new HTTP TRACE Request builder with the specified URI.
 -/
-def trace (uri : String) : Builder :=
+def trace (uri : RequestTarget) : Builder :=
   new
   |>.method .trace
   |>.uri uri

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

@@ -0,0 +1,97 @@
+/-
+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.URI.Basic
+public import Std.Internal.Http.Data.URI.Parser
+
+public section
+
+/-!
+# URI
+
+This module defines the `URI` and `RequestTarget` types that represent and manipulate components of
+URIs as defined by RFC 3986. It provides parsing, rendering, and normalization utilities for working
+with URIs and request targets in HTTP messages.
+
+References:
+* https://www.rfc-editor.org/rfc/rfc3986.html
+* https://www.rfc-editor.org/rfc/rfc9112.html#section-3.3
+-/
+
+namespace Std.Http.RequestTarget
+
+set_option linter.all true
+
+/--
+Attempts to parse a `RequestTarget` from the given string.
+-/
+@[inline]
+def parse? (string : String) : Option RequestTarget :=
+  (URI.Parser.parseRequestTarget <* Std.Internal.Parsec.eof).run string.toUTF8 |>.toOption
+
+/--
+Parses a `RequestTarget` from the given string. Panics if parsing fails. Use `parse?`
+if you need a safe option-returning version.
+-/
+@[inline]
+def parse! (string : String) : RequestTarget :=
+  match parse? string with
+  | some res => res
+  | none => panic! "invalid request target"
+
+/--
+Creates an origin-form request target from a path string.
+The path should start with '/' (e.g., "/api/users" or "/search?q=test").
+Panics if the string is not a valid origin-form request target.
+-/
+@[inline]
+def originForm! (path : String) : RequestTarget :=
+  match parse? path with
+  | some (.originForm p q) => .originForm p q
+  | _ => panic! s!"invalid origin-form request target: {path}"
+
+end RequestTarget
+
+namespace URI
+
+/--
+Attempts to parse a `URI` from the given string.
+-/
+@[inline]
+def parse? (string : String) : Option URI :=
+  (Parser.parseURI <* Std.Internal.Parsec.eof).run string.toUTF8 |>.toOption
+
+/--
+Parses a `URI` from the given string. Panics if parsing fails. Use `parse?` if you need a safe
+option-returning version.
+-/
+@[inline]
+def parse! (string : String) : URI :=
+  match parse? string with
+  | some res => res
+  | none => panic! "invalid URI"
+
+namespace Path
+
+/--
+Attempts to parse a URI path from the given string.
+Returns `none` if the string is not a valid path.
+-/
+@[inline]
+def parse? (s : String) : Option Std.Http.URI.Path :=
+  (Std.Http.URI.Parser.parsePath {} true true <* Std.Internal.Parsec.eof).run s.toUTF8 |>.toOption
+
+/--
+Parses a URI path from the given string. Returns the root path `"/"` if parsing fails.
+-/
+@[inline]
+def parseOrRoot (s : String) : Std.Http.URI.Path :=
+  parse? s |>.getD { segments := #[], absolute := true }
+
+end Std.Http.URI.Path
+

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

@@ -0,0 +1,916 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+import Init.Data.ToString
+public import Std.Net
+public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Data.URI.Encoding
+
+public section
+
+/-!
+# URI Structure
+
+This module defines an HTTP-oriented URI structure aligned with RFC 3986 and RFC 9110, including
+schemes, authorities, paths, queries, fragments, and request targets.
+
+Host handling is intentionally strict: this module accepts IPv4, bracketed IPv6, and DNS-style
+domain names (LDH labels). RFC 3986 `reg-name` forms that are not DNS-compatible are rejected.
+
+All text components use the encoding types from `Std.Http.URI.Encoding` to ensure proper
+percent-encoding is maintained throughout.
+
+References:
+* https://www.rfc-editor.org/rfc/rfc3986.html
+* https://www.rfc-editor.org/rfc/rfc9110.html#name-uri-references
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+open Internal Char
+
+namespace URI
+
+/--
+Proposition that `s` is a valid URI scheme per RFC 3986:
+`scheme = ALPHA *( ALPHA / DIGIT / "+" / "-" / "." )`.
+
+The scheme value stored in this module is normalized to lowercase.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.1
+-/
+abbrev IsValidScheme (s : String) : Prop :=
+  IsLowerCase s ∧
+  s.toList.all isValidSchemeChar ∧
+  (s.toList.head?.map isAlpha |>.getD false) -- first character must be ALPHA
+
+/--
+URI scheme identifier (e.g., "http", "https", "ftp").
+-/
+abbrev Scheme := { s : String // IsValidScheme s }
+
+instance : Inhabited Scheme where
+  default := ⟨"http", ⟨by decide, by decide, by decide⟩⟩
+
+namespace Scheme
+
+/--
+Attempts to create a `Scheme` from a string, normalizing to lowercase.
+Returns `none` if the scheme is invalid per RFC 3986 Section 3.1.
+-/
+def ofString? (s : String) : Option Scheme :=
+  let lower := s.toLower
+
+  if h : IsValidScheme lower then
+    some ⟨lower, h⟩
+  else
+    none
+
+/--
+Creates a `Scheme` from a string, normalizing to lowercase. Panics if invalid.
+-/
+def ofString! (s : String) : Scheme :=
+  match ofString? s with
+  | some scheme => scheme
+  | none => panic! s!"invalid URI scheme: {s.quote}"
+
+/--
+Returns the default port number for this URI scheme: 443 for `https`, 80 for everything else.
+-/
+def defaultPort (scheme : URI.Scheme) : UInt16 :=
+  if scheme.val == "https" then 443 else 80
+
+/--
+Returns the URI scheme for a given port: `"https"` for 443, `"http"` otherwise.
+-/
+def ofPort (port : UInt16) : URI.Scheme :=
+  if port == 443 then ⟨"https", by decide⟩ else ⟨"http", by decide⟩
+
+end Scheme
+
+/--
+User information component containing an encoded username and optional encoded password.
+
+The stored strings use URI userinfo percent-encoding so parsed URIs can be rendered without
+losing percent-encoding choices (for example, `%3A` versus `:`).
+
+Note: embedding passwords in URIs is deprecated per RFC 9110 Section 4.2.4. Avoid using the
+password field in new code, and never include it in logs or error messages.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.1
+-/
+structure UserInfo where
+  /--
+  The encoded username.
+  -/
+  username : EncodedUserInfo
+
+  /--
+  The optional encoded password.
+  -/
+  password : Option EncodedUserInfo
+deriving Inhabited, Repr, BEq
+
+namespace UserInfo
+
+/--
+Builds a `UserInfo` value from raw strings by applying userinfo percent-encoding.
+-/
+@[inline]
+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.
+-/
+@[inline]
+def username? (ui : UserInfo) : Option String :=
+  ui.username.decode
+
+/--
+Returns the decoded password when present, or `none` if absent or decoding fails UTF-8 validation.
+-/
+@[inline]
+def password? (ui : UserInfo) : Option String :=
+  ui.password.bind EncodedUserInfo.decode
+
+end UserInfo
+
+/--
+Checks whether a single domain label is valid. A label must be non-empty, contain only ASCII
+alphanumeric characters and `-`, cannot start or end with `-`, and must be at most 63 characters.
+
+References:
+* https://www.rfc-editor.org/rfc/rfc1034.html#section-3.5
+* https://www.rfc-editor.org/rfc/rfc1123.html#section-2.1
+-/
+def isValidDomainLabel (s : String) : Bool :=
+  let chars := s.toList
+  decide (chars.length ≤ 63) &&
+    chars.all (fun c => isAsciiAlphaNumChar c ∨ c = '-') &&
+    (chars.head?.map isAsciiAlphaNumChar |>.getD false) &&
+    (chars.getLast?.map isAsciiAlphaNumChar |>.getD false)
+
+/--
+Proposition that asserts `s` is a valid dot-separated domain name.
+Each label must satisfy `IsValidDomainLabel`, and the full name must be at most 255 characters.
+-/
+abbrev IsValidDomainName (s : String) : Prop :=
+  let labels := s.splitOn "."
+  ¬labels.isEmpty ∧ labels.all isValidDomainLabel ∧ s.length ≤ 255
+
+/--
+A domain name represented as a validated, lowercase-normalized string.
+Only ASCII alphanumeric characters, hyphens, and dots are allowed.
+Each label cannot start or end with `-` and is limited to 63 characters.
+Internationalized domain names must be converted to punycode before use.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.2
+-/
+abbrev DomainName := { s : String // IsLowerCase s ∧ IsValidDomainName s ∧ ¬s.isEmpty }
+
+namespace DomainName
+
+/--
+Attempts to create a normalized domain name from a string.
+Returns `none` if the name is empty, longer than 255 characters, or any label violates DNS label
+constraints.
+-/
+def ofString? (s : String) : Option DomainName :=
+  let lower := s.toLower
+  if h₁ : lower.isEmpty then
+    none
+  else if h₃ : IsValidDomainName lower then
+    some ⟨lower, IsLowerCase.isLowerCase_toLower, h₃, h₁⟩
+  else
+    none
+
+end DomainName
+
+/--
+Host component of a URI, supporting domain names and IP addresses.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.2
+-/
+inductive Host
+  /--
+  A domain name (lowercase-normalized).
+  -/
+  | name (name : DomainName)
+
+  /--
+  An IPv4 address.
+  -/
+  | ipv4 (ipv4 : Net.IPv4Addr)
+
+  /--
+  An IPv6 address.
+  -/
+  | ipv6 (ipv6 : Net.IPv6Addr)
+deriving Inhabited, BEq
+
+instance : Repr Host where
+  reprPrec x prec :=
+    let nestPrec := (if prec ≥ 1024 then 1 else 2)
+    let name := "Std.Http.URI.Host"
+
+    let repr (ctr : String) a :=
+      Repr.addAppParen (Format.nest nestPrec (.text s!"{name}.{ctr}" ++ .line ++ a)).group prec
+
+    match x with
+    | Host.name a => repr "name" (reprArg a)
+    | Host.ipv4 a => repr "ipv4" (toString a)
+    | Host.ipv6 a => repr "ipv6" (toString a)
+
+instance : ToString Host where
+  toString
+    | .name n => n
+    | .ipv4 addr => toString addr
+    | .ipv6 addr => s!"[{toString addr}]"
+
+/--
+Authority port representation, preserving the distinction between:
+* no port separator (`example.com`)
+* empty port (`example.com:`)
+* numeric port (`example.com:443`)
+-/
+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.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2
+-/
+structure Authority where
+  /--
+  Optional user information (username and password).
+  -/
+  userInfo : Option UserInfo := none
+
+  /--
+  The host identifying the network location.
+  -/
+  host : Host
+
+  /--
+  Port component, preserving whether it is omitted (`example.com`),
+  explicitly empty (`example.com:`), or numeric (`example.com:443`).
+  -/
+  port : Port := .omitted
+deriving Inhabited, Repr, BEq
+
+instance : ToString Authority where
+  toString auth :=
+    let userPart := match auth.userInfo with
+      | none => ""
+      | some ⟨name, some pass⟩ => s!"{name}:{pass}@"
+      | some ⟨name, none⟩ => s!"{name}@"
+    let hostPart := toString auth.host
+    let portPart := match auth.port with
+      | .omitted => ""
+      | .empty => ":"
+      | .value p => s!":{p}"
+    s!"{userPart}{hostPart}{portPart}"
+
+/--
+Hierarchical path component of a URI. Each segment is stored as an `EncodedSegment` to maintain
+proper percent-encoding.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.3
+-/
+structure Path where
+  /--
+  The path segments making up the hierarchical structure (each segment is percent-encoded).
+  -/
+  segments : Array EncodedSegment
+
+  /--
+  Whether the path is absolute (begins with '/') or relative.
+  -/
+  absolute : Bool
+deriving Inhabited, Repr, BEq
+
+instance : ToString Path where
+  toString path :=
+    let result := String.intercalate "/" (path.segments.map toString).toList
+    if path.absolute then "/" ++ result else result
+
+namespace Path
+
+/--
+Returns true if the path has no segments.
+-/
+def isEmpty (p : Path) : Bool := p.segments.isEmpty
+
+/--
+Returns the parent path by removing the last segment. If the path is empty, returns the path unchanged.
+-/
+def parent (p : Path) : Path :=
+  if p.segments.isEmpty then p
+  else { p with segments := p.segments.pop }
+
+/--
+Joins two paths. If the second path is absolute, it is returned as-is. Otherwise, the second path's
+segments are appended to the first path.
+-/
+def join (p1 : Path) (p2 : Path) : Path :=
+  if p2.absolute then p2
+  else { p1 with segments := p1.segments ++ p2.segments }
+
+/--
+Appends a single segment to the path. The segment will be percent-encoded.
+-/
+def append (p : Path) (segment : String) : Path :=
+  { p with segments := p.segments.push (EncodedSegment.encode segment) }
+
+/--
+Appends an already-encoded segment to the path.
+-/
+def appendEncoded (p : Path) (segment : EncodedSegment) : Path :=
+  { p with segments := p.segments.push segment }
+
+/--
+Removes dot segments from the path according to RFC 3986 Section 5.2.4. This handles "."
+(current directory) and ".." (parent directory) segments.
+-/
+def normalize (p : Path) : Path :=
+  let rec loop (input : List (EncodedSegment)) (output : List (EncodedSegment)) : List (EncodedSegment) :=
+    match input with
+    | [] =>
+      output.reverse
+    | segStr :: rest =>
+      if toString segStr == "." then
+        loop rest output
+      else if toString segStr == ".." then
+        match output with
+        | [] => loop rest []
+        | _ :: tail => loop rest tail
+      else
+        loop rest (segStr :: output)
+
+  { p with segments := (loop p.segments.toList []).toArray }
+
+/--
+Returns the path segments as decoded strings.
+Segments that cannot be decoded as UTF-8 are returned as their raw encoded form.
+-/
+def toDecodedSegments (p : Path) : Array String :=
+  p.segments.map fun seg =>
+    seg.decode.getD (toString seg)
+
+end Path
+
+/--
+Query string represented as an array of key-value pairs. Both keys and values are stored as
+`EncodedQueryParam` for proper application/x-www-form-urlencoded encoding. Values are optional to
+support parameters without values (e.g., "?flag"). Order is preserved based on insertion order.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.4
+-/
+@[expose]
+def Query := Array (EncodedQueryParam × Option EncodedQueryParam)
+deriving Repr, Inhabited, BEq
+
+namespace Query
+
+/--
+Extracts all unique query parameter names.
+-/
+@[expose]
+def names (query : Query) : Array EncodedQueryParam :=
+  query.map (fun p => p.fst)
+  |> Array.toList
+  |> List.eraseDups
+  |> List.toArray
+
+/--
+Extracts all query parameter values.
+-/
+@[expose]
+def values (query : Query) : Array (Option EncodedQueryParam) :=
+  query.map (fun p => p.snd)
+
+/--
+Returns the query as an array of (key, value) pairs. This is an identity function since Query is
+already an array of pairs.
+-/
+@[expose]
+def toArray (query : Query) : Array (EncodedQueryParam × Option EncodedQueryParam) :=
+  query
+
+/--
+Formats a query parameter as a string in the format "key" or "key=value". The key and value are
+already percent-encoded as `EncodedQueryParam`.
+-/
+def formatQueryParam (key : EncodedQueryParam) (value : Option EncodedQueryParam) : String :=
+  match value with
+  | none => toString key
+  | some v => s!"{toString key}={toString v}"
+
+/--
+Finds the first value of a query parameter by key name. Returns `none` if the key is not found.
+The value remains encoded as `EncodedQueryParam`.
+-/
+def findEncoded? (query : Query) (key : EncodedQueryParam) : Option (Option EncodedQueryParam) :=
+  let matchingKey := Array.find? (fun x => x.fst.toByteArray = key.toByteArray) query
+  matchingKey.map (fun x => x.snd)
+
+/--
+Finds the first value of a query parameter by raw key string. The key is percent-encoded before
+matching. This avoids aliasing between raw and pre-encoded spellings.
+-/
+def find? (query : Query) (key : String) : Option (Option EncodedQueryParam) :=
+  query.findEncoded? (EncodedQueryParam.encode key)
+
+/--
+Finds all values of a query parameter by key name. Returns an empty array if the key is not found.
+The values remain encoded as `EncodedQueryParam`.
+-/
+def findAllEncoded (query : Query) (key : EncodedQueryParam) : Array (Option EncodedQueryParam) :=
+  query.filterMap (fun x =>
+    if x.fst.toByteArray = key.toByteArray then
+      some x.snd
+    else
+      none)
+
+/--
+Finds all values of a query parameter by raw key string. The key is percent-encoded before matching.
+-/
+def findAll (query : Query) (key : String) : Array (Option EncodedQueryParam) :=
+  query.findAllEncoded (EncodedQueryParam.encode key)
+
+/--
+Adds a query parameter to the query string.
+-/
+def insert (query : Query) (key : String) (value : String) : Query :=
+  let encodedKey : EncodedQueryParam := EncodedQueryParam.encode key
+  let encodedValue : EncodedQueryParam := EncodedQueryParam.encode value
+  query.push (encodedKey, some encodedValue)
+
+/--
+Adds an already-encoded key-value pair to the query string.
+-/
+def insertEncoded (query : Query) (key : EncodedQueryParam) (value : Option EncodedQueryParam) : Query :=
+  query.push (key, value)
+
+/--
+Creates an empty query string.
+-/
+def empty : Query := #[]
+
+/--
+Creates a query string from a list of key-value pairs.
+-/
+def ofList (pairs : List (EncodedQueryParam × Option EncodedQueryParam)) : Query :=
+  pairs.toArray
+
+/--
+Checks if a query parameter exists.
+-/
+def containsEncoded (query : Query) (key : EncodedQueryParam) : Bool :=
+  query.any (fun x => x.fst.toByteArray = key.toByteArray)
+
+/--
+Checks if a query parameter exists by raw key string. The key is percent-encoded before matching.
+-/
+def contains (query : Query) (key : String) : Bool :=
+  query.containsEncoded (EncodedQueryParam.encode key)
+
+/--
+Removes all occurrences of a query parameter by key name.
+-/
+def eraseEncoded (query : Query) (key : EncodedQueryParam) : Query :=
+  query.filter (fun x =>
+    x.fst.toByteArray ≠ key.toByteArray
+  )
+
+/--
+Removes all occurrences of a query parameter by raw key string. The key is percent-encoded before matching.
+-/
+def erase (query : Query) (key : String) : Query :=
+  query.eraseEncoded (EncodedQueryParam.encode key)
+
+/--
+Gets the first value of a query parameter by key name, decoded as a string.
+Returns `none` if the key is not found or if the value cannot be decoded as UTF-8.
+-/
+def get (query : Query) (key : String) : Option String :=
+  match query.find? key with
+  | none => none
+  | some none => some ""  -- Key exists but has no value
+  | some (some encoded) => encoded.decode
+
+/--
+Gets the first value of a query parameter by key name, decoded as a string.
+Returns the default value if the key is not found or if the value cannot be decoded.
+-/
+def getD (query : Query) (key : String) (default : String) : String :=
+  query.get key |>.getD default
+
+/--
+Sets a query parameter, replacing all existing values for that key.
+Both key and value will be automatically percent-encoded.
+-/
+def set (query : Query) (key : String) (value : String) : Query :=
+  query.erase key |>.insert key value
+
+/--
+Converts the query to a properly encoded query string format.
+Example: "key1=value1&key2=value2&flag"
+-/
+def toRawString (query : Query) : String :=
+  let params := query.map (fun (k, v) => formatQueryParam k v)
+  String.intercalate "&" params.toList
+
+instance : EmptyCollection Query :=
+  ⟨Query.empty⟩
+
+instance : Singleton (String × String) Query :=
+  ⟨fun ⟨k, v⟩ => Query.empty.insert k v⟩
+
+instance : Insert (String × String) Query :=
+  ⟨fun ⟨k, v⟩ q => q.insert k v⟩
+
+instance : ToString Query where
+  toString q :=
+    if q.isEmpty then "" else
+      let encodedParams := q.toList.map fun (key, value) =>
+        Query.formatQueryParam key value
+      "?" ++ String.intercalate "&" encodedParams
+
+end Query
+
+end URI
+
+/--
+Complete URI structure following RFC 3986. All text components use encoded string types to ensure
+proper percent-encoding.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html
+-/
+structure URI where
+  /--
+  The URI scheme (e.g., "http", "https", "ftp").
+  -/
+  scheme : URI.Scheme
+
+  /--
+  Optional authority component (user info, host, and port).
+  -/
+  authority : Option URI.Authority
+
+  /--
+  The hierarchical path component.
+  -/
+  path : URI.Path
+
+  /--
+  Optional query string as key-value pairs.
+  -/
+  query : URI.Query
+
+  /--
+  Optional fragment identifier (the part after '#'), percent-encoded.
+  -/
+  fragment : Option String
+deriving Repr, Inhabited, BEq
+
+instance : ToString URI where
+  toString uri :=
+    let schemePart := uri.scheme
+    let authorityPart := match uri.authority with
+      | none => ""
+      | some auth => s!"//{toString auth}"
+    let pathPart := toString uri.path
+    let queryPart := toString uri.query
+    let fragmentPart := uri.fragment.map (fun f => "#" ++ toString (URI.EncodedFragment.encode f)) |>.getD ""
+    s!"{schemePart}:{authorityPart}{pathPart}{queryPart}{fragmentPart}"
+
+namespace URI
+
+/--
+Fluent builder for constructing URIs. Takes raw (unencoded) strings and handles encoding
+automatically when building the final URI.
+-/
+structure Builder where
+  /--
+  The URI scheme (e.g., "http", "https").
+  -/
+  scheme : Option URI.Scheme := none
+
+  /--
+  User information (username and optional password).
+  -/
+  userInfo : Option UserInfo := none
+
+  /--
+  The host component.
+  -/
+  host : Option Host := none
+
+  /--
+  The port number.
+  -/
+  port : URI.Port := .omitted
+
+  /--
+  Path segments (will be encoded when building).
+  -/
+  pathSegments : Array String := #[]
+
+  /--
+  Query parameters as (key, optional value) pairs (will be encoded when building).
+  -/
+  query : Array (String × Option String) := #[]
+
+  /--
+  Fragment identifier (will be encoded when building).
+  -/
+  fragment : Option String := none
+deriving Inhabited
+
+namespace Builder
+
+/--
+Creates an empty URI builder.
+-/
+def empty : Builder := {}
+
+/--
+Attempts to set the URI scheme (e.g., "http", "https").
+Returns `none` if the scheme is not a valid RFC 3986 scheme.
+The stored scheme is normalized to lowercase.
+-/
+def setScheme? (b : Builder) (scheme : String) : Option Builder :=
+  URI.Scheme.ofString? scheme |>.map (fun scheme => { b with scheme := some scheme })
+
+/--
+Sets the URI scheme (e.g., "http", "https"). Panics if the scheme is invalid.
+Use `setScheme?` if you need a safe option-returning version.
+-/
+def setScheme! (b : Builder) (scheme : String) : Builder :=
+  match b.setScheme? scheme with
+  | some b => b
+  | none   => panic! s!"invalid URI scheme: {scheme.quote}"
+
+/--
+Sets the user information with username and optional password.
+The strings will be automatically percent-encoded.
+-/
+def setUserInfo (b : Builder) (username : String) (password : Option String := none) : Builder :=
+  { b with userInfo := some (UserInfo.ofStrings username password) }
+
+/--
+Sets the host as a domain name, returning `none` if the name contains invalid characters.
+The domain name will be automatically lowercased.
+Only ASCII alphanumeric characters, hyphens, and dots are allowed.
+Each label cannot start or end with `-` and is limited to 63 characters.
+Internationalized domain names must be converted to punycode before use.
+-/
+def setHost? (b : Builder) (name : String) : Option Builder :=
+  URI.DomainName.ofString? name |>.map (fun name => { b with host := some (Host.name name) })
+
+/--
+Sets the host as a domain name, panicking if the name contains invalid characters.
+The domain name will be automatically lowercased.
+Only ASCII alphanumeric characters, hyphens, and dots are allowed.
+Each label cannot start or end with `-` and is limited to 63 characters.
+Internationalized domain names must be converted to punycode before use.
+-/
+def setHost! (b : Builder) (name : String) : Builder :=
+  match b.setHost? name with
+  | some b => b
+  | none   => panic! s!"invalid domain name: {name.quote}"
+
+/--
+Sets the host as an IPv4 address.
+-/
+def setHostIPv4 (b : Builder) (addr : Net.IPv4Addr) : Builder :=
+  { b with host := some (Host.ipv4 addr) }
+
+/--
+Sets the host as an IPv6 address.
+-/
+def setHostIPv6 (b : Builder) (addr : Net.IPv6Addr) : Builder :=
+  { b with host := some (Host.ipv6 addr) }
+
+/--
+Sets the port number.
+-/
+def setPort (b : Builder) (port : UInt16) : Builder :=
+  { b with port := .value port }
+
+/--
+Replaces all path segments. Segments will be automatically percent-encoded when building.
+-/
+def setPath (b : Builder) (segments : Array String) : Builder :=
+  { b with pathSegments := segments }
+
+/--
+Appends a single segment to the path. The segment will be automatically percent-encoded when building.
+-/
+def appendPathSegment (b : Builder) (segment : String) : Builder :=
+  { b with pathSegments := b.pathSegments.push segment }
+
+/--
+Adds a query parameter with a value. Both key and value will be automatically percent-encoded when
+building.
+-/
+def addQueryParam (b : Builder) (key : String) (value : String) : Builder :=
+  { b with query := b.query.push (key, some value) }
+
+/--
+Adds a query parameter without a value (flag parameter). The key will be automatically
+percent-encoded when building.
+-/
+def addQueryFlag (b : Builder) (key : String) : Builder :=
+  { b with query := b.query.push (key, none) }
+
+/--
+Replaces all query parameters. Keys and values will be automatically percent-encoded when building.
+-/
+def setQuery (b : Builder) (query : Array (String × Option String)) : Builder :=
+  { b with query := query }
+
+/--
+Sets the fragment identifier. The fragment will be automatically percent-encoded when building.
+-/
+def setFragment (b : Builder) (fragment : String) : Builder :=
+  { b with fragment := some fragment }
+
+/--
+Builds a complete URI from the builder state, encoding all components. Defaults to "https" scheme if
+none is specified.
+-/
+def build (b : Builder) : URI :=
+  let scheme := (b.scheme.getD ⟨"https", by decide⟩)
+
+  let authority :=
+    if b.host.isSome then
+      some {
+        userInfo := b.userInfo
+        host := b.host.getD default
+        port := b.port
+      }
+    else none
+
+  let path : Path := {
+    segments := b.pathSegments.map EncodedSegment.encode
+    absolute := true
+  }
+
+  let query :=
+    b.query.map fun (k, v) =>
+      (EncodedQueryParam.encode k, v.map EncodedQueryParam.encode)
+
+  let query := URI.Query.ofList query.toList
+
+  {
+    scheme
+    authority := authority
+    path
+    query := query
+    fragment := b.fragment
+  }
+
+end Builder
+
+/--
+Returns a new URI with the scheme replaced.
+-/
+def withScheme! (uri : URI) (scheme : String) : URI :=
+  { uri with scheme := URI.Scheme.ofString! scheme }
+
+/--
+Returns a new URI with the authority replaced.
+-/
+def withAuthority (uri : URI) (authority : Option URI.Authority) : URI :=
+  { uri with authority }
+
+/--
+Returns a new URI with the path replaced.
+-/
+def withPath (uri : URI) (path : URI.Path) : URI :=
+  { uri with path }
+
+/--
+Returns a new URI with the query replaced.
+-/
+def withQuery (uri : URI) (query : URI.Query) : URI :=
+  { uri with query }
+
+/--
+Returns a new URI with the fragment replaced.
+-/
+def withFragment (uri : URI) (fragment : Option String) : URI :=
+  { uri with fragment }
+
+/--
+Partially normalizes a URI by removing dot-segments from the path (`.` and `..`)
+according to RFC 3986 Section 5.2.4.
+
+This does not apply the full normalization set from RFC 3986 Section 6 — for example,
+case normalization, percent-encoding normalization, and default-port normalization are
+not performed.
+-/
+def normalize (uri : URI) : URI :=
+  { uri with path := uri.path.normalize }
+
+end URI
+
+/--
+HTTP request target forms as defined in RFC 9112 Section 3.3.
+
+Reference: https://www.rfc-editor.org/rfc/rfc9112.html#section-3.3
+-/
+inductive RequestTarget where
+  /--
+  Origin-form request target (most common for HTTP requests). Consists of a path and an optional query string.
+  Example: `/path/to/resource?key=value`
+  -/
+  | originForm (path : URI.Path) (query : Option URI.Query)
+
+  /--
+  Absolute-form request target containing a complete URI. Used when making requests through a proxy.
+  Example: `http://example.com:8080/path?key=value`
+  -/
+  | absoluteForm (uri : URI)
+
+  /--
+  Authority-form request target (used for CONNECT requests).
+  Example: `example.com:443`
+  -/
+  | authorityForm (authority : URI.Authority)
+
+  /--
+  Asterisk-form request target (used with OPTIONS requests).
+  Example: `*`
+  -/
+  | asteriskForm
+deriving Inhabited, Repr
+
+namespace RequestTarget
+
+/--
+Extracts the path component from a request target, if available.
+Returns an empty relative path for targets without a path.
+-/
+def path : RequestTarget → URI.Path
+  | .originForm p _ => p
+  | .absoluteForm uri => uri.path
+  | _ => { segments := #[], absolute := false }
+
+/--
+Extracts the query component from a request target, if available.
+Returns an empty array for targets without a query.
+-/
+def query : RequestTarget → URI.Query
+  | .originForm _ q => q.getD URI.Query.empty
+  | .absoluteForm uri => uri.query
+  | _ => URI.Query.empty
+
+/--
+Extracts the authority component from a request target, if available.
+-/
+def authority? : RequestTarget → Option URI.Authority
+  | .authorityForm a => some a
+  | .absoluteForm uri => uri.authority
+  | _ => none
+
+instance : ToString RequestTarget where
+  toString
+    | .originForm path query =>
+        let pathStr := toString path
+        let queryStr := query.map toString |>.getD ""
+        s!"{pathStr}{queryStr}"
+    | .absoluteForm uri => toString uri
+    | .authorityForm auth => toString auth
+    | .asteriskForm => "*"
+
+instance : Encode .v11 RequestTarget where
+  encode buffer target := buffer.writeString (toString target)
+
+end Std.Http.RequestTarget

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

@@ -0,0 +1,80 @@
+/-
+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.Nat
+
+public section
+
+/-!
+# URI Parser Configuration
+
+This module defines `URI.Config`, which controls per-component size limits used during URI
+parsing. All limits default to the values previously hardcoded in the parser, except
+`maxQueryLength`, which is raised from 1024 to 8192 to match `H1.Config.maxUriLength` and
+accommodate real-world query strings.
+-/
+
+namespace Std.Http.URI
+
+set_option linter.all true
+
+/--
+Per-component size limits for the URI parser.
+-/
+structure Config where
+  /--
+  Maximum length of the URI scheme component (e.g. `https`), in bytes.
+  The scheme grammar requires at least one leading ALPHA; the remaining budget is
+  `max(0, maxSchemeLength - 1)` additional characters.
+  -/
+  maxSchemeLength : Nat := 13
+
+  /--
+  Maximum length of the host `reg-name` component, in bytes.
+  -/
+  maxHostLength : Nat := 253
+
+  /--
+  Maximum length of the userinfo component (username and password each), in bytes.
+  -/
+  maxUserInfoLength : Nat := 1024
+
+  /--
+  Maximum length of a single path segment, in bytes.
+  -/
+  maxSegmentLength : Nat := 256
+
+  /--
+  Maximum length of the query string, in bytes.
+  Raised from the previously hardcoded 1024 to 8192 to match `H1.Config.maxUriLength`
+  and allow real-world query strings.
+  -/
+  maxQueryLength : Nat := 8192
+
+  /--
+  Maximum length of the fragment component, in bytes.
+  -/
+  maxFragmentLength : Nat := 1024
+
+  /--
+  Maximum number of path segments.
+  Prevents excessive segment counts that could arise from paths like `/a/b/c/…` repeated many times.
+  -/
+  maxPathSegments : Nat := 128
+
+  /--
+  Maximum total byte length of the path (all segments combined, including separating slashes).
+  -/
+  maxTotalPathLength : Nat := 8192
+
+  /--
+  Maximum number of query parameters (key-value pairs separated by `&`).
+  -/
+  maxQueryParams : Nat := 100
+
+end Std.Http.URI

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

@@ -0,0 +1,688 @@
+/-
+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.While
+import Init.Data.SInt.Lemmas
+import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Bitwise
+import Init.Data.Array.Lemmas
+public import Init.Data.String
+public import Std.Internal.Http.Internal.Char
+
+public section
+
+/-!
+# URI Encoding
+
+This module provides utilities for percent-encoding URI components according to RFC 3986. It includes
+character validation, encoding/decoding functions, and types that maintain encoding invariants through
+Lean's dependent type system.
+
+Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-2.1
+-/
+
+namespace Std.Http.URI
+
+set_option linter.all true
+
+open Internal Char
+
+/--
+Checks if a byte is a valid character in a percent-encoded URI component. Valid characters are
+unreserved characters or the percent sign (for escape sequences).
+-/
+def isEncodedChar (rule : UInt8 → Bool) (c : UInt8) : Bool :=
+  isAsciiByte c ∧ (rule c ∨ isHexDigitByte c ∨ c = '%'.toUInt8)
+
+/--
+Checks if a byte is valid in a percent-encoded query string component. Extends `isEncodedChar` to also
+allow '+' which represents space in application/x-www-form-urlencoded format.
+-/
+def isEncodedQueryChar (rule : UInt8 → Bool) (c : UInt8) : Bool :=
+  isEncodedChar rule c ∨ c = '+'.toUInt8
+
+/--
+Checks if all characters in a `ByteArray` are allowed in an encoded URI component. This is a fast check
+that only verifies the character set, not full encoding validity.
+-/
+@[inline]
+abbrev IsAllowedEncodedChars (rule : UInt8 → Bool) (s : ByteArray) : Prop :=
+  s.data.all (isEncodedChar rule)
+
+instance : Decidable (IsAllowedEncodedChars r s) :=
+  inferInstanceAs (Decidable (s.data.all (isEncodedChar r) = true))
+
+/--
+Checks if all characters in a `ByteArray` are allowed in an encoded query parameter. Allows '+' as an
+alternative encoding for space (application/x-www-form-urlencoded).
+-/
+@[inline]
+abbrev IsAllowedEncodedQueryChars (rule : UInt8 → Bool) (s : ByteArray) : Prop :=
+  s.data.all (isEncodedQueryChar rule)
+
+instance : Decidable (IsAllowedEncodedQueryChars r s) :=
+  inferInstanceAs (Decidable (s.data.all (isEncodedQueryChar r) = true))
+
+/--
+Validates that all percent signs in a byte array are followed by exactly two hexadecimal digits.
+This ensures proper percent-encoding according to RFC 3986.
+
+For example:
+- `%20` is valid (percent followed by two hex digits)
+- `%` is invalid (percent with no following digits)
+- `%2` is invalid (percent followed by only one digit)
+- `%GG` is invalid (percent followed by non-hex characters)
+-/
+def isValidPercentEncoding (ba : ByteArray) : Bool :=
+  let rec loop (i : Nat) : Bool :=
+    if h : i < ba.size then
+      let c := ba[i]'h
+      if c = '%'.toUInt8 then
+          if h₂ : i + 2 < ba.size then
+            let d1 := ba[i + 1]'(by omega)
+            let d2 := ba[i + 2]'h₂
+            if isHexDigitByte d1 && isHexDigitByte d2 then
+              loop (i + 3)
+          else false
+        else false
+      else loop (i + 1)
+    else true
+  termination_by ba.size - i
+  loop 0
+
+/--
+Converts a nibble (4-bit value, 0-15) to its hexadecimal digit representation. Returns '0'-'9' for
+values 0-9, and 'A'-'F' for values 10-15.
+-/
+def hexDigit (n : UInt8) : UInt8 :=
+  if n < 10 then (n + '0'.toUInt8)
+  else (n - 10 + 'A'.toUInt8)
+
+/--
+Converts a hexadecimal digit character to its numeric value (0-15).
+Returns `none` if the character is not a valid hex digit.
+-/
+def hexDigitToUInt8? (c : UInt8) : Option UInt8 :=
+  if c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8 then
+    some (c - '0'.toUInt8)
+  else if c ≥ 'a'.toUInt8 && c ≤ 'f'.toUInt8 then
+    some (c - 'a'.toUInt8 + 10)
+  else if c ≥ 'A'.toUInt8 && c ≤ 'F'.toUInt8 then
+    some (c - 'A'.toUInt8 + 10)
+  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 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 *
+  exact h.left
+
+private theorem isEncodedQueryChar_isAscii (c : UInt8) (h : isEncodedQueryChar r c) : isAsciiByte c := by
+  unfold isEncodedQueryChar isAsciiByte at *
+  simp at h
+  rcases h
+  next h => exact isEncodedChar_isAscii c h
+  next h => subst_vars; decide
+
+private theorem hexDigit_isHexDigit (h₀ : x < 16) : isHexDigitByte (hexDigit x) := by
+  unfold hexDigit isHexDigitByte
+  have h₁ : x.toNat < 16 := h₀
+  split <;> simp
+
+  next p =>
+    have h₂ : x.toNat < 10 := p
+    have h₂ : 48 ≤ x.toNat + 48 := by omega
+    have h₃ : x.toNat + 48 ≤ 57 := by omega
+    have h₄ : x.toNat + 48 < 256 := by omega
+
+    refine Or.inl (Or.inl ⟨?_, ?_⟩)
+    · exact (UInt8.ofNat_le_iff_le (by decide) h₄ |>.mpr h₂)
+    · exact (UInt8.ofNat_le_iff_le h₄ (by decide) |>.mpr h₃)
+
+  next p =>
+    have h₂ : ¬(x.toNat < 10) := p
+    have h₃ : 65 ≤ x.toNat - 10 + 65 := by omega
+    have h₅ : x.toNat - 10 + 65 ≤ 70 := by omega
+    have h₄ : x.toNat - 10 + 65 < 256 := by omega
+
+    refine Or.inr ⟨?_, ?_⟩
+    · simpa [UInt8.ofNat_sub (by omega : 10 ≤ x.toNat)] using
+        UInt8.ofNat_le_iff_le (by decide : 65 < 256) h₄ |>.mpr h₃
+    · simpa [UInt8.ofNat_add, UInt8.ofNat_sub (by omega : 10 ≤ x.toNat)] using
+        UInt8.ofNat_le_iff_le h₄ (by decide : 70 < 256) |>.mpr h₅
+
+private theorem isHexDigit_isAscii {c : UInt8} (h : isHexDigitByte c) : isAsciiByte c := by
+  simp [isHexDigitByte, isAsciiByte] at *
+  rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩
+  · exact UInt8.lt_of_le_of_lt h2 (by decide)
+  next h => exact UInt8.lt_of_le_of_lt h.right (by decide)
+  · exact UInt8.lt_of_le_of_lt h2 (by decide)
+
+private theorem isHexDigit_isEncodedChar {c : UInt8} (h : isHexDigitByte c) : isEncodedChar r c := by
+  unfold isEncodedChar
+  simp at *
+  exact And.intro (isHexDigit_isAscii h) (Or.inr (Or.inl h))
+
+private theorem isHexDigit_isEncodedQueryChar {c : UInt8} (h : isHexDigitByte c) : isEncodedQueryChar r c := by
+  unfold isEncodedQueryChar isEncodedChar
+  simp at *
+  exact Or.inl (And.intro (isHexDigit_isAscii h) (Or.inr (Or.inl h)))
+
+theorem all_of_all_of_imp {b : ByteArray} (h : b.data.all p) (imp : ∀ c, p c → q c) : b.data.all q := by
+  rw [Array.all_eq] at *
+  simp at *
+  intro i x
+  exact (imp b.data[i]) (h i x)
+
+private theorem autf8EncodeChar_flatMap_ascii {a : List UInt8}
+    (is_ascii_list : ∀ (x : UInt8), x ∈ a → x < 128) :
+    List.flatMap (fun a => String.utf8EncodeChar (Char.ofUInt8 a)) a = a := by
+  have h_encode {i : UInt8} (h : i < 128) : String.utf8EncodeChar (Char.ofUInt8 i) = [i] := by
+    simp [Char.ofUInt8, String.utf8EncodeChar, show ¬127 < i.toNat from Nat.not_lt_of_le (Nat.le_pred_of_lt h)]
+  induction a with
+  | nil => simp
+  | cons head tail ih =>
+    simp [List.flatMap_cons]
+    rw [h_encode]
+    · simp
+      rw [ih]
+      intro x hx
+      exact is_ascii_list x (by simp [hx])
+    · exact is_ascii_list head (by simp)
+
+private theorem List.toByteArray_loop_eq (xs : List UInt8) (acc : ByteArray) :
+    (List.toByteArray.loop xs acc).data = acc.data ++ xs.toArray := by
+  induction xs generalizing acc with
+  | nil => simp [List.toByteArray.loop]
+  | cons x xs ih => simp [List.toByteArray.loop, ih, Array.push]
+
+private theorem ByteArray.toList_toByteArray (ba : ByteArray) :
+    ba.data.toList.toByteArray = ba := by
+  cases ba with
+  | mk data =>
+    simp [List.toByteArray]
+    apply ByteArray.ext
+    simp [List.toByteArray_loop_eq, ByteArray.empty]
+    decide
+
+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]
+  have is_ascii : ∀ (x : UInt8), x ∈ ba.data.toList → x < 128 := by
+    let is_ascii := Array.all_eq_true_iff_forall_mem.mp s
+    simp [isAsciiByte] at is_ascii
+    intro x hx
+    exact is_ascii x (by simp_all)
+  rw [autf8EncodeChar_flatMap_ascii is_ascii]
+  exact ByteArray.toList_toByteArray ba |>.symm
+
+/--
+A percent-encoded URI component with a compile-time proof that it contains only valid encoded characters.
+This provides type-safe URI encoding without runtime validation.
+
+The invariant guarantees that the string contains only unreserved characters (alphanumeric, hyphen, period,
+underscore, tilde) and percent signs (for escape sequences).
+-/
+structure EncodedString (r : UInt8 → Bool) where
+  private mk ::
+
+  /--
+  The underlying byte array containing the percent-encoded data.
+  -/
+  toByteArray : ByteArray
+
+  /--
+  Proof that all characters in the byte array are valid encoded characters.
+  -/
+  valid : IsAllowedEncodedChars r toByteArray
+
+namespace EncodedString
+
+/--
+Creates an empty encoded string.
+-/
+def empty : EncodedString r :=
+  ⟨.empty, by simp []; exact fun i h => by contradiction⟩
+
+instance : Inhabited (EncodedString r) where
+  default := EncodedString.empty
+
+/--
+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⟩
+
+/--
+Converts a byte to its percent-encoded hexadecimal representation (%XX). For example, a space
+character (0x20) becomes "%20".
+-/
+private def byteToHex (b : UInt8) (s : EncodedString r) : EncodedString r :=
+  let ba := s.toByteArray.push '%'.toUInt8
+    |>.push (hexDigit (b >>> 4))
+    |>.push (hexDigit (b &&& 0xF))
+  let valid := by
+    have h1 : isEncodedChar r '%'.toUInt8 :=
+      by simp [isEncodedChar]; decide
+
+    have h2 : isEncodedChar r (hexDigit (b >>> 4)) :=
+      let h₀ := hexDigit_isHexDigit (BitVec.toNat_ushiftRight_lt b.toBitVec 4 (by decide))
+      isHexDigit_isEncodedChar h₀
+
+    have h3 : isEncodedChar r (hexDigit (b &&& 0xF)) :=
+      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
+  ⟨ba, valid⟩
+
+/--
+Encodes a raw string into an `EncodedString` with automatic proof construction. Unreserved characters
+(alphanumeric, hyphen, period, underscore, tilde) are kept as-is, while all other characters are percent-encoded.
+-/
+def encode (s : String) : EncodedString r :=
+  s.toUTF8.foldl (init := EncodedString.empty) fun acc c =>
+    if h : isAsciiByte c ∧ r c then
+      acc.push c (by simp [isEncodedChar]; exact And.intro h.left (Or.inl h.right))
+    else
+      byteToHex c acc
+
+/--
+Attempts to create an `EncodedString` from a `ByteArray`. Returns `some` if the byte array contains only
+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 isValidPercentEncoding ba then some ⟨ba, h⟩ else none
+  else none
+
+/--
+Creates an `EncodedString` from a `ByteArray`, panicking if the byte array is invalid.
+-/
+def ofByteArray! (ba : ByteArray) : EncodedString r :=
+  match ofByteArray? ba with
+  | some es => es
+  | none => panic! "invalid encoded string"
+
+/--
+Creates an `EncodedString` from a `String` by checking if it's already a valid percent-encoded string.
+Returns `some` if valid, `none` otherwise.
+-/
+def ofString? (s : String) : Option (EncodedString r) :=
+  ofByteArray? s.toUTF8
+
+/--
+Creates an `EncodedString` from a `String`, panicking if the string is not a valid percent-encoded string.
+-/
+def ofString! (s : String) : EncodedString r :=
+  ofByteArray! s.toUTF8
+
+/--
+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 :=
+  ⟨ba, valid⟩
+
+instance : ToString (EncodedString r) where
+  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")
+back to their original characters. Returns `none` if the decoded bytes are not valid UTF-8.
+-/
+def decode (es : EncodedString r) : Option String := Id.run do
+  let mut decoded : ByteArray := ByteArray.empty
+  let rawBytes := es.toByteArray
+  let len := rawBytes.size
+  let mut i := 0
+  let percent := '%'.toNat.toUInt8
+  while h : i < len do
+    let c := rawBytes[i]
+    (decoded, i) := if h₁ : c == percent ∧ i + 1 < len then
+      let h1 := rawBytes[i + 1]
+      if let some hd1 := hexDigitToUInt8? h1 then
+        if h₂ : i + 2 < len then
+          let h2 := rawBytes[i + 2]
+          if let some hd2 := hexDigitToUInt8? h2 then
+            (decoded.push (hd1 * 16 + hd2), i + 3)
+          else
+            (((decoded.push c).push h1).push h2, i + 3)
+        else
+          ((decoded.push c).push h1, i + 2)
+      else
+        ((decoded.push c).push h1, i + 2)
+    else
+      (decoded.push c, i + 1)
+  return String.fromUTF8? decoded
+
+instance : Repr (EncodedString r) where
+  reprPrec es n := reprPrec (toString es) n
+
+instance : BEq (EncodedString r) where
+  beq x y := x.toByteArray = y.toByteArray
+
+instance : Hashable (EncodedString r) where
+  hash x := Hashable.hash x.toByteArray
+
+end EncodedString
+
+/--
+A percent-encoded query string component with a compile-time proof that it contains only valid encoded
+query characters. Extends `EncodedString` to support the '+' character for spaces, following the
+application/x-www-form-urlencoded format.
+
+This type is specifically designed for encoding query parameters where spaces can be represented as '+'
+instead of "%20".
+-/
+structure EncodedQueryString (r : UInt8 → Bool) where
+  private mk ::
+
+  /--
+  The underlying byte array containing the percent-encoded query data.
+  -/
+  toByteArray : ByteArray
+
+  /--
+  Proof that all characters in the byte array are valid encoded query characters.
+  -/
+  valid : IsAllowedEncodedQueryChars r toByteArray
+
+namespace EncodedQueryString
+
+/--
+Creates an empty encoded query string.
+-/
+def empty : EncodedQueryString r :=
+  ⟨.empty, by simp; intro a h; contradiction⟩
+
+instance : Inhabited (EncodedQueryString r) where
+  default := EncodedQueryString.empty
+
+/--
+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⟩
+
+/--
+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 isValidPercentEncoding ba then some ⟨ba, h⟩ else none
+  else none
+
+/--
+Creates an `EncodedQueryString` from a `ByteArray`, panicking if the byte array is invalid.
+-/
+def ofByteArray! (ba : ByteArray) (r : UInt8 → Bool := isQueryChar) : EncodedQueryString r :=
+  match ofByteArray? ba r with
+  | some es => es
+  | none => panic! "invalid encoded query string"
+
+/--
+Creates an `EncodedQueryString` from a `String` by checking if it's already a valid percent-encoded string.
+Returns `some` if valid, `none` otherwise.
+-/
+def ofString? (s : String) (r : UInt8 → Bool := isQueryChar) : Option (EncodedQueryString r) :=
+  ofByteArray? s.toUTF8 r
+
+/--
+Creates an `EncodedQueryString` from a `String`, panicking if the string is not a valid percent-encoded string.
+-/
+def ofString! (s : String) (r : UInt8 → Bool := isQueryChar) : EncodedQueryString r :=
+  ofByteArray! s.toUTF8 r
+
+/--
+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 :=
+  ⟨ba, valid⟩
+
+/--
+Converts a byte to its percent-encoded hexadecimal representation (%XX). For example, a space character
+(0x20) becomes "%20".
+-/
+private def byteToHex (b : UInt8) (s : EncodedQueryString r) : EncodedQueryString r :=
+  let ba := s.toByteArray.push '%'.toUInt8
+    |>.push (hexDigit (b >>> 4))
+    |>.push (hexDigit (b &&& 0xF))
+  let valid := by
+    have h1 : isEncodedQueryChar r '%'.toUInt8 := by
+      simp [isEncodedQueryChar, isEncodedChar]; decide
+    have h2 : isEncodedQueryChar r (hexDigit (b >>> 4)) :=
+      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
+  ⟨ba, valid⟩
+
+/--
+Encodes a raw string into an `EncodedQueryString` with automatic proof construction. Unreserved characters
+are kept as-is, spaces are encoded as '+', and all other characters are percent-encoded.
+-/
+def encode (s : String) (r : UInt8 → Bool := isQueryChar) : EncodedQueryString r :=
+  s.toUTF8.foldl (init := EncodedQueryString.empty) fun acc c =>
+    if h : isAsciiByte c ∧ r c then
+      acc.push c (by simp [isEncodedQueryChar, isEncodedChar]; exact Or.inl (And.intro h.left (Or.inl h.right)))
+    else if _ : c = ' '.toUInt8 then
+      acc.push '+'.toUInt8 (by simp [isEncodedQueryChar])
+    else
+      byteToHex c acc
+
+/--
+Converts an `EncodedQueryString` to a `String`, given a proof that all characters satisfying `r` are ASCII.
+-/
+def toString (es : EncodedQueryString r) : String :=
+  ⟨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 '+'
+signs back to their original characters. Returns `none` if the decoded bytes are not valid UTF-8.
+
+This is almost the same code from `System.Uri.UriEscape.decodeUri`, but with `Option` instead.
+-/
+def decode (es : EncodedQueryString r) : Option String := Id.run do
+  let mut decoded : ByteArray := ByteArray.empty
+  let rawBytes := es.toByteArray
+  let len := rawBytes.size
+  let mut i := 0
+  let percent := '%'.toNat.toUInt8
+  let plus := '+'.toNat.toUInt8
+  while h : i < len do
+    let c := rawBytes[i]
+    (decoded, i) := if c == plus then
+      (decoded.push ' '.toNat.toUInt8, i + 1)
+    else if h₁ : c == percent ∧ i + 1 < len then
+      let h1 := rawBytes[i + 1]
+      if let some hd1 := hexDigitToUInt8? h1 then
+        if h₂ : i + 2 < len then
+          let h2 := rawBytes[i + 2]
+          if let some hd2 := hexDigitToUInt8? h2 then
+            (decoded.push (hd1 * 16 + hd2), i + 3)
+          else
+            (((decoded.push c).push h1).push h2, i + 3)
+        else
+          ((decoded.push c).push h1, i + 2)
+      else
+        ((decoded.push c).push h1, i + 2)
+    else
+      (decoded.push c, i + 1)
+  return String.fromUTF8? decoded
+
+end EncodedQueryString
+
+instance : ToString (EncodedQueryString r) where
+  toString := EncodedQueryString.toString
+
+instance : Repr (EncodedQueryString r) where
+  reprPrec es n := reprPrec (toString es) n
+
+instance : BEq (EncodedQueryString r) where
+  beq x y := x.toByteArray = y.toByteArray
+
+instance : Hashable (EncodedQueryString r) where
+  hash x := Hashable.hash x.toByteArray
+
+instance : Hashable (Option (EncodedQueryString r)) where
+  hash
+    | some x =>  Hashable.hash ((ByteArray.mk #[1] ++ x.toByteArray))
+    | none =>  Hashable.hash (ByteArray.mk #[0])
+
+/--
+A percent-encoded URI path segment. Valid characters are `pchar` (unreserved, sub-delims, ':', '@').
+-/
+abbrev EncodedSegment := EncodedString isPChar
+
+namespace EncodedSegment
+
+/--
+Encodes a raw string into an encoded path segment.
+-/
+def encode (s : String) : EncodedSegment :=
+  EncodedString.encode (r := isPChar) s
+
+/--
+Attempts to create an encoded path segment from raw bytes.
+-/
+def ofByteArray? (ba : ByteArray) : Option EncodedSegment :=
+  EncodedString.ofByteArray? (r := isPChar) ba
+
+/--
+Creates an encoded path segment from raw bytes, panicking on invalid encoding.
+-/
+def ofByteArray! (ba : ByteArray) : EncodedSegment :=
+  EncodedString.ofByteArray! (r := isPChar) ba
+
+/--
+Decodes an encoded path segment back to a UTF-8 string.
+-/
+def decode (segment : EncodedSegment) : Option String :=
+  EncodedString.decode segment
+
+end EncodedSegment
+
+/--
+A percent-encoded URI fragment component. Valid characters are `pchar / "/" / "?"`.
+-/
+abbrev EncodedFragment := EncodedString isFragmentChar
+
+namespace EncodedFragment
+
+/--
+Encodes a raw string into an encoded fragment component.
+-/
+def encode (s : String) : EncodedFragment :=
+  EncodedString.encode (r := isFragmentChar) s
+
+/--
+Attempts to create an encoded fragment component from raw bytes.
+-/
+def ofByteArray? (ba : ByteArray) : Option EncodedFragment :=
+  EncodedString.ofByteArray? (r := isFragmentChar) ba
+
+/--
+Creates an encoded fragment component from raw bytes, panicking on invalid encoding.
+-/
+def ofByteArray! (ba : ByteArray) : EncodedFragment :=
+  EncodedString.ofByteArray! (r := isFragmentChar) ba
+
+/--
+Decodes an encoded fragment component back to a UTF-8 string.
+-/
+def decode (fragment : EncodedFragment) : Option String :=
+  EncodedString.decode fragment
+
+end EncodedFragment
+
+/--
+A percent-encoded URI userinfo component. Valid characters are `unreserved / sub-delims / ":"`.
+-/
+abbrev EncodedUserInfo := EncodedString isUserInfoChar
+
+namespace EncodedUserInfo
+
+/--
+Encodes a raw string into an encoded userinfo component.
+-/
+def encode (s : String) : EncodedUserInfo :=
+  EncodedString.encode (r := isUserInfoChar) s
+
+/--
+Attempts to create an encoded userinfo component from raw bytes.
+-/
+def ofByteArray? (ba : ByteArray) : Option EncodedUserInfo :=
+  EncodedString.ofByteArray? (r := isUserInfoChar) ba
+
+/--
+Creates an encoded userinfo component from raw bytes, panicking on invalid encoding.
+-/
+def ofByteArray! (ba : ByteArray) : EncodedUserInfo :=
+  EncodedString.ofByteArray! (r := isUserInfoChar) ba
+
+/--
+Decodes an encoded userinfo component back to a UTF-8 string.
+-/
+def decode (userInfo : EncodedUserInfo) : Option String :=
+  EncodedString.decode userInfo
+
+end EncodedUserInfo
+
+/--
+A percent-encoded URI query parameter. Valid characters are `pchar / "/" / "?"` with '+' for spaces.
+-/
+abbrev EncodedQueryParam := EncodedQueryString isQueryDataChar
+
+namespace EncodedQueryParam
+
+/--
+Encodes a raw string into an encoded query parameter.
+-/
+def encode (s : String) : EncodedQueryParam :=
+  EncodedQueryString.encode (r := isQueryDataChar) s
+
+/--
+Attempts to create an encoded query parameter from raw bytes.
+-/
+def ofByteArray? (ba : ByteArray) : Option EncodedQueryParam :=
+  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 := isQueryDataChar) ba
+
+/--
+Attempts to create an encoded query parameter from an encoded string.
+-/
+def fromString? (s : String) : Option EncodedQueryParam :=
+  EncodedQueryString.ofString? (r := isQueryDataChar) s
+
+/--
+Decodes an encoded query parameter back to a UTF-8 string.
+-/
+def decode (param : EncodedQueryParam) : Option String :=
+  EncodedQueryString.decode param
+
+end EncodedQueryParam
+
+end Std.Http.URI

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

@@ -0,0 +1,430 @@
+/-
+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.While
+public import Init.Data.String
+public import Std.Internal.Parsec
+public import Std.Internal.Parsec.ByteArray
+public import Std.Internal.Http.Data.URI.Basic
+public import Std.Internal.Http.Data.URI.Config
+
+public section
+
+/-!
+# URI Parser
+
+This module provides parsers for HTTP request targets and HTTP-oriented URIs aligned with RFC 3986.
+It handles parsing of schemes, authorities, paths, queries, and fragments.
+
+Notable intentional constraints:
+* hosts are limited to IPv4, bracketed IPv6, and DNS-style domain names
+* IPvFuture (`v...`) inside `IP-literal` is currently rejected
+
+References:
+* https://www.rfc-editor.org/rfc/rfc3986.html
+* https://www.rfc-editor.org/rfc/rfc9110.html#name-uri-references
+* https://www.rfc-editor.org/rfc/rfc9112.html#section-3.3
+-/
+
+namespace Std.Http.URI.Parser
+
+set_option linter.all true
+
+open Internal Char
+open Std Internal Parsec ByteArray
+
+@[inline]
+private def tryOpt (p : Parser α) : Parser (Option α) :=
+  optional (attempt p)
+
+@[inline]
+private def peekIs (p : UInt8 → Bool) : Parser Bool := do
+  return (← peekWhen? p).isSome
+
+-- scheme = ALPHA *( ALPHA / DIGIT / "+" / "-" / "." )
+private def parseScheme (config : URI.Config) : Parser URI.Scheme := do
+  if config.maxSchemeLength = 0 then
+    fail "scheme length limit is 0 (no scheme allowed)"
+
+  let first ← takeWhileUpTo1 isAlphaByte 1
+  let rest ← takeWhileUpTo
+    (fun c =>
+      isAlphaNum c ∨
+      c = '+'.toUInt8 ∨ c = '-'.toUInt8 ∨ c = '.'.toUInt8)
+    (config.maxSchemeLength - 1)
+  let schemeBytes := first.toByteArray ++ rest.toByteArray
+  let str := String.fromUTF8! schemeBytes |>.toLower
+
+  if h : URI.IsValidScheme str then
+    return ⟨str, h⟩
+  else
+    fail "invalid scheme"
+
+-- port = 1*DIGIT
+private def parsePortNumber : Parser UInt16 := do
+  let portBytes ← takeWhileUpTo1 isDigitByte 5
+
+  let portStr := String.fromUTF8! portBytes.toByteArray
+
+  let some portNum := String.toNat? portStr
+    | fail s!"invalid port number: {portStr}"
+
+  if portNum > 65535 then
+    fail s!"port number too large: {portNum}"
+
+  return portNum.toUInt16
+
+-- userinfo = *( unreserved / pct-encoded / sub-delims / ":" )
+private def parseUserInfo (config : URI.Config) : Parser URI.UserInfo := do
+  let userBytesName ← takeWhileUpTo
+    (fun x =>
+      x ≠ ':'.toUInt8 ∧
+      (isUserInfoChar x ∨ x = '%'.toUInt8))
+    config.maxUserInfoLength
+
+  let some userNameEncoded := URI.EncodedUserInfo.ofByteArray? userBytesName.toByteArray
+    | fail "invalid percent encoding in user info"
+
+  let userPassEncoded ← if ← peekIs (· == ':'.toUInt8) then
+      skip
+
+      let userBytesPass ← takeWhileUpTo
+        (fun x => isUserInfoChar x ∨ x = '%'.toUInt8)
+        config.maxUserInfoLength
+
+      let some userPassEncoded := URI.EncodedUserInfo.ofByteArray? userBytesPass.toByteArray
+        | fail "invalid percent encoding in user info"
+
+      pure <| some userPassEncoded
+    else
+      pure none
+
+  return ⟨userNameEncoded, userPassEncoded⟩
+
+-- Parses bracketed IPv6 literals.
+-- Note: RFC 3986 also allows IPvFuture inside `IP-literal`; this parser
+-- currently rejects IPvFuture.
+private def parseIPv6 : Parser Net.IPv6Addr := do
+  skipByte '['.toUInt8
+
+  let result ← takeWhileUpTo1
+    (fun x => x = ':'.toUInt8 ∨ x = '.'.toUInt8 ∨ isHexDigitByte x)
+    256
+
+  skipByte ']'.toUInt8
+
+  let ipv6Str := String.fromUTF8! result.toByteArray
+  let some ipv6Addr := Std.Net.IPv6Addr.ofString ipv6Str
+    | fail s!"invalid IPv6 address: {ipv6Str}"
+
+  return ipv6Addr
+
+-- IPv4address = dec-octet "." dec-octet "." dec-octet "." dec-octet
+private def parseIPv4 : Parser Net.IPv4Addr := do
+  let result ← takeWhileUpTo1
+    (fun x => x = '.'.toUInt8 ∨ isDigitByte x)
+    256
+
+  let ipv4Str := String.fromUTF8! result.toByteArray
+  let some ipv4Addr := Std.Net.IPv4Addr.ofString ipv4Str
+    | fail s!"invalid IPv4 address: {ipv4Str}"
+
+  return ipv4Addr
+
+-- host = IP-literal / IPv4address / reg-name
+-- Note: RFC 1123 allows domain labels to start with digits, so we must try IPv4
+-- first and fall back to reg-name parsing if it fails.
+private def parseHost (config : URI.Config) : Parser URI.Host := do
+  if (← peekWhen? (· == '['.toUInt8)).isSome then
+    return .ipv6 (← parseIPv6)
+  else
+    if (← peekWhen? isDigitByte).isSome then
+      if let some ipv4 ← tryOpt parseIPv4 then
+        return .ipv4 ipv4
+
+    -- We intentionally parse DNS names here (not full RFC 3986 reg-name).
+    let some str := String.fromUTF8? (← takeWhileUpTo1
+      (fun x => isAlphaNum x ∨ x = '-'.toUInt8 ∨ x = '.'.toUInt8)
+      config.maxHostLength).toByteArray
+      | fail s!"invalid host"
+
+    let lower := str.toLower
+    if h : URI.IsValidDomainName lower ∧ ¬lower.isEmpty then
+      return .name ⟨lower, .isLowerCase_toLower, h⟩
+    else
+      fail s!"invalid domain name: {str}"
+
+-- authority = [ userinfo "@" ] host [ ":" port ]
+private def parseAuthority (config : URI.Config) : Parser URI.Authority := do
+  let userInfo ← tryOpt do
+    let ui ← parseUserInfo config
+    skipByte '@'.toUInt8
+    return ui
+
+  let host ← parseHost config
+
+  let port : URI.Port ←
+    if ← peekIs (· == ':'.toUInt8) then
+      skipByte ':'.toUInt8
+      if (← peekWhen? isDigitByte).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, host, port }
+
+-- segment = *pchar
+private def parseSegment (config : URI.Config) : Parser ByteSlice := do
+  takeWhileUpTo (fun c => isPChar c ∨ c = '%'.toUInt8) config.maxSegmentLength
+
+/-
+path = path-abempty ; begins with "/" or is empty
+  / path-absolute   ; begins with "/" but not "//"
+  / path-noscheme   ; begins with a non-colon segment
+  / path-rootless   ; begins with a segment
+  / path-empty      ; zero characters
+
+path-abempty  = *( "/" segment )
+path-absolute = "/" [ segment-nz *( "/" segment ) ]
+path-noscheme = segment-nz-nc *( "/" segment )
+path-rootless = segment-nz *( "/" segment )
+path-empty    = 0<pchar>
+-/
+
+/--
+Parses a URI path with combined parsing and validation.
+-/
+def parsePath (config : URI.Config) (forceAbsolute : Bool) (allowEmpty : Bool) : Parser URI.Path := do
+  let isPathDelimiter : UInt8 → Bool := fun c => c = '?'.toUInt8 ∨ c = '#'.toUInt8
+  let mut isAbsolute := false
+  let mut segments : Array _ := #[]
+  let mut totalLength := 0
+
+  let isSegmentOrSlash ←
+    peekIs (fun c => isPChar c ∨ c = '%'.toUInt8 ∨ c = '/'.toUInt8)
+
+  if ¬allowEmpty ∧ ((← isEof) ∨ ¬isSegmentOrSlash) then
+    fail "need a path"
+
+  -- Check if path is absolute
+  if ← peekIs (· == '/'.toUInt8) then
+    isAbsolute := true
+    totalLength := totalLength + 1
+    skip
+  else if forceAbsolute then
+    if allowEmpty ∧ ((← isEof) ∨ ¬isSegmentOrSlash) then
+      return { segments := segments, absolute := isAbsolute }
+    else
+      fail "require '/' in path"
+  else
+    pure ()
+
+  -- Parse segments
+  while (← peek?).isSome do
+    let some next := (← peek?) | break
+    if isPathDelimiter next then
+      break
+
+    if ¬(next = '/'.toUInt8 ∨ isPChar next ∨ next = '%'.toUInt8) then
+      break
+
+    if segments.size >= config.maxPathSegments then
+      fail s!"too many path segments (limit: {config.maxPathSegments})"
+
+    let segmentBytes ← parseSegment config
+    let some segmentStr := URI.EncodedSegment.ofByteArray? segmentBytes.toByteArray
+      | fail "invalid percent encoding in path segment"
+
+    totalLength := totalLength + segmentBytes.size
+    if totalLength > config.maxTotalPathLength then
+      fail s!"path too long (limit: {config.maxTotalPathLength} bytes)"
+
+    segments := segments.push segmentStr
+
+    if (← peek?).any (· == '/'.toUInt8) then
+      totalLength := totalLength + 1
+      if totalLength > config.maxTotalPathLength then
+        fail s!"path too long (limit: {config.maxTotalPathLength} bytes)"
+      skip
+      -- If path ends with '/', add empty segment
+      let next ← peek?
+      if next.isNone || next.any isPathDelimiter then
+        if segments.size >= config.maxPathSegments then
+          fail s!"too many path segments (limit: {config.maxPathSegments})"
+        segments := segments.push (URI.EncodedString.empty)
+    else
+      break
+
+  return { segments := segments, absolute := isAbsolute }
+
+-- query = *( pchar / "/" / "?" )
+private def parseQuery (config : URI.Config) : Parser URI.Query := do
+  let queryBytes ←
+    takeWhileUpTo (fun c => isQueryChar c ∨ c = '%'.toUInt8) config.maxQueryLength
+
+  let some queryStr := String.fromUTF8? queryBytes.toByteArray
+    | fail "invalid query string"
+
+  if queryStr.isEmpty then
+    return URI.Query.empty
+
+  let rawPairs := queryStr.splitOn "&"
+
+  if rawPairs.length > config.maxQueryParams then
+    fail s!"too many query parameters (limit: {config.maxQueryParams})"
+
+  let pairs : Option URI.Query := rawPairs.foldlM (init := URI.Query.empty) fun acc pair => do
+    match pair.splitOn "=" with
+    | [key] =>
+      let key ← URI.EncodedQueryParam.fromString? key
+      pure (acc.insertEncoded key none)
+    | key :: value =>
+      let key ← URI.EncodedQueryParam.fromString? key
+      let value ← URI.EncodedQueryParam.fromString? (String.intercalate "=" value)
+      pure (acc.insertEncoded key (some value))
+    | [] => pure acc  -- unreachable: splitOn always returns at least one element
+
+  if let some pairs := pairs then
+    return pairs
+  else
+    fail "invalid query string"
+
+--  fragment = *( pchar / "/" / "?" )
+private def parseFragment (config : URI.Config) : Parser URI.EncodedFragment := do
+  let fragmentBytes ←
+    takeWhileUpTo (fun c => isFragmentChar c ∨ c = '%'.toUInt8) config.maxFragmentLength
+
+  let some fragmentStr := URI.EncodedFragment.ofByteArray? fragmentBytes.toByteArray
+    | fail "invalid percent encoding in fragment"
+
+  return fragmentStr
+
+private def parseHierPart (config : URI.Config) : Parser (Option URI.Authority × URI.Path) := do
+  -- Check for "//" authority path-abempty
+  if (← tryOpt (skipString "//")).isSome then
+    let authority ← parseAuthority config
+    let path ← parsePath config true true  -- path-abempty (must start with "/" or be empty)
+    return (some authority, path)
+  else
+    -- path-absolute / path-rootless / path-empty
+    let path ← parsePath config false true
+    return (none, path)
+
+/--
+Parses a URI (Uniform Resource Identifier).
+
+URI = scheme ":" hier-part [ "?" query ] [ "#" fragment ]
+hier-part = "//" authority path-abempty / path-absolute / path-rootless / path-empty
+-/
+public def parseURI (config : URI.Config := {}) : Parser URI := do
+  let scheme ← parseScheme config
+  skipByte ':'.toUInt8
+
+  let (authority, path) ← parseHierPart config
+
+  let query ← optional (skipByteChar '?' *> parseQuery config)
+  let query := query.getD .empty
+
+  let fragment ← optional do
+    let some result := (← (skipByteChar '#' *> parseFragment config)) |>.decode
+      | fail "invalid fragment parse encoding"
+    return result
+
+  return { scheme, authority, path, query, fragment }
+
+/--
+Parses a request target with combined parsing and validation.
+-/
+public def parseRequestTarget (config : URI.Config := {}) : Parser RequestTarget :=
+  asterisk <|> origin <|> absoluteHttp <|> authority <|> absolute
+where
+  -- The asterisk form
+  asterisk : Parser RequestTarget := do
+    skipByte '*'.toUInt8
+    return .asteriskForm
+
+  -- origin-form = absolute-path [ "?" query ]
+  -- absolute-path = 1*( "/" segment )
+  origin : Parser RequestTarget := attempt do
+    if ← peekIs (· == '/'.toUInt8) then
+      let path ← parsePath config true true
+      let query ← optional (skipByte '?'.toUInt8 *> parseQuery config)
+
+      return .originForm path query
+    else
+      fail "not origin"
+
+  absoluteFromScheme (scheme : URI.Scheme) : Parser RequestTarget := do
+    skipByte ':'.toUInt8
+    let (auth, path) ← parseHierPart config
+    let query ← optional (skipByteChar '?' *> parseQuery config)
+    let query := query.getD URI.Query.empty
+
+    return .absoluteForm { path, scheme, authority := auth, query, fragment := none }
+
+  -- Prefer absolute-form for explicit HTTP(S) scheme targets with a path or authority.
+  -- This avoids misclassifying `http://host/path` as authority-form while still
+  -- letting `http:80` fall through to authority-form parsing.
+  absoluteHttp : Parser RequestTarget := attempt do
+    let scheme ← parseScheme config
+    if scheme.val = "http" || scheme.val = "https" then
+      skipByte ':'.toUInt8
+      if ← peekIs (· == '/'.toUInt8) then
+        let (authority, path) ← parseHierPart config
+        let query ← optional (skipByteChar '?' *> parseQuery config)
+        let query := query.getD .empty
+        return .absoluteForm { scheme, path, authority, query, fragment := none }
+      else
+        fail "not http absolute uri with path"
+    else
+      fail "not http absolute uri"
+
+  -- absolute-URI  = scheme ":" hier-part [ "?" query ]
+  absolute : Parser RequestTarget := attempt do
+    let scheme ← parseScheme config
+    absoluteFromScheme scheme
+
+  -- authority-form = host ":" port
+  authority : Parser RequestTarget := attempt do
+    let host ← parseHost config
+    skipByteChar ':'
+    let port ← parsePortNumber
+    return .authorityForm { host, port := .value port }
+
+/--
+Parses an HTTP `Host` header value.
+-/
+public def parseHostHeader (config : URI.Config := {}) : Parser (URI.Host × URI.Port) := do
+  let host ← parseHost config
+
+  let port : URI.Port ←
+    if ← peekIs (· == ':'.toUInt8) then
+      skipByte ':'.toUInt8
+      if (← peekWhen? isDigitByte).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"
+
+  return (host, port)
+
+end Std.Http.URI.Parser

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

@@ -299,4 +299,15 @@ that provides it.
 def isUserInfoChar (c : UInt8) : Bool :=
   isUnreserved c || isSubDelims c || c = ':'.toUInt8
 
+/--
+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.
+-/
+@[inline, expose]
+def isQueryDataChar (c : UInt8) : Bool :=
+  isQueryChar c && c ≠ '&'.toUInt8 && c ≠ '='.toUInt8
+
 end Std.Http.Internal.Char

tests/elab/async_http_encode.lean

@@ -141,13 +141,13 @@ info: "X-Custom-Header: value\x0d\n"
 info: "GET /path HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr ({ method := .get, version := .v11, uri := "/path" } : Request.Head)
+#eval encodeStr ({ method := .get, version := .v11, uri := .parse! "/path" } : Request.Head)
 
 /--
 info: "POST /submit HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr ({ method := .post, version := .v11, uri := "/submit" } : Request.Head)
+#eval encodeStr ({ method := .post, version := .v11, uri := .parse! "/submit" } : Request.Head)
 
 /--
 info: "PUT /resource HTTP/2.0\x0d\nContent-Type: application/json\x0d\n\x0d\n"
@@ -156,7 +156,7 @@ info: "PUT /resource HTTP/2.0\x0d\nContent-Type: application/json\x0d\n\x0d\n"
 #eval encodeStr ({
     method := .put
     version := .v20
-    uri := "/resource"
+    uri := .parse! "/resource"
     headers := Headers.empty.insert! "content-type" "application/json"
   } : Request.Head)
 
@@ -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 "/index.html" |>.body ()).line
+#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 "/api/data" |>.body ()).line
+#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 "/resource" |>.body ()).line
+#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 "/item" |>.body ()).line
+#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 "/update" |>.body ()).line
+#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 "/check" |>.body ()).line
+#eval encodeStr (Request.head (.parse! "/check") |>.body ()).line
 
 /--
 info: "OPTIONS * HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr (Request.options "*" |>.body ()).line
+#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 "proxy:8080" |>.body ()).line
+#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 "/debug" |>.body ()).line
+#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 "/v2" |>.version .v20 |>.body ()).line
+#eval encodeStr (Request.new |>.method .post |>.uri (.parse! "/v2") |>.version .v20 |>.body ()).line
 
 /-! ## Response builder -/
 
@@ -578,35 +578,14 @@ info: true
 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\x0d\n"
--/
-#guard_msgs in
-#eval encodeStr ({ method := .get, version := .v11, uri := "/page#section" } : Request.Head)
+#eval encodeStr ({ method := .get, version := .v11, uri := .parse! "/search?q=hello&lang=en" } : Request.Head)
 
 -- URI with percent-encoded characters
 /--
 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\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\x0d\n"
--/
-#guard_msgs in
-#eval encodeStr ({ method := .get, version := .v11, uri := "" } : Request.Head)
+#eval encodeStr ({ method := .get, version := .v11, uri :=.parse!  "/path%20with%20spaces" } : Request.Head)
 
 /-! ## Edge cases: Response with unusual statuses -/
 

tests/elab/async_http_uri.lean

@@ -0,0 +1,927 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+import Std.Internal.Http.Data.URI
+import Std.Internal.Http.Data.URI.Encoding
+
+open Std.Http
+open Std.Http.URI
+open Std.Http.URI.Parser
+
+/-!
+# URI Tests
+
+Comprehensive tests for URI parsing, encoding, normalization, and manipulation.
+This file consolidates tests from multiple URI-related test files.
+-/
+
+-- ============================================================================
+-- Helper Functions
+-- ============================================================================
+
+def runParser (parser : Std.Internal.Parsec.ByteArray.Parser α) (s : String) : IO α :=
+  IO.ofExcept ((parser <* Std.Internal.Parsec.eof).run s.toUTF8)
+
+def parseCheck (s : String) (exact : String := s) : IO Unit := do
+  let result ← runParser parseRequestTarget s
+  if toString result = exact then
+    pure ()
+  else
+    throw (.userError s!"expect {exact.quote} but got {(toString result).quote}")
+
+def parseCheckFail (s : String) : IO Unit := do
+  match (parseRequestTarget <* Std.Internal.Parsec.eof).run s.toUTF8 with
+  | .ok r =>
+      throw <| .userError
+        s!"expected parse failure, but succeeded with {(repr r)}"
+  | .error _ =>
+      pure ()
+
+-- ============================================================================
+-- Percent Encoding Tests (EncodedString)
+-- ============================================================================
+
+-- Valid percent encoding validation
+/--
+info: some "abc"
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "abc".toUTF8))
+
+/--
+info: some "%20"
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%20".toUTF8))
+
+/--
+info: some "hello%20world"
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "hello%20world".toUTF8))
+
+/--
+info: some "%FF"
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%FF".toUTF8))
+
+/--
+info: some "%00"
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%00".toUTF8))
+
+-- Invalid percent encoding: incomplete
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%".toUTF8))
+
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "hello%".toUTF8))
+
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%2".toUTF8))
+
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%A".toUTF8))
+
+-- Invalid percent encoding: non-hex characters
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%GG".toUTF8))
+
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%2G".toUTF8))
+
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedSegment.ofByteArray? "%G2".toUTF8))
+
+-- ============================================================================
+-- Percent Encoding Decode Tests
+-- ============================================================================
+
+/--
+info: some "abc"
+-/
+#guard_msgs in
+#eval IO.println (repr <| EncodedSegment.decode =<< (EncodedSegment.ofByteArray? "abc".toUTF8))
+
+/--
+info: some " "
+-/
+#guard_msgs in
+#eval IO.println (repr <| EncodedSegment.decode =<< (EncodedSegment.ofByteArray? "%20".toUTF8))
+
+/--
+info: some "hello world"
+-/
+#guard_msgs in
+#eval IO.println (repr <| EncodedSegment.decode =<< (EncodedSegment.ofByteArray? "hello%20world".toUTF8))
+
+/--
+info: some " !"
+-/
+#guard_msgs in
+#eval IO.println (repr <| EncodedSegment.decode =<< (EncodedSegment.ofByteArray? "%20%21".toUTF8))
+
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr <| EncodedSegment.decode =<< (EncodedSegment.ofByteArray? "%FF".toUTF8))
+
+/--
+info: some "\x00"
+-/
+#guard_msgs in
+#eval IO.println (repr <| EncodedSegment.decode =<< (EncodedSegment.ofByteArray? "%00".toUTF8))
+
+-- ============================================================================
+-- Query String Encoding Tests
+-- ============================================================================
+
+/--
+info: some "hello+world"
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedQueryString.ofByteArray? "hello+world".toUTF8))
+
+/--
+info: none
+-/
+#guard_msgs in
+#eval IO.println (repr (EncodedQueryString.ofByteArray? "%".toUTF8))
+
+/--
+info: some "hello world"
+-/
+#guard_msgs in
+#eval IO.println (repr <| EncodedQueryString.decode =<< (EncodedQueryString.ofByteArray? "hello+world".toUTF8))
+
+/--
+info: some " "
+-/
+#guard_msgs in
+#eval IO.println (repr <| EncodedQueryString.decode =<< (EncodedQueryString.ofByteArray? "%20".toUTF8))
+
+-- ============================================================================
+-- Request Target Parsing - Basic Tests
+-- ============================================================================
+
+#eval parseCheck "///path/with/encoded%20space"
+#eval parseCheck "/path/with/encoded%20space"
+#eval parseCheck "/path/with/encoded%20space/"
+#eval parseCheck "*"
+#eval parseCheck "/api/search?q=hello%20world&category=tech%2Bgames"
+#eval parseCheck "/"
+#eval parseCheck "/api/v1/users/123/posts/456/comments/789"
+#eval parseCheck "/files/../etc/passwd"
+#eval parseCheck "example.com:8080"
+#eval parseCheck "https://example.com:8080/ata"
+#eval parseCheck "https://example.com:8080////./ata"
+#eval parseCheck "192.168.1.1:3000"
+#eval parseCheck "[::1]:8080"
+#eval parseCheck "http://example.com/path/to/resource?query=value"
+#eval parseCheck "https://api.example.com:443/v1/users?limit=10"
+#eval parseCheck "http://[2001:db8::1]:8080/path"
+#eval parseCheck "https://xn--nxasmq6b.xn--o3cw4h/path"
+#eval parseCheck "localhost:65535"
+#eval parseCheck "http:80"
+#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"
+#eval parseCheck "///////"
+
+-- `&` 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
+  | .ok (.authorityForm _) => true
+  | _ => false
+
+-- Parse failure tests
+#eval parseCheckFail "/path with space"
+#eval parseCheckFail "/path/%"
+#eval parseCheckFail "/path/%2"
+#eval parseCheckFail "/path/%ZZ"
+#eval parseCheckFail ""
+#eval parseCheckFail "[::1"
+#eval parseCheckFail "[:::1]:80"
+#eval parseCheckFail "#frag"
+#eval parseCheckFail "/path/\n"
+#eval parseCheckFail "/path/\u0000"
+#eval parseCheckFail "/page#section"
+#eval parseCheckFail "/api/v1/users/[id]:action"
+
+-- maxPathSegments should apply to trailing empty segments as well.
+#guard
+  match (parseURI { maxPathSegments := 1 } <* Std.Internal.Parsec.eof).run
+      "http://example.com/a/".toUTF8 with
+  | .error _ => true
+  | .ok _ => false
+
+-- ============================================================================
+-- Request Target Parsing - Detailed Output Tests
+-- ============================================================================
+
+/--
+info: Std.Http.RequestTarget.originForm { segments := #["path", "with", "encoded%20space"], absolute := true } none
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/path/with/encoded%20space"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.originForm { segments := #["", "", "path", "with", "encoded%20space"], absolute := true } none
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "///path/with/encoded%20space"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.asteriskForm
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "*"
+  IO.println (repr result)
+
+/--
+info: #[("q", some "hello%20world"), ("category", some "tech%2Bgames")]
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/api/search?q=hello%20world&category=tech%2Bgames"
+  IO.println (repr result.query)
+
+/--
+info: Std.Http.RequestTarget.originForm { segments := #[], absolute := true } none
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.authorityForm
+  { 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
+  let result ← runParser parseRequestTarget "example.com:8080"
+  IO.println (repr result)
+
+/--
+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
+  let result ← runParser parseRequestTarget "192.168.1.1:3000"
+  IO.println (repr result)
+
+/--
+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
+  let result ← runParser parseRequestTarget "[::1]:8080"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.absoluteForm
+  { scheme := "https",
+    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 }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "https://example.com:8080/ata"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.absoluteForm
+  { scheme := "http",
+    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 }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "http://[2001:db8::1]:8080/path"
+  IO.println (repr result)
+
+/--
+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 := Std.Http.URI.Port.omitted },
+    path := { segments := #["private"], absolute := true },
+    query := #[],
+    fragment := none }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "https://user%20b:pass@secure.example.com/private"
+  IO.println (repr result)
+
+-- ============================================================================
+-- IPv6 Host Tests
+-- ============================================================================
+
+/--
+info: Std.Http.URI.Host.ipv6 ::1
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "[::1]:8080"
+  match result.authority? with
+  | some auth => IO.println (repr auth.host)
+  | none => IO.println "no authority"
+
+/--
+info: Std.Http.URI.Host.ipv6 2001:db8::8a2e:370:7334
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "http://[2001:db8::8a2e:370:7334]:8080/api"
+  match result.authority? with
+  | some auth => IO.println (repr auth.host)
+  | none => IO.println "no authority"
+
+/--
+info: Std.Http.URI.Host.ipv6 ::
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "http://[::]/path"
+  match result.authority? with
+  | some auth => IO.println (repr auth.host)
+  | none => IO.println "no authority"
+
+-- ============================================================================
+-- UserInfo Tests
+-- ============================================================================
+
+/--
+info: some { username := "user", password := some "pass" }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "https://user:pass@example.com/private"
+  match result.authority? with
+  | some auth => IO.println (repr auth.userInfo)
+  | none => IO.println "no authority"
+
+/--
+info: some { username := "user%20only", password := none }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "https://user%20only@example.com/path"
+  match result.authority? with
+  | some auth => IO.println (repr auth.userInfo)
+  | none => IO.println "no authority"
+
+/--
+info: some { username := "", password := some "pass" }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "https://:pass@example.com/path"
+  match result.authority? with
+  | some auth => IO.println (repr auth.userInfo)
+  | none => IO.println "no authority"
+
+/--
+info: some { username := "user", password := some "p%40ss%3Aw0rd" }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "https://user:p%40ss%3Aw0rd@example.com/"
+  match result.authority? with
+  | some auth => IO.println (repr auth.userInfo)
+  | none => IO.println "no authority"
+
+-- ============================================================================
+-- Path.normalize Tests (RFC 3986 Section 5.2.4)
+-- ============================================================================
+
+/--
+info: /a/b
+-/
+#guard_msgs in
+#eval IO.println <| toString (URI.parse! "http://example.com/a/./b").path.normalize
+
+/--
+info: /a
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/b/..").path.normalize
+
+/--
+info: /a/g
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/b/c/./../../g").path.normalize
+
+/--
+info: /g
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/../../../g").path.normalize
+
+/--
+info: /a/c
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/b/../c").path.normalize
+
+/--
+info: /a/
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/b/c/../.././").path.normalize
+
+/--
+info: /
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/b/../../..").path.normalize
+
+/--
+info: /
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/../../../").path.normalize
+
+/--
+info: /a/b/c
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/./a/./b/./c/.").path.normalize
+
+/--
+info: /c
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/../b/../c").path.normalize
+
+-- ============================================================================
+-- Path.parent Tests
+-- ============================================================================
+
+/--
+info: /a/b
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/b/c").path.parent
+
+/--
+info: /a
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/b").path.parent
+
+/--
+info: /
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a").path.parent
+
+/--
+info: /
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/").path.parent
+
+-- ============================================================================
+-- Path.join Tests
+-- ============================================================================
+
+/--
+info: /a/b/c/d
+-/
+#guard_msgs in
+#eval do
+  let p1 := (URI.parse! "http://example.com/a/b").path
+  let p2 : URI.Path := { segments := #[URI.EncodedString.encode "c", URI.EncodedString.encode "d"], absolute := false }
+  IO.println (p1.join p2)
+
+/--
+info: /x/y
+-/
+#guard_msgs in
+#eval do
+  let p1 := (URI.parse! "http://example.com/a/b").path
+  let p2 : URI.Path := { segments := #[URI.EncodedString.encode "x", URI.EncodedString.encode "y"], absolute := true }
+  IO.println (p1.join p2)
+
+-- ============================================================================
+-- Path.isEmpty Tests
+-- ============================================================================
+
+#guard (URI.parse! "http://example.com").path.isEmpty = true
+#guard (URI.parse! "http://example.com/").path.absolute = true
+#guard (URI.parse! "http://example.com/a").path.isEmpty = false
+#guard (URI.parse! "http://example.com/a").path.absolute = true
+
+-- ============================================================================
+-- URI Modification Helpers
+-- ============================================================================
+
+#guard ((URI.parse! "http://example.com").withScheme! "htTps" |>.scheme) == "https"
+#guard ((URI.parse! "http://example.com").withScheme! "ftP" |>.scheme) == "ftp"
+
+/--
+info: http://example.com/#section1
+-/
+#guard_msgs in
+#eval IO.println ((URI.parse! "http://example.com/").withFragment (some (toString (URI.EncodedString.encode "section1" : URI.EncodedFragment))))
+
+/--
+info: http://example.com/?key=value
+-/
+#guard_msgs in
+#eval do
+  let uri := URI.parse! "http://example.com/"
+  let query := URI.Query.empty.insert "key" "value"
+  IO.println (uri.withQuery query)
+
+/--
+info: http://example.com/new/path
+-/
+#guard_msgs in
+#eval do
+  let uri := URI.parse! "http://example.com/old/path"
+  let newPath : URI.Path := { segments := #[URI.EncodedString.encode "new", URI.EncodedString.encode "path"], absolute := true }
+  IO.println (uri.withPath newPath)
+
+-- ============================================================================
+-- URI.normalize Tests (RFC 3986 Section 6)
+-- ============================================================================
+
+#guard (URI.parse! "HTTP://example.com").normalize.scheme == "http"
+#guard (URI.parse! "HtTpS://example.com").normalize.scheme == "https"
+
+/--
+info: http://example.com/
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://EXAMPLE.COM/").normalize
+
+/--
+info: http://example.com/
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "HTTP://Example.COM/").normalize
+
+/--
+info: http://example.com/a/c
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "http://example.com/a/b/../c").normalize
+
+/--
+info: http://example.com/a/g
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "HTTP://EXAMPLE.COM/a/b/c/./../../g").normalize
+
+/--
+info: https://www.example.com/PATH
+-/
+#guard_msgs in
+#eval IO.println (URI.parse! "HTTPS://WWW.EXAMPLE.COM/PATH").normalize
+
+-- ============================================================================
+-- Query Parameter Tests
+-- ============================================================================
+
+-- Query with duplicate keys
+/--
+info: 3
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/search?tag=a&tag=b&tag=c"
+  let all := result.query.findAll "tag"
+  IO.println all.size
+
+/--
+info: #[some "a", some "b", some "c"]
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/search?tag=a&tag=b&tag=c"
+  let all := result.query.findAll "tag"
+  IO.println (repr all)
+
+/--
+info: some (some "a")
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/search?key=a&key=b&key=c"
+  IO.println (repr (result.query.find? "key"))
+
+-- Empty value vs no value
+/--
+info: some (some "")
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/api?key="
+  IO.println (repr (result.query.find? "key"))
+
+/--
+info: some none
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/api?key"
+  IO.println (repr (result.query.find? "key"))
+
+/--
+info: some (some "value")
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/api?key=value"
+  IO.println (repr (result.query.find? "key"))
+
+-- Raw lookup APIs should not alias with pre-encoded key spellings.
+#guard
+  match (parseRequestTarget <* Std.Internal.Parsec.eof).run "/api?%61=1&a=2".toUTF8 with
+  | .ok result =>
+      let encodedA? := EncodedQueryParam.fromString? "%61"
+      ((result.query.find? "a" |>.bind id |>.bind EncodedQueryParam.decode) == some "2") &&
+      (result.query.find? "%61").isNone &&
+      result.query.contains "a" &&
+      !result.query.contains "%61" &&
+      (match encodedA? with
+       | some encodedA =>
+           ((result.query.findEncoded? encodedA |>.bind id |>.bind EncodedQueryParam.decode) == some "1") &&
+           result.query.containsEncoded encodedA
+       | none => false)
+  | .error _ => false
+
+#guard
+  match (parseRequestTarget <* Std.Internal.Parsec.eof).run "/api?%61=1&a=2".toUTF8 with
+  | .ok result =>
+      match EncodedQueryParam.fromString? "%61" with
+      | some encodedA =>
+          let erasedRaw := result.query.erase "a"
+          let erasedEncoded := result.query.eraseEncoded encodedA
+          !erasedRaw.contains "a" &&
+          erasedRaw.containsEncoded encodedA &&
+          !erasedEncoded.containsEncoded encodedA &&
+          erasedEncoded.contains "a"
+      | none => false
+  | .error _ => false
+
+-- ============================================================================
+-- Query Operations
+-- ============================================================================
+
+#guard (URI.Query.empty.insert "a" "1" |>.contains "a") = true
+#guard (URI.Query.empty.contains "nonexistent") = false
+
+/--
+info: a=1&b=2
+-/
+#guard_msgs in
+#eval do
+  let query := URI.Query.empty
+    |>.insert "a" "1"
+    |>.insert "b" "2"
+  IO.println query.toRawString
+
+/--
+info: b=2
+-/
+#guard_msgs in
+#eval do
+  let query := URI.Query.empty
+    |>.insert "a" "1"
+    |>.insert "b" "2"
+    |>.erase "a"
+  IO.println query.toRawString
+
+/--
+info: key=new
+-/
+#guard_msgs in
+#eval do
+  let query := URI.Query.empty
+    |>.insert "key" "old"
+    |>.set "key" "new"
+  IO.println query.toRawString
+
+-- ============================================================================
+-- URI Builder Tests
+-- ============================================================================
+
+-- Domain names longer than 255 characters are rejected.
+#guard
+  let label := String.ofList (List.replicate 63 'a')
+  let longDomain := s!"{label}.{label}.{label}.{label}."
+  (URI.DomainName.ofString? longDomain).isNone
+
+#guard
+  let label := String.ofList (List.replicate 63 'a')
+  let longDomain := s!"{label}.{label}.{label}.{label}."
+  (URI.Builder.empty.setHost? longDomain).isNone
+
+/--
+info: https://example.com/api/users?page=1
+-/
+#guard_msgs in
+#eval do
+  let uri := URI.Builder.empty
+    |>.setScheme! "https"
+    |>.setHost! "example.com"
+    |>.appendPathSegment "api"
+    |>.appendPathSegment "users"
+    |>.addQueryParam "page" "1"
+    |>.build
+  IO.println uri
+
+/--
+info: http://localhost:8080/
+-/
+#guard_msgs in
+#eval do
+  let uri := URI.Builder.empty
+    |>.setScheme! "http"
+    |>.setHost! "localhost"
+    |>.setPort 8080
+    |>.build
+  IO.println uri
+
+/--
+info: https://user:pass@secure.example.com/private
+-/
+#guard_msgs in
+#eval do
+  let uri := URI.Builder.empty
+    |>.setScheme! "https"
+    |>.setUserInfo "user" (some "pass")
+    |>.setHost! "secure.example.com"
+    |>.appendPathSegment "private"
+    |>.build
+  IO.println uri
+
+-- ============================================================================
+-- Encoded Path Segment Tests
+-- ============================================================================
+
+/--
+info: Std.Http.RequestTarget.originForm { segments := #["path%2Fwith%2Fslashes"], absolute := true } none
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/path%2Fwith%2Fslashes"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.originForm { segments := #["file%20name.txt"], absolute := true } none
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/file%20name.txt"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.originForm { segments := #["caf%C3%A9"], absolute := true } none
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "/caf%C3%A9"
+  IO.println (repr result)
+
+-- ============================================================================
+-- Authority Form Tests
+-- ============================================================================
+
+/--
+info: Std.Http.RequestTarget.authorityForm
+  { 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
+  let result ← runParser parseRequestTarget "proxy.example.com:3128"
+  IO.println (repr result)
+
+/--
+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
+  let result ← runParser parseRequestTarget "127.0.0.1:8080"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.authorityForm
+  { 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
+  let result ← runParser parseRequestTarget "1example.com:8080"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.absoluteForm
+  { scheme := "http",
+    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 }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "http://1example.com/path"
+  IO.println (repr result)
+
+/--
+info: Std.Http.RequestTarget.absoluteForm
+  { scheme := "http",
+    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 }
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let result ← runParser parseRequestTarget "http://123abc.example.com/page"
+  IO.println (repr result)