lean4-htt/tests/elab/async_http_headers.lean
Sofia Rodrigues 2e48cd293a
refactor: move Async and Http from Internal to Std (#13511)
This PR moves Async and Http from Internal to Std
2026-04-23 19:55:22 +00:00

380 lines
12 KiB
Text

import Std.Http.Data.Headers
import Std.Http.Protocol.H1
open Std.Http
open Std.Http.Header
/-! ## Header.Name tests -/
-- Valid header names
#guard (Name.ofString? "content-type").isSome
#guard (Name.ofString? "host").isSome
#guard (Name.ofString? "x-custom-header").isSome
#guard (Name.ofString? "accept").isSome
-- Trimming: leading/trailing whitespace is stripped
#guard (Name.ofString? " content-type ").isSome
#guard (Name.ofString? " content-type ") == Name.ofString? "content-type"
#guard (Name.ofString? " host ").isSome
-- Invalid header names (empty, spaces, control chars)
#guard (Name.ofString? "").isNone
#guard (Name.ofString? " ").isNone
#guard (Name.ofString? "invalid header").isNone
#guard (Name.ofString? "bad\nname").isNone
#guard (Name.ofString? "bad\x00name").isNone
#guard (Name.ofString? "bad(name").isNone
#guard (Name.ofString? "bad)name").isNone
#guard (Name.ofString? "bad,name").isNone
#guard (Name.ofString? "bad;name").isNone
#guard (Name.ofString? "bad[name").isNone
#guard (Name.ofString? "bad]name").isNone
#guard (Name.ofString? "bad{name").isNone
#guard (Name.ofString? "bad}name").isNone
#guard (Name.ofString? "bad\"name").isNone
-- Case normalization
/--
info: "content-type"
-/
#guard_msgs in
#eval (Name.ofString! "Content-Type").value
/--
info: "content-type"
-/
#guard_msgs in
#eval (Name.ofString! "CONTENT-TYPE").value
-- Canonical form
/--
info: "Content-Type"
-/
#guard_msgs in
#eval toString (Name.ofString! "content-type")
/--
info: "X-Custom-Header"
-/
#guard_msgs in
#eval toString (Name.ofString! "x-custom-header")
/--
info: "Host"
-/
#guard_msgs in
#eval toString (Name.ofString! "host")
-- Name.is case-insensitive comparison
#guard (Name.ofString! "content-type").is "Content-Type"
#guard (Name.ofString! "content-type").is "CONTENT-TYPE"
#guard (Name.ofString! "content-type").is "content-type"
#guard !(Name.ofString! "content-type").is "host"
-- Predefined names
#guard Name.contentType.value == "content-type"
#guard Name.contentLength.value == "content-length"
#guard Name.host.value == "host"
#guard Name.authorization.value == "authorization"
#guard Name.userAgent.value == "user-agent"
#guard Name.accept.value == "accept"
#guard Name.connection.value == "connection"
#guard Name.transferEncoding.value == "transfer-encoding"
#guard Name.server.value == "server"
-- Name equality
#guard Name.ofString! "content-type" == Name.ofString! "Content-Type"
#guard Name.ofString! "HOST" == Name.ofString! "host"
#guard !(Name.ofString! "content-type" == Name.ofString! "host")
/-! ## Header.Value tests -/
-- Trimming: leading/trailing whitespace is stripped
#guard (Value.ofString? " text/html ") == Value.ofString? "text/html"
#guard (Value.ofString? " value ") == Value.ofString? "value"
-- Valid header values (printable ASCII, tab, space)
#guard (Value.ofString? "text/html").isSome
#guard (Value.ofString? "application/json; charset=utf-8").isSome
#guard (Value.ofString? "").isSome
#guard (Value.ofString? "value with spaces").isSome
#guard (Value.ofString? "value\twith\ttabs").isSome
-- Invalid header values (control characters except tab)
#guard (Value.ofString? "bad\x00value").isNone
#guard (Value.ofString? "bad\nvalue").isNone
#guard (Value.ofString? "bad\rvalue").isNone
-- Value.is case-insensitive comparison
#guard (Value.ofString! "text/html").is "TEXT/HTML"
#guard (Value.ofString! "text/html").is "text/html"
#guard !(Value.ofString! "text/html").is "application/json"
-- Value toString
/--
info: "text/html"
-/
#guard_msgs in
#eval toString (Value.ofString! "text/html")
/-! ## Headers collection tests -/
-- Empty headers
#guard Headers.empty.isEmpty
#guard Headers.empty.size == 0
-- Add and retrieve
#guard (Headers.empty.insert! "content-type" "text/html").size == 1
#guard !(Headers.empty.insert! "content-type" "text/html").isEmpty
#guard (Headers.empty.insert! "content-type" "text/html").contains (Name.ofString! "content-type")
#guard (Headers.empty.insert? "content-type" "text/html").isSome
#guard (Headers.empty.insert? "bad header name" "text/html").isNone
#guard (Headers.empty.insert? "content-type" "bad\nvalue").isNone
-- get? retrieves the value
/--
info: "text/html"
-/
#guard_msgs in
#eval do
let h := Headers.empty.insert! "content-type" "text/html"
return (h.get? (Name.ofString! "content-type")).get!.value
-- get? returns none for missing headers
#guard (Headers.empty.get? (Name.ofString! "content-type")).isNone
-- Multiple headers
#guard
let h := Headers.empty
|>.insert! "content-type" "text/html"
|>.insert! "host" "example.com"
|>.insert! "accept" "application/json"
h.size == 3
#guard
let h := Headers.empty.insert! "host" "example.com"
h.contains (Name.ofString! "host") && !h.contains (Name.ofString! "accept")
#guard
let h := Headers.empty
|>.insert! "content-type" "text/html"
|>.insert! "host" "example.com"
let h' := h.erase (Name.ofString! "content-type")
!h'.contains (Name.ofString! "content-type") && h'.contains (Name.ofString! "host")
#guard
let h := Headers.empty
|>.insert! "content-type" "text/html"
|>.insert! "host" "example.com"
(h.erase (Name.ofString! "content-type")).size == 1
-- hasEntry
#guard
let h := Headers.empty.insert! "content-type" "text/html"
h.hasEntry (Name.ofString! "content-type") (Value.ofString! "text/html")
#guard
let h := Headers.empty.insert! "content-type" "text/html"
!h.hasEntry (Name.ofString! "content-type") (Value.ofString! "application/json")
-- update existing
/--
info: "TEXT/HTML"
-/
#guard_msgs in
#eval do
let h := Headers.empty.insert! "content-type" "text/html"
let h' := h.update (Name.ofString! "content-type") (fun v => Value.ofString! v.value.toUpper)
return (h'.get? (Name.ofString! "content-type")).get!.value
-- ofList
#guard
let h := Headers.ofList [
(Name.ofString! "host", Value.ofString! "example.com"),
(Name.ofString! "accept", Value.ofString! "*/*")
]
h.size == 2 && h.contains (Name.ofString! "host")
-- merge
#guard
let h1 := Headers.empty.insert! "content-type" "text/html"
let h2 := Headers.empty.insert! "host" "example.com"
let merged := h1.merge h2
merged.contains (Name.ofString! "content-type") && merged.contains (Name.ofString! "host")
-- filter
#guard
let h := Headers.empty
|>.insert! "content-type" "text/html"
|>.insert! "host" "example.com"
|>.insert! "accept" "application/json"
let filtered := h.filter (fun name _ => name.is "host")
filtered.size == 1 && filtered.contains (Name.ofString! "host")
-- fold
/--
info: 3
-/
#guard_msgs in
#eval do
let h := Headers.empty
|>.insert! "a" "1"
|>.insert! "b" "2"
|>.insert! "c" "3"
return h.fold 0 (fun acc _ _ => acc + 1)
-- getD with default
/--
info: "fallback"
-/
#guard_msgs in
#eval do
let h := Headers.empty
return (h.getD (Name.ofString! "missing") (Value.ofString! "fallback")).value
-- mapValues
/--
info: "TEXT/HTML"
-/
#guard_msgs in
#eval do
let h := Headers.empty.insert! "content-type" "text/html"
let h' := h.mapValues (fun _ v => Value.ofString! v.value.toUpper)
return (h'.get? (Name.ofString! "content-type")).get!.value
-- toArray preserves insertion order
#guard
let h := Headers.empty
|>.insert! "content-type" "text/html"
|>.insert! "host" "example.com"
|>.insert! "accept" "application/json"
h.toArray.map (fun (n, v) => (n.value, v.value)) ==
#[("content-type", "text/html"), ("host", "example.com"), ("accept", "application/json")]
-- toArray with duplicate keys: both values appear in insertion order
#guard
let h := Headers.empty
|>.insert! "accept" "text/html"
|>.insert! "accept" "application/json"
h.toArray.map (fun (n, v) => (n.value, v.value)) ==
#[("accept", "text/html"), ("accept", "application/json")]
-- toArray after erase preserves remaining insertion order
#guard
let h := Headers.empty
|>.insert! "content-type" "text/html"
|>.insert! "host" "example.com"
|>.insert! "accept" "application/json"
(h.erase (Name.ofString! "host")).toArray.map (fun (n, v) => (n.value, v.value)) ==
#[("content-type", "text/html"), ("accept", "application/json")]
/-! ## Header typeclass tests -/
-- ContentLength parse
#guard
match Header.ContentLength.parse (Value.ofString! "42") with
| some cl => cl.length == 42
| none => false
#guard
match Header.ContentLength.parse (Value.ofString! "0") with
| some cl => cl.length == 0
| none => false
#guard (Header.ContentLength.parse =<< (Value.ofString! "abc")).isNone
#guard (Header.ContentLength.parse =<< (Value.ofString? "")).isNone
/--
info: ("content-length", "42")
-/
#guard_msgs in
#eval do
let (name, value) := Header.ContentLength.serialize ⟨42⟩
return (name.value, value.value)
#guard
match Header.TransferEncoding.parse (Value.ofString! "chunked") with
| some te => te.isChunked
| none => false
#guard
match Header.TransferEncoding.parse (Value.ofString! "gzip, chunked") with
| some te => te.isChunked && te.codings.size == 2
| none => false
#guard
match Header.TransferEncoding.parse (Value.ofString! "gzip") with
| some te => !te.isChunked
| none => false
#guard (Header.TransferEncoding.parse =<< (Value.ofString? "chunked, gzip")).isNone
#guard (Header.TransferEncoding.parse =<< (Value.ofString? "chunked, chunked")).isNone
#guard (Header.TransferEncoding.parse =<< (Value.ofString? "")).isNone
#guard (Header.TransferEncoding.parse =<< (Value.ofString? ",")).isNone
#guard (Header.TransferEncoding.parse =<< (Value.ofString? " , , ")).isNone
#guard (Header.TransferEncoding.parse =<< (Value.ofString? "g zip")).isNone
#guard (Header.TransferEncoding.parse =<< (Value.ofString? "\"chunked\"")).isNone
/--
info: ("transfer-encoding", "gzip,chunked")
-/
#guard_msgs in
#eval do
let te : Header.TransferEncoding := ⟨#["gzip", "chunked"], by native_decide⟩
let (name, value) := Header.TransferEncoding.serialize te
return (name.value, value.value)
#guard
match Header.Connection.parse (Value.ofString! "keep-alive, Close") with
| some c => c.containsToken "close" && c.shouldClose
| none => false
#guard (Header.Connection.parse =<< (Value.ofString? "keep alive")).isNone
/--
info: ("connection", "keep-alive,close")
-/
#guard_msgs in
#eval do
let c : Header.Connection := ⟨#["keep-alive", "close"], by native_decide⟩
let (name, value) := Header.Connection.serialize c
return (name.value, value.value)
/-! ## Aggregate header byte limit (maxHeaderBytes) -/
section HeaderByteLimit
open Std.Http.Protocol.H1
-- Helper: feed all bytes at once and run one step, return the machine state.
private def runMachine (raw : String) (cfg : Config) : Machine .receiving :=
let machine : Machine .receiving := { config := cfg }
(machine.feed raw.toUTF8).step.1
-- With a tight limit (35 bytes), two headers whose combined byte count exceeds
-- the limit should cause the machine to fail.
-- "host" (4) + "example.com" (11) + 4 = 19 bytes for the first header.
-- "x-a" (3) + "somevalue1" (10) + 4 = 17 bytes for the second → total 36 > 35.
#guard
let raw := "GET / HTTP/1.1\r\nhost: example.com\r\nx-a: somevalue1\r\n\r\n"
let cfg : Config := { maxHeaderBytes := 35 }
(runMachine raw cfg).failed
-- With a generous limit the same request succeeds (machine is not failed).
#guard
let raw := "GET / HTTP/1.1\r\nhost: example.com\r\nx-a: somevalue1\r\n\r\n"
let cfg : Config := { maxHeaderBytes := 100 }
!(runMachine raw cfg).failed
-- Exactly at the boundary: 19 bytes for host header alone, limit = 19 → ok.
#guard
let raw := "GET / HTTP/1.1\r\nhost: example.com\r\n\r\n"
let cfg : Config := { maxHeaderBytes := 19 }
!(runMachine raw cfg).failed
-- One byte under the two-header total → second header pushes it over.
#guard
let raw := "GET / HTTP/1.1\r\nhost: example.com\r\nx-a: somevalue1\r\n\r\n"
let cfg : Config := { maxHeaderBytes := 19 }
(runMachine raw cfg).failed
end HeaderByteLimit