fix: correct HTTP/1.1 parsing, framing and connection handling

src/Std/Http.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Std.Http.Server
-public import Std.Http.Test.Helpers
+import Std.Http.Test.Helpers
 
 public section
 
@@ -67,13 +67,13 @@ small and large payloads efficiently.
 ### Reading Headers
 
 ```lean
-def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Any) := do
   -- Access request method and URI
-  let method := req.head.method      -- Method.get, Method.post, etc.
-  let uri := req.head.uri            -- RequestTarget
+  let method := req.line.method      -- Method.get, Method.post, etc.
+  let uri := req.line.uri            -- RequestTarget
 
   -- Read a specific header
-  if let some contentType := req.head.headers.get? (.mk "content-type") then
+  if let some contentType := req.line.headers.get? (.mk "content-type") then
     IO.println s!"Content-Type: {contentType}"
 
   Response.ok |>.text "OK"
@@ -83,7 +83,7 @@ def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) :=
 
 `RequestTarget.query` is parsed using form-style key/value conventions (`k=v&...`), and `+` is decoded as a
 space in query components. If you need RFC 3986 opaque query handling, use the raw request target string
-(`toString req.head.uri`) and parse it with custom logic.
+(`toString req.line.uri`) and parse it with custom logic.
 
 ### Reading the Request Body
 
@@ -92,7 +92,7 @@ collected into memory. The `readAll` method reads the entire body, with an optio
 limit to protect against unbounded payloads.
 
 ```lean
-def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Any) := do
   -- Collect entire body as a String
   let bodyStr : String ← req.body.readAll
 
@@ -108,7 +108,8 @@ Responses are constructed using a builder API that starts from a status code and
 headers and a body. Common helpers exist for text, HTML, JSON, and binary responses, while
 still allowing full control over status codes and header values.
 
-Response builders produce `Async (Response Body.Stream)`.
+Response builders produce `Async (Response Body.Full)`, which converts to the `Response Body.Any` a
+handler returns.
 
 ```lean
 -- Text response
@@ -138,7 +139,7 @@ Response.ok
 For large responses or server-sent events, use streaming:
 
 ```lean
-def handler (req : Request Body.Stream) : ContextAsync (Response Body.Stream) := do
+def handler (req : Request Body.Stream) : ContextAsync (Response Body.Any) := do
   Response.ok
     |>.header! "Content-Type" "text/plain"
     |>.stream fun stream => do

src/Std/Http/Data/Body/Full.lean

@@ -178,8 +178,19 @@ instance : Coe (Async (Response Full)) (ContextAsync (Response Any)) where
 
 end Body
 
+/--
+Adds `Content-Type: value` unless `headers` already has a `Content-Type`, so a type the caller chose
+is not followed by a second, default one.
+-/
+private def Headers.withDefaultContentType (headers : Headers) (value : String) : Headers :=
+  if headers.contains Header.Name.contentType then headers
+  else headers.insert Header.Name.contentType (Header.Value.ofString! value)
+
 namespace Request.Builder
 
+private def defaultContentType (builder : Builder) (value : String) : Builder :=
+  { builder with line.headers := builder.line.headers.withDefaultContentType value }
+
 open Async
 
 /--
@@ -191,36 +202,40 @@ def fromBytes (builder : Builder) (content : ByteArray) : Async (Request Body.Fu
 
 /--
 Builds a request with a binary body.
-Sets `Content-Type: application/octet-stream`.
+Sets `Content-Type: application/octet-stream` unless a `Content-Type` was already set.
 Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
 -/
 def bytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
+  fromBytes (builder.defaultContentType "application/octet-stream") content
 
 /--
 Builds a request with a text body.
-Sets `Content-Type: text/plain; charset=utf-8`.
+Sets `Content-Type: text/plain; charset=utf-8` unless a `Content-Type` was already set.
 -/
 def text (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
+  fromBytes (builder.defaultContentType "text/plain; charset=utf-8") content.toUTF8
 
 /--
 Builds a request with a JSON body.
-Sets `Content-Type: application/json`.
+Sets `Content-Type: application/json` unless a `Content-Type` was already set.
 -/
 def json (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
+  fromBytes (builder.defaultContentType "application/json") content.toUTF8
 
 /--
 Builds a request with an HTML body.
-Sets `Content-Type: text/html; charset=utf-8`.
+Sets `Content-Type: text/html; charset=utf-8` unless a `Content-Type` was already set.
 -/
 def html (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
+  fromBytes (builder.defaultContentType "text/html; charset=utf-8") content.toUTF8
 
 end Request.Builder
 
 namespace Response.Builder
+
+private def defaultContentType (builder : Builder) (value : String) : Builder :=
+  { builder with line.headers := builder.line.headers.withDefaultContentType value }
+
 open Async
 
 /--
@@ -232,31 +247,31 @@ def fromBytes (builder : Builder) (content : ByteArray) : Async (Response Body.F
 
 /--
 Builds a response with a binary body.
-Sets `Content-Type: application/octet-stream`.
+Sets `Content-Type: application/octet-stream` unless a `Content-Type` was already set.
 Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
 -/
 def bytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
+  fromBytes (builder.defaultContentType "application/octet-stream") content
 
 /--
 Builds a response with a text body.
-Sets `Content-Type: text/plain; charset=utf-8`.
+Sets `Content-Type: text/plain; charset=utf-8` unless a `Content-Type` was already set.
 -/
 def text (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
+  fromBytes (builder.defaultContentType "text/plain; charset=utf-8") content.toUTF8
 
 /--
 Builds a response with a JSON body.
-Sets `Content-Type: application/json`.
+Sets `Content-Type: application/json` unless a `Content-Type` was already set.
 -/
 def json (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
+  fromBytes (builder.defaultContentType "application/json") content.toUTF8
 
 /--
 Builds a response with an HTML body.
-Sets `Content-Type: text/html; charset=utf-8`.
+Sets `Content-Type: text/html; charset=utf-8` unless a `Content-Type` was already set.
 -/
 def html (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
+  fromBytes (builder.defaultContentType "text/html; charset=utf-8") content.toUTF8
 
 end Response.Builder

src/Std/Http/Data/Body/Stream.lean

@@ -458,7 +458,7 @@ context is cancelled).
 -/
 partial def readAll
     [FromByteArray α]
-    [Monad m] [MonadExceptOf IO.Error m] [NextChunk m]
+    [Monad m] [MonadExceptOf IO.Error m] [MonadLiftT Async m] [NextChunk m]
     (stream : Stream)
     (maximumSize : Option UInt64 := none) :
     m α := do
@@ -470,6 +470,7 @@ partial def readAll
       let result := result ++ chunk.data
       if let some max := maximumSize then
         if result.size.toUInt64 > max then
+          (stream.close : Async Unit)
           throw (.userError s!"body exceeded maximum size of {max} bytes")
       loop result
 

src/Std/Http/Data/Headers/Basic.lean

@@ -133,7 +133,7 @@ Reference: https://www.rfc-editor.org/rfc/rfc9112#section-6.1
 structure TransferEncoding where
 
   /--
-  The ordered list of transfer codings.
+  The ordered list of transfer coding names, lowercased and without their parameters.
   -/
   codings : Array String
 
@@ -153,15 +153,55 @@ def isChunked (te : TransferEncoding) : Bool :=
   te.codings.back? == some "chunked"
 
 /--
-Parses a comma-separated list of transfer codings from a header value, validating chunked placement.
+Checks a transfer parameter: `token BWS "=" BWS ( token / quoted-string )` (RFC 9112 §7).
+-/
+private def isTransferParameter (param : String) : Bool :=
+  match param.split '=' |>.toStringList with
+  | name :: value@(_ :: _) =>
+    let value := ("=".intercalate value).trimAscii.toString
+    isToken name.trimAscii.toString && !value.isEmpty && (unquoteHttpString? value).isSome
+  | _ => false
+
+/--
+Parses a comma-separated list of transfer codings into their lowercased names, without the chunked
+placement rules of `parse`.
+
+Transfer parameters (`gzip;level=1`) are checked and dropped. `chunked` defines none, so a list in
+which `chunked` has one is rejected. A quoted parameter value that contains `,` or `;` is not
+supported.
+-/
+def parseCodings? (v : Value) : Option (Array String) :=
+  (v.value.split ',' |>.toStringList).toArray.mapM fun element => do
+    let name :: params := element.split ';' |>.toStringList | none
+    let name := name.trimAscii.toString.toLower
+    guard (isToken name && params.all isTransferParameter)
+    guard (params.isEmpty || name != "chunked")
+    return name
+
+/--
+Parses a comma-separated list of transfer codings from a header value (`parseCodings?`), validating
+chunked placement. Transfer parameters are accepted and dropped.
 -/
 def parse (v : Value) : Option TransferEncoding := do
-  let codings ← parseTokenList v
+  let codings ← parseCodings? v
   if h : TransferEncoding.Validate codings then
     some ⟨codings, h⟩
   else
     none
 
+/--
+Classifies a `Transfer-Encoding` value by its final coding, which decides how the message is framed
+(RFC 9112 §6.3): `some true` when it ends in `chunked` applied once, `some false` when it ends in
+another coding, and `none` when it is not a list of transfer codings (`parseCodings?`) or ends in a
+`chunked` applied more than once.
+-/
+def finalCodingIsChunked? (v : Value) : Option Bool := do
+  let codings ← parseCodings? v
+  if codings.back? != some "chunked" then
+    return false
+  guard (codings.count "chunked" == 1)
+  return true
+
 /--
 Serializes a transfer encoding back to a comma-separated header value.
 -/

src/Std/Http/Data/Method.lean

@@ -355,6 +355,15 @@ Reference: https://httpwg.org/specs/rfc9110.html#safe.methods
 def isSafe (m : Method) : Bool :=
   m == .get || m == .head || m == .options || m == .trace
 
+/--
+Returns `false` for the methods whose semantics anticipate no request content: those RFC 9110 §8.6
+tells a user agent not to send `Content-Length` for when the request carries none.
+
+Reference: https://httpwg.org/specs/rfc9110.html#field.content-length
+-/
+def anticipatesContent (m : Method) : Bool :=
+  !(m == .get || m == .head || m == .delete || m == .options || m == .trace || m == .connect)
+
 instance : ToString Method where
   toString
     | .acl => "ACL"

src/Std/Http/Data/Status.lean

@@ -590,6 +590,19 @@ Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 def isInformational (c : Status) : Bool :=
   100 ≤ c.toCode ∧ c.toCode < 200
 
+/--
+Checks if the status code is an *interim* response: one that precedes a final response, so a client
+that receives it keeps reading the same exchange.
+
+This is every informational status except `101 Switching Protocols`, after which the connection
+speaks another protocol (RFC 9110 §15.2.2), so no final response follows.
+
+Reference: https://httpwg.org/specs/rfc9110.html#status.101
+-/
+@[inline]
+def isInterim (c : Status) : Bool :=
+  c.isInformational ∧ c.toCode != 101
+
 /--
 Checks if the status code is a success status, meaning that the request was successfully received,
 understood, and accepted.

src/Std/Http/Internal/Char.lean

@@ -132,12 +132,15 @@ theorem not_quotedStringChar_of_not_qdtext_not_dquote_backslash :
       c.toNat hlt (by simpa [Char.ofNat_toNat] using hq))
 
 /--
-field-vchar = VCHAR
-; ASCII-only variant (no obs-text).
+field-vchar = VCHAR / obs-text
+
+obs-text (bytes `%x80-FF`) is accepted, as RFC 9110 §5.5 asks of recipients: servers routinely send
+raw UTF-8 in fields such as `Location` and `Content-Disposition`. In a `String` it appears as the
+characters from U+0080 up. Control characters, including CR, LF, and NUL, are never field content.
 -/
 @[inline]
 def fieldVchar (c : Char) : Bool :=
-  vchar c
+  vchar c || c.val ≥ 0x80
 
 /--
 field-content character class:
@@ -197,14 +200,13 @@ def obsText (c : Char) : Bool :=
 
 /--
 reason-phrase character class:
-HTAB / SP / VCHAR
-; ASCII-only variant (no obs-text).
+HTAB / SP / VCHAR / obs-text
 
 Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase
 -/
 @[inline]
 def reasonPhraseChar (c : Char) : Bool :=
-  (c matches '\t' | ' ') || vchar c
+  (c matches '\t' | ' ') || vchar c || c.val ≥ 0x80
 
 /--
 Checks if a character is a hexadecimal digit (0-9, a-f, or A-F).