refactor: head -> line

2026-03-17 18:34:06 +00:00 · 2026-03-03 13:56:09 -03:00
parent f63639d42b
commit 41d2984f25
10 changed files with 616 additions and 38 deletions
--- a/src/Std/Internal/Http/Server/Connection.lean
+++ b/src/Std/Internal/Http/Server/Connection.lean
@@ -263,9 +263,9 @@ private def handle
      | .close =>
        pure ()

-    if let some head := pendingHead then
+    if let some line := pendingHead then
      waitingResponse := true
-      let newResponse := Handler.onRequest handler { head, body := requestIncoming, extensions := connection.extensions } connectionContext
+      let newResponse := Handler.onRequest handler { line, body := requestIncoming, extensions := connection.extensions } connectionContext
      let task ← newResponse.asTask
      BaseIO.chainTask task fun x => discard <| response.send x
      pendingHead := none
@@ -376,11 +376,11 @@ private def handle
            machine := machine.setKnownSize knownSize

          let head ← do
-            if config.generateDate ∧ ¬res.head.headers.contains Header.Name.date then
+            if config.generateDate ∧ ¬res.line.headers.contains Header.Name.date then
              let now ← Std.Time.DateTime.now (tz := .UTC)
-              pure { res.head with headers := res.head.headers.insert Header.Name.date (Header.Value.ofString! now.toRFC822String) }
+              pure { res.line with headers := res.line.headers.insert Header.Name.date (Header.Value.ofString! now.toRFC822String) }
            else
-              pure res.head
+              pure res.line
          machine := machine.send head
          waitingResponse := false
          if machine.writer.omitBody then
--- a/tests/lean/run/async_http_body_edge.lean
+++ b/tests/lean/run/async_http_body_edge.lean
@@ -327,7 +327,7 @@ def echoBodyHandler : TestHandler := fun req => do
    let mut body := ByteArray.empty
    for chunk in req.body do
      body := body ++ chunk.data
-    Response.ok |>.text s!"{toString req.head.uri}:{String.fromUTF8! body}")
+    Response.ok |>.text s!"{toString req.line.uri}:{String.fromUTF8! body}")

  assertStatusCount "Pipelined parse after exact CL" response 2
  assertContains "Pipelined first response" response "/:hello"
--- a/tests/lean/run/async_http_connection.lean
+++ b/tests/lean/run/async_http_connection.lean
@@ -35,7 +35,7 @@ structure TestCase where
  deriving Inhabited

 def toByteArray (req : Request (Array Chunk)) (chunked := false) : IO ByteArray := Async.block do
-  let mut data := Internal.Encode.encode (v := .v11) .empty req.head
+  let mut data := Internal.Encode.encode (v := .v11) .empty req.line
  let toByteArray (chunkData : Internal.ChunkedBuffer) (part : Chunk) := Internal.Encode.encode .v11 chunkData part

  for part in req.body do data := toByteArray data part
@@ -79,18 +79,18 @@ def runTestCase (tc : TestCase) : IO Unit := do

 /-- Check if request is a basic GET requests to the specified URI and host. -/
 def isBasicGetRequest (req : Request Body.Incoming) (uri : String) (host : String) : Bool :=
-  req.head.method == .get ∧
-  req.head.version == .v11 ∧
-  toString req.head.uri = uri ∧
-  req.head.headers.hasEntry (.mk "host") (.ofString! host)
+  req.line.method == .get ∧
+  req.line.version == .v11 ∧
+  toString req.line.uri = uri ∧
+  req.line.headers.hasEntry (.mk "host") (.ofString! host)

 /-- Check if request has a specific Content-Length header. -/
 def hasContentLength (req : Request Body.Incoming) (length : String) : Bool :=
-  req.head.headers.hasEntry (.mk "content-length")  (.ofString! length)
+  req.line.headers.hasEntry (.mk "content-length")  (.ofString! length)

 /-- Check if request uses chunked transfer encoding. -/
 def isChunkedRequest (req : Request Body.Incoming) : Bool :=
-  if let some te := req.head.headers.get? (.mk "transfer-encoding") then
+  if let some te := req.line.headers.get? (.mk "transfer-encoding") then
    match Header.TransferEncoding.parse te with
    | some te => te.isChunked
    | none => false
@@ -100,17 +100,17 @@ def isChunkedRequest (req : Request Body.Incoming) : Bool :=
 /-- Check if request has a specific header with a specific value. -/
 def hasHeader (req : Request Body.Incoming) (name : String) (value : String) : Bool :=
  if let some name := Header.Name.ofString? name then
-    req.head.headers.hasEntry name (.ofString! value)
+    req.line.headers.hasEntry name (.ofString! value)
  else
    false

 /-- Check if request method matches the expected method. -/
 def hasMethod (req : Request Body.Incoming) (method : Method) : Bool :=
-  req.head.method == method
+  req.line.method == method

 /-- Check if request URI matches the expected URI string. -/
 def hasUri (req : Request Body.Incoming) (uri : String) : Bool :=
-  toString req.head.uri = uri
+  toString req.line.uri = uri

 -- Tests

@@ -412,7 +412,7 @@ def hasUri (req : Request Body.Incoming) (uri : String) : Bool :=
    |>.body #[]

  handler := fun req => do
-    Response.ok |>.text (toString (toString req.head.uri).length)
+    Response.ok |>.text (toString (toString req.line.uri).length)

  expected := "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
 }
@@ -429,7 +429,7 @@ def hasUri (req : Request Body.Incoming) (uri : String) : Bool :=
    |>.body #[]

  handler := fun req => do
-    Response.ok |>.text (toString (toString req.head.uri).length)
+    Response.ok |>.text (toString (toString req.line.uri).length)

  expected := "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
 }
--- a/tests/lean/run/async_http_fuzz.lean
+++ b/tests/lean/run/async_http_fuzz.lean
@@ -301,7 +301,7 @@ def runPipelinedReadAll
  let seenRef ← IO.mkRef (#[] : Array String)

  let handler : TestHandler := fun req => do
-    let uri := toString req.head.uri
+    let uri := toString req.line.uri
    seenRef.modify (·.push uri)
    let _body : String ← req.body.readAll
    Response.ok |>.text uri
--- a/tests/lean/run/async_http_h1_compliance.lean
+++ b/tests/lean/run/async_http_h1_compliance.lean
@@ -0,0 +1,235 @@
+import Std.Internal.Http
+
+open Std Http
+open Std.Http.Protocol.H1
+
+private def ensure (name : String) (cond : Bool) (msg : String) : IO Unit := do
+  unless cond do
+    throw <| IO.userError s!"Test '{name}' failed:\n{msg}"
+
+private def hasFailedEvent (events : Array (Event .receiving)) : Bool :=
+  events.any fun
+    | .failed _ => true
+    | _ => false
+
+private def runOneStep
+    (payload : ByteArray)
+    (config : Protocol.H1.Config := {}) :
+    Machine .receiving × StepResult .receiving :=
+  let machine0 : Machine .receiving := { config := config }
+  (machine0.feed payload).step
+
+private def assertFailedWith
+    (name : String)
+    (payload : ByteArray)
+    (expected : Error)
+    (config : Protocol.H1.Config := {}) : IO Unit := do
+  let (machine, step) := runOneStep payload config
+  ensure name (hasFailedEvent step.events) s!"expected failure event, events:\n{repr step.events}"
+  ensure name (machine.error == some expected)
+    s!"expected error {repr expected}, got {repr machine.error}"
+
+private def assertMachineSucceeds
+    (name : String)
+    (payload : ByteArray)
+    (config : Protocol.H1.Config := {}) : IO Unit := do
+  let (machine, step) := runOneStep payload config
+  ensure name (machine.error.isNone)
+    s!"expected machine success but it failed with {repr machine.error}\nevents:\n{repr step.events}"
+
+-- =========================================================================
+-- HTTP/1.0 transfer-encoding (RFC 2068 §19.4.6)
+-- Chunked transfer encoding is not defined for HTTP/1.0.
+-- =========================================================================
+
+-- HTTP/1.0 + Transfer-Encoding: chunked must be rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "HTTP/1.0 chunked TE rejected"
+    ("POST / HTTP/1.0\r\nHost: example.com\r\n" ++
+     "Transfer-Encoding: chunked\r\n\r\n" ++
+     "5\r\nhello\r\n0\r\n\r\n").toUTF8
+    .badMessage
+
+-- HTTP/1.0 + Transfer-Encoding: gzip, chunked (compound) must also be rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "HTTP/1.0 compound chunked TE rejected"
+    ("POST / HTTP/1.0\r\nHost: example.com\r\n" ++
+     "Transfer-Encoding: gzip, chunked\r\n\r\n" ++
+     "5\r\nhello\r\n0\r\n\r\n").toUTF8
+    .badMessage
+
+-- HTTP/1.1 + Transfer-Encoding: chunked must be accepted.
+#eval show IO Unit from do
+  assertMachineSucceeds
+    "HTTP/1.1 chunked TE accepted"
+    ("POST / HTTP/1.1\r\nHost: example.com\r\n" ++
+     "Transfer-Encoding: chunked\r\n\r\n" ++
+     "5\r\nhello\r\n0\r\n\r\n").toUTF8
+
+-- =========================================================================
+-- HTTP/1.0 Host header (RFC 2616 §14.23)
+-- Host is optional in HTTP/1.0; required only in HTTP/1.1 (RFC 9112 §3.2).
+-- =========================================================================
+
+-- HTTP/1.0 GET without a Host header must be accepted.
+#eval show IO Unit from do
+  assertMachineSucceeds
+    "HTTP/1.0 GET without Host accepted"
+    "GET / HTTP/1.0\r\n\r\n".toUTF8
+
+-- HTTP/1.0 POST without a Host header must be accepted.
+#eval show IO Unit from do
+  assertMachineSucceeds
+    "HTTP/1.0 POST without Host accepted"
+    "POST / HTTP/1.0\r\nContent-Length: 0\r\n\r\n".toUTF8
+
+-- HTTP/1.0 with a Host header must also be accepted.
+#eval show IO Unit from do
+  assertMachineSucceeds
+    "HTTP/1.0 with Host accepted"
+    "GET / HTTP/1.0\r\nHost: example.com\r\n\r\n".toUTF8
+
+-- HTTP/1.1 without a Host header must be rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "HTTP/1.1 without Host rejected"
+    "GET / HTTP/1.1\r\n\r\n".toUTF8
+    .badMessage
+
+-- =========================================================================
+-- Keep-alive persistence
+-- RFC 2616 §19.7.1: HTTP/1.0 + Connection: keep-alive requests persistence.
+-- RFC 9112: HTTP/1.1 is persistent by default; Connection: close disables it.
+-- =========================================================================
+
+-- HTTP/1.0 + Connection: keep-alive must enable persistence.
+#eval show IO Unit from do
+  let payload :=
+    "GET / HTTP/1.0\r\nHost: example.com\r\nConnection: keep-alive\r\n\r\n".toUTF8
+  let machine0 : Machine .receiving := { config := {} }
+  let (machine, step) := (machine0.feed payload).step
+  ensure
+    "HTTP/1.0 Connection: keep-alive enables keepAlive"
+    machine.keepAlive
+    s!"expected keepAlive=true for HTTP/1.0 + Connection: keep-alive\n{repr step.events}"
+
+-- HTTP/1.0 without Connection: keep-alive must be non-persistent.
+#eval show IO Unit from do
+  let payload := "GET / HTTP/1.0\r\nHost: example.com\r\n\r\n".toUTF8
+  let machine0 : Machine .receiving := { config := {} }
+  let (machine, _) := (machine0.feed payload).step
+  ensure
+    "HTTP/1.0 bare request is non-persistent"
+    (!machine.keepAlive)
+    "expected keepAlive=false for plain HTTP/1.0 request"
+
+-- HTTP/1.1 keep-alive defaults to true.
+#eval show IO Unit from do
+  let payload := "GET / HTTP/1.1\r\nHost: example.com\r\n\r\n".toUTF8
+  let machine0 : Machine .receiving := { config := {} }
+  let (machine, step) := (machine0.feed payload).step
+  ensure
+    "HTTP/1.1 keepAlive defaults to true"
+    machine.keepAlive
+    s!"expected keepAlive=true for HTTP/1.1 request\n{repr step.events}"
+
+-- HTTP/1.1 + Connection: close must disable keep-alive.
+#eval show IO Unit from do
+  let payload :=
+    "GET / HTTP/1.1\r\nHost: example.com\r\nConnection: close\r\n\r\n".toUTF8
+  let machine0 : Machine .receiving := { config := {} }
+  let (machine, _) := (machine0.feed payload).step
+  ensure
+    "HTTP/1.1 Connection: close disables keepAlive"
+    (!machine.keepAlive)
+    "expected keepAlive=false for HTTP/1.1 + Connection: close"
+
+-- =========================================================================
+-- RFC 9112 §2.2: bare LF in header section must be rejected.
+-- =========================================================================
+
+-- Header section ending with CRLF + bare LF (instead of two CRLFs) is rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "Bare LF blank line rejected"
+    "GET / HTTP/1.1\r\nHost: example.com\r\n\n".toUTF8
+    .badMessage
+
+-- Bare LF blank line with a body following must also be rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "Bare LF blank line with body rejected"
+    ("POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: 5\r\n\nhello").toUTF8
+    .badMessage
+
+-- =========================================================================
+-- Regression: well-established behaviours must not regress.
+-- =========================================================================
+
+-- Content-Length + Transfer-Encoding together must be rejected (request smuggling guard).
+#eval show IO Unit from do
+  assertFailedWith
+    "CL + TE together rejected"
+    ("POST / HTTP/1.1\r\nHost: example.com\r\n" ++
+     "Content-Length: 5\r\nTransfer-Encoding: chunked\r\n\r\n" ++
+     "5\r\nhello\r\n0\r\n\r\n").toUTF8
+    .badMessage
+
+-- Duplicate Host header must be rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "Duplicate Host rejected"
+    "GET / HTTP/1.1\r\nHost: a.example\r\nHost: b.example\r\n\r\n".toUTF8
+    .badMessage
+
+-- CONNECT requires authority-form target.
+#eval show IO Unit from do
+  assertFailedWith
+    "CONNECT with non-authority target rejected"
+    "CONNECT / HTTP/1.1\r\nHost: example.com\r\n\r\n".toUTF8
+    .badMessage
+
+-- Asterisk-form is reserved for OPTIONS only.
+#eval show IO Unit from do
+  assertFailedWith
+    "GET * rejected"
+    "GET * HTTP/1.1\r\nHost: example.com\r\n\r\n".toUTF8
+    .badMessage
+
+-- =========================================================================
+-- Host/authority matching with default ports.
+-- =========================================================================
+
+-- https default-port equivalence: URI omits port, Host uses :443 => accepted.
+#eval show IO Unit from do
+  assertMachineSucceeds
+    "absolute https + Host :443 accepted"
+    "GET https://a.com/path HTTP/1.1\r\nHost: a.com:443\r\n\r\n".toUTF8
+
+-- https default-port equivalence: URI uses :443, Host omits port => accepted.
+#eval show IO Unit from do
+  assertMachineSucceeds
+    "absolute https:443 + Host omitted port accepted"
+    "GET https://a.com:443/path HTTP/1.1\r\nHost: a.com\r\n\r\n".toUTF8
+
+-- http default-port equivalence: URI omits port, Host uses :80 => accepted.
+#eval show IO Unit from do
+  assertMachineSucceeds
+    "absolute http + Host :80 accepted"
+    "GET http://a.com/path HTTP/1.1\r\nHost: a.com:80\r\n\r\n".toUTF8
+
+-- Non-default port mismatch must be rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "absolute https + Host :555 rejected"
+    "GET https://a.com/path HTTP/1.1\r\nHost: a.com:555\r\n\r\n".toUTF8
+    .badMessage
+
+-- Explicit non-default URI port must not match omitted Host port.
+#eval show IO Unit from do
+  assertFailedWith
+    "absolute https:444 + Host omitted port rejected"
+    "GET https://a.com:444/path HTTP/1.1\r\nHost: a.com\r\n\r\n".toUTF8
+    .badMessage
--- a/tests/lean/run/async_http_h1_incremental.lean
+++ b/tests/lean/run/async_http_h1_incremental.lean
@@ -27,6 +27,23 @@ private def hasCloseBodyEvent (events : Array (Event .receiving)) : Bool :=
    | .closeBody => true
    | _ => false

+private def hasContinueEvent (events : Array (Event .receiving)) : Bool :=
+  events.any fun
+    | .«continue» => true
+    | _ => false
+
+private def countNeedAnswerEvents (events : Array (Event .receiving)) : Nat :=
+  events.foldl (init := 0) fun n e =>
+    match e with
+    | .needAnswer => n + 1
+    | _ => n
+
+private def countFailedEvents (events : Array (Event .receiving)) : Nat :=
+  events.foldl (init := 0) fun n e =>
+    match e with
+    | .failed _ => n + 1
+    | _ => n
+
 private def pulledBodyBytes (chunks : Array PulledChunk) : ByteArray :=
  chunks.foldl (fun acc c => acc ++ c.chunk.data) .empty

@@ -185,6 +202,23 @@ private def assertIncrementalSuccess
  else
    pure ()

+private def runOneStepReceiving
+    (payload : ByteArray)
+    (config : Protocol.H1.Config := {}) :
+    Machine .receiving × StepResult .receiving :=
+  let machine0 : Machine .receiving := { config := config }
+  (machine0.feed payload).step
+
+private def assertFailedWith
+    (name : String)
+    (payload : ByteArray)
+    (expected : Error)
+    (config : Protocol.H1.Config := {}) : IO Unit := do
+  let (machine, step) := runOneStepReceiving payload config
+  ensure name (hasFailedEvent step.events) s!"expected failure event, events:\n{repr step.events}"
+  ensure name (machine.error == some expected)
+    s!"expected error {repr expected}, got {repr machine.error}"
+
 -- Deterministic: one-byte incremental content-length request.
 #eval show IO Unit from do
  let body := "hello".toUTF8
@@ -276,3 +310,110 @@ private def assertIncrementalSuccess

    let trace := runIncrementalReceiving parts
    assertIncrementalSuccess s!"Property chunked #{i}" trace body (expectNeedMoreData := parts.size > 1)
+
+-- Edge case: unsupported HTTP version in request-line.
+#eval show IO Unit from do
+  assertFailedWith
+    "Unsupported HTTP version"
+    "GET / HTTP/2.0\r\nHost: example.com\r\n\r\n".toUTF8
+    .unsupportedVersion
+
+-- Edge case: URI length limit must map to uriTooLong.
+#eval show IO Unit from do
+  let cfg : Protocol.H1.Config := { maxUriLength := 8, maxStartLineLength := 256 }
+  assertFailedWith
+    "URI too long"
+    "GET /this/path/is/way/too/long HTTP/1.1\r\nHost: example.com\r\n\r\n".toUTF8
+    .uriTooLong
+    cfg
+
+-- Edge case: header count limit exceeded.
+#eval show IO Unit from do
+  let cfg : Protocol.H1.Config := { maxHeaders := 1 }
+  assertFailedWith
+    "Too many headers"
+    "GET / HTTP/1.1\r\nHost: example.com\r\nX-Test: 1\r\n\r\n".toUTF8
+    .tooManyHeaders
+    cfg
+
+-- Edge case: aggregate header bytes limit exceeded.
+#eval show IO Unit from do
+  let cfg : Protocol.H1.Config := { maxHeaderBytes := 8 }
+  assertFailedWith
+    "Headers too large"
+    "GET / HTTP/1.1\r\nHost: example.com\r\n\r\n".toUTF8
+    .headersTooLarge
+    cfg
+
+-- Edge case: duplicate Host headers rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "Duplicate Host rejected"
+    "GET / HTTP/1.1\r\nHost: a.example\r\nHost: b.example\r\n\r\n".toUTF8
+    .badMessage
+
+-- Edge case: mixed Content-Length and Transfer-Encoding rejected.
+#eval show IO Unit from do
+  assertFailedWith
+    "TE and CL mixed"
+    "POST / HTTP/1.1\r\nHost: example.com\r\nContent-Length: 4\r\nTransfer-Encoding: chunked\r\n\r\n4\r\nWiki\r\n0\r\n\r\n".toUTF8
+    .badMessage
+
+-- Edge case: CONNECT must use authority-form target.
+#eval show IO Unit from do
+  assertFailedWith
+    "CONNECT non-authority target rejected"
+    "CONNECT / HTTP/1.1\r\nHost: example.com\r\n\r\n".toUTF8
+    .badMessage
+
+-- Edge case: asterisk-form reserved for OPTIONS.
+#eval show IO Unit from do
+  assertFailedWith
+    "GET * rejected"
+    "GET * HTTP/1.1\r\nHost: example.com\r\n\r\n".toUTF8
+    .badMessage
+
+-- Edge case: Expect: 100-continue pauses reader and can be accepted/rejected.
+#eval show IO Unit from do
+  let request :=
+    "POST /expect HTTP/1.1\r\nHost: example.com\r\nExpect: 100-continue\r\nContent-Length: 4\r\n\r\n".toUTF8
+
+  let machine0 : Machine .receiving := { config := {} }
+  let (machine1, step1) := (machine0.feed request).step
+
+  ensure "Expect setup not failed" (!machine1.failed) s!"unexpected failure:\n{repr step1.events}"
+  ensure "Expect emitted continue event" (hasContinueEvent step1.events) s!"missing continue event:\n{repr step1.events}"
+  ensure "Expect reader paused"
+    (match machine1.reader.state with
+      | .«continue» _ => true
+      | _ => false)
+    s!"expected continue state, got {repr machine1.reader.state}"
+
+  let machine2 := machine1.canContinue .«continue»
+  ensure "Expect accepted"
+    (match machine2.reader.state with
+      | .readBody (.fixed 4) => true
+      | _ => false)
+    s!"expected fixed(4) body state, got {repr machine2.reader.state}"
+
+  let machine3 := machine1.canContinue .ok
+  ensure "Expect rejected closes reader"
+    (match machine3.reader.state with
+      | .closed => true
+      | _ => false)
+    s!"expected closed reader, got {repr machine3.reader.state}"
+  ensure "Expect rejected disables keep-alive" (!machine3.keepAlive) "keepAlive should be disabled after reject"
+
+-- Regression: receiving path should emit needAnswer only once per message.
+#eval show IO Unit from do
+  let payload := "GET / HTTP/1.1\r\nHost: example.com\r\n\r\n".toUTF8
+  let (_machine, step) := runOneStepReceiving payload
+  ensure "Single needAnswer event" (countNeedAnswerEvents step.events == 1)
+    s!"expected exactly one needAnswer event, got events:\n{repr step.events}"
+
+-- Regression: malformed request should emit failed only once.
+#eval show IO Unit from do
+  let payload := "GET / HTTP/2.0\r\nHost: example.com\r\n\r\n".toUTF8
+  let (_machine, step) := runOneStepReceiving payload
+  ensure "Single failed event" (countFailedEvents step.events == 1)
+    s!"expected exactly one failed event, got events:\n{repr step.events}"
--- a/tests/lean/run/async_http_h1_parser_fuzz.lean
+++ b/tests/lean/run/async_http_h1_parser_fuzz.lean
@@ -0,0 +1,202 @@
+import Std.Internal.Http
+import Std.Internal.Http.Protocol.H1.Parser
+
+open Std Internal Parsec ByteArray
+open Std.Http.Protocol.H1
+
+private def ensure (name : String) (cond : Bool) (msg : String) : IO Unit := do
+  unless cond do
+    throw <| IO.userError s!"{name}: {msg}"
+
+private def runParser (p : Parser α) (s : String) : Except String α :=
+  match (p <* eof).run s.toUTF8 with
+  | .ok x => .ok x
+  | .error e => .error e
+
+private def randBelow (gen : StdGen) (maxExclusive : Nat) : Nat × StdGen :=
+  if maxExclusive = 0 then
+    (0, gen)
+  else
+    randNat gen 0 (maxExclusive - 1)
+
+private def pick! [Inhabited α] (gen : StdGen) (xs : Array α) : α × StdGen :=
+  let (i, gen') := randBelow gen xs.size
+  (xs[i]!, gen')
+
+private def randomToken (gen : StdGen) (len : Nat) : String × StdGen := Id.run do
+  let mut g := gen
+  let mut out := ""
+  for _ in [0:len] do
+    let (r, g') := randBelow g 38
+    g := g'
+    let c :=
+      if r < 26 then Char.ofNat (97 + r)
+      else if r < 36 then Char.ofNat (48 + (r - 26))
+      else if r = 36 then '-'
+      else '_'
+    out := out.push c
+  (out, g)
+
+private def randomReason (gen : StdGen) (len : Nat) : String × StdGen := Id.run do
+  let mut g := gen
+  let mut out := ""
+  for _ in [0:len] do
+    let (r, g') := randBelow g 30
+    g := g'
+    let c := if r < 26 then Char.ofNat (65 + r) else ' '
+    out := out.push c
+  (out.trimAscii.toString, g)
+
+private def pad3 (n : Nat) : String :=
+  if n < 10 then s!"00{n}" else if n < 100 then s!"0{n}" else s!"{n}"
+
+private def expectRequestOk (s : String) : IO Unit := do
+  match runParser (parseRequestLine {}) s with
+  | .ok _ => pure ()
+  | .error e => throw <| IO.userError s!"expected request-line success for {s.quote}, got: {e}"
+
+private def expectRequestFail (s : String) : IO Unit := do
+  match runParser (parseRequestLine {}) s with
+  | .ok _ => throw <| IO.userError s!"expected request-line failure for {s.quote}"
+  | .error _ => pure ()
+
+private def expectStatusOk (s : String) : IO Unit := do
+  match runParser (parseStatusLine {}) s with
+  | .ok _ => pure ()
+  | .error e => throw <| IO.userError s!"expected status-line success for {s.quote}, got: {e}"
+
+private def expectStatusFail (s : String) : IO Unit := do
+  match runParser (parseStatusLine {}) s with
+  | .ok _ => throw <| IO.userError s!"expected status-line failure for {s.quote}"
+  | .error _ => pure ()
+
+private def expectOk {α} (name : String) (p : Parser α) (s : String) : IO α := do
+  match runParser p s with
+  | .ok x => pure x
+  | .error e => throw <| IO.userError s!"{name}: expected success for {s.quote}, got {e}"
+
+private def expectFail {α} (name : String) (p : Parser α) (s : String) : IO Unit := do
+  match runParser p s with
+  | .ok _ => throw <| IO.userError s!"{name}: expected failure for {s.quote}"
+  | .error _ => pure ()
+
+#eval show IO Unit from do
+  let methods : Array String := #["GET", "POST", "PUT", "PATCH", "DELETE", "OPTIONS", "HEAD", "CONNECT"]
+  let targets : Array String := #["/", "/a", "/a/b", "/a/b?q=1", "*", "http://example.com", "example.com:443"]
+  let versions : Array String := #["HTTP/1.1", "HTTP/1.0"]
+
+  let mut gen : StdGen := StdGen.mk 0x5eed1234 0x12345
+  for i in [0:400] do
+    let (m, g1) := pick! gen methods
+    let (t, g2) := pick! g1 targets
+    let (v, g3) := pick! g2 versions
+    gen := g3
+
+    let line := s!"{m} {t} {v}\r\n"
+    expectRequestOk line
+
+    -- Mutation 1: drop the first space
+    expectRequestFail s!"{m}{t} {v}\r\n"
+
+    -- Mutation 2: invalid version token
+    expectRequestFail s!"{m} {t} HTTP/2.0\r\n"
+
+    -- Mutation 3: bad method character
+    expectRequestFail s!"{m}! {t} {v}\r\n"
+
+    ensure "request fuzz progress" (i < 100000) "unreachable safety check"
+
+#eval show IO Unit from do
+  let knownCodes : Array Nat := #[200, 201, 204, 301, 400, 404, 500, 503]
+  let mut gen : StdGen := StdGen.mk 0xabcde123 0x777
+
+  for _ in [0:400] do
+    let (code, g1) := pick! gen knownCodes
+    let (len, g2) := randBelow g1 20
+    let (reasonRaw, g3) := randomReason g2 (len + 1)
+    gen := g3
+    let reason := if reasonRaw.isEmpty then "OK" else reasonRaw
+
+    let line := s!"HTTP/1.1 {pad3 code} {reason}\r\n"
+    expectStatusOk line
+
+    -- Mutation 1: unsupported version
+    expectStatusFail s!"HTTP/2.0 {pad3 code} {reason}\r\n"
+
+    -- Mutation 2: non-digit in status code
+    expectStatusFail s!"HTTP/1.1 A{(pad3 code).drop 1} {reason}\r\n"
+
+    -- Mutation 3: illegal reason byte (DEL)
+    expectStatusFail s!"HTTP/1.1 {pad3 code} bad{Char.ofNat 127}\r\n"
+
+#eval show IO Unit from do
+  -- Randomized malformed gibberish smoke: parser must simply return error or success,
+  -- but never crash/panic.
+  let mut gen : StdGen := StdGen.mk 0x31415926 0x27182818
+  for _ in [0:300] do
+    let (len, g1) := randBelow gen 80
+    let (tok, g2) := randomToken g1 (len + 1)
+    gen := g2
+    let _ := runParser (parseRequestLine {}) (tok ++ "\r\n")
+    let _ := runParser (parseStatusLine {}) (tok ++ "\r\n")
+  pure ()
+
+-- Component tests for individual parser parts.
+#eval show IO Unit from do
+  -- parseSingleHeader
+  let sh1 ← expectOk "parseSingleHeader some" (parseSingleHeader {} <* eof) "Host: x\r\n"
+  ensure "parseSingleHeader some present" sh1.isSome "expected some header"
+
+  let sh2 ← expectOk "parseSingleHeader none" (parseSingleHeader {} <* eof) "\r\n"
+  ensure "parseSingleHeader none present" sh2.isNone "expected header terminator"
+
+  -- parseChunkSize / parseChunkPartial
+  let (n1, ext1) ← expectOk "parseChunkSize bare" (parseChunkSize {} <* eof) "A\r\n"
+  ensure "parseChunkSize value" (n1 == 10) "chunk-size mismatch"
+  ensure "parseChunkSize ext empty" (ext1.isEmpty) "expected no extensions"
+
+  let (n2, ext2) ← expectOk "parseChunkSize ext" (parseChunkSize {} <* eof) "4;foo=bar;baz=\"qux\"\r\n"
+  ensure "parseChunkSize ext value" (n2 == 4) "chunk-size mismatch with ext"
+  ensure "parseChunkSize ext count" (ext2.size == 2) "expected 2 extensions"
+
+  let cp1 ← expectOk "parseChunkPartial some" (parseChunkPartial {} <* eof) "4\r\nWiki"
+  ensure "parseChunkPartial some isSome" cp1.isSome "expected chunk data"
+  ensure "parseChunkPartial some size" ((cp1.map (fun (n, _, _) => n)).getD 0 == 4) "size mismatch"
+
+  let cp0 ← expectOk "parseChunkPartial none" (parseChunkPartial {} <* eof) "0\r\n"
+  ensure "parseChunkPartial none isNone" cp0.isNone "expected last-chunk marker"
+
+  -- parseFixedSizeData / parseChunkSizedData
+  let fs1 ← expectOk "parseFixedSizeData complete" (parseFixedSizeData 4 <* eof) "Wiki"
+  ensure "parseFixedSizeData complete shape"
+    (match fs1 with | .complete _ => true | _ => false)
+    "expected complete result"
+  let fs2 ← expectOk "parseFixedSizeData incomplete" (parseFixedSizeData 4 <* eof) "Wi"
+  ensure "parseFixedSizeData incomplete shape"
+    (match fs2 with | .incomplete _ 2 => true | _ => false)
+    "expected incomplete result with remaining=2"
+
+  let cs1 ← expectOk "parseChunkSizedData complete" (parseChunkSizedData 4 <* eof) "Wiki\r\n"
+  ensure "parseChunkSizedData complete shape"
+    (match cs1 with | .complete _ => true | _ => false)
+    "expected complete chunk-sized result"
+  let cs2 ← expectOk "parseChunkSizedData incomplete" (parseChunkSizedData 4 <* eof) "Wi"
+  ensure "parseChunkSizedData incomplete shape"
+    (match cs2 with | .incomplete _ 2 => true | _ => false)
+    "expected incomplete chunk-sized result with remaining=2"
+
+  -- parseTrailers
+  let trailers ← expectOk "parseTrailers ok" (parseTrailers {} <* eof) "X-Test: a\r\nY-Test: b\r\n\r\n"
+  ensure "parseTrailers count" (trailers.size == 2) "expected 2 trailers"
+  expectFail "parseTrailers forbidden" (parseTrailers {} <* eof) "Content-Length: 1\r\n\r\n"
+
+  -- parseRequestLineRawVersion / parseStatusLineRawVersion
+  let (m1, _, v1) ← expectOk "parseRequestLineRawVersion" (parseRequestLineRawVersion {} <* eof) "GET / HTTP/1.1\r\n"
+  ensure "parseRequestLineRawVersion method" (m1 == Std.Http.Method.get) "method mismatch"
+  ensure "parseRequestLineRawVersion version" (v1 == some Std.Http.Version.v11) "expected recognized v11"
+  let (_, rv) ← expectOk "parseStatusLineRawVersion" (parseStatusLineRawVersion {} <* eof) "HTTP/1.1 204 No Content\r\n"
+  ensure "parseStatusLineRawVersion recognized" (rv == some Std.Http.Version.v11) "expected v11"
+
+  -- parseRequestLine / parseStatusLine failures
+  expectFail "parseRequestLine invalid version" (parseRequestLine {} <* eof) "GET / HTTP/2.0\r\n"
+  expectFail "parseStatusLine invalid version" (parseStatusLine {} <* eof) "HTTP/2.0 200 OK\r\n"
--- a/tests/lean/run/async_http_hang_regressions.lean
+++ b/tests/lean/run/async_http_hang_regressions.lean
@@ -104,7 +104,7 @@ def onesChunked (n : Nat) : String := Id.run do

 def ignoreHandler : TestHandler := fun _ => Response.ok |>.text "ok"

-def uriHandler : TestHandler := fun req => Response.ok |>.text (toString req.head.uri)
+def uriHandler : TestHandler := fun req => Response.ok |>.text (toString req.line.uri)

 def echoBodyHandler : TestHandler := fun req => do
  let mut body := ByteArray.empty
--- a/tests/lean/run/async_http_keepalive.lean
+++ b/tests/lean/run/async_http_keepalive.lean
@@ -41,7 +41,7 @@ def runPipelined
  let seenRef ← IO.mkRef (#[] : Array String)

  let handler : TestHandler := fun req => do
-    let uri := toString req.head.uri
+    let uri := toString req.line.uri
    seenRef.modify (·.push uri)

    let body ←
@@ -100,7 +100,7 @@ def assertSeenCount (name : String) (seen : Array String) (expected : Nat) : IO
  let req1 := "GET /first HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n"
  let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
  let response ← sendRaw client server (req1 ++ req2).toUTF8 (fun req =>
-    Response.ok |>.text (toString req.head.uri))
+    Response.ok |>.text (toString req.line.uri))

  assertStatusCount "Two keep-alive responses" response 2
  assertContains "Two keep-alive first" response "/first"
@@ -112,7 +112,7 @@ def assertSeenCount (name : String) (seen : Array String) (expected : Nat) : IO
  let req1 := "GET /first HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
  let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
  let response ← sendRaw client server (req1 ++ req2).toUTF8 (fun req =>
-    Response.ok |>.text (toString req.head.uri))
+    Response.ok |>.text (toString req.line.uri))

  assertStatusCount "Connection close response count" response 1
  assertContains "Connection close first served" response "/first"
@@ -124,7 +124,7 @@ def assertSeenCount (name : String) (seen : Array String) (expected : Nat) : IO
  let req1 := "GET /1 HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n"
  let req2 := "GET /2 HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
  let response ← sendRaw client server (req1 ++ req2).toUTF8
-    (fun req => Response.ok |>.text (toString req.head.uri))
+    (fun req => Response.ok |>.text (toString req.line.uri))
    (config := { lingeringTimeout := 3000, enableKeepAlive := false, generateDate := false })

  assertStatusCount "Keep-alive disabled response count" response 1
@@ -138,7 +138,7 @@ def assertSeenCount (name : String) (seen : Array String) (expected : Nat) : IO
  let req1 := "GET /1 HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n"
  let req2 := "GET /2 HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
  let response ← sendRaw client server (req0 ++ req1 ++ req2).toUTF8
-    (fun req => Response.ok |>.text (toString req.head.uri))
+    (fun req => Response.ok |>.text (toString req.line.uri))
    (config := { lingeringTimeout := 3000, maxRequests := 2, generateDate := false })

  assertStatusCount "maxRequests response count" response 2
@@ -152,7 +152,7 @@ def assertSeenCount (name : String) (seen : Array String) (expected : Nat) : IO
  let req1 := "POST /ignore HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\n\x0d\nhello"
  let req2 := "GET /after HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
  let response ← sendRaw client server (req1 ++ req2).toUTF8 (fun req =>
-    Response.ok |>.text (toString req.head.uri))
+    Response.ok |>.text (toString req.line.uri))

  assertStatusCount "Unread CL body keep-alive responses" response 2
  assertContains "Unread CL body first" response "/ignore"
@@ -164,7 +164,7 @@ def assertSeenCount (name : String) (seen : Array String) (expected : Nat) : IO
  let req1 := "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n"
  let req2 := "GET /next HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
  let response ← sendRaw client server (req1 ++ req2).toUTF8 (fun req =>
-    Response.ok |>.text (toString req.head.uri))
+    Response.ok |>.text (toString req.line.uri))

  assertStatusCount "Unread chunked body keep-alive responses" response 2
  assertContains "Unread chunked first" response "/chunked"
--- a/tests/lean/run/async_http_malformed.lean
+++ b/tests/lean/run/async_http_malformed.lean
@@ -219,11 +219,6 @@ def notImplemented : String :=
  let responseA ← sendRaw clientA serverA rawA okHandler
  assertExact "HTTP/2.0 rejected" responseA bad505

-  let (clientB, serverB) ← Mock.new
-  let rawB := "GET / HTTP/1.0\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
-  let responseB ← sendRaw clientB serverB rawB okHandler
-  assertExact "HTTP/1.0 rejected" responseB bad505
-
 -- Request-line parsing failures.
 #eval show IO _ from do
  let (clientA, serverA) ← Mock.new
@@ -312,14 +307,19 @@ def notImplemented : String :=
  assertExact "CONNECT authority-form accepted" responseC ok200

  let (clientD, serverD) ← Mock.new
-  let getAsterisk := "GET * HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
-  let responseD ← sendRaw clientD serverD getAsterisk okHandler
-  assertExact "Asterisk-form rejected for non-OPTIONS" responseD bad400
+  let badAuthorityPort := "CONNECT example.com:444 HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+  let responseD ← sendRaw clientD serverD badAuthorityPort okHandler
+  assertExact "CONNECT authority-form non-default port mismatch rejected" responseD bad400

  let (clientE, serverE) ← Mock.new
+  let getAsterisk := "GET * HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+  let responseE ← sendRaw clientE serverE getAsterisk okHandler
+  assertExact "Asterisk-form rejected for non-OPTIONS" responseE bad400
+
+  let (clientF, serverF) ← Mock.new
  let optionsAsterisk := "OPTIONS * HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
-  let responseE ← sendRaw clientE serverE optionsAsterisk okHandler
-  assertExact "Asterisk-form accepted for OPTIONS" responseE ok200
+  let responseF ← sendRaw clientF serverF optionsAsterisk okHandler
+  assertExact "Asterisk-form accepted for OPTIONS" responseF ok200

 -- h11-inspired: GET and HEAD should use the same framing headers.
 #eval show IO _ from do
@@ -448,7 +448,7 @@ def notImplemented : String :=
  let (clientD, serverD) ← Mock.new
  let unsupportedTe := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: gzip, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
  let responseD ← sendRaw clientD serverD unsupportedTe (fun req => do
-    let seenTe := match req.head.headers.getAll? Header.Name.transferEncoding with
+    let seenTe := match req.line.headers.getAll? Header.Name.transferEncoding with
      | some values => String.intercalate "|" (values.map (·.value) |>.toList)
      | none => "<none>"
    Response.ok |>.text seenTe)