From dbe1524591c29536350363c5fa8863c02d342aef Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 5 Nov 2026 11:00:20 -0300 Subject: [PATCH 1/5] fix: correct HTTP/1.1 parsing, framing and connection handling --- src/Std/Http.lean | 19 +- src/Std/Http/Data/Body/Full.lean | 49 +++-- src/Std/Http/Data/Body/Stream.lean | 3 +- src/Std/Http/Data/Headers/Basic.lean | 10 + src/Std/Http/Data/Method.lean | 9 + src/Std/Http/Data/Status.lean | 13 ++ src/Std/Http/Internal/Char.lean | 14 +- src/Std/Http/Protocol/H1.lean | 181 +++++++++++++----- src/Std/Http/Protocol/H1/Config.lean | 7 +- src/Std/Http/Protocol/H1/Parser.lean | 125 ++++++------ tests/async/elab/async_http_body.lean | 44 +++++ tests/async/elab/async_http_exports.lean | 12 ++ .../async_http_h1_client_request_version.lean | 36 ++++ .../elab/async_http_h1_line_limit_split.lean | 34 ++++ .../elab/async_http_h1_rfc_compliance.lean | 179 +++++++++++++++++ .../elab/async_http_h1_short_fixed_body.lean | 46 +++++ 16 files changed, 638 insertions(+), 143 deletions(-) create mode 100644 tests/async/elab/async_http_exports.lean create mode 100644 tests/async/elab/async_http_h1_client_request_version.lean create mode 100644 tests/async/elab/async_http_h1_line_limit_split.lean create mode 100644 tests/async/elab/async_http_h1_short_fixed_body.lean diff --git a/src/Std/Http.lean b/src/Std/Http.lean index 374ed69a951b..ff22577ce5bf 100644 --- a/src/Std/Http.lean +++ b/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 diff --git a/src/Std/Http/Data/Body/Full.lean b/src/Std/Http/Data/Body/Full.lean index 494ae799e55d..b635fb2a5a26 100644 --- a/src/Std/Http/Data/Body/Full.lean +++ b/src/Std/Http/Data/Body/Full.lean @@ -180,6 +180,14 @@ end Body namespace Request.Builder +/-- +Sets `Content-Type` to `value` unless the message being built already has one, so a type the caller +chose is not followed by a second, default one. +-/ +private def defaultContentType (builder : Builder) (value : String) : Builder := + if builder.line.headers.contains Header.Name.contentType then builder + else builder.header Header.Name.contentType (Header.Value.ofString! value) + open Async /-- @@ -191,36 +199,45 @@ 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 + +/-- +Sets `Content-Type` to `value` unless the message being built already has one, so a type the caller +chose is not followed by a second, default one. +-/ +private def defaultContentType (builder : Builder) (value : String) : Builder := + if builder.line.headers.contains Header.Name.contentType then builder + else builder.header Header.Name.contentType (Header.Value.ofString! value) + open Async /-- @@ -232,31 +249,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 diff --git a/src/Std/Http/Data/Body/Stream.lean b/src/Std/Http/Data/Body/Stream.lean index 08225582ea9c..39a6fdc13507 100644 --- a/src/Std/Http/Data/Body/Stream.lean +++ b/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 diff --git a/src/Std/Http/Data/Headers/Basic.lean b/src/Std/Http/Data/Headers/Basic.lean index 09e6dcccc63b..8940b00814eb 100644 --- a/src/Std/Http/Data/Headers/Basic.lean +++ b/src/Std/Http/Data/Headers/Basic.lean @@ -162,6 +162,16 @@ def parse (v : Value) : Option TransferEncoding := do else none +/-- +Parses a comma-separated list of transfer codings without the chunked placement rules. A response's +framing depends only on whether its final coding is `chunked` (RFC 9112 §6.3 rule 4), whatever the +other codings are. +-/ +def parseCodings? (v : Value) : Option (Array String) := do + let codings ← parseTokenList v + guard (codings.all isToken) + return codings + /-- Serializes a transfer encoding back to a comma-separated header value. -/ diff --git a/src/Std/Http/Data/Method.lean b/src/Std/Http/Data/Method.lean index c0bc4d4c8ca0..5f854cd73b05 100644 --- a/src/Std/Http/Data/Method.lean +++ b/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" diff --git a/src/Std/Http/Data/Status.lean b/src/Std/Http/Data/Status.lean index e193dcc14367..241cafebb48c 100644 --- a/src/Std/Http/Data/Status.lean +++ b/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. diff --git a/src/Std/Http/Internal/Char.lean b/src/Std/Http/Internal/Char.lean index bc72d7520330..24da881a5e7e 100644 --- a/src/Std/Http/Internal/Char.lean +++ b/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). diff --git a/src/Std/Http/Protocol/H1.lean b/src/Std/Http/Protocol/H1.lean index 9ec39325f4ce..790c1ea45e54 100644 --- a/src/Std/Http/Protocol/H1.lean +++ b/src/Std/Http/Protocol/H1.lean @@ -110,11 +110,6 @@ structure Machine (dir : Direction) where -/ keepAlive : Bool := config.enableKeepAlive - /-- - Whether a forced flush has been requested by the user. - -/ - forcedFlush : Bool := false - /-- Set when a previous `pullBody` call could not make progress in `.readBody`. Cleared on new input or state reset. @@ -334,33 +329,43 @@ private def hasFramingHeaders (message : Message.Head dir) : Bool := name == Header.Name.contentLength || name == Header.Name.transferEncoding /-- -Validates an outgoing response head and selects body framing mode. - -For status codes that must not carry a response body, framing headers are still -syntactically validated but the machine always uses `.fixed 0` framing. +Returns `true` when a response's only transfer coding field ends in a coding other than `chunked` +and no `Content-Length` competes with it. RFC 9112 §6.3 rule 4: such a body has no length of its +own and runs until the server closes the connection. -/ -private def checkSendingMessageHead (message : Message.Head .sending) : Except H1.Error BodyMode := - let framingInHeaders := hasFramingHeaders message +private def hasCloseDelimitedCoding (message : Message.Head .sending) : Bool := + message.version == .v11 && !message.headers.contains Header.Name.contentLength && + match message.headers.getAll? Header.Name.transferEncoding with + | some #[value] => + (Header.TransferEncoding.parseCodings? value).any (·.back? != some "chunked") + | _ => false - let parsedSize := message.getSize false +/-- +Validates an incoming response head, answering a request with `requestMethod`, and selects its body +framing mode. - if responseMustNotHaveBody message.status then - match parsedSize with - | some _ => pure (.fixed 0) - | none => if framingInHeaders then throw .badMessage else pure (.fixed 0) +RFC 9112 §6.3 rule 1: a response to `HEAD`, and every 1xx, 204 and 304 response, ends at the header +block whatever its framing fields say, so those fields are not validated. +-/ +private def checkSendingMessageHead (requestMethod : Method) (message : Message.Head .sending) : + Except H1.Error BodyMode := + if requestMethod == .head || responseMustNotHaveBody message.status then + pure (.fixed 0) else - match parsedSize with + match message.getSize false with | some (.fixed n) => pure (.fixed n) | some .chunked => pure .chunked - | none => if framingInHeaders then throw .badMessage else pure .eof + | none => + if !hasFramingHeaders message || hasCloseDelimitedCoding message then pure .eof + else throw .badMessage /-- -Direction-dispatched message-head validation. +Direction-dispatched validation of the message head the reader just finished. -/ -private def checkMessageHead (message : Message.Head dir) : Except H1.Error BodyMode := +private def checkMessageHead (machine : Machine dir) : Except H1.Error BodyMode := match dir with - | .receiving => checkReceivingMessageHead message - | .sending => checkSendingMessageHead message + | .receiving => checkReceivingMessageHead machine.reader.messageHead + | .sending => checkSendingMessageHead machine.writer.messageHead.method machine.reader.messageHead /-- Returns `true` when an `Expect` header includes `100-continue`. @@ -377,16 +382,27 @@ private def hasExpectContinue (message : Message.Head dir) : Bool := | some #[value] => Header.Expect.parse value |>.isSome | _ => false +/-- +The `Transfer-Encoding` value for a chunked message: the caller's own field when it ends in +`chunked` (`gzip, chunked`), since the body bytes were coded for it, and `chunked` otherwise. +-/ +private def chunkedCodings (headers : Headers) : Header.Value := + match headers.getAll? Header.Name.transferEncoding with + | some #[value] => + if (Header.TransferEncoding.parse value).any (·.isChunked) then value else .mk "chunked" + | _ => .mk "chunked" + /-- Builds canonical framing headers for a chosen transfer mode. The caller handles status/method exceptions that should skip normalization. -/ @[inline] private def normalizeFramingHeaders (headers : Headers) (size : Body.Length) : Headers := + let codings := chunkedCodings headers let headers := headers.erase Header.Name.contentLength |>.erase Header.Name.transferEncoding match size with | .fixed n => headers.insert Header.Name.contentLength (.ofString! <| toString n) - | .chunked => headers.insert Header.Name.transferEncoding (.mk "chunked") + | .chunked => headers.insert Header.Name.transferEncoding codings /-- Returns `true` when response status forbids framing headers entirely @@ -397,6 +413,16 @@ private def responseForbidsFramingHeaders (status : Status) : Bool := let code := status.toCode.toNat (100 ≤ code ∧ code < 200) ∨ code = 204 +/-- +Returns `true` when the body being read belongs to an interim (1xx) response. Such a response has no +message body of its own: it is part of an exchange whose final response is still to come. +-/ +@[inline] +private def isInterimResponseBody (machine : Machine dir) : Bool := + match dir with + | .receiving => false + | .sending => machine.reader.messageHead.status.isInterim + /-- Returns `true` when body chunks should be drained internally rather than surfaced to the caller. -/ @@ -404,7 +430,7 @@ Returns `true` when body chunks should be drained internally rather than surface private def drainBodyInternally (machine : Machine dir) : Bool := match dir with | .receiving => machine.writer.sentMessage - | .sending => machine.reader.messageHead.status.isInformational + | .sending => machine.isInterimResponseBody /-- Builds the externally exposed `PulledChunk` value from parsed body bytes. @@ -549,7 +575,9 @@ state transitions. - On success, advances reader input. - On EOF with open input, emits `needMoreData`. - On EOF after `noMoreInput`, fails with `connectionClosed`. -- On hard parse errors or size-limit breaches, fails with `onHardError`. +- On a size-limit breach, fails with `badMessage`. A hard parse error found at or past the limit + counts as a breach, so the outcome does not depend on how the input was split. +- On other hard parse errors, fails with `onHardError`. -/ private def parseWith (machine : Machine dir) (parser : Parser α) (limit : Option Nat) (expect : Option Nat := none) @@ -578,8 +606,11 @@ private def parseWith (machine : Machine dir) (parser : Parser α) (limit : Opti else (machine.addEvent (.needMoreData expect), none) else (machine.addEvent (.needMoreData expect), none) - | .error _ err => - (machine.setFailure (onHardError err), none) + | .error it err => + if limit.any (remaining - it.remainingBytes ≥ ·) then + (machine.setFailure .badMessage, none) + else + (machine.setFailure (onHardError err), none) -- Message Processing @@ -669,17 +700,6 @@ private def advanceAfterHeaders (machine : Machine dir) (state : Reader.State di | .receiving, nextState, machine => machine.setReaderState nextState |>.setWriterState .waitingHeaders |>.addEvent .needAnswer | .sending, nextState, machine => machine.setReaderState nextState -/-- -HEAD responses have no body, regardless of any framing headers. Override the -framing mode to `.fixed 0` so the reader doesn't block waiting for body bytes. --/ -@[inline] -private def suppressIncomingBodyIfHead (machine : Machine dir) (mode : BodyMode) : BodyMode := - match dir with - | .sending => - if machine.writer.messageHead.method == .head then .fixed 0 else mode - | .receiving => mode - /-- Processes a finished header block: 1. updates keep-alive policy from config and headers, @@ -691,20 +711,34 @@ private def processHeaders (machine : Machine dir) : Machine dir := let machine := machine.updateKeepAlive (machine.reader.messageCount + 1 < machine.config.maxMessages) let machine := machine.updateKeepAlive machine.reader.messageHead.shouldKeepAlive - match checkMessageHead machine.reader.messageHead with + match checkMessageHead machine with | .error err => machine.setFailure err | .ok mode => - let mode := suppressIncomingBodyIfHead machine mode if exceedsBodyLimitForMode machine mode then machine.setFailure .entityTooLarge else let (machine, state) := readerStateForMode machine mode advanceAfterHeaders machine state +/-- +The connection options of a handler's `Connection` fields other than `close` and `keep-alive`, which +the machine decides itself. +-/ +private def handlerConnectionOptions (headers : Headers) : Array String := + match headers.getAll? Header.Name.connection with + | none => #[] + | some values => + values.foldl (init := #[]) fun acc value => + match Header.Connection.parse value with + | some connection => + acc ++ connection.tokens.filter (fun t => t != "close" && t != "keep-alive") + | none => acc + /-- Encodes a server response head. The handler's fields are written in order without `Connection`, `Content-Length` and `Transfer-Encoding`, then `Server` unless the handler set one, then the -`Connection` and framing fields the machine chose. +`Connection` and framing fields the machine chose. The handler's own connection options (such as +`upgrade`) go in that `Connection` field, before the machine's `close` or `keep-alive`. -/ private def encodeServerHead (head : Response.Head) (version : Version) (keepAlive : Bool) (agentName : Option Header.Value) (size : Body.Length) : ByteArray := @@ -722,8 +756,16 @@ private def encodeServerHead (head : Response.Head) (version : Version) (keepAli if head.headers.contains Header.Name.server then out else appendFieldLine out Header.Name.server server | none => out + -- RFC 9110 §7.8: a response that sends `Upgrade` must also send the `upgrade` connection option. + let options := handlerConnectionOptions head.headers let out : ByteArray := - if !keepAlive then + if !options.isEmpty then + let options := + if !keepAlive then options.push "close" + else if version == .v10 then options.push "keep-alive" + else options + out ++ "Connection: " ++ ", ".intercalate options.toList ++ "\r\n" + else if !keepAlive then out ++ "Connection: close\r\n" else if version == .v10 then -- RFC 2616 §19.7.1: HTTP/1.0 keep-alive responses must echo Connection: keep-alive @@ -738,7 +780,9 @@ private def encodeServerHead (head : Response.Head) (version : Version) (keepAli else match size with | .fixed n => out ++ "Content-Length: " ++ n ++ "\r\n" - | .chunked => if version == .v10 then out else out ++ "Transfer-Encoding: chunked\r\n" + | .chunked => + if version == .v10 then out + else appendFieldLine out Header.Name.transferEncoding (chunkedCodings head.headers) out ++ "\r\n" /-- @@ -796,11 +840,19 @@ private def writeHead (messageHead : Message.Head dir.swap) (machine : Machine d let headers := if !keepAlive then headers.insert Header.Name.connection (.mk "close") - else if version == .v10 then + -- The request's own version: the reader may already hold the next response's status line. + else if messageHead.version == .v10 then headers.insert Header.Name.connection (.mk "keep-alive") else headers - let headers := normalizeFramingHeaders headers size + -- RFC 9110 §8.6: no `Content-Length` on a request without content whose method anticipates + -- none, unless the caller set a framing field. + let headers := + if size == .fixed 0 ∧ !messageHead.method.anticipatesContent ∧ + !hasFramingHeaders messageHead then + headers + else + normalizeFramingHeaders headers size outputData.push (ByteArray.empty ++ ({ messageHead with headers } : Request.Head)) machine.modifyWriter (fun writer => { writer with outputData, state }) @@ -908,6 +960,11 @@ private def maybeSuppressOutgoingBody (machine : Machine dir) (message : Message let suppressByMethod := machine.reader.messageHead.method == .head let forceZero := responseForbidsFramingHeaders message.status if suppressByStatus ∨ suppressByMethod then + -- RFC 9110 §9.3.2: a HEAD response has the framing fields GET would have. With no known + -- length that is chunked framing, not the `Content-Length: 0` of a body closed empty. + let machine := + if ¬suppressByStatus ∧ machine.writer.knownSize.isNone then machine.setKnownSize .chunked + else machine machine.suppressOutgoingBody (forceZero := forceZero) else machine @@ -925,10 +982,10 @@ Send the head of a message to the machine. Must only be called when `machine.isWaitingMessage` is true. If called in any other state (e.g. called twice), the machine panics. -Informational (1xx) responses are written directly to the output buffer; the writer -stays in `waitingHeaders` so the application can send additional interim responses or -the final response. The reader state is not affected — use `canContinue` to resolve -an `Expect: 100-continue` decision separately. +Informational (1xx) responses are written directly to the output buffer, or dropped when the +request is HTTP/1.0; the writer stays in `waitingHeaders` so the application can send additional +interim responses or the final response. The reader state is not affected — use `canContinue` to +resolve an `Expect: 100-continue` decision separately. -/ @[inline] def send (machine : Machine dir) (message : Message.Head dir.swap) : Machine dir := @@ -942,7 +999,10 @@ def send (machine : Machine dir) (message : Message.Head dir.swap) : Machine dir match dir with | .receiving => message.status.isInformational | .sending => false - if isInterim then + -- RFC 9110 §15.2: a server must not send a 1xx response to an HTTP/1.0 client. + if isInterim ∧ machine.reader.messageHead.version != .v11 then + machine + else if isInterim then -- RFC 9110 §15.2: 1xx responses MUST NOT carry a body, so framing headers -- are meaningless and must not be forwarded even if the handler set them. let message := Message.Head.setHeaders message @@ -1153,6 +1213,10 @@ private partial def processFixedBufferedBody (machine : Machine dir) (n : Nat) : machine.setWriterState (.writingBodyFixed 0) else closeOnBadMessage machine + else if writer.userClosedBody then + -- The producer finished short of the declared length. Reported in this step, since the caller + -- may have no other reason to step the machine again. + closeOnBadMessage machine else machine.setWriterState (.writingBodyFixed remaining) @@ -1311,6 +1375,8 @@ Common body-chunk emission helper. Updates size accounting and reader state, optionally emits `.closeBody`, and returns an optional pulled chunk (suppressed when body is being internally drained). + +`.closeBody` is withheld for interim responses: the body that follows belongs to the final response. -/ private def emitBodyChunk (machine : Machine dir) (nextState : Reader.State dir) @@ -1327,7 +1393,8 @@ private def emitBodyChunk (machine : Machine dir) let machine := machine |>.addBodyBytes bodySize |>.setReaderState nextState - let machine := if closeBody then machine.addEvent .closeBody else machine + let machine := + if closeBody ∧ ¬machine.isInterimResponseBody then machine.addEvent .closeBody else machine (machine, mkPulledChunk? machine final incomplete extensions data, true) /-- @@ -1381,7 +1448,11 @@ ends the section finalizes chunked body processing. private def parseTrailerState (machine : Machine dir) (ext : Array (Chunk.ExtensionName × Option Chunk.ExtensionValue)) (count : Nat) : Machine dir × Option PulledChunk × Bool := - let (machine, result) := parseWith machine (parseTrailerHeader machine.config) (limit := none) + -- A server rejects every field forbidden in a request's trailers; a client, which discards + -- trailers, only refuses those that would reframe the response. + let strict := match dir with | .receiving => true | .sending => false + let (machine, result) := + parseWith machine (parseTrailerHeader machine.config strict) (limit := none) match result with | some (some _) => if count ≥ machine.config.maxTrailerHeaders then @@ -1609,7 +1680,7 @@ private partial def processReaderCompleteState (machine : Machine dir) : Machine -- RFC 9110 §15.2: 1xx responses are not final; they must not count against the -- maxMessages quota (messageCount is not incremented here). - if machine.reader.messageHead.status.isInformational then + if machine.reader.messageHead.status.isInterim then { machine with reader := { state := .needStartLine, input := reader.input, @@ -1619,6 +1690,10 @@ private partial def processReaderCompleteState (machine : Machine dir) : Machine headerBytesRead := 0, noMoreInput := reader.noMoreInput }} + -- RFC 9110 §15.2.2: after `101 Switching Protocols` the connection speaks another protocol, so + -- the bytes that follow are not HTTP/1.1 and the connection cannot be reused. + else if machine.reader.messageHead.status.toCode == 101 then + machine.disableKeepAlive.setReaderState .closed else if (reader.noMoreInput ∧ reader.input.atEnd) ∨ ¬machine.keepAlive then machine.setReaderState .closed else diff --git a/src/Std/Http/Protocol/H1/Config.lean b/src/Std/Http/Protocol/H1/Config.lean index d4a7593e82a7..1106fae84f5b 100644 --- a/src/Std/Http/Protocol/H1/Config.lean +++ b/src/Std/Http/Protocol/H1/Config.lean @@ -114,9 +114,10 @@ structure Config where /-- Maximum allowed total body size per message in bytes (default: 64 MiB). - This limit applies across all body framing modes. For chunked transfer encoding, - chunk-size lines (including extensions) and the trailer section also count toward - this limit, so the total wire bytes consumed by the body cannot exceed this value. + This limit applies across all body framing modes and counts content bytes only. For chunked + transfer encoding, chunk-size lines and the trailer section do not count toward it: each + chunk-size line is bounded by `maxChunkLineLength`, and the trailer section by + `maxTrailerHeaders` fields of at most `maxHeaderNameLength` and `maxHeaderValueLength` bytes. -/ maxBodySize : Nat := 64 * 1024 * 1024 diff --git a/src/Std/Http/Protocol/H1/Parser.lean b/src/Std/Http/Protocol/H1/Parser.lean index 26fde7da3351..d87f31675031 100644 --- a/src/Std/Http/Protocol/H1/Parser.lean +++ b/src/Std/Http/Protocol/H1/Parser.lean @@ -10,6 +10,7 @@ public import Std.Internal.Parsec public import Std.Http.Data public import Std.Internal.Parsec.ByteArray public import Std.Http.Protocol.H1.Config +import Init.Data.String.Lossy /-! This module defines parsers for HTTP/1.1 request and response lines, headers, and body framing. The @@ -25,8 +26,7 @@ set_option linter.all true /-- Checks if a byte may appear inside a field value. -This parser enforces strict ASCII-only field values and allows only `field-content` -(`HTAB / SP / VCHAR`). +Allows `field-content`: `HTAB / SP / VCHAR / obs-text`. -/ @[inline] def isFieldVChar (c : UInt8) : Bool := @@ -67,9 +67,14 @@ def optionalUnlessEof (p : Parser α) : Parser (Option α) := fun it => /-- Repeatedly applies `parser` until it returns `none` or the `maxCount` limit is exceeded. Returns the collected results as an array. + +A `parser` that fails on exhausted input propagates that failure, so an item split across two reads +is re-parsed once the rest arrives instead of ending the list early. -/ -partial def manyItems {α : Type} (parser : Parser (Option α)) (maxCount : Nat) : Parser (Array α) := do - let rec go (acc : Array α) : Parser (Array α) := do +def manyItems {α : Type} (parser : Parser (Option α)) (maxCount : Nat) : Parser (Array α) := + go #[] +where + go (acc : Array α) : Parser (Array α) := do let step ← optionalUnlessEof do match ← parser with | none => fail "end of items" @@ -79,13 +84,12 @@ partial def manyItems {α : Type} (parser : Parser (Option α)) (maxCount : Nat) | none => return acc | some x => - let acc := acc.push x - - if acc.size > maxCount then - fail s!"too many items: {acc.size} > {maxCount}" - - go acc - go #[] + if acc.size + 1 > maxCount then + fail s!"too many items: {acc.size + 1} > {maxCount}" + else + go (acc.push x) + termination_by maxCount - acc.size + decreasing_by simp only [Array.size_push]; omega /-- @@ -164,8 +168,10 @@ def hexDigit : Parser UInt8 := do Parses a hexadecimal integer (one or more hex digits, up to 16 digits). Used for chunk-size lines in chunked transfer encoding. -/ -partial def hex : Parser Nat := do - let rec go (acc : Nat) (count : Nat) : Parser Nat := do +def hex : Parser Nat := + go 0 0 +where + go (acc : Nat) (count : Nat) : Parser Nat := do match ← optional (attempt hexDigit) with | some d => if count + 1 > 16 then @@ -180,7 +186,7 @@ partial def hex : Parser Nat := do fail "expected hex digit" else return acc - go 0 0 + termination_by 16 - count -- Actual parsers @@ -318,7 +324,8 @@ def parseFieldLine (limits : H1.Config) : Parser (String × String) := do let value ← skipByte ':'.toUInt8 *> ows limits *> optional (takeWhileUpTo isFieldVChar limits.maxHeaderValueLength) <* ows limits let name ← liftOption <| String.fromUTF8? name.toByteArray - let value ← liftOption <| String.fromUTF8? <| value.map (·.toByteArray) |>.getD .empty + -- obs-text need not be UTF-8; it is kept as opaque data, with any invalid sequence replaced. + let value := String.fromUTF8Lossy <| value.map (·.toByteArray) |>.getD .empty let value := value.trimAsciiEnd.toString return (name, value) @@ -358,10 +365,11 @@ Parses a quoted-string value, unescaping quoted-pairs. `quoted-string = DQUOTE *( qdtext / quoted-pair ) DQUOTE` -/ -partial def parseQuotedString (maxLength : Nat) : Parser String := do +def parseQuotedString (maxLength : Nat) : Parser String := do skipByte '"'.toUInt8 - - let rec loop (buf : ByteArray) (length : Nat) : Parser ByteArray := do + liftOption <| String.fromUTF8? (← loop .empty 0) +where + loop (buf : ByteArray) (length : Nat) : Parser ByteArray := do let b ← any if b == '"'.toUInt8 then @@ -370,22 +378,19 @@ partial def parseQuotedString (maxLength : Nat) : Parser String := do let next ← any if quotedPairChar (Char.ofUInt8 next) then - let length := length + 1 - if length > maxLength then + if length + 1 > maxLength then fail "quoted-string too long" else - loop (buf.push next) length + loop (buf.push next) (length + 1) else fail s!"invalid quoted-pair byte: {Char.ofUInt8 next |>.quote}" else if isQdText b then - let length := length + 1 - if length > maxLength then + if length + 1 > maxLength then fail "quoted-string too long" else - loop (buf.push b) length + loop (buf.push b) (length + 1) else fail s!"invalid qdtext byte: {Char.ofUInt8 b |>.quote}" - - liftOption <| String.fromUTF8? (← loop .empty 0) + termination_by maxLength - length -- chunk-ext = *( BWS ";" BWS chunk-ext-name [ BWS "=" BWS chunk-ext-val] ) def parseChunkExt (limits : H1.Config) : Parser (Chunk.ExtensionName × Option Chunk.ExtensionValue) := do @@ -414,7 +419,7 @@ Parses the size and extensions of a chunk. -/ public def parseChunkSize (limits : H1.Config) : Parser (Nat × Array (Chunk.ExtensionName × Option Chunk.ExtensionValue)) := do let size ← hex - let ext ← manyItems (optionalUnlessEof (parseChunkExt limits)) limits.maxChunkExtensions + let ext ← manyItems (some <$> parseChunkExt limits) limits.maxChunkExtensions crlf return (size, ext) @@ -455,28 +460,40 @@ public def parseChunkSizedData (size : Nat) : Parser TakeResult := do | .complete data => crlf *> return .complete data | .incomplete data res => return .incomplete data res +/-- +Returns `true` if `name` (compared case-insensitively) frames or routes a message +(`content-length`, `transfer-encoding`, `host`, `connection`, `te`, `upgrade`, `trailer`). In a +trailer section such a field is an attempt to reframe the message after the fact, which a downstream +proxy might act on, so the message is rejected. +-/ +def isFramingTrailerField (name : String) : Bool := + let n := name.toLower + n == "content-length" || n == "transfer-encoding" || n == "host" || + n == "connection" || n == "te" || n == "upgrade" || n == "trailer" + /-- Returns `true` if `name` (compared case-insensitively) is a field that MUST NOT appear in HTTP/1.1 -trailer sections per RFC 9112 §6.5. Forbidden fields are those required for message framing -(`content-length`, `transfer-encoding`), routing (`host`), or connection management (`connection`). +trailer sections per RFC 9112 §6.5: the framing and routing fields of `isFramingTrailerField`, and +fields that control how the message is processed (`expect`, `authorization`, `max-forwards`, +`cache-control`, `content-encoding`). -/ def isForbiddenTrailerField (name : String) : Bool := let n := name.toLower - n == "content-length" || n == "transfer-encoding" || n == "host" || - n == "connection" || n == "expect" || n == "te" || - n == "authorization" || n == "max-forwards" || n == "cache-control" || - n == "content-encoding" || n == "upgrade" || n == "trailer" + isFramingTrailerField name || n == "expect" || + n == "authorization" || n == "max-forwards" || n == "cache-control" || n == "content-encoding" /-- -Parses a trailer header (used after a chunked body), rejecting forbidden field names per RFC 9112 -§6.5. Fields used for message framing (`content-length`, `transfer-encoding`), routing (`host`), -or connection management (`connection`, `te`, `upgrade`) are rejected to prevent trailer injection -attacks where a downstream proxy might re-interpret them. +Parses a trailer header (used after a chunked body). Framing and routing fields +(`isFramingTrailerField`) are always rejected, to prevent trailer injection attacks where a +downstream proxy might re-interpret them. With `strict`, every field forbidden in trailers is +rejected; without it, the others are parsed and left for the caller to drop, since RFC 9110 §6.5.1 +asks recipients not to merge them rather than to reject a message that is otherwise complete. -/ -public def parseTrailerHeader (limits : H1.Config) : Parser (Option (String × String)) := do +public def parseTrailerHeader (limits : H1.Config) (strict : Bool := true) : + Parser (Option (String × String)) := do let result ← parseSingleHeader limits if let some (name, _) := result then - if isForbiddenTrailerField name then + if isFramingTrailerField name || (strict && isForbiddenTrailerField name) then fail s!"forbidden trailer field: {name}" return result @@ -493,7 +510,7 @@ public def parseTrailers (limits : H1.Config) : Parser (Array (String × String) return trailers /-- -Returns `true` if `c` is a valid reason-phrase byte (`HTAB / SP / VCHAR`, strict ASCII-only). +Returns `true` if `c` is a valid reason-phrase byte (`HTAB / SP / VCHAR / obs-text`). -/ @[inline] def isReasonPhraseByte (c : UInt8) : Bool := @@ -502,11 +519,12 @@ def isReasonPhraseByte (c : UInt8) : Bool := /-- Parses a reason phrase (text after status code). -Allows only `HTAB / SP / VCHAR` bytes (strict ASCII-only). +Allows `HTAB / SP / VCHAR / obs-text` bytes. A client ignores the phrase (RFC 9112 §4), so bytes +that are not UTF-8 are replaced rather than rejected. -/ def parseReasonPhrase (limits : H1.Config) : Parser String := do let bytes ← takeWhileUpTo isReasonPhraseByte limits.maxReasonPhraseLength - liftOption <| String.fromUTF8? bytes.toByteArray + return String.fromUTF8Lossy bytes.toByteArray /-- Parses a status-code (3 decimal digits), the following reason phrase, and the @@ -517,8 +535,9 @@ def parseStatusCode (limits : H1.Config) : Parser Status := do let d2 ← digit let d3 ← digit let code := (d1.toNat - 48) * 100 + (d2.toNat - 48) * 10 + (d3.toNat - 48) - sp - let phrase ← parseReasonPhrase limits <* crlf + -- Servers that send no reason phrase often leave out the space before it too. + let phrase := (← optional (sp *> parseReasonPhrase limits)).getD "" + crlf if h : IsValidReasonPhrase phrase then if let some status := Status.ofCode (some ⟨phrase, h⟩) code.toUInt16 then @@ -529,13 +548,13 @@ def parseStatusCode (limits : H1.Config) : Parser Status := do /-- Parses a status line and returns a fully-typed `Response.Head`. `status-line = HTTP-version SP status-code SP [ reason-phrase ]` -Accepts only HTTP/1.1. For parsing where the version may be unrecognized and must be -mapped to an error event, use `parseStatusLineRawVersion`. +Accepts only HTTP/1.x, read as HTTP/1.1 for any minor version above 1. For parsing where the version +may be unrecognized and must be mapped to an error event, use `parseStatusLineRawVersion`. -/ public def parseStatusLine (limits : H1.Config) : Parser Response.Head := do let (major, minor) ← parseHttpVersionNumber <* sp let status ← parseStatusCode limits - if major == 1 ∧ minor == 1 then + if major == 1 ∧ minor ≥ 1 then return { status, version := .v11, headers := .empty } else if major == 1 ∧ minor == 0 then return { status, version := .v10, headers := .empty } @@ -546,18 +565,14 @@ public def parseStatusLine (limits : H1.Config) : Parser Response.Head := do Parses a status line and returns the status code plus recognized HTTP version when available. Consumes and discards the reason phrase. +RFC 9110 §2.5: a response with a higher minor version than HTTP/1.1 (`HTTP/1.2`) is processed as +HTTP/1.1, the highest minor version this client implements. + status-line = HTTP-version SP status-code SP [ reason-phrase ] CRLF -/ public def parseStatusLineRawVersion (limits : H1.Config) : Parser (Status × Option Version) := do let (major, minor) ← parseHttpVersionNumber <* sp let status ← parseStatusCode limits - return (status, Version.ofNumber? major minor) - -/-- -Parses the trailer section that follows the last chunk size line (`0\r\n`). --/ -public def parseLastChunkBody (limits : H1.Config) : Parser Unit := do - discard <| manyItems (parseTrailerHeader limits) limits.maxTrailerHeaders - crlf + return (status, Version.ofNumber? major (if major == 1 then min minor 1 else minor)) end Std.Http.Protocol.H1 diff --git a/tests/async/elab/async_http_body.lean b/tests/async/elab/async_http_body.lean index 938524ef70aa..883706a74d91 100644 --- a/tests/async/elab/async_http_body.lean +++ b/tests/async/elab/async_http_body.lean @@ -405,6 +405,28 @@ def channelReadAllMaxSize : Async Unit := do #eval channelReadAllMaxSize.block +-- Test Stream.readAll closes the stream when it gives up on `maximumSize`, so the producer's next +-- send fails instead of waiting for a reader that is gone + +def channelReadAllMaxSizeCloses : Async Unit := do + let stream ← Body.mkStream + + let sendTask ← async (t := AsyncTask) <| do + stream.send (Chunk.ofByteArray "abcdefgh".toUTF8) + stream.send (Chunk.ofByteArray "ijkl".toUTF8) + + let failed ← + try + let _ : ByteArray ← stream.readAll (maximumSize := some 4) + pure false + catch _ => + pure true + assert! failed + assert! (← stream.isClosed) + assertThrows (await sendTask) + +#eval channelReadAllMaxSizeCloses.block + -- Test Stream.getKnownSize reflects the value set via setKnownSize def channelKnownSizeRoundtrip : Async Unit := do @@ -688,6 +710,17 @@ def requestBuilderHtml : Async Unit := do #eval requestBuilderHtml.block +-- Test the Request.Builder body helpers keep a Content-Type the caller already set + +def requestBuilderKeepsContentType : Async Unit := do + let req ← Request.post (.originForm! "/api") + |>.header! "Content-Type" "application/vnd.example+json" + |>.json "{}" + let types := (req.line.headers.getAll? Header.Name.contentType).getD #[] + assert! types == #[Header.Value.ofString! "application/vnd.example+json"] + +#eval requestBuilderKeepsContentType.block + -- Test Request.Builder.stream creates a streaming body def requestBuilderStream : Async Unit := do @@ -744,6 +777,17 @@ def responseBuilderJson : Async Unit := do #eval responseBuilderJson.block +-- Test the Response.Builder body helpers keep a Content-Type the caller already set + +def responseBuilderKeepsContentType : Async Unit := do + let res ← Response.ok + |>.header! "Content-Type" "text/markdown; charset=utf-8" + |>.text "# hi" + let types := (res.line.headers.getAll? Header.Name.contentType).getD #[] + assert! types == #[Header.Value.ofString! "text/markdown; charset=utf-8"] + +#eval responseBuilderKeepsContentType.block + -- Test Response.Builder.fromBytes sets body def responseBuilderFromBytes : Async Unit := do diff --git a/tests/async/elab/async_http_exports.lean b/tests/async/elab/async_http_exports.lean new file mode 100644 index 000000000000..39d225d53303 --- /dev/null +++ b/tests/async/elab/async_http_exports.lean @@ -0,0 +1,12 @@ +module + +import Std.Http + +/-! +`import Std.Http` gives the HTTP library, not the helpers its test suite uses: those come from +`import Std.Http.Test.Helpers`. +-/ + +/-- error: Unknown identifier `Std.Http.Internal.Test.mkGet` -/ +#guard_msgs in +#check Std.Http.Internal.Test.mkGet diff --git a/tests/async/elab/async_http_h1_client_request_version.lean b/tests/async/elab/async_http_h1_client_request_version.lean new file mode 100644 index 000000000000..d599b60c4370 --- /dev/null +++ b/tests/async/elab/async_http_h1_client_request_version.lean @@ -0,0 +1,36 @@ +import Std.Http + +open Std Http +open Std.Http.Protocol.H1 + +/-! +A client's request head depends only on the request: the `Connection` field must not change when +the next response's status line (here `HTTP/1.0`) has already arrived when the request is written. +-/ + +def get (method : Method) : Request.Head := + { method, version := .v11, uri := RequestTarget.parse! "/", headers := Headers.empty.insert .host (.mk "a") } + +/-- Sends a GET, reads `first` and `early`, then sends a HEAD; returns the bytes written for it. -/ +def secondRequest (early : ByteArray) : ByteArray := Id.run do + let mut m : Machine .sending := { config := {} } + m := m.send (get .get) |>.userClosedBody + let (m1, _) := m.step + m := m1.feed ("HTTP/1.1 204 No Content\r\n\r\n".toUTF8 ++ early) + for _ in [0:4] do + m := m.step.1 + m := m.send (get .head) |>.userClosedBody + let mut out := ByteArray.empty + for _ in [0:4] do + let (m', res) := m.step + m := m' + out := out ++ res.output.toByteArray + return out + +#eval show IO Unit from do + let late := secondRequest .empty + let early := secondRequest "HTTP/1.0 200 OK\r\n".toUTF8 + unless late == early do + throw <| IO.userError s!"request head changed: {(String.fromUTF8! late).quote} vs {(String.fromUTF8! early).quote}" + unless late == "HEAD / HTTP/1.1\r\nHost: a\r\n\r\n".toUTF8 do + throw <| IO.userError s!"unexpected request head: {(String.fromUTF8! late).quote}" diff --git a/tests/async/elab/async_http_h1_line_limit_split.lean b/tests/async/elab/async_http_h1_line_limit_split.lean new file mode 100644 index 000000000000..11bfed56d974 --- /dev/null +++ b/tests/async/elab/async_http_h1_line_limit_split.lean @@ -0,0 +1,34 @@ +import Std.Http + +open Std Http +open Std.Http.Protocol.H1 + +/-! +A request line over a limit fails the same way however its bytes arrive: an error found at or past +`maxStartLineLength` is reported as that limit, as it is when the limit is reached before the error. +-/ + +def errorOf (config : Protocol.H1.Config) (parts : Array ByteArray) : Option Error := Id.run do + let mut m : Machine .receiving := { config } + for p in parts do + m := m.feed p + m := m.step.1 + return m.error + +def bytewise (data : ByteArray) : Array ByteArray := + (Array.range data.size).map fun i => data.extract i (i + 1) + +#eval show IO Unit from do + let line := s!"OPTIONS /{String.ofList (List.replicate 30 'a')} HTTP/1.1\r\nHost: a\r\n\r\n".toUTF8 + -- The URI limit is reached past the start-line limit: both ways report the start-line limit. + let config : Protocol.H1.Config := { maxStartLineLength := 20, maxUriLength := 16 } + let whole := errorOf config #[line] + let pieces := errorOf config (bytewise line) + unless whole == pieces && whole == some .badMessage do + throw <| IO.userError s!"start-line limit: whole {repr whole}, pieces {repr pieces}" + -- The URI limit is reached first: both ways report it. + let config : Protocol.H1.Config := { maxStartLineLength := 64, maxUriLength := 16 } + let whole := errorOf config #[line] + let pieces := errorOf config (bytewise line) + unless whole == pieces && whole == some .uriTooLong do + throw <| IO.userError s!"URI limit: whole {repr whole}, pieces {repr pieces}" diff --git a/tests/async/elab/async_http_h1_rfc_compliance.lean b/tests/async/elab/async_http_h1_rfc_compliance.lean index 71a03bd083fb..546ac1e25460 100644 --- a/tests/async/elab/async_http_h1_rfc_compliance.lean +++ b/tests/async/elab/async_http_h1_rfc_compliance.lean @@ -359,6 +359,71 @@ private def minimalGetRequest : Request.Head := else t) |>.run +#eval runGroup "RFC 9110 §2.5, §5.5 / RFC 9112 §4: response start line and field values" do + -- §5.5: a recipient treats obs-text in a field value as opaque data + MachineTester.sending "§5.5: obs-text in a response field value is accepted" + |>.send minimalGetRequest |>.step + |>.feedBytes ("HTTP/1.1 200 OK\r\nContent-Disposition: attachment; filename=\"caf".toUTF8 + ++ ByteArray.mk #[0xC3, 0xA9] ++ ".txt\"\r\nX-Latin1: caf".toUTF8 ++ ByteArray.mk #[0xE9] + ++ "\r\nContent-Length: 0\r\n\r\n".toUTF8) + |>.step |>.assertNoError |>.assertHasEndHeaders + |>.onEndHeaders (fun t head => + let disposition := (head.headers.get? (.ofString! "Content-Disposition")).map (·.value) + let latin1 := (head.headers.get? (.ofString! "X-Latin1")).map (·.value) + if disposition != some "attachment; filename=\"café.txt\"" then + t.addError s!"Content-Disposition mismatch: {repr disposition}" + else if latin1 != some "caf\uFFFD" then + t.addError s!"X-Latin1 mismatch: {repr latin1}" + else t) + |>.run + + -- §4: obs-text in a reason phrase, which a client ignores + MachineTester.sending "§4: obs-text in the reason phrase is accepted" + |>.send minimalGetRequest |>.step + |>.feedBytes ("HTTP/1.1 200 Tr".toUTF8 ++ ByteArray.mk #[0xC3, 0xA8] ++ "s bien ".toUTF8 + ++ ByteArray.mk #[0xFF] ++ "\r\nContent-Length: 0\r\n\r\n".toUTF8) + |>.step |>.assertNoError + |>.onEndHeaders (fun t head => + if head.status.toCode != 200 then t.addError s!"expected 200, got {head.status.toCode}" else t) + |>.run + + -- §4: a status line that ends right after the status code + MachineTester.sending "§4: status line with no space after the code is accepted" + |>.send minimalGetRequest |>.step + |>.feed "HTTP/1.1 204\r\n\r\n" + |>.step |>.assertNoError + |>.onEndHeaders (fun t head => + if head.status != .noContent then t.addError s!"expected 204, got {head.status.toCode}" else t) + |>.run + + -- §2.5: a higher minor version is processed as the highest minor version the recipient implements + MachineTester.sending "§2.5: HTTP/1.2 response is read as HTTP/1.1" + |>.send minimalGetRequest |>.step + |>.feed "HTTP/1.2 200 OK\r\nContent-Length: 2\r\n\r\nok" + |>.step |>.assertNoError |>.assertKeepAlive + |>.onEndHeaders (fun t head => + if head.version != .v11 then t.addError s!"expected HTTP/1.1, got {repr head.version}" else t) + |>.drainBody |>.assertPulledBody "ok".toUTF8 |>.run + +#eval runGroup "RFC 9112 §7.1.2 / RFC 9110 §6.5: trailer fields" do + -- §6.5.1: a client drops a trailer field it must not process instead of failing the response + MachineTester.sending "§6.5: forbidden non-framing trailer field in a response is dropped" + |>.send minimalGetRequest |>.step + |>.feed "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n2\r\nok\r\n0\r\nCache-Control: no-cache\r\n\r\n" + |>.step |>.assertNoError + |>.drainBody |>.assertNoError |>.assertPulledBody "ok".toUTF8 |>.assertLastChunkFinal |>.run + + -- a field that frames the message is still refused in a response's trailers + MachineTester.sending "§6.5: framing field in response trailers → badMessage" + |>.send minimalGetRequest |>.step + |>.feed "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\n\r\n2\r\nok\r\n0\r\nContent-Length: 2\r\n\r\n" + |>.step |>.drainBody |>.assertFailedWith .badMessage |>.run + + -- a server keeps rejecting every field forbidden in a request's trailers + MachineTester.receiving "§6.5: forbidden trailer field in a request → badMessage" + |>.feed (mkChunkedPost "/" ++ "2\r\nok\r\n0\r\nCache-Control: no-cache\r\n\r\n") + |>.step |>.drainBody |>.assertFailedWith .badMessage |>.run + #eval runGroup "RFC 9112 §3.2–§3.3: request-target form and Host" do MachineTester.receiving "§3.2.1: origin-form path preserved" |>.feed "GET /api/v1/users?active=true HTTP/1.1\r\nHost: api.example.com\r\n\r\n" @@ -542,6 +607,58 @@ private def minimalGetRequest : Request.Head := |>.pullBody |>.assertPulledBody splitBody |>.assertLastChunkFinal |>.run +#eval runGroup "RFC 9112 §6: framing of messages without a body, and of written messages" do + -- §6.3 rule 1: a response to HEAD ends at its header block, whatever its framing fields say + MachineTester.sending "§6.3: HEAD response with contradictory framing fields completes" + |>.send { minimalGetRequest with method := .head } |>.step + |>.feed "HTTP/1.1 200 OK\r\nTransfer-Encoding: chunked\r\nContent-Length: 10\r\n\r\n" + |>.step |>.assertNoError |>.assertReaderComplete |>.run + + -- §6.3 rule 1: so does a 204 response + MachineTester.sending "§6.3: 204 response with contradictory framing fields completes" + |>.send minimalGetRequest |>.step + |>.feed "HTTP/1.1 204 No Content\r\nTransfer-Encoding: chunked\r\nContent-Length: 5\r\n\r\n" + |>.step |>.assertNoError |>.assertReaderComplete |>.run + + -- §6.3 rule 4: a response whose final transfer coding is not chunked is read until the server closes + for coding in ["gzip", "chunked, gzip"] do + MachineTester.sending s!"§6.3: Transfer-Encoding: {coding} response is close-delimited" + |>.send minimalGetRequest |>.step + |>.feed s!"HTTP/1.1 200 OK\r\nTransfer-Encoding: {coding}\r\n\r\nabc" + |>.step |>.assertNoError |>.assertNotKeepAlive + |>.noMoreInput |>.drainBody |>.assertNoError + |>.assertPulledBody "abc".toUTF8 |>.assertLastChunkFinal |>.run + + -- §6.1: a chunked message keeps the transfer codings its body was coded with + MachineTester.receiving "§6.1: server keeps the handler's Transfer-Encoding: gzip, chunked" + |>.feed (mkGet "/") |>.step |>.assertIsWaitingMessage + |>.send { status := .ok, headers := Headers.empty.insert! "Transfer-Encoding" "gzip, chunked" } + |>.sendBytes "abc".toUTF8 |>.userClosedBody |>.step + |>.assertOutputContains "Transfer-Encoding: gzip, chunked\r\n" "expected the handler's codings" + |>.assertOutputContains "3\r\nabc\r\n0\r\n\r\n" "expected a chunked body" |>.run + + MachineTester.sending "§6.1: client keeps the caller's Transfer-Encoding: gzip, chunked" + |>.send { minimalGetRequest with + method := .post, headers := minimalGetRequest.headers.insert! "Transfer-Encoding" "gzip, chunked" } + |>.sendBytes "abc".toUTF8 |>.userClosedBody |>.step + |>.assertOutputContains "Transfer-Encoding: gzip, chunked\r\n" "expected the caller's codings" + |>.assertOutputContains "3\r\nabc\r\n0\r\n\r\n" "expected a chunked body" |>.run + + -- RFC 9110 §8.6: no Content-Length on a request without content whose method anticipates none + MachineTester.sending "§8.6: bodyless GET request carries no Content-Length" + |>.send minimalGetRequest |>.userClosedBody |>.step + |>.assertOutputStartsWith "GET / HTTP/1.1\r\n" "expected the request line" + |>.assertOutputNotContains "Content-Length" "a bodyless GET must not carry Content-Length" |>.run + + MachineTester.sending "§8.6: bodyless POST request still carries Content-Length: 0" + |>.send { minimalGetRequest with method := .post } |>.userClosedBody |>.step + |>.assertOutputContains "Content-Length: 0\r\n" "a bodyless POST keeps Content-Length: 0" |>.run + + MachineTester.sending "§8.6: a GET whose caller set Content-Length: 0 keeps it" + |>.send { minimalGetRequest with headers := minimalGetRequest.headers.insert! "Content-Length" "0" } + |>.userClosedBody |>.step + |>.assertOutputContains "Content-Length: 0\r\n" "an explicit framing field is kept" |>.run + #eval runGroup "RFC 9112 §9.3: connection persistence" do -- §9.3: HTTP/1.1 connections are persistent by default MachineTester.receiving "§9.3: HTTP/1.1 default keep-alive = true" @@ -638,6 +755,24 @@ private def minimalGetRequest : Request.Head := |>.feed "HTTP/1.1 200 OK\r\nConnection: close\r\nContent-Length: 0\r\n\r\n" |>.step |>.assertNoError |>.assertNotKeepAlive |>.run + -- RFC 9110 §7.6.1, §7.8: the handler's connection options are kept, with the machine's `close` + let upgrade (connection : String) : Response.Head := + { status := .upgradeRequired, + headers := Headers.empty |>.insert! "Upgrade" "TLS/1.2" |>.insert! "Connection" connection } + MachineTester.receiving "§7.8: 426 keeps Connection: upgrade and appends close" + |>.feed "GET / HTTP/1.1\r\nHost: example.com\r\nConnection: close\r\n\r\n" + |>.step |>.assertIsWaitingMessage + |>.send (upgrade "Upgrade") + |>.setKnownSize (.fixed 0) |>.userClosedBody |>.step + |>.assertOutputContains "Connection: upgrade, close\r\n" "expected the handler's upgrade option and close" + |>.assertOutputContains "Upgrade: TLS/1.2\r\n" "expected the Upgrade field" |>.run + + MachineTester.receiving "§7.8: keep-alive response keeps the handler's Connection: upgrade" + |>.feed (mkGet "/") |>.step |>.assertKeepAlive + |>.send (upgrade "upgrade, keep-alive") + |>.setKnownSize (.fixed 0) |>.userClosedBody |>.step |>.assertKeepAlive + |>.assertOutputContains "Connection: upgrade\r\n" "expected only the upgrade option" |>.run + #eval runGroup "RFC 9110 §6–§7: header handling" do -- §6.3: custom application headers are preserved in the parsed head MachineTester.receiving "§6.3: custom headers preserved" @@ -711,6 +846,30 @@ private def minimalGetRequest : Request.Head := |>.send { status := .processing } |>.step |>.assertIsWaitingMessage |>.run + -- §15.2: an interim response has no body of its own, so it must not end the response body + MachineTester.sending "§15.2: 103 Early Hints → no closeBody until the final response" + |>.send minimalGetRequest |>.step + |>.feed "HTTP/1.1 103 Early Hints\r\nLink: ; rel=preload\r\n\r\n" |>.step + |>.assertNoError + |>.assertNoEvent (fun | .closeBody => true | _ => false) + "an interim response must not emit closeBody" + |>.feed "HTTP/1.1 200 OK\r\nContent-Length: 2\r\n\r\nok" |>.step + |>.drainBody |>.assertNoError |>.assertPulledBody "ok".toUTF8 + |>.assertHasCloseBody |>.run + + -- §15.2.2: after 101 the connection speaks the new protocol, so no final response follows and the + -- bytes after the head are not read as HTTP + MachineTester.sending "§15.2.2: 101 Switching Protocols ends the exchange" + |>.send { minimalGetRequest with + headers := minimalGetRequest.headers + |>.insert! "Connection" "upgrade" |>.insert! "Upgrade" "websocket" } + |>.step + |>.feed "HTTP/1.1 101 Switching Protocols\r\nUpgrade: websocket\r\nConnection: Upgrade\r\n\r\n" + |>.feedBytes (ByteArray.mk #[0x81, 0x02, 0x68, 0x69]) + |>.step + |>.assertNoError |>.assertHasEndHeaders |>.assertNotKeepAlive + |>.assertReaderClosed |>.run + #eval runGroup "RFC 7231 §4.3.2: HEAD request handling" do -- body bytes suppressed; Content-Length metadata still emitted so client knows size let body := "hello".toUTF8 @@ -724,6 +883,17 @@ private def minimalGetRequest : Request.Head := |>.assertOutputNotContains "hello" "HEAD response must not contain body bytes on the wire" |>.run + -- RFC 9110 §9.3.2, §8.6: with no known length a HEAD response has GET's framing; a + -- `Content-Length: 0` would claim the GET response is empty + MachineTester.receiving "§9.3.2: HEAD response of unknown length has no Content-Length: 0" + |>.feed ("HEAD / HTTP/1.1\r\nHost: example.com\r\n\r\n" ++ mkGet "/next") + |>.step |>.assertIsWaitingMessage + |>.send { status := .ok } |>.userClosedBody |>.step + |>.assertOutputNotContains "Content-Length" "unknown length must not be sent as Content-Length: 0" + |>.assertOutputContains "Transfer-Encoding: chunked\r\n" "expected the framing GET would have" + |>.assertOutputNotContains "0\r\n\r\n" "a HEAD response carries no body, not even a last chunk" + |>.assertHasNext |>.run + #eval runGroup "RFC 2616: HTTP/1.0 compatibility" do -- RFC 2068 §19.4.6: HTTP/1.0 does not define chunked transfer encoding MachineTester.receiving "§19.4.6: chunked TE on HTTP/1.0 → badMessage" @@ -779,6 +949,15 @@ private def minimalGetRequest : Request.Head := |>.assertOutputContains "Connection: keep-alive" "RFC 2616 §19.7.1: HTTP/1.0 keep-alive response must include Connection: keep-alive" |>.run + -- RFC 9110 §15.2: a server must not send a 1xx response to an HTTP/1.0 client + MachineTester.receiving "§15.2: 103 Early Hints is not sent to an HTTP/1.0 client" + |>.feed (mkGet10 "/") |>.step |>.assertIsWaitingMessage + |>.send { status := .earlyHints, headers := Headers.empty.insert! "Link" "; rel=preload" } + |>.step |>.assertIsWaitingMessage + |>.send { status := .ok } |>.setKnownSize (.fixed 0) |>.userClosedBody |>.step + |>.assertOutputNotContains "103" "a 1xx response must not reach an HTTP/1.0 client" + |>.assertOutputStartsWith "HTTP/1.0 200" "expected the final response first" |>.run + #eval runGroup "RFC 9110 §8.6 / §6.3: client-side bodyless response framing" do -- §8.6: a HEAD response has no body regardless of framing headers. The client reader must treat -- it as zero-length and finish without blocking, even though Content-Length advertises bytes that diff --git a/tests/async/elab/async_http_h1_short_fixed_body.lean b/tests/async/elab/async_http_h1_short_fixed_body.lean new file mode 100644 index 000000000000..89dbfe8c2311 --- /dev/null +++ b/tests/async/elab/async_http_h1_short_fixed_body.lean @@ -0,0 +1,46 @@ +module + +import Std.Http + +/-! +Tests that the HTTP/1.1 machine reports an outgoing body that ends short of its `Content-Length` in +the step that writes its last bytes. A connection loop steps the machine again only on an external +event, so a shortfall left for a later step can go unreported until a timeout. +-/ + +open Std Http Protocol H1 + +/-- Steps `machine` until a step writes `needle`, and reports whether that step also closed. -/ +private def closesWhenWriting (machine : Machine dir) (needle : String) : IO Bool := do + let mut machine := machine + for _ in [0:8] do + let (next, step) := machine.step + machine := next + let wrote := String.fromUTF8! (step.output.data.foldl (· ++ ·) .empty) + if wrote.contains needle then + return step.events.any (· matches .close) && machine.error == some .badMessage + throw <| IO.userError s!"{needle.quote} was never written" + +/-- A request head that declares a 10-byte body. -/ +private def putHead : Request.Head := + (Request.new |>.method .put |>.uri! "/upload" |>.header! "Host" "example.com" + |>.header! "Content-Length" "10").line + +-- Client side: the request body ends after 5 of its 10 declared bytes. +#eval show IO Unit from do + let machine : Machine .sending := { config := {} } + let machine := machine.send putHead + |>.sendData #[Chunk.ofByteArray "12345".toUTF8] |>.userClosedBody + unless ← closesWhenWriting machine "12345" do + throw <| IO.userError "a request body 5 bytes short was not reported in the step that wrote it" + +-- Control: the whole declared body completes the message without an error. +#eval show IO Unit from do + let machine : Machine .sending := { config := {} } + let mut machine := machine.send putHead + |>.sendData #[Chunk.ofByteArray "0123456789".toUTF8] |>.userClosedBody + for _ in [0:8] do + let (next, _) := machine.step + machine := next + if machine.error.isSome then + throw <| IO.userError s!"a complete body failed with {machine.error.map toString}" From bddbe5399a3d787caa988cacdc7da48bb86ba613 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 5 Nov 2026 17:35:16 -0300 Subject: [PATCH 2/5] fix: comments and usage of optinonalItem --- src/Std/Http/Data/Body/Full.lean | 22 +++++++++---------- src/Std/Http/Protocol/H1.lean | 7 ++++-- src/Std/Http/Protocol/H1/Parser.lean | 4 ++-- .../async/elab/async_http_h1_incremental.lean | 11 +++++++++- .../elab/async_http_h1_rfc_compliance.lean | 13 +++++++++++ 5 files changed, 40 insertions(+), 17 deletions(-) diff --git a/src/Std/Http/Data/Body/Full.lean b/src/Std/Http/Data/Body/Full.lean index b635fb2a5a26..b576a86cfd33 100644 --- a/src/Std/Http/Data/Body/Full.lean +++ b/src/Std/Http/Data/Body/Full.lean @@ -178,15 +178,18 @@ instance : Coe (Async (Response Full)) (ContextAsync (Response Any)) where end Body -namespace Request.Builder - /-- -Sets `Content-Type` to `value` unless the message being built already has one, so a type the caller -chose is not followed by a second, default one. +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 := - if builder.line.headers.contains Header.Name.contentType then builder - else builder.header Header.Name.contentType (Header.Value.ofString! value) + { builder with line.headers := builder.line.headers.withDefaultContentType value } open Async @@ -230,13 +233,8 @@ end Request.Builder namespace Response.Builder -/-- -Sets `Content-Type` to `value` unless the message being built already has one, so a type the caller -chose is not followed by a second, default one. --/ private def defaultContentType (builder : Builder) (value : String) : Builder := - if builder.line.headers.contains Header.Name.contentType then builder - else builder.header Header.Name.contentType (Header.Value.ofString! value) + { builder with line.headers := builder.line.headers.withDefaultContentType value } open Async diff --git a/src/Std/Http/Protocol/H1.lean b/src/Std/Http/Protocol/H1.lean index 790c1ea45e54..c5e08351b816 100644 --- a/src/Std/Http/Protocol/H1.lean +++ b/src/Std/Http/Protocol/H1.lean @@ -66,7 +66,8 @@ structure PulledChunk where incomplete : Bool /-- - The pulled body chunk. + The pulled body chunk. Chunked framing is removed; other transfer codings, such as the `gzip` of + `Transfer-Encoding: gzip`, are not decoded. -/ chunk : Chunk @@ -801,9 +802,11 @@ private def writeHead (messageHead : Message.Head dir.swap) (machine : Machine d -- RFC 7230 §3.3.1: HTTP/1.0 does not support Transfer-Encoding. When the -- response body length is unknown (chunked mode), fall back to connection-close -- framing: disable keep-alive and write raw bytes (no chunk encoding, no TE header). + -- An omitted body (a HEAD response) has nothing to delimit, so the connection stays open. let machine := match dir, machine.reader.messageHead.version, size with - | .receiving, Version.v10, .chunked => machine.disableKeepAlive + | .receiving, Version.v10, .chunked => + if machine.writer.omitBody then machine else machine.disableKeepAlive | _, _, _ => machine let state : Writer.State := diff --git a/src/Std/Http/Protocol/H1/Parser.lean b/src/Std/Http/Protocol/H1/Parser.lean index d87f31675031..7d9bf5ae6247 100644 --- a/src/Std/Http/Protocol/H1/Parser.lean +++ b/src/Std/Http/Protocol/H1/Parser.lean @@ -68,8 +68,8 @@ def optionalUnlessEof (p : Parser α) : Parser (Option α) := fun it => Repeatedly applies `parser` until it returns `none` or the `maxCount` limit is exceeded. Returns the collected results as an array. -A `parser` that fails on exhausted input propagates that failure, so an item split across two reads -is re-parsed once the rest arrives instead of ending the list early. +An item cut off by the end of the input fails with `.eof` instead of ending the list, so it is +re-parsed once the rest arrives. -/ def manyItems {α : Type} (parser : Parser (Option α)) (maxCount : Nat) : Parser (Array α) := go #[] diff --git a/tests/async/elab/async_http_h1_incremental.lean b/tests/async/elab/async_http_h1_incremental.lean index 100ec291bc7a..3bfa0689a14b 100644 --- a/tests/async/elab/async_http_h1_incremental.lean +++ b/tests/async/elab/async_http_h1_incremental.lean @@ -353,11 +353,20 @@ private def getEndHeadersHead (events : Array (Event .receiving)) : Option Reque -- A chunk-size line cut inside an extension must report `.eof` so the machine waits for more data. #eval show IO Unit from do - for input in ["5;", "5 ", "5;a", "5;a=", "5;a=\"b"] do + for input in ["5", "5;", "5 ", "5;a", "5;a=", "5;a=b", "5;a=\"b"] do match parseChunkSize {} input.toUTF8.iter with | .error _ .eof => pure () | _ => throw <| IO.userError s!"expected .eof for truncated chunk-size line {input.quote}" +-- A chunk-size line that is still arriving is held to `maxChunkLineLength` by every byte read so +-- far, including those of an extension the read cut off. +#eval show IO Unit from do + let config : Protocol.H1.Config := { maxChunkLineLength := 16 } + let input := mkChunkedHead "/inc-chunk-line" ++ s!"5;{String.ofList (List.replicate 40 'a')}".toUTF8 + let trace := runIncrementalReceiving #[input] config + ensure "Unfinished chunk-size line over the limit" (trace.machine.error == some .badMessage) + s!"expected badMessage, got {repr trace.machine.error}" + -- The trailer section is consumed one field at a time: after a read that ends inside the second -- field, only that field is still buffered, so the next read does not parse the first one again. #eval show IO Unit from do diff --git a/tests/async/elab/async_http_h1_rfc_compliance.lean b/tests/async/elab/async_http_h1_rfc_compliance.lean index 546ac1e25460..e2e1a46c54fe 100644 --- a/tests/async/elab/async_http_h1_rfc_compliance.lean +++ b/tests/async/elab/async_http_h1_rfc_compliance.lean @@ -958,6 +958,19 @@ private def minimalGetRequest : Request.Head := |>.assertOutputNotContains "103" "a 1xx response must not reach an HTTP/1.0 client" |>.assertOutputStartsWith "HTTP/1.0 200" "expected the final response first" |>.run + -- RFC 9112 §6.3: a HEAD response ends at its header block, so a length the server does not know + -- does not cost an HTTP/1.0 client its keep-alive connection + MachineTester.receiving "§6.3: HTTP/1.0 HEAD of unknown length keeps the connection alive" + |>.feed ("HEAD / HTTP/1.0\r\nConnection: keep-alive\r\n\r\n" ++ + "GET /second HTTP/1.0\r\nConnection: keep-alive\r\n\r\n") + |>.step |>.assertIsWaitingMessage + |>.send { status := .ok } |>.userClosedBody |>.step + |>.assertOutputContains "Connection: keep-alive\r\n" "expected the HTTP/1.0 keep-alive echo" + |>.assertOutputNotContains "Content-Length" "unknown length must not be sent as Content-Length: 0" + |>.assertOutputNotContains "close" "a HEAD response has no body to delimit by closing" + |>.assertHasNext + |>.step |>.assertHasEndHeaders |>.assertKeepAlive |>.run + #eval runGroup "RFC 9110 §8.6 / §6.3: client-side bodyless response framing" do -- §8.6: a HEAD response has no body regardless of framing headers. The client reader must treat -- it as zero-length and finish without blocking, even though Content-Length advertises bytes that From fb3c059c511ddd310d9f1af3b01eb640c40d8104 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 6 Nov 2026 00:51:16 -0300 Subject: [PATCH 3/5] fix: transfer-encoding options and comments --- src/Std/Http/Data/Headers/Basic.lean | 43 +++++++-- src/Std/Http/Protocol/H1.lean | 88 ++++++++++--------- src/Std/Http/Protocol/H1/Config.lean | 7 +- src/Std/Http/Protocol/H1/Message.lean | 4 +- src/Std/Http/Protocol/H1/Reader.lean | 3 +- tests/async/elab/async_http_fuzz.lean | 1 + tests/async/elab/async_http_fuzz_limits.lean | 11 +-- .../elab/async_http_h1_chunked_overhead.lean | 57 ++++++++++++ .../elab/async_http_h1_rfc_compliance.lean | 53 ++++++++++- 9 files changed, 204 insertions(+), 63 deletions(-) create mode 100644 tests/async/elab/async_http_h1_chunked_overhead.lean diff --git a/src/Std/Http/Data/Headers/Basic.lean b/src/Std/Http/Data/Headers/Basic.lean index 8940b00814eb..518e23b1a942 100644 --- a/src/Std/Http/Data/Headers/Basic.lean +++ b/src/Std/Http/Data/Headers/Basic.lean @@ -163,14 +163,43 @@ def parse (v : Value) : Option TransferEncoding := do none /-- -Parses a comma-separated list of transfer codings without the chunked placement rules. A response's -framing depends only on whether its final coding is `chunked` (RFC 9112 §6.3 rule 4), whatever the -other codings are. +Checks a transfer parameter: `token BWS "=" BWS ( token / quoted-string )` (RFC 9112 §7). -/ -def parseCodings? (v : Value) : Option (Array String) := do - let codings ← parseTokenList v - guard (codings.all isToken) - return codings +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 + +/-- +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. diff --git a/src/Std/Http/Protocol/H1.lean b/src/Std/Http/Protocol/H1.lean index c5e08351b816..101b4826d495 100644 --- a/src/Std/Http/Protocol/H1.lean +++ b/src/Std/Http/Protocol/H1.lean @@ -337,8 +337,7 @@ own and runs until the server closes the connection. private def hasCloseDelimitedCoding (message : Message.Head .sending) : Bool := message.version == .v11 && !message.headers.contains Header.Name.contentLength && match message.headers.getAll? Header.Name.transferEncoding with - | some #[value] => - (Header.TransferEncoding.parseCodings? value).any (·.back? != some "chunked") + | some #[value] => Header.TransferEncoding.finalCodingIsChunked? value == some false | _ => false /-- @@ -390,7 +389,7 @@ The `Transfer-Encoding` value for a chunked message: the caller's own field when private def chunkedCodings (headers : Headers) : Header.Value := match headers.getAll? Header.Name.transferEncoding with | some #[value] => - if (Header.TransferEncoding.parse value).any (·.isChunked) then value else .mk "chunked" + if Header.TransferEncoding.finalCodingIsChunked? value == some true then value else .mk "chunked" | _ => .mk "chunked" /-- @@ -722,18 +721,25 @@ private def processHeaders (machine : Machine dir) : Machine dir := advanceAfterHeaders machine state /-- -The connection options of a handler's `Connection` fields other than `close` and `keep-alive`, which -the machine decides itself. +The tokens of the `Connection` field the machine writes: the sender's own connection options, then +`close` when the connection ends, or `keep-alive` when an HTTP/1.0 connection persists (RFC 2616 +§19.7.1). The sender's `close` and `keep-alive` are dropped, since the machine decides those itself; +its other options are kept, such as the `upgrade` that RFC 9110 §7.8 requires next to `Upgrade`. -/ -private def handlerConnectionOptions (headers : Headers) : Array String := - match headers.getAll? Header.Name.connection with - | none => #[] - | some values => - values.foldl (init := #[]) fun acc value => - match Header.Connection.parse value with - | some connection => - acc ++ connection.tokens.filter (fun t => t != "close" && t != "keep-alive") - | none => acc +private def connectionTokens (headers : Headers) (keepAlive : Bool) (version : Version) : + Array String := + let options : Array String := + match headers.getAll? Header.Name.connection with + | none => #[] + | some values => + values.foldl (init := #[]) fun acc value => + match Header.Connection.parse value with + | some connection => + acc ++ connection.tokens.filter (fun t => t != "close" && t != "keep-alive") + | none => acc + if !keepAlive then options.push "close" + else if version == .v10 then options.push "keep-alive" + else options /-- Encodes a server response head. The handler's fields are written in order without `Connection`, @@ -757,22 +763,10 @@ private def encodeServerHead (head : Response.Head) (version : Version) (keepAli if head.headers.contains Header.Name.server then out else appendFieldLine out Header.Name.server server | none => out - -- RFC 9110 §7.8: a response that sends `Upgrade` must also send the `upgrade` connection option. - let options := handlerConnectionOptions head.headers + let tokens := connectionTokens head.headers keepAlive version let out : ByteArray := - if !options.isEmpty then - let options := - if !keepAlive then options.push "close" - else if version == .v10 then options.push "keep-alive" - else options - out ++ "Connection: " ++ ", ".intercalate options.toList ++ "\r\n" - else if !keepAlive then - out ++ "Connection: close\r\n" - else if version == .v10 then - -- RFC 2616 §19.7.1: HTTP/1.0 keep-alive responses must echo Connection: keep-alive - out ++ "Connection: keep-alive\r\n" - else - out + if tokens.isEmpty then out + else out ++ "Connection: " ++ ", ".intercalate tokens.toList ++ "\r\n" -- Framing fields are omitted for bodyless status codes (RFC 9110 §8.6, §15.4.5) and for -- HTTP/1.0 connection-close framing (RFC 7230 §3.3.1). let out : ByteArray := @@ -838,16 +832,12 @@ private def writeHead (messageHead : Message.Head dir.swap) (machine : Machine d else headers.insert Header.Name.userAgent userAgent | none => headers - -- Erase any user-supplied Connection value to avoid duplicate or conflicting headers. + -- The request's own version: the reader may already hold the next response's status line. + let tokens := connectionTokens headers keepAlive messageHead.version let headers := headers.erase Header.Name.connection let headers := - if !keepAlive then - headers.insert Header.Name.connection (.mk "close") - -- The request's own version: the reader may already hold the next response's status line. - else if messageHead.version == .v10 then - headers.insert Header.Name.connection (.mk "keep-alive") - else - headers + if tokens.isEmpty then headers + else headers.insert Header.Name.connection (.ofString! (", ".intercalate tokens.toList)) -- RFC 9110 §8.6: no `Content-Length` on a request without content whose method anticipates -- none, unless the caller set a framing field. let headers := @@ -1424,21 +1414,27 @@ private def parseFixedBody (machine : Machine dir) (size : Nat) : /-- Parses next chunk-size line in chunked mode and transitions to chunk-data state. + +The line, like the line break after the data and the trailer section, counts toward `maxBodySize`, +so the wire size of a chunked body stays bounded however small its chunks are. -/ private def parseChunkSizeBody (machine : Machine dir) : Machine dir × Option PulledChunk × Bool := + let start := machine.reader.input.remainingBytes let (machine, result) := parseWith machine (parseChunkSize machine.config) (limit := some machine.config.maxChunkLineLength) match result with | some (size, ext) => + let lineBytes := start - machine.reader.input.remainingBytes if size > machine.config.maxChunkSize then bodyTooLarge machine - else if !fitsBodyLimit machine size then + else if !fitsBodyLimit machine (lineBytes + size) then bodyTooLarge machine else - (machine.setReaderState (.readBody (.chunkedBody ext size)), none, true) + (machine.addBodyBytes lineBytes |>.setReaderState (.readBody (.chunkedBody ext size)), + none, true) | none => bodyNoProgress machine @@ -1454,15 +1450,21 @@ private def parseTrailerState (machine : Machine dir) -- A server rejects every field forbidden in a request's trailers; a client, which discards -- trailers, only refuses those that would reframe the response. let strict := match dir with | .receiving => true | .sending => false + let start := machine.reader.input.remainingBytes let (machine, result) := parseWith machine (parseTrailerHeader machine.config strict) (limit := none) + let lineBytes := start - machine.reader.input.remainingBytes match result with | some (some _) => if count ≥ machine.config.maxTrailerHeaders then (machine.setFailure .badMessage, none, false) + else if !fitsBodyLimit machine lineBytes then + bodyTooLarge machine else - (machine.setReaderState (.readBody (.trailers ext (count + 1))), none, true) - | some none => emitBodyChunk machine .complete true false ext .empty (closeBody := true) + (machine.addBodyBytes lineBytes |>.setReaderState (.readBody (.trailers ext (count + 1))), + none, true) + | some none => + emitBodyChunk (machine.addBodyBytes lineBytes) .complete true false ext .empty (closeBody := true) | none => bodyNoProgress machine /-- @@ -1473,10 +1475,12 @@ private def parseChunkedBodyState (machine : Machine dir) (ext : Array (Chunk.ExtensionName × Option Chunk.ExtensionValue)) (size : Nat) : Machine dir × Option PulledChunk × Bool := + let start := machine.reader.input.remainingBytes let (machine, result) := parseWith machine (parseChunkSizedData size) (limit := none) (some size) match result with | some (.complete body) => - emitBodyChunk machine (.readBody .chunkedSize) false false ext body + let lineBreak := start - machine.reader.input.remainingBytes - body.size + emitBodyChunk (machine.addBodyBytes lineBreak) (.readBody .chunkedSize) false false ext body | some (.incomplete body remaining) => emitBodyChunk machine (.readBody (.chunkedBody ext remaining)) false true ext body | none => diff --git a/src/Std/Http/Protocol/H1/Config.lean b/src/Std/Http/Protocol/H1/Config.lean index 1106fae84f5b..d4a7593e82a7 100644 --- a/src/Std/Http/Protocol/H1/Config.lean +++ b/src/Std/Http/Protocol/H1/Config.lean @@ -114,10 +114,9 @@ structure Config where /-- Maximum allowed total body size per message in bytes (default: 64 MiB). - This limit applies across all body framing modes and counts content bytes only. For chunked - transfer encoding, chunk-size lines and the trailer section do not count toward it: each - chunk-size line is bounded by `maxChunkLineLength`, and the trailer section by - `maxTrailerHeaders` fields of at most `maxHeaderNameLength` and `maxHeaderValueLength` bytes. + This limit applies across all body framing modes. For chunked transfer encoding, + chunk-size lines (including extensions) and the trailer section also count toward + this limit, so the total wire bytes consumed by the body cannot exceed this value. -/ maxBodySize : Nat := 64 * 1024 * 1024 diff --git a/src/Std/Http/Protocol/H1/Message.lean b/src/Std/Http/Protocol/H1/Message.lean index 9d86f27ff6d0..e4db678635c6 100644 --- a/src/Std/Http/Protocol/H1/Message.lean +++ b/src/Std/Http/Protocol/H1/Message.lean @@ -95,9 +95,7 @@ def Message.Head.getSize (message : Message.Head dir) (allowEOFBody : Bool) : Op -- Single transfer-encoding header. | some #[header] => - let te := Header.TransferEncoding.parse header - - match Header.TransferEncoding.isChunked <$> te, contentLength with + match Header.TransferEncoding.finalCodingIsChunked? header, contentLength with | some true, none => -- HTTP/1.0 does not define chunked transfer encoding (RFC 2068 §19.4.6). -- A server MUST NOT use chunked with an HTTP/1.0 peer; likewise, an diff --git a/src/Std/Http/Protocol/H1/Reader.lean b/src/Std/Http/Protocol/H1/Reader.lean index d0a9459910f7..cbaf3c7650fc 100644 --- a/src/Std/Http/Protocol/H1/Reader.lean +++ b/src/Std/Http/Protocol/H1/Reader.lean @@ -129,7 +129,8 @@ structure Reader (dir : Direction) where messageCount : Nat := 0 /-- - Number of body bytes read for the current message. + Number of body bytes read for the current message. For a chunked body this includes the framing: + chunk-size lines, the line break after each chunk's data, and the trailer section. -/ bodyBytesRead : Nat := 0 diff --git a/tests/async/elab/async_http_fuzz.lean b/tests/async/elab/async_http_fuzz.lean index 5c1c02b9cf0f..454a7999a61b 100644 --- a/tests/async/elab/async_http_fuzz.lean +++ b/tests/async/elab/async_http_fuzz.lean @@ -1,4 +1,5 @@ import Std.Http +import Std.Http.Test.Helpers import Std.Async import Std.Async.Timer diff --git a/tests/async/elab/async_http_fuzz_limits.lean b/tests/async/elab/async_http_fuzz_limits.lean index 628d53caea46..188c515fe7c9 100644 --- a/tests/async/elab/async_http_fuzz_limits.lean +++ b/tests/async/elab/async_http_fuzz_limits.lean @@ -130,8 +130,8 @@ def fuzzBodySizeLimitContentLength (iterations : Nat) (seed0 : Nat) : IO Unit := -- maxBodySize — chunked framing -- ============================================================================ --- Property: chunked bodies with total bytes at or below maxBodySize → 200. --- Chunked bodies exceeding maxBodySize → 413. +-- Property: chunked bodies whose wire size (data plus chunk framing) is at or below +-- maxBodySize → 200. Chunked bodies exceeding maxBodySize → 413. def fuzzBodySizeLimitChunked (iterations : Nat) (seed0 : Nat) : IO Unit := do let limit : Nat := 64 let config : Config := { lingeringTimeout := 1000, generateDate := false, maxBodySize := limit } @@ -160,10 +160,11 @@ def fuzzBodySizeLimitChunked (iterations : Nat) (seed0 : Nat) : IO Unit := do let (client, server) ← Mock.new let response ← sendRaw client server raw (fun req => do let _body : String ← req.body.readAll; Response.ok |>.text "ok") config - if totalSize ≤ limit then - assertStatusPrefix s!"fuzzBodySizeLimitChunked iter={i} seed={caseSeed} total={totalSize}" response "HTTP/1.1 200" + let label := s!"fuzzBodySizeLimitChunked iter={i} seed={caseSeed} total={totalSize} wire={chunkedBody.size}" + if chunkedBody.size ≤ limit then + assertStatusPrefix label response "HTTP/1.1 200" else - assertStatusPrefix s!"fuzzBodySizeLimitChunked iter={i} seed={caseSeed} total={totalSize}" response "HTTP/1.1 413" + assertStatusPrefix label response "HTTP/1.1 413" -- ============================================================================ -- maxHeaders — header count limit diff --git a/tests/async/elab/async_http_h1_chunked_overhead.lean b/tests/async/elab/async_http_h1_chunked_overhead.lean new file mode 100644 index 000000000000..462c4cd68bfd --- /dev/null +++ b/tests/async/elab/async_http_h1_chunked_overhead.lean @@ -0,0 +1,57 @@ +import Std.Http + +open Std Http +open Std.Http.Protocol.H1 + +/-! +Tests that chunked framing counts toward `maxBodySize`: chunk-size lines with their extensions, the +line break after each chunk's data, and the trailer section. Otherwise a body of small chunks with +long extensions makes the server read many times `maxBodySize` from the network for a body that +fits the limit. +-/ + +/-- +Feeds `data` to a server machine `piece` bytes at a time, pulling the body as it arrives. Returns +the machine's error, whether the body completed, and the number of content bytes pulled. +-/ +def run (config : Protocol.H1.Config) (data : ByteArray) (piece : Nat) : + Option Error × Bool × Nat := Id.run do + let mut m : Machine .receiving := { config } + let mut pulled := 0 + let mut complete := false + let mut i := 0 + while i < data.size && !m.failed do + m := m.feed (data.extract i (i + piece)) + i := i + piece + for _ in [0:4] do + m := m.step.1 + let (m', chunk) := m.pullBody + m := m' + if let some c := chunk then + pulled := pulled + c.chunk.data.size + complete := complete || c.final + return (m.error, complete, pulled) + +def chunkedPost : String := + "POST / HTTP/1.1\r\nHost: a\r\nTransfer-Encoding: chunked\r\n\r\n" + +-- 1000 one-byte chunks with ~100-byte extensions: 1000 content bytes, over 100 KB on the wire. +#eval show IO Unit from do + let ext := s!";name={String.ofList (List.replicate 100 'x')}" + let body := String.join (List.replicate 1000 s!"1{ext}\r\nX\r\n") ++ "0\r\n\r\n" + let (error, complete, pulled) := run { maxBodySize := 2000 } (chunkedPost ++ body).toUTF8 4096 + unless error == some .entityTooLarge && !complete && pulled < 2000 do + throw <| IO.userError s!"framing not counted: {repr error}, complete {complete}, pulled {pulled}" + +-- The limit is exactly the body's wire size: it fits, and one byte less does not, however the +-- input is split. The last byte over the limit is the line break that ends the trailer section. +#eval show IO Unit from do + let body := "5\r\nhello\r\n3;x=y\r\nabc\r\n0\r\nX-Trace: 1\r\n\r\n" + let data := (chunkedPost ++ body).toUTF8 + for piece in [data.size, 1] do + let (error, complete, pulled) := run { maxBodySize := body.utf8ByteSize } data piece + unless error.isNone && complete && pulled == 8 do + throw <| IO.userError s!"exact fit, pieces of {piece}: {repr error}, complete {complete}, pulled {pulled}" + let (error, complete, _) := run { maxBodySize := body.utf8ByteSize - 1 } data piece + unless error == some .entityTooLarge && !complete do + throw <| IO.userError s!"one byte over, pieces of {piece}: {repr error}, complete {complete}" diff --git a/tests/async/elab/async_http_h1_rfc_compliance.lean b/tests/async/elab/async_http_h1_rfc_compliance.lean index e2e1a46c54fe..7c16ea6c852d 100644 --- a/tests/async/elab/async_http_h1_rfc_compliance.lean +++ b/tests/async/elab/async_http_h1_rfc_compliance.lean @@ -1,4 +1,5 @@ import Std.Http +import Std.Http.Test.Helpers open Std Http open Std.Http.Internal.Test @@ -481,6 +482,18 @@ private def minimalGetRequest : Request.Head := |>.feed "POST / HTTP/1.1\r\nHost: example.com\r\nTransfer-Encoding: identity\r\n\r\n" |>.step |>.assertFailedWith .badMessage |>.run + -- §7: transfer parameters on a coding before `chunked` leave the request chunked + MachineTester.receiving "§7: Transfer-Encoding: gzip;level=1, chunked request is chunked" + |>.feed ("POST / HTTP/1.1\r\nHost: example.com\r\nTransfer-Encoding: gzip;level=1, chunked\r\n\r\n" ++ + "3\r\nabc\r\n0\r\n\r\n") + |>.step |>.assertNoError + |>.drainBody |>.assertNoError |>.assertPulledBody "abc".toUTF8 |>.assertLastChunkFinal |>.run + + -- RFC 9112 §7.1: `chunked` defines no parameters + MachineTester.receiving "§7: Transfer-Encoding: chunked;x=1 request → badMessage" + |>.feed "POST / HTTP/1.1\r\nHost: example.com\r\nTransfer-Encoding: chunked;x=1\r\n\r\n0\r\n\r\n" + |>.step |>.assertFailedWith .badMessage |>.run + #eval runGroup "RFC 9112 §6.3: body framing" do MachineTester.receiving "§6.3: no CL/TE → empty body" |>.feed (mkGet "/") @@ -621,7 +634,7 @@ private def minimalGetRequest : Request.Head := |>.step |>.assertNoError |>.assertReaderComplete |>.run -- §6.3 rule 4: a response whose final transfer coding is not chunked is read until the server closes - for coding in ["gzip", "chunked, gzip"] do + for coding in ["gzip", "chunked, gzip", "gzip;level=1", "gzip ; level = \"9\""] do MachineTester.sending s!"§6.3: Transfer-Encoding: {coding} response is close-delimited" |>.send minimalGetRequest |>.step |>.feed s!"HTTP/1.1 200 OK\r\nTransfer-Encoding: {coding}\r\n\r\nabc" @@ -629,6 +642,20 @@ private def minimalGetRequest : Request.Head := |>.noMoreInput |>.drainBody |>.assertNoError |>.assertPulledBody "abc".toUTF8 |>.assertLastChunkFinal |>.run + -- §7: transfer parameters do not change which coding is final + MachineTester.sending "§6.3: Transfer-Encoding: gzip;level=1, chunked response is chunked" + |>.send minimalGetRequest |>.step + |>.feed "HTTP/1.1 200 OK\r\nTransfer-Encoding: gzip;level=1, chunked\r\n\r\n3\r\nabc\r\n0\r\n\r\n" + |>.step |>.assertNoError |>.assertKeepAlive + |>.drainBody |>.assertNoError |>.assertPulledBody "abc".toUTF8 |>.assertLastChunkFinal |>.run + + -- §7.1: chunked defines no parameters + for coding in ["chunked;x=1", "gzip;level, chunked", "gzip;=1, chunked"] do + MachineTester.sending s!"§7: Transfer-Encoding: {coding} → badMessage" + |>.send minimalGetRequest |>.step + |>.feed s!"HTTP/1.1 200 OK\r\nTransfer-Encoding: {coding}\r\n\r\n3\r\nabc\r\n0\r\n\r\n" + |>.step |>.assertFailedWith .badMessage |>.run + -- §6.1: a chunked message keeps the transfer codings its body was coded with MachineTester.receiving "§6.1: server keeps the handler's Transfer-Encoding: gzip, chunked" |>.feed (mkGet "/") |>.step |>.assertIsWaitingMessage @@ -637,6 +664,13 @@ private def minimalGetRequest : Request.Head := |>.assertOutputContains "Transfer-Encoding: gzip, chunked\r\n" "expected the handler's codings" |>.assertOutputContains "3\r\nabc\r\n0\r\n\r\n" "expected a chunked body" |>.run + MachineTester.receiving "§6.1: server keeps the handler's Transfer-Encoding: gzip;level=1, chunked" + |>.feed (mkGet "/") |>.step |>.assertIsWaitingMessage + |>.send { status := .ok, headers := Headers.empty.insert! "Transfer-Encoding" "gzip;level=1, chunked" } + |>.sendBytes "abc".toUTF8 |>.userClosedBody |>.step + |>.assertOutputContains "Transfer-Encoding: gzip;level=1, chunked\r\n" "expected the handler's codings" + |>.assertOutputContains "3\r\nabc\r\n0\r\n\r\n" "expected a chunked body" |>.run + MachineTester.sending "§6.1: client keeps the caller's Transfer-Encoding: gzip, chunked" |>.send { minimalGetRequest with method := .post, headers := minimalGetRequest.headers.insert! "Transfer-Encoding" "gzip, chunked" } @@ -773,6 +807,23 @@ private def minimalGetRequest : Request.Head := |>.setKnownSize (.fixed 0) |>.userClosedBody |>.step |>.assertKeepAlive |>.assertOutputContains "Connection: upgrade\r\n" "expected only the upgrade option" |>.run + -- RFC 9110 §7.8: a client that sends `Upgrade` also sends the `upgrade` connection option + MachineTester.sending "§7.8: client keeps the caller's Connection: upgrade" + |>.send { minimalGetRequest with + headers := minimalGetRequest.headers + |>.insert! "Connection" "Upgrade" |>.insert! "Upgrade" "websocket" } + |>.userClosedBody |>.step + |>.assertOutputContains "Connection: upgrade\r\n" "expected the caller's upgrade option" + |>.assertOutputContains "Upgrade: websocket\r\n" "expected the Upgrade field" |>.run + + MachineTester.sending "§7.8: client appends close to the caller's connection options" + |>.send { minimalGetRequest with + headers := minimalGetRequest.headers + |>.insert! "Connection" "upgrade, close" |>.insert! "Upgrade" "websocket" } + |>.userClosedBody |>.step |>.assertNotKeepAlive + |>.assertOutputContains "Connection: upgrade, close\r\n" "expected the upgrade option, then close" + |>.run + #eval runGroup "RFC 9110 §6–§7: header handling" do -- §6.3: custom application headers are preserved in the parsed head MachineTester.receiving "§6.3: custom headers preserved" From a74e015f8e3fa44015cbbc7742a2fc0245e7953d Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 6 Nov 2026 11:09:50 -0300 Subject: [PATCH 4/5] fix: answer a contradictory framing head with 500 instead of spinning --- src/Std/Http/Data/Headers/Basic.lean | 23 +-- src/Std/Http/Protocol/H1.lean | 83 ++++++---- .../elab/async_http_h1_framing_mismatch.lean | 149 ++++++++++++++++++ tests/async/elab/async_http_headers.lean | 16 ++ 4 files changed, 232 insertions(+), 39 deletions(-) create mode 100644 tests/async/elab/async_http_h1_framing_mismatch.lean diff --git a/src/Std/Http/Data/Headers/Basic.lean b/src/Std/Http/Data/Headers/Basic.lean index 518e23b1a942..ba0de157c94e 100644 --- a/src/Std/Http/Data/Headers/Basic.lean +++ b/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 @@ -152,16 +152,6 @@ Returns `true` if the transfer encoding ends with chunked. 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. --/ -def parse (v : Value) : Option TransferEncoding := do - let codings ← parseTokenList v - if h : TransferEncoding.Validate codings then - some ⟨codings, h⟩ - else - none - /-- Checks a transfer parameter: `token BWS "=" BWS ( token / quoted-string )` (RFC 9112 §7). -/ @@ -188,6 +178,17 @@ def parseCodings? (v : Value) : Option (Array String) := 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 ← 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 diff --git a/src/Std/Http/Protocol/H1.lean b/src/Std/Http/Protocol/H1.lean index 101b4826d495..f1542defe9f8 100644 --- a/src/Std/Http/Protocol/H1.lean +++ b/src/Std/Http/Protocol/H1.lean @@ -917,30 +917,36 @@ def suppressOutgoingBody (machine : Machine dir) (forceZero : Bool := false) : M { w with omitBody := true, userClosedBody := true, knownSize, userData := #[], userDataBytes := 0 } /-- -Rejects user-provided framing headers when framing must come from machine state. +Reconciles the body length the caller set (`knownSize`) with the framing fields of the message head +passed to `send`, adopting the fields' length when none was set. Returns `none` when the two +contradict, or when the fields describe no length. -/ -@[inline] -private def failOnFramingHeaders (machine : Machine dir) (framingInHeaders : Bool) : Machine dir := - if framingInHeaders then - failBadMessage machine - else - machine +private def reconcileOutgoingFraming (machine : Machine dir) + (headerSize : Option Body.Length) (framingInHeaders : Bool) : Option (Machine dir) := + match machine.writer.knownSize, headerSize with + | some explicit, some parsed => if explicit == parsed then some machine else none + | none, some parsed => some (machine.setKnownSize parsed) + | _, none => if framingInHeaders then none else some machine /-- -Reconciles explicit machine framing (`knownSize`) with user-provided framing -headers from `send` and rejects contradictory inputs. +Handles a message head that `reconcileOutgoingFraming` rejected. None of that message is written: +a server answers `500 Internal Server Error` without a body and closes the connection, and a client +ends the exchange. Both report `.failed .badMessage`, and the machine halts once its output is taken. -/ -private def reconcileOutgoingFraming (machine : Machine dir) - (headerSize : Option Body.Length) (framingInHeaders : Bool) : Machine dir := - match machine.writer.knownSize, headerSize with - | some explicit, some parsed => - if explicit == parsed then machine else failBadMessage machine - | some _, none => - failOnFramingHeaders machine framingInHeaders - | none, some parsed => - machine.setKnownSize parsed - | none, none => - failOnFramingHeaders machine framingInHeaders +private def rejectOutgoingFraming (machine : Machine dir) : Machine dir := + let machine := machine + |>.addEvent (.failed .badMessage) + |>.setError .badMessage + |>.disableKeepAlive + |>.closeReader + |>.setReaderState .closed + match dir, machine with + | .receiving, machine => + -- `omitBody` makes the connection drop the handler's body instead of draining it. + machine.modifyWriter (fun w => { w with + messageHead := { status := .internalServerError }, sentMessage := true, state := .waitingForFlush }) + |>.suppressOutgoingBody (forceZero := true) + | .sending, machine => machine.closeWriter /-- Marks outgoing bodies as omitted when response semantics (or HEAD method) require @@ -969,6 +975,17 @@ private def isWriterClosed (machine : Machine dir) : Bool := | .closed => true | _ => false +/-- +Returns `true` when the outgoing message is a response that carries no body: one to a `HEAD` +request, or one whose status forbids a body. +-/ +@[inline] +private def omitsResponseBody (machine : Machine dir) (message : Message.Head dir.swap) : Bool := + match dir with + | .receiving => + responseMustNotHaveBody message.status ∨ machine.reader.messageHead.method == .head + | .sending => false + /-- Send the head of a message to the machine. @@ -979,6 +996,12 @@ Informational (1xx) responses are written directly to the output buffer, or drop request is HTTP/1.0; the writer stays in `waitingHeaders` so the application can send additional interim responses or the final response. The reader state is not affected — use `canContinue` to resolve an `Expect: 100-continue` decision separately. + +A head whose `Content-Length` or `Transfer-Encoding` contradicts the length set with +`setKnownSize`, or describes no length, is not written: a server answers `500 Internal Server +Error` and closes the connection, and a client ends the exchange, both reporting +`.failed .badMessage`. A response without a body (to `HEAD`, or a 204 or 304) cannot contradict +it, and a HEAD response advertises the `Content-Length` of its head. -/ @[inline] def send (machine : Machine dir) (message : Message.Head dir.swap) : Machine dir := @@ -1007,17 +1030,21 @@ def send (machine : Machine dir) (message : Message.Head dir.swap) : Machine dir w with outputData := w.outputData.push (ByteArray.empty ++ message) }) else - let hadFailure := machine.failed - let machine := machine.modifyWriter ({ · with messageHead := message, sentMessage := true }) let framingInHeaders := hasFramingHeaders message let headerSize := if framingInHeaders then message.getSize false else none + let reconciled := + if omitsResponseBody machine message then + -- No body goes out, so none can contradict the fields. RFC 9110 §8.6: `Content-Length` on + -- a HEAD response is the length a GET would have, which only the handler knows. + some (headerSize.elim machine machine.setKnownSize) + else + reconcileOutgoingFraming machine headerSize framingInHeaders - let machine := reconcileOutgoingFraming machine headerSize framingInHeaders - let machine := maybeSuppressOutgoingBody machine message - - if machine.failed && !hadFailure then - machine - else + match reconciled with + | none => rejectOutgoingFraming machine + | some machine => + let machine := machine.modifyWriter ({ · with messageHead := message, sentMessage := true }) + let machine := maybeSuppressOutgoingBody machine message match dir, machine with | .sending, machine => machine.setWriterState .waitingForFlush |>.setReaderState .needStartLine | .receiving, machine => machine.setWriterState .waitingForFlush diff --git a/tests/async/elab/async_http_h1_framing_mismatch.lean b/tests/async/elab/async_http_h1_framing_mismatch.lean new file mode 100644 index 000000000000..e5f595141c53 --- /dev/null +++ b/tests/async/elab/async_http_h1_framing_mismatch.lean @@ -0,0 +1,149 @@ +import Std.Http +import Std.Http.Test.Helpers + +open Std.Async +open Std Http Internal Test +open Std.Http.Protocol.H1 + +/-! +Tests a message head whose framing fields contradict the body length set for it, such as a handler +response with `Content-Length: 3` and a streamed body. The server answers `500 Internal Server +Error` and closes the connection instead of spinning in its connection loop, and a client ends the +exchange. A response that carries no body (to `HEAD`, 204, 304) cannot contradict it: a HEAD +response advertises the handler's `Content-Length`. +-/ + +/-- +Steps `machine` until it halts. Returns everything it wrote and every event it emitted, or `none` +if it has not halted after 16 steps. +-/ +def runToHalt (machine : Machine dir) : Option (String × Array (Event dir)) := Id.run do + let mut machine := machine + let mut out := "" + let mut events := #[] + for _ in [0:16] do + let (next, step) := machine.step + machine := next + out := out ++ String.fromUTF8! step.output.toByteArray + events := events ++ step.events + if machine.halted then return some (out, events) + return none + +/-- A server machine that has read `request`. -/ +def server (request : String) : Machine .receiving := + (({ config := {} } : Machine .receiving).feed request.toUTF8).step.1 + +def headers (fields : List (Header.Name × String)) : Headers := + fields.foldl (fun hs (name, value) => hs.insert name (Header.Value.ofString! value)) .empty + +def get : String := "GET / HTTP/1.1\r\nHost: a\r\n\r\n" + +def abc : Array Chunk := #[Chunk.ofByteArray "abc".toUTF8] + +/-- Runs `machine` to a halt and checks that it answered 500 without writing the body. -/ +def expect500 (name : String) (machine : Machine .receiving) : IO Unit := do + let some (out, events) := runToHalt (machine.sendData abc |>.userClosedBody) + | throw <| IO.userError s!"[{name}] the server never halted" + unless out.startsWith "HTTP/1.1 500 Internal Server Error\r\n" && + out.contains "Content-Length: 0\r\n" && out.contains "Connection: close\r\n" && + !out.contains "abc" do + throw <| IO.userError s!"[{name}] expected an empty 500, got:\n{out.quote}" + unless events.any (· matches .failed .badMessage) do + throw <| IO.userError s!"[{name}] no failure reported: {repr events}" + +/-- Runs `machine` to a halt and returns its output, failing on a reported failure. -/ +def expectOk (name : String) (machine : Machine .receiving) : IO String := do + let some (out, events) := runToHalt machine + | throw <| IO.userError s!"[{name}] the server never halted" + if events.any (· matches .failed _) then + throw <| IO.userError s!"[{name}] unexpected failure: {repr events}\n{out.quote}" + return out + +#eval runGroup "server machine: contradictory framing" do + -- A streamed body with a handler's `Content-Length`. + expect500 "chunked body, Content-Length: 3" <| server get + |>.setKnownSize .chunked + |>.send { status := .ok, headers := headers [(Header.Name.contentLength, "3")] } + + -- An empty body with a handler's `Content-Length`. + expect500 "empty body, Content-Length: 1234" <| server get + |>.setKnownSize (.fixed 0) + |>.send { status := .ok, headers := headers [(Header.Name.contentLength, "1234")] } + + -- Framing fields that describe no length. + let both := headers [(Header.Name.contentLength, "3"), (Header.Name.transferEncoding, "chunked")] + expect500 "Content-Length with Transfer-Encoding" <| server get + |>.send { status := .ok, headers := both } + + -- Control: matching framing writes the response. + let out ← expectOk "matching Content-Length" <| server + "GET / HTTP/1.1\r\nHost: a\r\nConnection: close\r\n\r\n" + |>.setKnownSize (.fixed 3) + |>.send { status := .ok, headers := headers [(Header.Name.contentLength, "3")] } + |>.sendData abc |>.userClosedBody + unless out.startsWith "HTTP/1.1 200 OK\r\n" && out.endsWith "\r\n\r\nabc" do + throw <| IO.userError s!"matching Content-Length: got\n{out.quote}" + +#eval runGroup "server machine: bodyless responses keep the handler's length" do + let head := "HEAD / HTTP/1.1\r\nHost: a\r\nConnection: close\r\n\r\n" + for size in [Body.Length.chunked, .fixed 0] do + let out ← expectOk s!"HEAD, {repr size}" <| server head + |>.setKnownSize size + |>.send { status := .ok, headers := headers [(Header.Name.contentLength, "1234")] } + unless out.startsWith "HTTP/1.1 200 OK\r\n" && out.contains "Content-Length: 1234\r\n" && + !out.contains "Transfer-Encoding" do + throw <| IO.userError s!"HEAD, {repr size}: expected Content-Length: 1234, got\n{out.quote}" + + let close := "GET / HTTP/1.1\r\nHost: a\r\nConnection: close\r\n\r\n" + for status in [Status.noContent, .notModified] do + let out ← expectOk s!"{status}" <| server close + |>.setKnownSize (.fixed 0) + |>.send { status, headers := headers [(Header.Name.contentLength, "9")] } + unless out.startsWith s!"HTTP/1.1 {status.toCode} " && !out.contains "Content-Length" do + throw <| IO.userError s!"{status}: expected no framing fields, got\n{out.quote}" + +#eval show IO Unit from do + -- Client side: a request declaring 10 bytes for a 3-byte body ends the exchange unwritten. + let request : Request.Head := + (Request.new |>.method .put |>.uri! "/upload" |>.header! "Host" "example.com" + |>.header! "Content-Length" "10").line + let machine := ({ config := {} } : Machine .sending) + |>.setKnownSize (.fixed 3) + |>.send request + |>.sendData abc |>.userClosedBody + let some (out, events) := runToHalt machine + | throw <| IO.userError "the client never halted" + unless out.isEmpty && events.any (· matches .failed .badMessage) do + throw <| IO.userError s!"client: expected a failure and no output, got {repr events}\n{out.quote}" + +#eval runGroup "server: handler framing contradicts its body" do + checkTimed "streamed body with Content-Length: 3" + (raw := get) + (handler := fun _ => Response.ok |>.header! "Content-Length" "3" + |>.stream fun s => s.send (Chunk.ofByteArray "abc".toUTF8)) + (expect := fun r => do + assertStatus r "HTTP/1.1 500 Internal Server Error" + assertAbsent r "abc") + + checkTimed "empty body with Content-Length: 1234" + (raw := get) + (handler := fun _ => Response.ok |>.header! "Content-Length" "1234" |>.text "") + (expect := (assertStatus · "HTTP/1.1 500 Internal Server Error")) + + -- The 500 closes the connection, so a pipelined request gets no answer. + checkTimed "pipelined request after the 500" + (raw := get ++ get) + (handler := fun _ => Response.ok |>.header! "Content-Length" "1234" |>.text "") + (expect := fun r => do + let text := String.fromUTF8! r + unless (text.splitOn "HTTP/1.1 ").length == 2 do + throw <| IO.userError s!"expected exactly one response, got:\n{text.quote}") + + checkTimed "HEAD with a streamed body and Content-Length: 1234" + (raw := "HEAD / HTTP/1.1\r\nHost: a\r\nConnection: close\r\n\r\n") + (handler := fun _ => Response.ok |>.header! "Content-Length" "1234" + |>.stream fun s => s.send (Chunk.ofByteArray "abc".toUTF8)) + (expect := fun r => do + assertStatus r "HTTP/1.1 200 OK" + assertContains r "Content-Length: 1234\r\n" + assertAbsent r "abc") diff --git a/tests/async/elab/async_http_headers.lean b/tests/async/elab/async_http_headers.lean index 857ae2afdeef..85d63c109480 100644 --- a/tests/async/elab/async_http_headers.lean +++ b/tests/async/elab/async_http_headers.lean @@ -315,6 +315,22 @@ info: ("content-length", "42") #guard (Header.TransferEncoding.parse =<< (Value.ofString? "g zip")).isNone #guard (Header.TransferEncoding.parse =<< (Value.ofString? "\"chunked\"")).isNone +-- Transfer parameters are checked and dropped, as by the machine's `parseCodings?`; `chunked` has none. +#guard ((Header.TransferEncoding.parse =<< Value.ofString? "gzip;level=1, chunked").map (·.codings)) + == some #["gzip", "chunked"] +#guard ((Header.TransferEncoding.parse =<< Value.ofString? "GZIP ; q=\"a b\" , Chunked").map (·.codings)) + == some #["gzip", "chunked"] +#guard (Header.TransferEncoding.parse =<< (Value.ofString? "chunked;x=1")).isNone +#guard (Header.TransferEncoding.parse =<< (Value.ofString? "gzip;level, chunked")).isNone +#guard (Header.TransferEncoding.parse =<< (Value.ofString? "gzip;=1, chunked")).isNone + +-- Wherever `parse` accepts a value, it frames the message as the machine does. +#guard ["chunked", "gzip, chunked", "gzip;level=1, chunked", "gzip", "x-custom;a=b"].all fun s => + match Value.ofString? s with + | some v => (Header.TransferEncoding.parse v).map (·.isChunked) == + Header.TransferEncoding.finalCodingIsChunked? v + | none => false + /-- info: ("transfer-encoding", "gzip,chunked") -/ From 9bb7954653b7ee600985b77b325e9c45737d7d73 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 6 Nov 2026 13:21:41 -0300 Subject: [PATCH 5/5] fix: remove useless test --- src/Std/Http/Protocol/H1.lean | 48 +++++++----- .../elab/async_http_h1_framing_mismatch.lean | 74 +++++++++++++++---- .../elab/async_http_h1_line_limit_split.lean | 34 --------- 3 files changed, 90 insertions(+), 66 deletions(-) delete mode 100644 tests/async/elab/async_http_h1_line_limit_split.lean diff --git a/src/Std/Http/Protocol/H1.lean b/src/Std/Http/Protocol/H1.lean index f1542defe9f8..d7a552a79041 100644 --- a/src/Std/Http/Protocol/H1.lean +++ b/src/Std/Http/Protocol/H1.lean @@ -575,9 +575,8 @@ state transitions. - On success, advances reader input. - On EOF with open input, emits `needMoreData`. - On EOF after `noMoreInput`, fails with `connectionClosed`. -- On a size-limit breach, fails with `badMessage`. A hard parse error found at or past the limit - counts as a breach, so the outcome does not depend on how the input was split. -- On other hard parse errors, fails with `onHardError`. +- On a size-limit breach, fails with `badMessage`. +- On hard parse errors, fails with `onHardError`. -/ private def parseWith (machine : Machine dir) (parser : Parser α) (limit : Option Nat) (expect : Option Nat := none) @@ -606,11 +605,8 @@ private def parseWith (machine : Machine dir) (parser : Parser α) (limit : Opti else (machine.addEvent (.needMoreData expect), none) else (machine.addEvent (.needMoreData expect), none) - | .error it err => - if limit.any (remaining - it.remainingBytes ≥ ·) then - (machine.setFailure .badMessage, none) - else - (machine.setFailure (onHardError err), none) + | .error _ err => + (machine.setFailure (onHardError err), none) -- Message Processing @@ -918,25 +914,38 @@ def suppressOutgoingBody (machine : Machine dir) (forceZero : Bool := false) : M /-- Reconciles the body length the caller set (`knownSize`) with the framing fields of the message head -passed to `send`, adopting the fields' length when none was set. Returns `none` when the two -contradict, or when the fields describe no length. +passed to `send`. The fields' length is adopted when none was set, or when only `chunked` was, which +leaves the length unknown (a `Body.stream` starts that way). Returns `none` when the two contradict, +or when the fields describe no length. -/ private def reconcileOutgoingFraming (machine : Machine dir) (headerSize : Option Body.Length) (framingInHeaders : Bool) : Option (Machine dir) := match machine.writer.knownSize, headerSize with - | some explicit, some parsed => if explicit == parsed then some machine else none + | some explicit, some parsed => + if explicit == parsed then some machine + -- The fixed-length writer closes the connection if the body then runs over or falls short. + else if explicit == .chunked then some (machine.setKnownSize parsed) + else none | none, some parsed => some (machine.setKnownSize parsed) | _, none => if framingInHeaders then none else some machine +/-- +The failure `rejectOutgoingFraming` reports: a mistake of the sender's own code, not a malformed +message from the peer. A server passes it to `Handler.onFailure`. +-/ +private def framingMismatchError : H1.Error := + .other "Content-Length or Transfer-Encoding contradicts the body" + /-- Handles a message head that `reconcileOutgoingFraming` rejected. None of that message is written: a server answers `500 Internal Server Error` without a body and closes the connection, and a client -ends the exchange. Both report `.failed .badMessage`, and the machine halts once its output is taken. +ends the exchange. Both report `framingMismatchError`, and the machine halts once its output is +taken. -/ private def rejectOutgoingFraming (machine : Machine dir) : Machine dir := let machine := machine - |>.addEvent (.failed .badMessage) - |>.setError .badMessage + |>.addEvent (.failed framingMismatchError) + |>.setError framingMismatchError |>.disableKeepAlive |>.closeReader |>.setReaderState .closed @@ -997,11 +1006,14 @@ request is HTTP/1.0; the writer stays in `waitingHeaders` so the application can interim responses or the final response. The reader state is not affected — use `canContinue` to resolve an `Expect: 100-continue` decision separately. -A head whose `Content-Length` or `Transfer-Encoding` contradicts the length set with +A `Content-Length` in the head gives the length of a body set as `chunked`, whose length is unknown. +A head whose `Content-Length` or `Transfer-Encoding` otherwise contradicts the length set with `setKnownSize`, or describes no length, is not written: a server answers `500 Internal Server -Error` and closes the connection, and a client ends the exchange, both reporting -`.failed .badMessage`. A response without a body (to `HEAD`, or a 204 or 304) cannot contradict -it, and a HEAD response advertises the `Content-Length` of its head. +Error` and closes the connection, and a client ends the exchange. Both emit `.failed` with an +`.other` error and set `error`, but the reader ends `.closed`, not failed, so the machine halts and +`failed` stays `false`. +A response without a body (to `HEAD`, or a 204 or 304) cannot contradict it, and a HEAD response +advertises the `Content-Length` of its head. -/ @[inline] def send (machine : Machine dir) (message : Message.Head dir.swap) : Machine dir := diff --git a/tests/async/elab/async_http_h1_framing_mismatch.lean b/tests/async/elab/async_http_h1_framing_mismatch.lean index e5f595141c53..7f352b547060 100644 --- a/tests/async/elab/async_http_h1_framing_mismatch.lean +++ b/tests/async/elab/async_http_h1_framing_mismatch.lean @@ -7,10 +7,11 @@ open Std.Http.Protocol.H1 /-! Tests a message head whose framing fields contradict the body length set for it, such as a handler -response with `Content-Length: 3` and a streamed body. The server answers `500 Internal Server -Error` and closes the connection instead of spinning in its connection loop, and a client ends the -exchange. A response that carries no body (to `HEAD`, 204, 304) cannot contradict it: a HEAD -response advertises the handler's `Content-Length`. +response with `Content-Length: 3` and an empty body. The server answers `500 Internal Server Error` +and closes the connection instead of spinning in its connection loop, and a client ends the +exchange. A `Content-Length` gives the length of a streamed body, which has none of its own. A +response that carries no body (to `HEAD`, 204, 304) cannot contradict it: a HEAD response +advertises the handler's `Content-Length`. -/ /-- @@ -48,8 +49,8 @@ def expect500 (name : String) (machine : Machine .receiving) : IO Unit := do out.contains "Content-Length: 0\r\n" && out.contains "Connection: close\r\n" && !out.contains "abc" do throw <| IO.userError s!"[{name}] expected an empty 500, got:\n{out.quote}" - unless events.any (· matches .failed .badMessage) do - throw <| IO.userError s!"[{name}] no failure reported: {repr events}" + unless events.any (· matches .failed (.other _)) do + throw <| IO.userError s!"[{name}] no framing failure reported: {repr events}" /-- Runs `machine` to a halt and returns its output, failing on a reported failure. -/ def expectOk (name : String) (machine : Machine .receiving) : IO String := do @@ -60,11 +61,6 @@ def expectOk (name : String) (machine : Machine .receiving) : IO String := do return out #eval runGroup "server machine: contradictory framing" do - -- A streamed body with a handler's `Content-Length`. - expect500 "chunked body, Content-Length: 3" <| server get - |>.setKnownSize .chunked - |>.send { status := .ok, headers := headers [(Header.Name.contentLength, "3")] } - -- An empty body with a handler's `Content-Length`. expect500 "empty body, Content-Length: 1234" <| server get |>.setKnownSize (.fixed 0) @@ -84,6 +80,28 @@ def expectOk (name : String) (machine : Machine .receiving) : IO String := do unless out.startsWith "HTTP/1.1 200 OK\r\n" && out.endsWith "\r\n\r\nabc" do throw <| IO.userError s!"matching Content-Length: got\n{out.quote}" +#eval runGroup "server machine: Content-Length gives a streamed body its length" do + let close := "GET / HTTP/1.1\r\nHost: a\r\nConnection: close\r\n\r\n" + -- `Body.stream` sets `chunked` before its producer runs, and a producer may set the length + -- itself before the server reads it: the head's length wins over `chunked` and matches the other. + for size in [Body.Length.chunked, .fixed 3] do + let out ← expectOk s!"{repr size}, Content-Length: 3" <| server close + |>.setKnownSize size + |>.send { status := .ok, headers := headers [(Header.Name.contentLength, "3")] } + |>.sendData abc |>.userClosedBody + unless out.startsWith "HTTP/1.1 200 OK\r\n" && out.contains "Content-Length: 3\r\n" && + !out.contains "Transfer-Encoding" && out.endsWith "\r\n\r\nabc" do + throw <| IO.userError s!"{repr size}, Content-Length: 3: got\n{out.quote}" + + -- A stream longer than its `Content-Length` closes the connection without writing its bytes. + let some (out, events) := runToHalt (server close + |>.setKnownSize .chunked + |>.send { status := .ok, headers := headers [(Header.Name.contentLength, "3")] } + |>.sendData #[Chunk.ofByteArray "abcd".toUTF8] |>.userClosedBody) + | throw <| IO.userError "overlong stream: the server never halted" + unless out.endsWith "Content-Length: 3\r\n\r\n" && events.any (· matches .close) do + throw <| IO.userError s!"overlong stream: got {repr events}\n{out.quote}" + #eval runGroup "server machine: bodyless responses keep the handler's length" do let head := "HEAD / HTTP/1.1\r\nHost: a\r\nConnection: close\r\n\r\n" for size in [Body.Length.chunked, .fixed 0] do @@ -113,16 +131,44 @@ def expectOk (name : String) (machine : Machine .receiving) : IO String := do |>.sendData abc |>.userClosedBody let some (out, events) := runToHalt machine | throw <| IO.userError "the client never halted" - unless out.isEmpty && events.any (· matches .failed .badMessage) do + unless out.isEmpty && events.any (· matches .failed (.other _)) do throw <| IO.userError s!"client: expected a failure and no output, got {repr events}\n{out.quote}" + -- A streamed upload takes its length from the request's `Content-Length`. + let request : Request.Head := + (Request.new |>.method .put |>.uri! "/upload" |>.header! "Host" "example.com" + |>.header! "Content-Length" "3").line + let machine := ({ config := {} } : Machine .sending) + |>.setKnownSize .chunked + |>.send request + |>.sendData abc |>.userClosedBody + let mut machine := machine + let mut out := "" + for _ in [0:8] do + let (next, step) := machine.step + machine := next + out := out ++ String.fromUTF8! step.output.toByteArray + unless out.contains "Content-Length: 3\r\n" && !out.contains "Transfer-Encoding" && + out.endsWith "\r\n\r\nabc" && machine.error.isNone do + throw <| IO.userError s!"streamed upload: got {repr machine.error}\n{out.quote}" + #eval runGroup "server: handler framing contradicts its body" do checkTimed "streamed body with Content-Length: 3" - (raw := get) + (raw := mkGetClose) (handler := fun _ => Response.ok |>.header! "Content-Length" "3" |>.stream fun s => s.send (Chunk.ofByteArray "abc".toUTF8)) (expect := fun r => do - assertStatus r "HTTP/1.1 500 Internal Server Error" + assertStatus r "HTTP/1.1 200 OK" + assertContains r "Content-Length: 3\r\n" + assertAbsent r "Transfer-Encoding" + assertContains r "\r\n\r\nabc") + + checkTimed "streamed body longer than its Content-Length: 3" + (raw := get) + (handler := fun _ => Response.ok |>.header! "Content-Length" "3" + |>.stream fun s => s.send (Chunk.ofByteArray "abcd".toUTF8)) + (expect := fun r => do + assertStatus r "HTTP/1.1 200 OK" assertAbsent r "abc") checkTimed "empty body with Content-Length: 1234" diff --git a/tests/async/elab/async_http_h1_line_limit_split.lean b/tests/async/elab/async_http_h1_line_limit_split.lean deleted file mode 100644 index 11bfed56d974..000000000000 --- a/tests/async/elab/async_http_h1_line_limit_split.lean +++ /dev/null @@ -1,34 +0,0 @@ -import Std.Http - -open Std Http -open Std.Http.Protocol.H1 - -/-! -A request line over a limit fails the same way however its bytes arrive: an error found at or past -`maxStartLineLength` is reported as that limit, as it is when the limit is reached before the error. --/ - -def errorOf (config : Protocol.H1.Config) (parts : Array ByteArray) : Option Error := Id.run do - let mut m : Machine .receiving := { config } - for p in parts do - m := m.feed p - m := m.step.1 - return m.error - -def bytewise (data : ByteArray) : Array ByteArray := - (Array.range data.size).map fun i => data.extract i (i + 1) - -#eval show IO Unit from do - let line := s!"OPTIONS /{String.ofList (List.replicate 30 'a')} HTTP/1.1\r\nHost: a\r\n\r\n".toUTF8 - -- The URI limit is reached past the start-line limit: both ways report the start-line limit. - let config : Protocol.H1.Config := { maxStartLineLength := 20, maxUriLength := 16 } - let whole := errorOf config #[line] - let pieces := errorOf config (bytewise line) - unless whole == pieces && whole == some .badMessage do - throw <| IO.userError s!"start-line limit: whole {repr whole}, pieces {repr pieces}" - -- The URI limit is reached first: both ways report it. - let config : Protocol.H1.Config := { maxStartLineLength := 64, maxUriLength := 16 } - let whole := errorOf config #[line] - let pieces := errorOf config (bytewise line) - unless whole == pieces && whole == some .uriTooLong do - throw <| IO.userError s!"URI limit: whole {repr whole}, pieces {repr pieces}"