feat: introduce URI data type for HTTP

[algebraic-dev]

This PR introduces the URI data type.

This contains the same code as #10478, divided into separate pieces to facilitate easier review.

The pieces of this feature are:

• Core data structures: feat: add core HTTP data types #12126
• Headers: feat: introduce Headers data type for HTTP #12127
• URI: feat: introduce URI data type for HTTP #12128
• Body: feat: introduce Body type class and some Body types for HTTP #12144
• H1: feat: introduce HTTP/1.1 protocol state machine #12146
• Server: feat: introduce HTTP/1.1 server #12151
• Client:

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto 57003e5c7962bd5db93fb51d4536969c3631c1db. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-24 02:14:09)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto 4c1e4a77b4952098ea043f9b8c2d155c20b24523. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-25 00:36:31)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto e9a1c9ef63d8e53803c16077f03e2dacd4a890bd. You can force reference manual CI using the force-manual-ci label. (2026-01-24 02:14:10)

[kim-em]

RFC 7230 Section 5.3.1 defines origin-form as:

origin-form = absolute-path [ "?" query ]

There's no fragment component—fragments are client-side only and should not be sent to servers in HTTP request targets. Should originForm exclude the fragment field, or is there a use case I'm missing?

[kim-em]

The username and password are stored decoded (per UserInfo docstring), but this ToString instance doesn't percent-encode them before serialization. This can produce invalid/ambiguous URIs.

Test case:

-- Expected: "user%40example:pass%3Aword@host.com"
-- Actual: "user@example:pass:word@host.com" (ambiguous - multiple @ and :)
#eval toString ({
  userInfo := some ⟨"user@example", some "pass:word"⟩,
  host := .name ⟨"host.com", by decide⟩
} : URI.Authority)

Should this use EncodedString.encode for the userinfo components?

[kim-em]

Domain names can start with digits (RFC 1123 relaxed RFC 952). A host like 1example.com would trigger the IPv4 branch, fail validation in Net.IPv4Addr.ofString, and not fall back to reg-name parsing.

Should there be a fallback to reg-name if IPv4 parsing fails? Or is rejecting digit-leading domain names intentional?

[kim-em]

The docstring says "The domain name will be automatically percent-encoded" but the implementation just lowercases—no percent-encoding happens. (Domain names typically use punycode for internationalization rather than percent-encoding anyway.) Should the docstring be corrected?