diff --git a/src/Std/Internal/Async/Select.lean b/src/Std/Internal/Async/Select.lean
index 996a160039cb..36318d47a52c 100644
--- a/src/Std/Internal/Async/Select.lean
+++ b/src/Std/Internal/Async/Select.lean
@@ -10,6 +10,8 @@ public import Init.Data.Random
public import Std.Internal.Async.Basic
import Init.Data.ByteArray.Extra
import Init.Data.Array.Lemmas
+public import Std.Sync.Mutex
+public import Std.Sync.Barrier
import Init.Omega
public section
@@ -132,6 +134,8 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
let gen := mkStdGen seed
let selectables := shuffleIt selectables gen
+ let gate ← IO.Promise.new
+
for selectable in selectables do
if let some val ← selectable.selector.tryFn then
let result ← selectable.cont val
@@ -141,6 +145,9 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
let promise ← IO.Promise.new
for selectable in selectables do
+ if ← finished.get then
+ break
+
let waiterPromise ← IO.Promise.new
let waiter := Waiter.mk finished waiterPromise
selectable.selector.registerFn waiter
@@ -157,18 +164,20 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
let async : Async _ :=
try
let res ← IO.ofExcept res
+ discard <| await gate.result?
for selectable in selectables do
selectable.selector.unregisterFn
- let contRes ← selectable.cont res
- promise.resolve (.ok contRes)
+ promise.resolve (.ok (← selectable.cont res))
catch e =>
promise.resolve (.error e)
async.toBaseIO
- Async.ofPromise (pure promise)
+ gate.resolve ()
+ let result ← Async.ofPromise (pure promise)
+ return result
/--
Performs fair and data-loss free non-blocking multiplexing on the `Selectable`s in `selectables`.
@@ -224,6 +233,8 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
let derivedWaiter := Waiter.mk waiter.finished waiterPromise
selectable.selector.registerFn derivedWaiter
+ let barrier ← IO.Promise.new
+
discard <| IO.bindTask (t := waiterPromise.result?) fun res? => do
match res? with
| none => return (Task.pure (.ok ()))
@@ -231,6 +242,7 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
let async : Async _ := do
let mainPromise := waiter.promise
+ await barrier
for selectable in selectables do
selectable.selector.unregisterFn
diff --git a/src/Std/Internal/Http.lean b/src/Std/Internal/Http.lean
index 9c7ee1f6899b..c882b9bb3573 100644
--- a/src/Std/Internal/Http.lean
+++ b/src/Std/Internal/Http.lean
@@ -6,5 +6,188 @@ Authors: Sofia Rodrigues
module
prelude
-public import Std.Internal.Http.Data
-public import Std.Internal.Http.Protocol.H1
+public import Std.Internal.Http.Server
+
+public section
+
+/-!
+# HTTP Library
+
+A low-level HTTP/1.1 server implementation for Lean. This library provides a pure,
+sans-I/O protocol implementation that can be used with the `Async` library or with
+custom connection handlers.
+
+## Overview
+
+This module provides a complete HTTP/1.1 server implementation with support for:
+
+- Request/response handling with directional streaming bodies
+- Keep-alive connections
+- Chunked transfer encoding
+- Header validation and management
+- Configurable timeouts and limits
+
+**Sans I/O Architecture**: The core protocol logic doesn't perform any actual I/O itself -
+it just defines how data should be processed. This separation allows the protocol implementation
+to remain pure and testable, while different transports (TCP sockets, mock clients) handle
+the actual reading and writing of bytes.
+
+## Quick Start
+
+The main entry point is `Server.serve`, which starts an HTTP/1.1 server. Implement the
+`Server.Handler` type class to define how the server handles requests, errors, and
+`Expect: 100-continue` headers:
+
+```lean
+import Std.Internal.Http
+
+open Std Internal IO Async
+open Std Http Server
+
+structure MyHandler
+
+instance : Handler MyHandler where
+ onRequest _ req := do
+ Response.ok |>.text "Hello, World!"
+
+def main : IO Unit := Async.block do
+ let addr : Net.SocketAddress := .v4 ⟨.ofParts 127 0 0 1, 8080⟩
+ let server ← Server.serve addr MyHandler.mk
+ server.waitShutdown
+```
+
+## Working with Requests
+
+Incoming requests are represented by `Request Body.Incoming`, which bundles the request
+line, parsed headers, and a lazily-consumed body. Headers are available immediately,
+while the body can be streamed or collected on demand, allowing handlers to process both
+small and large payloads efficiently.
+
+### Reading Headers
+
+```lean
+def handler (req : Request Body.Incoming) : ContextAsync (Response Body.Outgoing) := do
+ -- Access request method and URI
+ let method := req.head.method -- Method.get, Method.post, etc.
+ let uri := req.head.uri -- RequestTarget
+
+ -- Read a specific header
+ if let some contentType := req.head.headers.get? (.mk "content-type") then
+ IO.println s!"Content-Type: {contentType}"
+
+ Response.ok |>.text "OK"
+```
+
+### URI Query Semantics
+
+`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.
+
+### Reading the Request Body
+
+The request body is exposed as `Body.Incoming`, which can be consumed incrementally or
+collected into memory. The `readAll` method reads the entire body, with an optional size
+limit to protect against unbounded payloads.
+
+```lean
+def handler (req : Request Body.Incoming) : ContextAsync (Response Body.Outgoing) := do
+ -- Collect entire body as a String
+ let bodyStr : String ← req.body.readAll
+
+ -- Or with a maximum size limit
+ let bodyStr : String ← req.body.readAll (maximumSize := some 1024)
+
+ Response.ok |>.text s!"Received: {bodyStr}"
+```
+
+## Building Responses
+
+Responses are constructed using a builder API that starts from a status code and adds
+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.Outgoing)`.
+
+```lean
+-- Text response
+Response.ok |>.text "Hello!"
+
+-- HTML response
+Response.ok |>.html "Hello!
"
+
+-- JSON response
+Response.ok |>.json "{\"key\": \"value\"}"
+
+-- Binary response
+Response.ok |>.bytes someByteArray
+
+-- Custom status
+Response.new |>.status .created |>.text "Resource created"
+
+-- With custom headers
+Response.ok
+ |>.header! "X-Custom-Header" "value"
+ |>.header! "Cache-Control" "no-cache"
+ |>.text "Response with headers"
+```
+
+### Streaming Responses
+
+For large responses or server-sent events, use streaming:
+
+```lean
+def handler (req : Request Body.Incoming) : ContextAsync (Response Body.Outgoing) := do
+ Response.ok
+ |>.header! "Content-Type" "text/plain"
+ |>.stream fun stream => do
+ for i in [0:10] do
+ stream.send { data := s!"chunk {i}\n".toUTF8 }
+ Async.sleep 1000
+ stream.close
+```
+
+## Server Configuration
+
+Configure server behavior with `Config`:
+
+```lean
+def config : Config := {
+ maxRequests := 10000000,
+ lingeringTimeout := 5000,
+}
+
+let server ← Server.serve addr MyHandler.mk config
+```
+
+## Handler Type Class
+
+Implement `Server.Handler` to define how the server processes events. The class has three
+methods, all with default implementations:
+
+- `onRequest` — called for each incoming request; returns a response inside `ContextAsync`
+- `onFailure` — called when an error occurs while processing a request
+- `onContinue` — called when a request includes an `Expect: 100-continue` header; return
+ `true` to accept the body or `false` to reject it
+
+```lean
+structure MyHandler where
+ greeting : String
+
+instance : Handler MyHandler where
+ onRequest self req := do
+ Response.ok |>.text self.greeting
+
+ onFailure self err := do
+ IO.eprintln s!"Error: {err}"
+```
+
+The handler methods operate in the following monads:
+
+- `onRequest` uses `ContextAsync` — an asynchronous monad (`ReaderT CancellationContext Async`) that provides:
+ - Full access to `Async` operations (spawning tasks, sleeping, concurrent I/O)
+ - A `CancellationContext` tied to the client connection — when the client disconnects, the
+ context is cancelled, allowing your handler to detect this and stop work early
+- `onFailure` uses `Async`
+- `onContinue` uses `Async`
+-/
diff --git a/src/Std/Internal/Http/Protocol/H1.lean b/src/Std/Internal/Http/Protocol/H1.lean
index 481ebb3b349e..b627b4b0c719 100644
--- a/src/Std/Internal/Http/Protocol/H1.lean
+++ b/src/Std/Internal/Http/Protocol/H1.lean
@@ -280,9 +280,9 @@ private def hasSingleAcceptedHostHeader (message : Message.Head .receiving) : Bo
| some ⟨host, _⟩ => authority.host == host -- && authority.port == port (Not so strict!)
| none => false
| _ =>
- match parsed with
- | some _ => true
- | none => false
+ -- RFC 9110 §7.2: when the target URI has no authority (origin-form, asterisk-form),
+ -- a client MUST send Host with an empty field value, so an empty value is valid here.
+ hostValue.value.isEmpty ∨ parsed.isSome
| _ => false
/--
@@ -1205,6 +1205,7 @@ private def parseChunkSizeBody (machine : Machine dir) :
let (machine, result) := parseWith machine
(parseChunkSize machine.config)
(limit := some machine.config.maxChunkLineLength)
+
match result with
| some (size, ext) =>
if size > machine.config.maxChunkSize then
@@ -1224,10 +1225,8 @@ private def parseLastChunkBodyState (machine : Machine dir)
Machine dir × Option PulledChunk × Bool :=
let (machine, result) := parseWith machine (parseLastChunkBody machine.config) (limit := none)
match result with
- | some _ =>
- emitBodyChunk machine .complete true false ext .empty (closeBody := true)
- | none =>
- bodyNoProgress machine
+ | some _ => emitBodyChunk machine .complete true false ext .empty (closeBody := true)
+ | none => bodyNoProgress machine
/--
Consumes chunk-data bytes for the current chunk, handling complete and partial
@@ -1296,8 +1295,6 @@ mutual
/--
Parses one request start-line in server mode and initializes `reader.messageHead`
for header parsing.
-
-Unsupported methods or versions are converted into protocol failures.
-/
private partial def processReceivingStartLine (machine : Machine .receiving) : Machine .receiving :=
diff --git a/src/Std/Internal/Http/Server.lean b/src/Std/Internal/Http/Server.lean
new file mode 100644
index 000000000000..8f84947d7369
--- /dev/null
+++ b/src/Std/Internal/Http/Server.lean
@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async
+public import Std.Internal.Async.TCP
+public import Std.Sync.CancellationToken
+public import Std.Sync.Semaphore
+public import Std.Internal.Http.Server.Config
+public import Std.Internal.Http.Server.Handler
+public import Std.Internal.Http.Server.Connection
+
+public section
+
+/-!
+# HTTP Server
+
+This module defines a simple, asynchronous HTTP/1.1 server implementation.
+
+It provides the `Std.Http.Server` structure, which encapsulates all server state, and functions for
+starting, managing, and gracefully shutting down the server.
+
+The server runs entirely using `Async` and uses a shared `CancellationContext` to signal shutdowns.
+Each active client connection is tracked, and the server automatically resolves its shutdown
+promise once all connections have closed.
+-/
+
+namespace Std.Http
+open Std.Internal.IO.Async TCP
+
+set_option linter.all true
+
+/--
+The `Server` structure holds all state required to manage the lifecycle of an HTTP server, including
+connection tracking and shutdown coordination.
+-/
+structure Server where
+
+ /--
+ The context used for shutting down all connections and the server.
+ -/
+ context : Std.CancellationContext
+
+ /--
+ Active HTTP connections
+ -/
+ activeConnections : Std.Mutex UInt64
+
+ /--
+ Semaphore used to enforce the maximum number of simultaneous active connections.
+ `none` means no connection limit.
+ -/
+ connectionLimit : Option Std.Semaphore
+
+ /--
+ Indicates when the server has successfully shut down.
+ -/
+ shutdownPromise : Std.Channel Unit
+
+ /--
+ Configuration of the server
+ -/
+ config : Std.Http.Config
+
+namespace Server
+
+/--
+Create a new `Server` structure with an optional configuration.
+-/
+def new (config : Std.Http.Config := {}) : IO Server := do
+ let context ← Std.CancellationContext.new
+ let activeConnections ← Std.Mutex.new 0
+ let connectionLimit ←
+ if config.maxConnections = 0 then
+ pure none
+ else
+ some <$> Std.Semaphore.new config.maxConnections
+ let shutdownPromise ← Std.Channel.new
+
+ return { context, activeConnections, connectionLimit, shutdownPromise, config }
+
+/--
+Triggers cancellation of all requests and the accept loop in the server. This function should be used
+in conjunction with `waitShutdown` to properly coordinate the shutdown sequence.
+-/
+@[inline]
+def shutdown (s : Server) : Async Unit :=
+ s.context.cancel .shutdown
+
+/--
+Waits for the server to shut down. Blocks until another task or async operation calls the `shutdown` function.
+-/
+@[inline]
+def waitShutdown (s : Server) : Async Unit := do
+ Async.ofAsyncTask ((← s.shutdownPromise.recv).map Except.ok)
+
+/--
+Returns a `Selector` that waits for the server to shut down.
+-/
+@[inline]
+def waitShutdownSelector (s : Server) : Selector Unit :=
+ s.shutdownPromise.recvSelector
+
+/--
+Triggers cancellation of all requests and the accept loop, then waits for the server to fully shut down.
+This is a convenience function combining `shutdown` and then `waitShutdown`.
+-/
+@[inline]
+def shutdownAndWait (s : Server) : Async Unit := do
+ s.context.cancel .shutdown
+ s.waitShutdown
+
+@[inline]
+private def frameCancellation (s : Server) (releaseConnectionPermit : Bool := false)
+ (action : ContextAsync α) : ContextAsync α := do
+ s.activeConnections.atomically (modify (· + 1))
+ try
+ action
+ finally
+ if releaseConnectionPermit then
+ if let some limit := s.connectionLimit then
+ limit.release
+
+ s.activeConnections.atomically do
+ modify (· - 1)
+
+ if (← get) = 0 ∧ (← s.context.isCancelled) then
+ discard <| s.shutdownPromise.send ()
+
+/--
+Start a new HTTP/1.1 server on the given socket address. This function uses `Async` to handle tasks
+and TCP connections, and returns a `Server` structure that can be used to cancel the server.
+-/
+def serve {σ : Type} [Handler σ]
+ (addr : Net.SocketAddress)
+ (handler : σ)
+ (config : Config := {}) (backlog : UInt32 := 1024) : Async Server := do
+
+ let httpServer ← Server.new config
+
+ let server ← Socket.Server.mk
+ server.bind addr
+ server.listen backlog
+ server.noDelay
+
+ let runServer := do
+ frameCancellation httpServer (action := do
+ while true do
+ let permitAcquired ←
+ if let some limit := httpServer.connectionLimit then
+ let permit ← limit.acquire
+ await permit
+ pure true
+ else
+ pure false
+
+ let result ← Selectable.one #[
+ .case (server.acceptSelector) (fun x => pure <| some x),
+ .case (← ContextAsync.doneSelector) (fun _ => pure none)
+ ]
+
+ match result with
+ | some client =>
+ let extensions ← do
+ match (← EIO.toBaseIO client.getPeerName) with
+ | .ok addr => pure <| Extensions.empty.insert (Server.RemoteAddr.mk addr)
+ | .error _ => pure Extensions.empty
+
+ ContextAsync.background
+ (frameCancellation httpServer (releaseConnectionPermit := permitAcquired)
+ (action := do
+ serveConnection client handler config extensions))
+ | none =>
+ if permitAcquired then
+ if let some limit := httpServer.connectionLimit then
+ limit.release
+ break
+ )
+
+ background (runServer httpServer.context)
+
+ return httpServer
+
+end Std.Http.Server
diff --git a/src/Std/Internal/Http/Server/Config.lean b/src/Std/Internal/Http/Server/Config.lean
new file mode 100644
index 000000000000..03aab54304ba
--- /dev/null
+++ b/src/Std/Internal/Http/Server/Config.lean
@@ -0,0 +1,196 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Time
+public import Std.Internal.Http.Protocol.H1
+
+public section
+
+/-!
+# Config
+
+This module exposes the `Config`, a structure that describes timeout, request and headers
+configuration of an HTTP Server.
+-/
+
+namespace Std.Http
+
+set_option linter.all true
+
+/--
+Connection limits configuration with validation.
+-/
+structure Config where
+ /--
+ Maximum number of simultaneous active connections (default: 1024).
+ Setting this to `0` disables the limit entirely: the server will accept any number of
+ concurrent connections and no semaphore-based cap is enforced. Use with care — an
+ unconstrained server may exhaust file descriptors or memory under adversarial load.
+ -/
+ maxConnections : Nat := 1024
+
+ /--
+ Maximum number of requests per connection.
+ -/
+ maxRequests : Nat := 100
+
+ /--
+ Maximum number of headers allowed per request.
+ -/
+ maxHeaders : Nat := 50
+
+ /--
+ Maximum aggregate byte size of all header field lines in a single message
+ (name + value bytes plus 4 bytes per line for `: ` and `\r\n`). Default: 64 KiB.
+ -/
+ maxHeaderBytes : Nat := 65536
+
+ /--
+ Timeout (in milliseconds) for receiving additional data while a request is actively being
+ processed (e.g. reading the request body). Applies after the request headers have been parsed
+ and replaces the keep-alive timeout for the duration of the request.
+ -/
+ lingeringTimeout : Time.Millisecond.Offset := 10000
+
+ /--
+ Timeout for keep-alive connections
+ -/
+ keepAliveTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨12000, by decide⟩
+
+ /--
+ Maximum time (in milliseconds) allowed to receive the complete request headers after the first
+ byte of a new request arrives. This prevents Slowloris-style attacks where a client sends bytes
+ at a slow rate to hold a connection slot open without completing a request. Once a request starts,
+ each individual read must complete within this window. Default: 5 seconds.
+ -/
+ headerTimeout : Time.Millisecond.Offset := 5000
+
+ /--
+ Whether to enable keep-alive connections by default.
+ -/
+ enableKeepAlive : Bool := true
+
+ /--
+ The maximum size that the connection can receive in a single recv call.
+ -/
+ maximumRecvSize : Nat := 8192
+
+ /--
+ Default buffer size for the connection
+ -/
+ defaultPayloadBytes : Nat := 8192
+
+ /--
+ Whether to automatically generate the `Date` header in responses.
+ -/
+ generateDate : Bool := true
+
+ /--
+ The `Server` header value injected into outgoing responses.
+ `none` suppresses the header entirely.
+ -/
+ serverName : Option Header.Value := some (.mk "LeanHTTP/1.1")
+
+ /--
+ Maximum length of request URI (default: 8192 bytes)
+ -/
+ maxUriLength : Nat := 8192
+
+ /--
+ Maximum number of bytes consumed while parsing request start-lines (default: 8192 bytes).
+ -/
+ maxStartLineLength : Nat := 8192
+
+ /--
+ Maximum length of header field name (default: 256 bytes)
+ -/
+ maxHeaderNameLength : Nat := 256
+
+ /--
+ Maximum length of header field value (default: 8192 bytes)
+ -/
+ maxHeaderValueLength : Nat := 8192
+
+ /--
+ Maximum number of spaces in delimiter sequences (default: 16)
+ -/
+ maxSpaceSequence : Nat := 16
+
+ /--
+ Maximum number of leading empty lines (bare CRLF) to skip before a request-line
+ (RFC 9112 §2.2 robustness). Default: 8.
+ -/
+ maxLeadingEmptyLines : Nat := 8
+
+ /--
+ Maximum length of chunk extension name (default: 256 bytes)
+ -/
+ maxChunkExtNameLength : Nat := 256
+
+ /--
+ Maximum length of chunk extension value (default: 256 bytes)
+ -/
+ maxChunkExtValueLength : Nat := 256
+
+ /--
+ Maximum number of bytes consumed while parsing one chunk-size line with extensions (default: 8192 bytes).
+ -/
+ maxChunkLineLength : Nat := 8192
+
+ /--
+ Maximum allowed chunk payload size in bytes (default: 8 MiB).
+ -/
+ maxChunkSize : Nat := 8 * 1024 * 1024
+
+ /--
+ Maximum allowed total body size per request in bytes (default: 64 MiB).
+ -/
+ maxBodySize : Nat := 64 * 1024 * 1024
+
+ /--
+ Maximum length of reason phrase (default: 512 bytes)
+ -/
+ maxReasonPhraseLength : Nat := 512
+
+ /--
+ Maximum number of trailer headers (default: 20)
+ -/
+ maxTrailerHeaders : Nat := 20
+
+ /--
+ Maximum number of extensions on a single chunk-size line (default: 16).
+ -/
+ maxChunkExtensions : Nat := 16
+
+namespace Config
+
+/--
+Converts to HTTP/1.1 config.
+-/
+def toH1Config (config : Config) : Protocol.H1.Config where
+ maxMessages := config.maxRequests
+ maxHeaders := config.maxHeaders
+ maxHeaderBytes := config.maxHeaderBytes
+ enableKeepAlive := config.enableKeepAlive
+ serverName := config.serverName
+ maxUriLength := config.maxUriLength
+ maxStartLineLength := config.maxStartLineLength
+ maxHeaderNameLength := config.maxHeaderNameLength
+ maxHeaderValueLength := config.maxHeaderValueLength
+ maxSpaceSequence := config.maxSpaceSequence
+ maxLeadingEmptyLines := config.maxLeadingEmptyLines
+ maxChunkExtensions := config.maxChunkExtensions
+ maxChunkExtNameLength := config.maxChunkExtNameLength
+ maxChunkExtValueLength := config.maxChunkExtValueLength
+ maxChunkLineLength := config.maxChunkLineLength
+ maxChunkSize := config.maxChunkSize
+ maxBodySize := config.maxBodySize
+ maxReasonPhraseLength := config.maxReasonPhraseLength
+ maxTrailerHeaders := config.maxTrailerHeaders
+
+end Std.Http.Config
diff --git a/src/Std/Internal/Http/Server/Connection.lean b/src/Std/Internal/Http/Server/Connection.lean
new file mode 100644
index 000000000000..6657d369e6c3
--- /dev/null
+++ b/src/Std/Internal/Http/Server/Connection.lean
@@ -0,0 +1,431 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async.TCP
+public import Std.Internal.Async.ContextAsync
+public import Std.Internal.Http.Transport
+public import Std.Internal.Http.Protocol.H1
+public import Std.Internal.Http.Server.Config
+public import Std.Internal.Http.Server.Handler
+
+public section
+
+namespace Std
+namespace Http
+namespace Server
+
+open Std Internal IO Async TCP Protocol
+open Time
+
+/-!
+# Connection
+
+This module defines `Server.Connection`, a structure used to handle a single HTTP connection with
+possibly multiple requests.
+-/
+
+set_option linter.all true
+
+/--
+Represents the remote address of a client connection.
+-/
+public structure RemoteAddr where
+ /--
+ The socket address of the remote client.
+ -/
+ addr : Net.SocketAddress
+deriving TypeName
+
+instance : ToString RemoteAddr where
+ toString addr := toString addr.addr.ipAddr ++ ":" ++ toString addr.addr.port
+
+/--
+A single HTTP connection.
+-/
+public structure Connection (α : Type) where
+ /--
+ The client connection.
+ -/
+ socket : α
+
+ /--
+ The processing machine for HTTP/1.1.
+ -/
+ machine : H1.Machine .receiving
+
+ /--
+ Extensions to attach to each request (e.g., remote address).
+ -/
+ extensions : Extensions := .empty
+
+namespace Connection
+
+private inductive Recv (β : Type)
+ | bytes (x : Option ByteArray)
+ | responseBody (x : Option Chunk)
+ | bodyInterest (x : Bool)
+ | response (x : (Except Error (Response β)))
+ | timeout
+ | shutdown
+ | close
+
+private def receiveWithTimeout {α : Type} {β : Type}
+ [Transport α] [Body.Reader β]
+ (socket : Option α)
+ (expect : UInt64)
+ (responseBody : Option β)
+ (requestBody : Option Body.Outgoing)
+ (response : Option (Std.Channel (Except Error (Response β))))
+ (timeoutMs : Millisecond.Offset)
+ (keepAliveTimeoutMs : Option Millisecond.Offset)
+ (headerTimeout : Option Timestamp)
+ (connectionContext : CancellationContext) : Async (Recv β) := do
+
+ let mut baseSelectables : Array (Selectable (Recv β)) := #[
+ .case connectionContext.doneSelector (fun _ => do
+ let reason ← connectionContext.getCancellationReason
+ match reason with
+ | some .deadline => pure .timeout
+ | _ => pure .shutdown)
+ ]
+
+ if let some socket := socket then
+ baseSelectables := baseSelectables.push (.case (Transport.recvSelector socket expect) (Recv.bytes · |> pure))
+
+ if let some keepAliveTimeout := keepAliveTimeoutMs then
+ baseSelectables := baseSelectables.push (.case (← Selector.sleep keepAliveTimeout) (fun _ => pure .timeout))
+ else if let some timeout := headerTimeout then
+ baseSelectables := baseSelectables.push (.case (← Selector.sleep (timeout - (← Timestamp.now)).toMilliseconds) (fun _ => pure .timeout))
+ else
+ baseSelectables := baseSelectables.push (.case (← Selector.sleep timeoutMs) (fun _ => pure .timeout))
+
+ if let some responseBody := responseBody then
+ baseSelectables := baseSelectables.push (.case (Body.Reader.recvSelector responseBody) (Recv.responseBody · |> pure))
+
+ if let some requestBody := requestBody then
+ baseSelectables := baseSelectables.push (.case (Body.Writer.interestSelector requestBody) (Recv.bodyInterest · |> pure))
+
+ if let some response := response then
+ baseSelectables := baseSelectables.push (.case response.recvSelector (Recv.response · |> pure))
+
+ Selectable.one baseSelectables
+
+private def processNeedMoreData
+ {σ : Type} {β : Type} [Transport α] [Handler σ] [Body.Reader β]
+ (config : Config)
+ (handler : σ)
+ (socket : Option α)
+ (expect : Option Nat)
+ (response : Option (Std.Channel (Except Error (Response β))))
+ (responseBody : Option β)
+ (requestBody : Option Body.Outgoing)
+ (timeout : Millisecond.Offset)
+ (keepAliveTimeout : Option Millisecond.Offset)
+ (headerTimeout : Option Timestamp)
+ (connectionContext : CancellationContext) : Async (Recv β) := do
+
+ let expectedBytes := expect
+ |>.getD config.defaultPayloadBytes
+ |>.min config.maximumRecvSize
+ |>.toUInt64
+
+ try
+ receiveWithTimeout socket expectedBytes responseBody requestBody response timeout keepAliveTimeout headerTimeout connectionContext
+ catch e =>
+ Handler.onFailure handler e
+ pure .close
+
+private def handleError (machine : H1.Machine .receiving) (status : Status) (waitingResponse : Bool) : H1.Machine .receiving × Bool :=
+ if machine.isWaitingMessage ∧ waitingResponse then
+ let machine := machine.send { status, headers := .empty |>.insert .connection (.mk "close") }
+ |>.userClosedBody
+ |>.closeReader
+ |>.noMoreInput
+ (machine, false)
+ else
+ (machine.closeWriter.noMoreInput, waitingResponse)
+
+private def handle
+ {σ : Type} [Transport α] [h : Handler σ]
+ (connection : Connection α)
+ (config : Config)
+ (connectionContext : CancellationContext)
+ (handler : σ) : Async Unit := do
+ let _ : Body.Reader (Handler.ResponseBody σ) := Handler.responseBodyReader
+ let _ : Body.Writer (Handler.ResponseBody σ) := Handler.responseBodyWriter
+
+ let mut machine := connection.machine
+ let socket := connection.socket
+
+ let (initRequestOut, initRequestIn) ← Body.mkChannel
+ let mut requestOutgoing := initRequestOut
+ let mut requestIncoming := initRequestIn
+ let mut keepAliveTimeout := some config.keepAliveTimeout.val
+ let mut currentTimeout := config.keepAliveTimeout.val
+
+ let mut headerTimeout : Option Timestamp := none
+
+ let mut response : Std.Channel (Except Error (Response (Handler.ResponseBody σ))) ← Std.Channel.new
+ let mut respStream : Option (Handler.ResponseBody σ) := none
+ let mut requiresData := false
+
+ let mut expectData := none
+ let mut waitingResponse := false
+ let mut pendingHead : Option Request.Head := none
+
+ while ¬machine.halted do
+ let (newMachine, step) := machine.step
+
+ machine := newMachine
+
+ if step.output.size > 0 then
+ try Transport.sendAll socket #[step.output.toByteArray]
+ catch e =>
+ Handler.onFailure handler e
+ break
+
+ for event in step.events do
+ match event with
+ | .needMoreData expect => do
+ requiresData := true
+ expectData := expect
+
+ | .needAnswer =>
+ pure ()
+
+ | .endHeaders head =>
+ currentTimeout := config.lingeringTimeout
+ keepAliveTimeout := none
+ headerTimeout := none
+
+ if let some length := head.getSize true then
+ Body.Writer.setKnownSize requestOutgoing (some length)
+
+ pendingHead := some head
+
+ | .«continue» =>
+ if let some head := pendingHead then
+
+ let continueChannel : Std.Channel Bool ← Std.Channel.new
+ let continueTask ← (Handler.onContinue handler head).asTask
+ BaseIO.chainTask continueTask fun
+ | .ok v => discard <| continueChannel.send v
+ | .error _ => discard <| continueChannel.send false
+ let canContinue ← Selectable.one #[
+ .case continueChannel.recvSelector pure,
+ .case connectionContext.doneSelector (fun _ => pure false),
+ .case (← Selector.sleep config.lingeringTimeout) (fun _ => pure false)
+ ]
+
+ let status := if canContinue then Status.«continue» else Status.expectationFailed
+ machine := machine.canContinue status
+ if ¬canContinue then
+ pendingHead := none
+
+ | .next => do
+ if ¬(← Body.Writer.isClosed requestOutgoing) then
+ Body.Writer.close requestOutgoing
+
+ let (newRequestOutgoing, newRequestIncoming) ← Body.mkChannel
+ requestOutgoing := newRequestOutgoing
+ requestIncoming := newRequestIncoming
+
+ response ← Std.Channel.new
+
+ if let some res := respStream then
+ if ¬(← Body.Reader.isClosed res) then Body.Reader.close res
+
+ respStream := none
+
+ keepAliveTimeout := some config.keepAliveTimeout.val
+ currentTimeout := config.keepAliveTimeout.val
+ headerTimeout := none
+ waitingResponse := false
+
+ | .failed err =>
+ Handler.onFailure handler (toString err)
+
+ pendingHead := none
+ requiresData := false
+ if ¬(← Body.Writer.isClosed requestOutgoing) then
+ Body.Writer.close requestOutgoing
+ break
+
+ | .closeBody =>
+ if ¬(← Body.Writer.isClosed requestOutgoing) then
+ Body.Writer.close requestOutgoing
+
+ | .close =>
+ pure ()
+
+ if let some head := pendingHead then
+ waitingResponse := true
+ let newResponse := Handler.onRequest handler { head, body := requestIncoming, extensions := connection.extensions } connectionContext
+ let task ← newResponse.asTask
+ BaseIO.chainTask task fun x => discard <| response.send x
+ pendingHead := none
+
+ if requiresData ∨ waitingResponse ∨ respStream.isSome ∨ machine.canPullBody then
+ let answer := if waitingResponse then some response else none
+
+ let requestBodyOpen ←
+ if machine.canPullBody then
+ pure !(← Body.Writer.isClosed requestOutgoing)
+ else
+ pure false
+
+ let requestBodyInterested ←
+ if machine.canPullBody ∧ requestBodyOpen then
+ Body.Writer.hasInterest requestOutgoing
+ else
+ pure false
+
+ let requestBody ←
+ if machine.canPullBodyNow ∧ requestBodyOpen then
+ pure (some requestOutgoing)
+ else
+ pure none
+
+ let shouldPollSocket :=
+ requiresData ∨
+ !waitingResponse ∨
+ respStream.isSome ∨
+ machine.writer.sentMessage ∨
+ (machine.canPullBody ∧ requestBodyInterested)
+
+ let socket := if shouldPollSocket then some socket else none
+
+ requiresData := false
+
+ let event ← processNeedMoreData
+ config handler socket expectData answer respStream requestBody currentTimeout keepAliveTimeout headerTimeout connectionContext
+
+ match event with
+ | .bytes (some bs) =>
+ if keepAliveTimeout.isSome then
+ keepAliveTimeout := none
+ headerTimeout := some <| (← Timestamp.now) + config.headerTimeout
+
+ machine := machine.feed bs
+
+ | .bytes none =>
+ machine := machine.noMoreInput
+
+ | .responseBody (some chunk) =>
+ machine := machine.sendData #[chunk]
+
+ | .responseBody none =>
+ machine := machine.userClosedBody
+
+ if let some res := respStream then
+ if ¬(← Body.Reader.isClosed res) then Body.Reader.close res
+
+ respStream := none
+
+ | .bodyInterest interested =>
+ if interested then
+ let (newMachine, pulledChunk) := machine.pullBody
+ machine := newMachine
+
+ if let some pulled := pulledChunk then
+ try
+ Body.Writer.send requestOutgoing pulled.chunk pulled.incomplete
+ catch e =>
+ Handler.onFailure handler e
+
+ if pulled.final then
+ if ¬(← Body.Writer.isClosed requestOutgoing) then
+ Body.Writer.close requestOutgoing
+ else
+ pure ()
+
+ | .close =>
+ break
+
+ | .timeout =>
+ Handler.onFailure handler "request header timeout"
+ machine := machine.closeReader
+ let (newMachine, newWaitingResponse) := handleError machine .requestTimeout waitingResponse
+ machine := newMachine
+ waitingResponse := newWaitingResponse
+
+ | .shutdown =>
+ let (newMachine, newWaitingResponse) := handleError machine .serviceUnavailable waitingResponse
+ machine := newMachine
+ waitingResponse := newWaitingResponse
+
+ | .response (.error err) =>
+ Handler.onFailure handler err
+ let (newMachine, newWaitingResponse) := handleError machine .internalServerError waitingResponse
+ machine := newMachine
+ waitingResponse := newWaitingResponse
+
+ | .response (.ok res) =>
+ if machine.failed then
+ waitingResponse := false
+ if ¬(← Body.Reader.isClosed res.body) then
+ Body.Reader.close res.body
+ else
+ let size ← Body.Writer.getKnownSize res.body
+ if let some knownSize := size then
+ machine := machine.setKnownSize knownSize
+
+ let head ← do
+ if config.generateDate ∧ ¬res.head.headers.contains Header.Name.date then
+ let now ← Std.Time.DateTime.now (tz := .UTC)
+ pure { res.head with headers := res.head.headers.insert Header.Name.date (Header.Value.ofString! now.toRFC822String) }
+ else
+ pure res.head
+ machine := machine.send head
+ waitingResponse := false
+ if machine.writer.omitBody then
+ if ¬(← Body.Reader.isClosed res.body) then
+ Body.Reader.close res.body
+ respStream := none
+ else
+ respStream := some res.body
+
+ if ¬(← Body.Writer.isClosed requestOutgoing) then
+ Body.Writer.close requestOutgoing
+
+ if let some res := respStream then
+ if ¬(← Body.Reader.isClosed res) then
+ Body.Reader.close res
+
+ Transport.close socket
+
+end Connection
+
+/--
+Handles request/response processing for a single connection using an `Async` handler.
+The library-level entry point for running a server is `Server.serve`.
+This function can be used with a `TCP.Socket` or any other type that implements
+`Transport` to build custom server loops.
+
+# Example
+
+```lean
+-- Create a TCP socket server instance
+let server ← Socket.Server.mk
+server.bind addr
+server.listen backlog
+
+-- Enter an infinite loop to handle incoming client connections
+while true do
+ let client ← server.accept
+ background (serveConnection client handler config)
+```
+-/
+def serveConnection
+ {σ : Type} [Transport t] [Handler σ]
+ (client : t) (handler : σ)
+ (config : Config) (extensions : Extensions := .empty) : ContextAsync Unit := do
+ (Connection.mk client { config := config.toH1Config } extensions)
+ |>.handle config (← ContextAsync.getContext) handler
+
+end Std.Http.Server
diff --git a/src/Std/Internal/Http/Server/Handler.lean b/src/Std/Internal/Http/Server/Handler.lean
new file mode 100644
index 000000000000..04d987ceadb1
--- /dev/null
+++ b/src/Std/Internal/Http/Server/Handler.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Async
+public import Std.Internal.Http.Data
+public import Std.Internal.Async.ContextAsync
+
+public section
+
+namespace Std.Http.Server
+
+open Std.Internal.IO.Async
+
+set_option linter.all true
+
+/--
+A type class for handling HTTP server requests. Implement this class to define how the server
+responds to incoming requests, failures, and `Expect: 100-continue` headers.
+-/
+class Handler (σ : Type) where
+ /--
+ Concrete body type produced by `onRequest`.
+ Defaults to `Body.AnyBody`, but handlers may override it with any reader/writer-compatible body.
+ -/
+ ResponseBody : Type := Body.AnyBody
+
+ /--
+ Reader instance required by the connection loop for sending response chunks.
+ -/
+ [responseBodyReader : Body.Reader ResponseBody]
+
+ /--
+ Writer instance used for known-size metadata and protocol integration.
+ -/
+ [responseBodyWriter : Body.Writer ResponseBody]
+
+ /--
+ Called for each incoming HTTP request.
+ -/
+ onRequest (self : σ) (request : Request Body.Incoming) : ContextAsync (Response ResponseBody)
+
+ /--
+ Called when an I/O or transport error occurs while processing a request (e.g. broken socket,
+ handler exception). This is a **notification only**: the connection will close regardless of
+ the handler's response. Use this for logging and metrics. The default implementation does nothing.
+ -/
+ onFailure (self : σ) (error : IO.Error) : Async Unit :=
+ pure ()
+
+ /--
+ Called when a request includes an `Expect: 100-continue` header. Return `true` to send a
+ `100 Continue` response and accept the body. If `false` is returned the server sends
+ `417 Expectation Failed`, disables keep-alive, and closes the request body reader.
+ This function is guarded by `Config.lingeringTimeout` and may be cancelled on server shutdown.
+ The default implementation always returns `true`.
+ -/
+ onContinue (self : σ) (request : Request.Head) : Async Bool :=
+ pure true
+
+end Std.Http.Server
diff --git a/src/Std/Internal/Http/Transport.lean b/src/Std/Internal/Http/Transport.lean
new file mode 100644
index 000000000000..2810e4ba8e90
--- /dev/null
+++ b/src/Std/Internal/Http/Transport.lean
@@ -0,0 +1,249 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Internal.Http.Protocol.H1
+
+public section
+
+/-!
+# Transport
+
+This module exposes a `Transport` type class that is used to represent different transport mechanisms
+that can be used with an HTTP connection.
+-/
+
+namespace Std.Http
+open Std Internal IO Async TCP
+
+set_option linter.all true
+
+/--
+Generic HTTP interface that abstracts over different transport mechanisms.
+-/
+class Transport (α : Type) where
+ /--
+ Receive data from the client connection, up to the expected size.
+ Returns None if the connection is closed or no data is available.
+ -/
+ recv : α → UInt64 → Async (Option ByteArray)
+
+ /--
+ Send all data through the client connection.
+ -/
+ sendAll : α → Array ByteArray → Async Unit
+
+ /--
+ Get a selector for receiving data asynchronously.
+ -/
+ recvSelector : α → UInt64 → Selector (Option ByteArray)
+
+ /--
+ Close the transport connection.
+ The default implementation is a no-op; override this for transports that require explicit teardown.
+ For `Socket.Client`, the runtime closes the file descriptor when the object is finalized.
+ -/
+ close : α → IO Unit := fun _ => pure ()
+
+instance : Transport Socket.Client where
+ recv client expect := client.recv? expect
+ sendAll client data := client.sendAll data
+ recvSelector client expect := client.recvSelector expect
+
+open Internal.IO.Async in
+
+/--
+Shared state for a bidirectional mock connection.
+-/
+private structure MockLink.SharedState where
+ /--
+ Client to server direction.
+ -/
+ clientToServer : Std.CloseableChannel ByteArray
+
+ /--
+ Server to client direction.
+ -/
+ serverToClient : Std.CloseableChannel ByteArray
+
+/--
+Mock client endpoint for testing.
+-/
+structure Mock.Client where
+ private shared : MockLink.SharedState
+
+/--
+Mock server endpoint for testing.
+-/
+structure Mock.Server where
+ private shared : MockLink.SharedState
+
+namespace Mock
+
+/--
+Creates a mock server and client that are connected to each other and share the
+same underlying state, enabling bidirectional communication.
+-/
+def new : BaseIO (Mock.Client × Mock.Server) := do
+ let first ← Std.CloseableChannel.new
+ let second ← Std.CloseableChannel.new
+
+ return (⟨⟨first, second⟩⟩, ⟨⟨first, second⟩⟩)
+
+/--
+Receives data from a channel, joining all available data up to the expected size. First does a
+blocking recv, then greedily consumes available data with tryRecv until `expect` bytes are reached.
+-/
+def recvJoined (recvChan : Std.CloseableChannel ByteArray) (expect : Option UInt64) : Async (Option ByteArray) := do
+ match ← await (← recvChan.recv) with
+ | none => return none
+ | some first =>
+ let mut result := first
+ repeat
+ if let some expect := expect then
+ if result.size.toUInt64 ≥ expect then break
+
+ match ← recvChan.tryRecv with
+ | none => break
+ | some chunk => result := result ++ chunk
+ return some result
+
+/--
+Sends a single ByteArray through a channel.
+-/
+def send (sendChan : Std.CloseableChannel ByteArray) (data : ByteArray) : Async Unit := do
+ Async.ofAsyncTask ((← sendChan.send data) |>.map (Except.mapError (IO.userError ∘ toString)))
+
+/--
+Sends ByteArrays through a channel.
+-/
+def sendAll (sendChan : Std.CloseableChannel ByteArray) (data : Array ByteArray) : Async Unit := do
+ for chunk in data do
+ send sendChan chunk
+
+/--
+Creates a selector for receiving from a channel.
+-/
+def recvSelector (recvChan : Std.CloseableChannel ByteArray) : Selector (Option ByteArray) :=
+ recvChan.recvSelector
+
+end Mock
+
+namespace Mock.Client
+
+/--
+Gets the receive channel for a client (server to client direction).
+-/
+def getRecvChan (client : Mock.Client) : Std.CloseableChannel ByteArray :=
+ client.shared.serverToClient
+
+/--
+Gets the send channel for a client (client to server direction).
+-/
+def getSendChan (client : Mock.Client) : Std.CloseableChannel ByteArray :=
+ client.shared.clientToServer
+
+/--
+Sends a single ByteArray.
+-/
+def send (client : Mock.Client) (data : ByteArray) : Async Unit :=
+ Mock.send (getSendChan client) data
+
+/--
+Receives data, joining all available chunks.
+-/
+def recv? (client : Mock.Client) (expect : Option UInt64 := none) : Async (Option ByteArray) :=
+ Mock.recvJoined (getRecvChan client) expect
+
+/--
+Tries to receive data without blocking, joining all immediately available chunks.
+Returns `none` if no data is available.
+-/
+def tryRecv? (client : Mock.Client) (_expect : UInt64 := 0) : BaseIO (Option ByteArray) := do
+ match ← (getRecvChan client).tryRecv with
+ | none => return none
+ | some first =>
+ let mut result := first
+ repeat
+ match ← (getRecvChan client).tryRecv with
+ | none => break
+ | some chunk => result := result ++ chunk
+ return some result
+
+/--
+Closes the mock server and client.
+-/
+def close (client : Mock.Client) : IO Unit := do
+ if !(← client.shared.clientToServer.isClosed) then client.shared.clientToServer.close
+ if !(← client.shared.serverToClient.isClosed) then client.shared.serverToClient.close
+
+end Mock.Client
+
+namespace Mock.Server
+
+/--
+Gets the receive channel for a server (client to server direction).
+-/
+def getRecvChan (server : Mock.Server) : Std.CloseableChannel ByteArray :=
+ server.shared.clientToServer
+
+/--
+Gets the send channel for a server (server to client direction).
+-/
+def getSendChan (server : Mock.Server) : Std.CloseableChannel ByteArray :=
+ server.shared.serverToClient
+
+/--
+Sends a single ByteArray.
+-/
+def send (server : Mock.Server) (data : ByteArray) : Async Unit :=
+ Mock.send (getSendChan server) data
+
+/--
+Receives data, joining all available chunks.
+-/
+def recv? (server : Mock.Server) (expect : Option UInt64 := none) : Async (Option ByteArray) :=
+ Mock.recvJoined (getRecvChan server) expect
+
+/--
+Tries to receive data without blocking, joining all immediately available chunks. Returns `none` if no
+data is available.
+-/
+def tryRecv? (server : Mock.Server) (_expect : UInt64 := 0) : BaseIO (Option ByteArray) := do
+ match ← (getRecvChan server).tryRecv with
+ | none => return none
+ | some first =>
+ let mut result := first
+ repeat
+ match ← (getRecvChan server).tryRecv with
+ | none => break
+ | some chunk => result := result ++ chunk
+ return some result
+
+/--
+Closes the mock server and client.
+-/
+def close (server : Mock.Server) : IO Unit := do
+ if !(← server.shared.clientToServer.isClosed) then server.shared.clientToServer.close
+ if !(← server.shared.serverToClient.isClosed) then server.shared.serverToClient.close
+
+
+end Mock.Server
+
+instance : Transport Mock.Client where
+ recv client expect := Mock.recvJoined (Mock.Client.getRecvChan client) (some expect)
+ sendAll client data := Mock.sendAll (Mock.Client.getSendChan client) data
+ recvSelector client _ := Mock.recvSelector (Mock.Client.getRecvChan client)
+ close client := client.close
+
+instance : Transport Mock.Server where
+ recv server expect := Mock.recvJoined (Mock.Server.getRecvChan server) (some expect)
+ sendAll server data := Mock.sendAll (Mock.Server.getSendChan server) data
+ recvSelector server _ := Mock.recvSelector (Mock.Server.getRecvChan server)
+ close server := server.close
+
+end Std.Http
diff --git a/src/Std/Sync.lean b/src/Std/Sync.lean
index c79ce06a5c8e..ca568c15118c 100644
--- a/src/Std/Sync.lean
+++ b/src/Std/Sync.lean
@@ -11,6 +11,7 @@ public import Std.Sync.Channel
public import Std.Sync.Mutex
public import Std.Sync.RecursiveMutex
public import Std.Sync.Barrier
+public import Std.Sync.Semaphore
public import Std.Sync.SharedMutex
public import Std.Sync.Notify
public import Std.Sync.Broadcast
diff --git a/src/Std/Sync/Semaphore.lean b/src/Std/Sync/Semaphore.lean
new file mode 100644
index 000000000000..c9c197e22116
--- /dev/null
+++ b/src/Std/Sync/Semaphore.lean
@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean FRO Contributors
+-/
+module
+
+prelude
+public import Init.Data.Queue
+public import Init.System.Promise
+public import Std.Sync.Mutex
+
+public section
+
+namespace Std
+
+private structure SemaphoreState where
+ permits : Nat
+ waiters : Std.Queue (IO.Promise Unit) := ∅
+deriving Nonempty
+
+/--
+Counting semaphore.
+
+`Semaphore.acquire` returns a promise that is resolved once a permit is available.
+If a permit is currently available, the returned promise is already resolved.
+`Semaphore.release` either resolves one waiting promise or increments the available permits.
+-/
+structure Semaphore where private mk ::
+ private lock : Mutex SemaphoreState
+
+/--
+Creates a resolved promise.
+-/
+private def mkResolvedPromise [Nonempty α] (a : α) : BaseIO (IO.Promise α) := do
+ let promise ← IO.Promise.new
+ promise.resolve a
+ return promise
+
+/--
+Creates a new semaphore with `permits` initially available permits.
+-/
+def Semaphore.new (permits : Nat) : BaseIO Semaphore := do
+ return { lock := ← Mutex.new { permits } }
+
+/--
+Requests one permit.
+Returns a promise that resolves once the permit is acquired.
+-/
+def Semaphore.acquire (sem : Semaphore) : BaseIO (IO.Promise Unit) := do
+ sem.lock.atomically do
+ let st ← get
+ if st.permits > 0 then
+ set { st with permits := st.permits - 1 }
+ mkResolvedPromise ()
+ else
+ let promise ← IO.Promise.new
+ set { st with waiters := st.waiters.enqueue promise }
+ return promise
+
+/--
+Tries to acquire a permit without blocking. Returns `true` on success.
+-/
+def Semaphore.tryAcquire (sem : Semaphore) : BaseIO Bool := do
+ sem.lock.atomically do
+ let st ← get
+ if st.permits > 0 then
+ set { st with permits := st.permits - 1 }
+ return true
+ else
+ return false
+
+/--
+Releases one permit and resolves one waiting acquirer, if any.
+-/
+def Semaphore.release (sem : Semaphore) : BaseIO Unit := do
+ let waiter? ← sem.lock.atomically do
+ let st ← get
+ match st.waiters.dequeue? with
+ | some (waiter, waiters) =>
+ set { st with waiters }
+ return some waiter
+ | none =>
+ set { st with permits := st.permits + 1 }
+ return none
+ if let some waiter := waiter? then
+ waiter.resolve ()
+
+/--
+Returns the number of currently available permits.
+-/
+def Semaphore.availablePermits (sem : Semaphore) : BaseIO Nat :=
+ sem.lock.atomically do
+ return (← get).permits
+
+end Std
diff --git a/tests/lean/run/async_http_body.lean b/tests/lean/run/async_http_body.lean
index cc58f2045dcd..7225c9f2aea6 100644
--- a/tests/lean/run/async_http_body.lean
+++ b/tests/lean/run/async_http_body.lean
@@ -73,6 +73,32 @@ def channelRecvAfterClose : Async Unit := do
#eval channelRecvAfterClose.block
+-- Test Body.stream runs producer concurrently and transfers chunks
+
+def bodyStreamSends : Async Unit := do
+ let incoming ← Body.stream fun outgoing => do
+ outgoing.send (Chunk.ofByteArray "x".toUTF8)
+
+ let first ← incoming.recv
+ assert! first.isSome
+ assert! first.get!.data == "x".toUTF8
+
+ let done ← incoming.recv
+ assert! done.isNone
+
+#eval bodyStreamSends.block
+
+-- Test Body.stream closes channel when generator throws
+
+def bodyStreamThrowCloses : Async Unit := do
+ let incoming ← Body.stream fun _ => do
+ throw (.userError "boom")
+
+ let result ← incoming.recv
+ assert! result.isNone
+
+#eval bodyStreamThrowCloses.block
+
-- Test for-in iteration collects chunks until close
def channelForIn : Async Unit := do
@@ -108,6 +134,34 @@ def channelExtensions : Async Unit := do
#eval channelExtensions.block
+-- Test incomplete sends are collapsed before delivery
+
+def channelCollapseIncompleteChunks : Async Unit := do
+ let (outgoing, incoming) ← Body.mkChannel
+
+ let first : Chunk := { data := "aaaaaaaaaa".toUTF8, extensions := #[(.mk "part", some <| .ofString! "first")] }
+ let second : Chunk := { data := "bbbbbbbbbb".toUTF8, extensions := #[(.mk "part", some <| .ofString! "second")] }
+ let last : Chunk := { data := "cccccccccccccccccccc".toUTF8, extensions := #[(.mk "part", some <| .ofString! "last")] }
+
+ outgoing.send first (incomplete := true)
+ outgoing.send second (incomplete := true)
+
+ let noChunkYet ← incoming.tryRecv
+ assert! noChunkYet.isNone
+
+ let sendFinal ← async (t := AsyncTask) <| outgoing.send last
+ let result ← incoming.recv
+
+ assert! result.isSome
+ let merged := result.get!
+ assert! merged.data == "aaaaaaaaaabbbbbbbbbbcccccccccccccccccccc".toUTF8
+ assert! merged.data.size == 40
+ assert! merged.extensions == #[(.mk "part", some <| .ofString! "first")]
+
+ await sendFinal
+
+#eval channelCollapseIncompleteChunks.block
+
-- Test known size metadata
def channelKnownSize : Async Unit := do
diff --git a/tests/lean/run/async_http_body_edge.lean b/tests/lean/run/async_http_body_edge.lean
new file mode 100644
index 000000000000..3a78d63f0e3e
--- /dev/null
+++ b/tests/lean/run/async_http_body_edge.lean
@@ -0,0 +1,335 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+
+def sendRaw
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 1000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+
+def sendRawAndClose
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 1000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ client.getSendChan.close
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+
+def responseText (response : ByteArray) : String :=
+ String.fromUTF8! response
+
+
+def assertStatusPrefix (name : String) (response : ByteArray) (prefix_ : String) : IO Unit := do
+ let text := responseText response
+ unless text.startsWith prefix_ do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected status prefix {prefix_.quote}\nGot:\n{text.quote}"
+
+
+def assertContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := responseText response
+ unless text.contains needle do
+ throw <| IO.userError s!"Test '{name}' failed:\nMissing {needle.quote}\nGot:\n{text.quote}"
+
+
+def assertNotContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := responseText response
+ if text.contains needle then
+ throw <| IO.userError s!"Test '{name}' failed:\nUnexpected {needle.quote}\nGot:\n{text.quote}"
+
+
+def assertExact (name : String) (response : ByteArray) (expected : String) : IO Unit := do
+ let text := responseText response
+ if text != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected:\n{expected.quote}\nGot:\n{text.quote}"
+
+
+def countOccurrences (s : String) (needle : String) : Nat :=
+ if needle.isEmpty then
+ 0
+ else
+ (s.splitOn needle).length - 1
+
+
+def assertStatusCount (name : String) (response : ByteArray) (expected : Nat) : IO Unit := do
+ let text := responseText response
+ let got := countOccurrences text "HTTP/1.1 "
+ if got != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {expected} responses but saw {got}\n{text.quote}"
+
+
+def bad400 : String :=
+ "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def notImplemented : String :=
+ "HTTP/1.1 501 Not Implemented\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def echoBodyHandler : TestHandler := fun req => do
+ let body : String ← req.body.readAll
+ Response.ok |>.text body
+
+
+-- Content-Length body is read exactly.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /echo HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertStatusPrefix "CL body accepted" response "HTTP/1.1 200"
+ assertContains "CL body echoed" response "hello"
+
+-- Chunked body baseline.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertStatusPrefix "Chunked baseline" response "HTTP/1.1 200"
+ assertContains "Chunked baseline body" response "hello"
+
+-- Uppercase and leading-zero chunk-size are accepted.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n000A\x0d\n0123456789\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertStatusPrefix "Chunk-size uppercase+leading-zero" response "HTTP/1.1 200"
+ assertContains "Chunk-size uppercase+leading-zero body" response "0123456789"
+
+-- Chunk extensions with token and quoted value are accepted.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;ext=value;quoted=\"ok\"\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertStatusPrefix "Chunk extensions accepted" response "HTTP/1.1 200"
+ assertContains "Chunk extensions body" response "hello"
+
+-- h11-inspired: invalid chunk-size token is rejected.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /bad HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\nG\x0d\nabc\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact "Invalid chunk-size token" response bad400
+
+-- h11-inspired: reject bad bytes where chunk terminator must be CRLF.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /smuggle HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nxxx__1a\x0d\n".toUTF8
+ let response ← sendRawAndClose client server raw echoBodyHandler
+ assertExact "Chunk terminator bytes validated" response bad400
+
+-- Missing terminal 0-chunk is rejected once EOF arrives.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /incomplete HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n".toUTF8
+ let response ← sendRawAndClose client server raw echoBodyHandler
+ assertExact "Missing terminal zero chunk" response bad400
+
+-- TE+CL mixed framing is rejected.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /mix HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact "TE+CL rejected" response bad400
+
+-- Duplicate chunked coding is rejected.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /dup HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact "Duplicate chunked coding" response bad400
+
+-- Duplicate Transfer-Encoding lines with unsupported coding are rejected.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /dup-lines HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nTransfer-Encoding: gzip\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact "Duplicate TE headers with gzip" response bad400
+
+-- Transfer-coding chains that end in chunked are accepted as chunked framing.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /gzip HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: gzip, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertStatusPrefix "gzip, chunked accepted as chunked framing" response "HTTP/1.1 200"
+ assertContains "gzip, chunked body delivered" response "hello"
+
+-- Unsupported transfer codings without chunked framing are rejected.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /identity HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: identity\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact "identity transfer-coding rejected with 400" response bad400
+
+-- Malformed Transfer-Encoding token list is rejected.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /bad-te-list HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: ,chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact "Malformed Transfer-Encoding token list" response bad400
+
+-- Strict chunk-extension name/value limits.
+#eval show IO _ from do
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxChunkExtNameLength := 4
+ maxChunkExtValueLength := 4
+ }
+
+ let (clientA, serverA) ← Mock.new
+ let okName := "POST /ok-name HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;name=1\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA okName echoBodyHandler (config := config)
+ assertStatusPrefix "Chunk ext name at limit" responseA "HTTP/1.1 200"
+
+ let (clientB, serverB) ← Mock.new
+ let badName := "POST /bad-name HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;toolong=1\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB badName echoBodyHandler (config := config)
+ assertExact "Chunk ext name too long" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let okValue := "POST /ok-value HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;name=abcd\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC okValue echoBodyHandler (config := config)
+ assertStatusPrefix "Chunk ext value at limit" responseC "HTTP/1.1 200"
+
+ let (clientD, serverD) ← Mock.new
+ let badQuoted := "POST /bad-value HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;name=\"abcde\"\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD badQuoted echoBodyHandler (config := config)
+ assertExact "Quoted chunk ext value too long" responseD bad400
+
+ let (clientE, serverE) ← Mock.new
+ let badToken := "POST /bad-token HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;na@e=1\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseE ← sendRaw clientE serverE badToken echoBodyHandler (config := config)
+ assertExact "Invalid chunk ext token char" responseE bad400
+
+ let (clientF, serverF) ← Mock.new
+ let mixed := "POST /mixed-ext HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;a=1;b=2;toolong=3\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseF ← sendRaw clientF serverF mixed echoBodyHandler (config := config)
+ assertExact "Mixed valid/invalid chunk extensions" responseF bad400
+
+-- maxChunkExtensions boundary is enforced.
+#eval show IO _ from do
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxChunkExtensions := 2
+ }
+
+ let (clientA, serverA) ← Mock.new
+ let okRaw := "POST /ext-count HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;a=1;b=2\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let okResponse ← sendRaw clientA serverA okRaw echoBodyHandler (config := config)
+ assertStatusPrefix "maxChunkExtensions at limit" okResponse "HTTP/1.1 200"
+
+ let (clientB, serverB) ← Mock.new
+ let badRaw := "POST /ext-count-overflow HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;a=1;b=2;c=3\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let badResponse ← sendRaw clientB serverB badRaw echoBodyHandler (config := config)
+ assertExact "maxChunkExtensions overflow" badResponse bad400
+
+-- Content-Length with leading zeros is accepted.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /leading-zeros HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 005\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertStatusPrefix "Content-Length leading zeros" response "HTTP/1.1 200"
+ assertContains "Content-Length leading zeros body" response "hello"
+
+-- Very large Content-Length is rejected with 413.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /too-large HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 99999999999999999999\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertStatusPrefix "Huge Content-Length" response "HTTP/1.1 413"
+
+-- Duplicate Content-Length (same and different values) are rejected.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let same := "POST /dup-cl-same HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let responseA ← sendRaw clientA serverA same echoBodyHandler
+ assertExact "Duplicate Content-Length same" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let diff := "POST /dup-cl-diff HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 3\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nabc".toUTF8
+ let responseB ← sendRaw clientB serverB diff echoBodyHandler
+ assertExact "Duplicate Content-Length different" responseB bad400
+
+-- Chunk-size line trailing whitespace is rejected.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /bad-space HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5 \x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact "Chunk-size trailing space" response bad400
+
+-- Transfer-Encoding trailing OWS is currently accepted.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST /te-ows HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked \x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertStatusPrefix "Transfer-Encoding trailing OWS" response "HTTP/1.1 200"
+ assertContains "Transfer-Encoding trailing OWS body" response "hello"
+
+-- h11-inspired: early invalid-byte detection before CRLF.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let responseA ← sendRawAndClose clientA serverA (ByteArray.mk #[0x00]) echoBodyHandler
+ assertExact "Early invalid NUL" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let responseB ← sendRawAndClose clientB serverB (ByteArray.mk #[0x20]) echoBodyHandler
+ assertExact "Early invalid SP" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let responseC ← sendRawAndClose clientC serverC (ByteArray.mk #[0x16, 0x03, 0x01, 0x00, 0xa5]) echoBodyHandler
+ assertExact "Early invalid TLS prefix" responseC bad400
+
+-- h11-inspired: reject garbage after request-line version token.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "GET / HTTP/1.1 xxxxxx\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact "Garbage after request-line" response bad400
+
+-- Extra bytes beyond Content-Length become the next pipelined request.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw :=
+ ("POST / HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\n\x0d\nhello" ++
+ "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n").toUTF8
+
+ let response ← sendRaw client server raw (fun req => do
+ let mut body := ByteArray.empty
+ for chunk in req.body do
+ body := body ++ chunk.data
+ Response.ok |>.text s!"{toString req.head.uri}:{String.fromUTF8! body}")
+
+ assertStatusCount "Pipelined parse after exact CL" response 2
+ assertContains "Pipelined first response" response "/:hello"
+ assertContains "Pipelined second response" response "/second:"
+ assertNotContains "No parse confusion" response "/second:hello"
diff --git a/tests/lean/run/async_http_chunk_ext_limits.lean b/tests/lean/run/async_http_chunk_ext_limits.lean
new file mode 100644
index 000000000000..d5934ae05a62
--- /dev/null
+++ b/tests/lean/run/async_http_chunk_ext_limits.lean
@@ -0,0 +1,199 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+
+def sendRaw
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 1000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+
+def assertStatus (name : String) (response : ByteArray) (status : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.startsWith status do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {status}\nGot:\n{text.quote}"
+
+
+def assertExact (name : String) (response : ByteArray) (expected : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ if text != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected:\n{expected.quote}\nGot:\n{text.quote}"
+
+
+def echoHandler : TestHandler :=
+ fun req => do
+ let body : String ← req.body.readAll
+ Response.ok |>.text body
+
+def bad400 : String :=
+ "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+
+-- Chunk extension name length limits.
+-- Default maxChunkExtNameLength = 256.
+#eval show IO _ from do
+ let name256 := String.ofList (List.replicate 256 'a')
+ let name257 := String.ofList (List.replicate 257 'a')
+
+ -- Name at exactly the limit → accepted.
+ let (clientA, serverA) ← Mock.new
+ let rawA := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;{name256}\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA echoHandler
+ assertStatus "Ext name at 256 → accepted" responseA "HTTP/1.1 200"
+
+ -- Name one byte over the limit → rejected.
+ let (clientB, serverB) ← Mock.new
+ let rawB := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;{name257}\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB echoHandler
+ assertExact "Ext name at 257 → rejected" responseB bad400
+
+
+-- Chunk extension value length limits (unquoted token value).
+-- Default maxChunkExtValueLength = 256.
+#eval show IO _ from do
+ let val256 := String.ofList (List.replicate 256 'v')
+ let val257 := String.ofList (List.replicate 257 'v')
+
+ -- Token value at exactly the limit → accepted.
+ let (clientA, serverA) ← Mock.new
+ let rawA := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;ext={val256}\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA echoHandler
+ assertStatus "Ext token value at 256 → accepted" responseA "HTTP/1.1 200"
+
+ -- Token value one byte over the limit → rejected.
+ let (clientB, serverB) ← Mock.new
+ let rawB := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;ext={val257}\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB echoHandler
+ assertExact "Ext token value at 257 → rejected" responseB bad400
+
+
+-- Chunk extension value length limits (quoted string value).
+-- The limit applies to the unquoted content length.
+#eval show IO _ from do
+ let val256 := String.ofList (List.replicate 256 'v')
+ let val257 := String.ofList (List.replicate 257 'v')
+
+ -- Quoted value at exactly the limit → accepted.
+ let (clientA, serverA) ← Mock.new
+ let rawA := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;ext=\"{val256}\"\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA echoHandler
+ assertStatus "Ext quoted value at 256 → accepted" responseA "HTTP/1.1 200"
+
+ -- Quoted value one byte over the limit → rejected.
+ let (clientB, serverB) ← Mock.new
+ let rawB := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;ext=\"{val257}\"\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB echoHandler
+ assertExact "Ext quoted value at 257 → rejected" responseB bad400
+
+
+-- Chunk extension count limits.
+-- Default maxChunkExtensions = 16.
+#eval show IO _ from do
+ -- Build extension lists: ";ext0;ext1;...;extN"
+ let exts16 := (List.range 16).foldl (fun acc i => acc ++ s!";e{i}") ""
+ let exts17 := (List.range 17).foldl (fun acc i => acc ++ s!";e{i}") ""
+
+ -- Exactly 16 extensions → accepted.
+ let (clientA, serverA) ← Mock.new
+ let rawA := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5{exts16}\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA echoHandler
+ assertStatus "16 extensions → accepted" responseA "HTTP/1.1 200"
+
+ -- 17 extensions → rejected.
+ let (clientB, serverB) ← Mock.new
+ let rawB := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5{exts17}\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB echoHandler
+ assertExact "17 extensions → rejected" responseB bad400
+
+
+-- maxChunkExtensions config override.
+#eval show IO _ from do
+ let cfg1 : Config := { lingeringTimeout := 1000, maxChunkExtensions := 1, generateDate := false }
+
+ -- 1 extension with limit=1 → accepted.
+ let (clientA, serverA) ← Mock.new
+ let rawA := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;ext1\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA echoHandler (config := cfg1)
+ assertStatus "1 ext with limit=1 → accepted" responseA "HTTP/1.1 200"
+
+ -- 2 extensions with limit=1 → rejected.
+ let (clientB, serverB) ← Mock.new
+ let rawB := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;ext1;ext2\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB echoHandler (config := cfg1)
+ assertExact "2 exts with limit=1 → rejected" responseB bad400
+
+ -- 0 extensions with limit=1 → accepted (no extensions is always fine).
+ let (clientC, serverC) ← Mock.new
+ let rawC := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC rawC echoHandler (config := cfg1)
+ assertStatus "0 exts with limit=1 → accepted" responseC "HTTP/1.1 200"
+
+
+-- Extension with no value (name-only extension token).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;novalue\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "Ext with no value → accepted" response "HTTP/1.1 200"
+ -- Body is still correctly delivered.
+ let text := String.fromUTF8! response
+ unless text.contains "hello" do
+ throw <| IO.userError "Body not delivered with name-only extension"
+
+
+-- Extensions on the terminal (last) chunk are accepted.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0;final-ext=done\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "Extension on last chunk → accepted" response "HTTP/1.1 200"
+
+
+-- Extension with name and quoted-string value.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;ext=\"hello world\"\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "Ext with quoted-string value → accepted" response "HTTP/1.1 200"
+
+
+-- Extension with non-token character in name → rejected.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ -- '@' is not a valid token character
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;bad@name\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertExact "Ext with non-token name char → rejected" response bad400
+
+
+-- Multiple extensions with name=value pairs.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5;a=1;b=2;c=3\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "Multiple name=value extensions → accepted" response "HTTP/1.1 200"
diff --git a/tests/lean/run/async_http_connection.lean b/tests/lean/run/async_http_connection.lean
new file mode 100644
index 000000000000..3b48feb01bd2
--- /dev/null
+++ b/tests/lean/run/async_http_connection.lean
@@ -0,0 +1,630 @@
+import Std.Internal.Http
+import Std.Internal.Async
+import Std.Internal.Async.Timer
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+
+structure TestCase where
+ /-- Descriptive name for the test -/
+ name : String
+ /-- The HTTP request to send -/
+ request : Request (Array Chunk)
+ /-- Handler function to process the request -/
+ handler : Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+ /-- Expected response string -/
+ expected : String
+ /-- Whether to use chunked encoding -/
+ chunked : Bool := false
+ deriving Inhabited
+
+def toByteArray (req : Request (Array Chunk)) (chunked := false) : IO ByteArray := Async.block do
+ let mut data := Internal.Encode.encode (v := .v11) .empty req.head
+ let toByteArray (chunkData : Internal.ChunkedBuffer) (part : Chunk) := Internal.Encode.encode .v11 chunkData part
+
+ for part in req.body do data := toByteArray data part
+
+ if chunked then data := toByteArray data (Chunk.mk .empty .empty)
+
+ return data.toByteArray
+
+/-- Send multiple requests through a mock connection and return the response data. -/
+def sendRequests (client : Mock.Client) (server : Mock.Server) (reqs : Array (Request (Array Chunk)))
+ (onRequest : Request Body.Incoming → ContextAsync (Response Body.AnyBody))
+ (chunked : Bool := false) : IO ByteArray := Async.block do
+ let mut data := .empty
+ for req in reqs do data := data ++ (← toByteArray req chunked)
+
+ client.send data
+ Std.Http.Server.serveConnection server onRequest { lingeringTimeout := 3000, generateDate := false }
+ |>.run
+
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+/-- Run a single test case, comparing actual response against expected response. -/
+def runTest (name : String) (client : Mock.Client) (server : Mock.Server) (req : Request (Array Chunk))
+ (handler : Request Body.Incoming → ContextAsync (Response Body.AnyBody)) (expected : String) (chunked : Bool := false) :
+ IO Unit := do
+ let response ← sendRequests client server #[req] handler chunked
+ let responseData := String.fromUTF8! response
+
+ if responseData != expected then
+ throw <| IO.userError s!
+ "Test '{name}' failed:\n\
+ Expected:\n{expected.quote}\n\
+ Got:\n{responseData.quote}"
+
+def runTestCase (tc : TestCase) : IO Unit := do
+ let (client, server) ← Mock.new
+ Async.block <| runTest tc.name client server tc.request tc.handler tc.expected tc.chunked
+
+-- Request Predicates
+
+/-- Check if request is a basic GET requests to the specified URI and host. -/
+def isBasicGetRequest (req : Request Body.Incoming) (uri : String) (host : String) : Bool :=
+ req.head.method == .get ∧
+ req.head.version == .v11 ∧
+ toString req.head.uri = uri ∧
+ req.head.headers.hasEntry (.mk "host") (.ofString! host)
+
+/-- Check if request has a specific Content-Length header. -/
+def hasContentLength (req : Request Body.Incoming) (length : String) : Bool :=
+ req.head.headers.hasEntry (.mk "content-length") (.ofString! length)
+
+/-- Check if request uses chunked transfer encoding. -/
+def isChunkedRequest (req : Request Body.Incoming) : Bool :=
+ if let some te := req.head.headers.get? (.mk "transfer-encoding") then
+ match Header.TransferEncoding.parse te with
+ | some te => te.isChunked
+ | none => false
+ else
+ false
+
+/-- Check if request has a specific header with a specific value. -/
+def hasHeader (req : Request Body.Incoming) (name : String) (value : String) : Bool :=
+ if let some name := Header.Name.ofString? name then
+ req.head.headers.hasEntry name (.ofString! value)
+ else
+ false
+
+/-- Check if request method matches the expected method. -/
+def hasMethod (req : Request Body.Incoming) (method : Method) : Bool :=
+ req.head.method == method
+
+/-- Check if request URI matches the expected URI string. -/
+def hasUri (req : Request Body.Incoming) (uri : String) : Bool :=
+ toString req.head.uri = uri
+
+-- Tests
+
+#eval runTestCase {
+ name := "GET with Content-Length"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/"
+ |>.header! "Host" "example.com"
+ |>.header! "Connection" "close"
+ |>.header! "Content-Length" "7"
+ |>.body #[.mk "survive".toUTF8 #[]]
+
+ handler := fun req => do
+ if isBasicGetRequest req "/" "example.com" ∧ hasContentLength req "7"
+ then Response.ok |>.text "ok"
+ else Response.badRequest |>.text "closed"
+
+ expected := "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 2\x0d\n\x0d\nok"
+}
+
+#eval runTestCase {
+ name := "Simple GET request"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/api/users"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ if hasMethod req .get ∧ hasUri req "/api/users"
+ then Response.ok |>.text "users list"
+ else Response.notFound |>.text ""
+
+ expected := "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 10\x0d\n\x0d\nusers list"
+}
+
+#eval runTestCase {
+ name := "POST with body"
+ request := Request.new
+ |>.method .post
+ |>.uri! "/api/users"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Content-Type" "application/json"
+ |>.header! "Content-Length" "16"
+ |>.header! "Connection" "close"
+ |>.body #[.mk "{\"name\":\"Alice\"}".toUTF8 #[]]
+
+ handler := fun req => do
+ if hasMethod req .post ∧ hasHeader req "Content-Type" "application/json"
+ then Response.new |>.status .created |>.text "Created"
+ else Response.badRequest |>.text ""
+ expected := "HTTP/1.1 201 Created\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 7\x0d\n\x0d\nCreated"
+}
+
+#eval runTestCase {
+ name := "DELETE request"
+
+ request := Request.new
+ |>.method .delete
+ |>.uri! "/api/users/123"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ if hasMethod req .delete ∧ hasUri req "/api/users/123"
+ then Response.new |>.status .noContent |>.text ""
+ else Response.notFound |>.text ""
+
+ expected := "HTTP/1.1 204 No Content\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "HEAD request"
+
+ request := Request.new
+ |>.method .head
+ |>.uri! "/api/users"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ if hasMethod req .head
+ then Response.ok |>.text ""
+ else Response.notFound |>.text ""
+
+ expected := "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "OPTIONS request"
+
+ request := Request.new
+ |>.method .options
+ |>.uri! "*"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ if hasMethod req .options
+ then Response.new
+ |>.status .ok
+ |>.header! "Allow" "GET, POST, PUT, DELETE, OPTIONS"
+ |>.text ""
+ else Response.badRequest |>.text ""
+
+ expected := "HTTP/1.1 200 OK\x0d\nAllow: GET, POST, PUT, DELETE, OPTIONS\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "Request with multiple headers"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/api/data"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Accept" "application/json"
+ |>.header! "User-Agent" "TestClient/1.0"
+ |>.header! "Authorization" "Bearer token123"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ if hasHeader req "Authorization" "Bearer token123" ∧ hasHeader req "Accept" "application/json"
+ then Response.ok |>.text "authenticated"
+ else Response.new |>.status .unauthorized |>.text "unauthorized"
+
+ expected := "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 13\x0d\n\x0d\nauthenticated"
+}
+
+#eval runTestCase {
+ name := "Request with query parameters"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/api/search?q=test&limit=10"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ if hasUri req "/api/search?q=test&limit=10"
+ then Response.ok |>.text "search results"
+ else Response.notFound |>.text ""
+
+ expected := "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 14\x0d\n\x0d\nsearch results"
+}
+
+#eval runTestCase {
+ name := "POST with empty body"
+
+ request := Request.new
+ |>.method .post
+ |>.uri! "/api/trigger"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Content-Length" "0"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ if hasMethod req .post ∧ hasContentLength req "0"
+ then Response.new |>.status .accepted |>.text "triggered"
+ else Response.badRequest |>.text ""
+
+ expected := "HTTP/1.1 202 Accepted\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 9\x0d\n\x0d\ntriggered"
+}
+
+#eval runTestCase {
+ name := "Large response body"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/api/large"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun _ => do
+ let largeBody := String.ofList (List.replicate 1000 'X')
+ Response.ok |>.text largeBody
+
+ expected := s!"HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 1000\x0d\n\x0d\n{String.ofList (List.replicate 1000 'X')}"
+}
+
+#eval runTestCase {
+ name := "Custom status code"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/api/teapot"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun _ => do
+ Response.new
+ |>.status .imATeapot
+ |>.text "I'm a teapot"
+
+ expected := "HTTP/1.1 418 I'm a teapot\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 12\x0d\n\x0d\nI'm a teapot"
+}
+
+#eval runTestCase {
+ name := "Request with special characters in URI"
+ request := Request.new
+ |>.method .get
+ |>.uri! "/api/users/%C3%A9"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+ handler := fun req => do
+ if hasUri req "/api/users/%C3%A9"
+ then Response.ok |>.text "found"
+ else Response.notFound |>.text ""
+ expected := "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 5\x0d\n\x0d\nfound"
+}
+
+#eval runTestCase {
+ name := "Response with custom headers"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/api/data"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.header! "Cache-Control" "no-cache"
+ |>.body #[]
+
+ handler := fun _ => do
+ Response.new
+ |>.status .ok
+ |>.header! "Cache-Control" "no-cache"
+ |>.header! "X-Custom-Header" "custom-value"
+ |>.text "data"
+
+ expected := "HTTP/1.1 200 OK\x0d\nCache-Control: no-cache\x0d\nX-Custom-Header: custom-value\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 4\x0d\n\x0d\ndata"
+}
+
+#eval runTestCase {
+ name := "Request with Content-Type and body"
+
+ request := Request.new
+ |>.method .post
+ |>.uri! "/api/xml"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Content-Type" "application/xml"
+ |>.header! "Content-Length" "17"
+ |>.header! "Connection" "close"
+ |>.body #[.mk "test".toUTF8 #[]]
+
+ handler := fun req => do
+ if hasHeader req "Content-Type" "application/xml"
+ then Response.ok |>.text "processed xml"
+ else Response.new |>.status .unsupportedMediaType |>.text "unsupported"
+
+ expected := "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 13\x0d\n\x0d\nprocessed xml"
+}
+
+-- Limits
+
+#eval
+ let bigString := String.fromUTF8! (ByteArray.mk (Array.ofFn (n := 257) (fun _ => 65)))
+
+ runTestCase {
+ name := "Huge String request"
+
+ request := Request.new
+ |>.method .head
+ |>.uri! "/api/users"
+ |>.header! "Host" "api.example.com"
+ |>.header! bigString "a"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ if hasMethod req .head
+ then Response.ok
+ |>.header (.ofString! bigString) (.ofString! "ata")
+ |>.text ""
+ else Response.notFound |>.text ""
+ expected := "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "Request line too long"
+
+ request :=
+ Request.new
+ |>.method .get
+ |>.uri (.originForm (.mk #[URI.EncodedString.encode <| String.ofList (List.replicate 2000 'a')] true) none)
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ Response.ok |>.text (toString (toString req.head.uri).length)
+
+ expected := "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "Header long"
+
+ request :=
+ Request.new
+ |>.method .get
+ |>.uri (.originForm (.mk #[URI.EncodedString.encode <| String.ofList (List.replicate 200 'a')] true) none)
+ |>.header! "Host" (String.ofList (List.replicate 8230 'a'))
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun req => do
+ Response.ok |>.text (toString (toString req.head.uri).length)
+
+ expected := "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "Too many headers"
+
+ request := Id.run do
+ let mut req := Request.new
+ |>.method .get
+ |>.uri! "/api/data"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+
+ for i in [0:101] do
+ req := req |>.header! s!"X-Header-{i}" s!"value{i}"
+
+ return req |>.body #[]
+
+ handler := fun _ => do
+ Response.ok |>.text "success"
+
+ expected := "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "Header value too long"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/api/test"
+ |>.header! "Host" "api.example.com"
+ |>.header! "X-Long-Value" (String.ofList (List.replicate 9000 'x'))
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun _ => do
+ Response.ok |>.text "ok"
+
+ expected := "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "Total headers size too large"
+
+ request := Id.run do
+ let mut req := Request.new
+ |>.method .get
+ |>.uri! "/api/data"
+ |>.header! "Host" "api.example.com"
+ |>.header! "Connection" "close"
+
+ for i in [0:200] do
+ req := req |>.header! s!"X-Header-{i}" (String.ofList (List.replicate 200 'a'))
+ return req |>.body #[]
+
+ handler := fun _ => do
+ Response.ok |>.text "success"
+
+ expected := "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+}
+
+-- Tests
+
+#eval runTestCase {
+ name := "Streaming response with fixed Content-Length"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/stream"
+ |>.header! "Host" "example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun _ => do
+ let (stream, _incoming) ← Body.mkChannel
+
+ background do
+ for i in [0:3] do
+ let sleep ← Sleep.mk 5
+ sleep.wait
+ stream.send <| Chunk.ofByteArray s!"chunk{i}\n".toUTF8
+ stream.close
+
+ return Response.ok
+ |>.header (.mk "content-length") (.mk "21")
+ |>.body stream
+
+ expected := "HTTP/1.1 200 OK\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 21\x0d\n\x0d\nchunk0\nchunk1\nchunk2\n"
+}
+
+#eval runTestCase {
+ name := "Streaming response with setKnownSize fixed"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/stream-sized"
+ |>.header! "Host" "example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun _ => do
+ let (stream, _incoming) ← Body.mkChannel
+ stream.setKnownSize (some (.fixed 15))
+
+ background do
+ for i in [0:3] do
+ stream.send <| Chunk.ofByteArray s!"data{i}".toUTF8
+
+ stream.close
+
+ return Response.ok
+ |>.body stream
+
+ expected := "HTTP/1.1 200 OK\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 15\x0d\n\x0d\ndata0data1data2"
+}
+
+#eval runTestCase {
+ name := "Streaming response with chunked encoding"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/stream-chunked"
+ |>.header! "Host" "example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun _ => do
+ let (stream, _incoming) ← Body.mkChannel
+
+ background do
+ stream.send <| Chunk.ofByteArray "hello".toUTF8
+ stream.send <| Chunk.ofByteArray "world".toUTF8
+ stream.close
+ return Response.ok
+ |>.body stream
+
+ expected := "HTTP/1.1 200 OK\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\n5\x0d\nhello\x0d\n5\x0d\nworld\x0d\n0\x0d\n\x0d\n"
+}
+
+#eval runTestCase {
+ name := "Chunked request with streaming response"
+
+ request := Request.new
+ |>.method .post
+ |>.uri! "/"
+ |>.header! "Host" "example.com"
+ |>.header! "Transfer-Encoding" "chunked"
+ |>.header! "Connection" "close"
+ |>.body #[
+ .mk "data1".toUTF8 #[],
+ .mk "data2".toUTF8 #[]
+ ]
+
+ handler := fun req => do
+ let (stream, _incoming) ← Body.mkChannel
+
+ if isChunkedRequest req
+ then
+ background do
+ for i in [0:2] do
+ stream.send <| Chunk.ofByteArray s!"response{i}".toUTF8
+ stream.close
+ return Response.ok
+ |>.header (.mk "content-length") (.mk "18")
+ |>.body stream
+ else
+ stream.send <| Chunk.ofByteArray "not chunked".toUTF8
+ stream.close
+
+ return Response.badRequest
+ |>.body stream
+
+ expected := "HTTP/1.1 200 OK\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 18\x0d\n\x0d\nresponse0response1"
+ chunked := true
+}
+
+#eval runTestCase {
+ name := "Fixed-length response overflow closes connection"
+
+ request := Request.new
+ |>.method .get
+ |>.uri! "/overflow"
+ |>.header! "Host" "example.com"
+ |>.header! "Connection" "close"
+ |>.body #[]
+
+ handler := fun _ => do
+ let (stream, _incoming) ← Body.mkChannel
+ background do
+ stream.send <| Chunk.ofByteArray "abcdef".toUTF8
+ stream.close
+ return Response.ok
+ |>.header (.mk "content-length") (.mk "3")
+ |>.body stream
+
+ expected := "HTTP/1.1 200 OK\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 3\x0d\n\x0d\n"
+}
diff --git a/tests/lean/run/async_http_expect_reject.lean b/tests/lean/run/async_http_expect_reject.lean
new file mode 100644
index 000000000000..f28936709aef
--- /dev/null
+++ b/tests/lean/run/async_http_expect_reject.lean
@@ -0,0 +1,213 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+structure RejectContinueHandler where
+ onRequestCalls : IO.Ref Nat
+
+instance : Std.Http.Server.Handler RejectContinueHandler where
+ onRequest self _request := do
+ self.onRequestCalls.modify (· + 1)
+ Response.ok |>.text "request-ran"
+
+ onContinue _self _head :=
+ pure false
+
+structure AcceptContinueHandler where
+ onRequestCalls : IO.Ref Nat
+
+instance : Std.Http.Server.Handler AcceptContinueHandler where
+ onRequest self request := do
+ self.onRequestCalls.modify (· + 1)
+ let body : String ← request.body.readAll
+ Response.ok |>.text s!"accepted:{body}"
+
+ onContinue _self _head :=
+ pure true
+
+
+def sendRaw {σ : Type} [Std.Http.Server.Handler σ]
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : σ)
+ (config : Config := { lingeringTimeout := 3000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+
+def assertContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.contains needle do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected to contain: {needle.quote}\nGot:\n{text.quote}"
+
+
+def assertNotContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ if text.contains needle then
+ throw <| IO.userError s!"Test '{name}' failed:\nDid not expect: {needle.quote}\nGot:\n{text.quote}"
+
+
+def assertCallCount (name : String) (calls : IO.Ref Nat) (expected : Nat) : IO Unit := do
+ let got ← calls.get
+ if got != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected onRequest calls {expected}, got {got}"
+
+
+def countOccurrences (s : String) (needle : String) : Nat :=
+ if needle.isEmpty then
+ 0
+ else
+ (s.splitOn needle).length - 1
+
+
+def assertOccurrenceCount (name : String) (response : ByteArray) (needle : String) (expected : Nat) : IO Unit := do
+ let text := String.fromUTF8! response
+ let got := countOccurrences text needle
+ if got != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {expected} occurrences of {needle.quote}, got {got}\n{text.quote}"
+
+
+-- Rejecting Expect returns 417 and does not execute user handler.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let calls ← IO.mkRef 0
+ let handler : RejectContinueHandler := { onRequestCalls := calls }
+
+ let raw := "POST /upload HTTP/1.1\x0d\nHost: example.com\x0d\nExpect: 100-continue\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw handler
+
+ assertContains "Expect rejected status" response "HTTP/1.1 417 Expectation Failed"
+ assertNotContains "Expect rejected no 100 Continue" response "100 Continue"
+ assertNotContains "Expect rejected no handler body" response "request-ran"
+ assertOccurrenceCount "Expect rejected single response" response "HTTP/1.1 " 1
+ assertCallCount "Expect rejected call count" calls 0
+
+-- Rejected Expect closes the exchange and blocks pipelined follow-up requests.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let calls ← IO.mkRef 0
+ let handler : RejectContinueHandler := { onRequestCalls := calls }
+
+ let req1 := "POST /first HTTP/1.1\x0d\nHost: example.com\x0d\nExpect: 100-continue\x0d\nContent-Length: 5\x0d\n\x0d\nhello"
+ let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let response ← sendRaw client server (req1 ++ req2).toUTF8 handler
+
+ assertContains "Expect rejected still 417" response "HTTP/1.1 417 Expectation Failed"
+ assertNotContains "Expect rejected no second request" response "/second"
+ assertCallCount "Expect rejected pipelined call count" calls 0
+
+-- Accepted Expect emits 100 Continue followed by final 200.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let calls ← IO.mkRef 0
+ let handler : AcceptContinueHandler := { onRequestCalls := calls }
+
+ let raw := "POST /ok HTTP/1.1\x0d\nHost: example.com\x0d\nExpect: 100-continue\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw handler
+
+ assertContains "Expect accepted has 100" response "HTTP/1.1 100 Continue"
+ assertContains "Expect accepted has final 200" response "HTTP/1.1 200 OK"
+ assertContains "Expect accepted body" response "accepted:hello"
+ assertOccurrenceCount "Expect accepted exactly one 100" response "HTTP/1.1 100 Continue" 1
+ assertOccurrenceCount "Expect accepted exactly one 200" response "HTTP/1.1 200 OK" 1
+ assertCallCount "Expect accepted call count" calls 1
+
+-- Non-100 Expect token proceeds as a normal request.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let calls ← IO.mkRef 0
+ let handler : RejectContinueHandler := { onRequestCalls := calls }
+
+ let raw := "POST /odd HTTP/1.1\x0d\nHost: example.com\x0d\nExpect: something-else\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw handler
+
+ assertContains "Non-100 Expect status" response "HTTP/1.1 200 OK"
+ assertContains "Non-100 Expect handler ran" response "request-ran"
+ assertNotContains "Non-100 Expect no 100 Continue" response "100 Continue"
+ assertCallCount "Non-100 Expect call count" calls 1
+
+-- h11-inspired: Expect token matching is case-insensitive.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let calls ← IO.mkRef 0
+ let handler : AcceptContinueHandler := { onRequestCalls := calls }
+
+ let raw := "POST /case HTTP/1.1\x0d\nHost: example.com\x0d\nExpect: 100-CONTINUE\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw handler
+
+ assertContains "Case-insensitive Expect has 100" response "HTTP/1.1 100 Continue"
+ assertContains "Case-insensitive Expect final 200" response "HTTP/1.1 200 OK"
+ assertCallCount "Case-insensitive Expect call count" calls 1
+
+-- Normal requests without Expect do not emit 100 Continue.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let calls ← IO.mkRef 0
+ let handler : AcceptContinueHandler := { onRequestCalls := calls }
+
+ let raw := "POST /no-expect HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRaw client server raw handler
+
+ assertContains "No Expect status" response "HTTP/1.1 200 OK"
+ assertContains "No Expect body" response "accepted:hello"
+ assertNotContains "No Expect no interim 100" response "100 Continue"
+ assertOccurrenceCount "No Expect exactly one 200" response "HTTP/1.1 200 OK" 1
+ assertCallCount "No Expect call count" calls 1
+
+-- Date header is generated when enabled.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "GET /date HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let handler : TestHandler := fun _ => Response.ok |>.text "hello"
+ let response ← sendRaw client server raw handler (config := { lingeringTimeout := 3000, generateDate := true })
+
+ assertContains "Date generated status" response "HTTP/1.1 200 OK"
+ assertContains "Date generated header" response "Date: "
+
+-- Date header is absent when disabled.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "GET /no-date HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let handler : TestHandler := fun _ => Response.ok |>.text "hello"
+ let response ← sendRaw client server raw handler (config := { lingeringTimeout := 3000, generateDate := false })
+
+ assertContains "Date disabled status" response "HTTP/1.1 200 OK"
+ assertNotContains "Date disabled header" response "Date: "
+
+-- User-specified Date header is preserved and not duplicated.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "GET /custom-date HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let handler : TestHandler := fun _ =>
+ Response.ok
+ |>.header! "Date" "Mon, 01 Jan 2024 00:00:00 GMT"
+ |>.text "hello"
+ let response ← sendRaw client server raw handler (config := { lingeringTimeout := 3000, generateDate := true })
+
+ assertContains "User Date preserved" response "Date: Mon, 01 Jan 2024 00:00:00 GMT"
+
+ let text := String.fromUTF8! response
+ let count := countOccurrences text "Date: "
+ if count != 1 then
+ throw <| IO.userError s!"Test 'User Date not duplicated' failed:\nExpected one Date header, got {count}\n{text.quote}"
diff --git a/tests/lean/run/async_http_fuzz.lean b/tests/lean/run/async_http_fuzz.lean
new file mode 100644
index 000000000000..8327428b9649
--- /dev/null
+++ b/tests/lean/run/async_http_fuzz.lean
@@ -0,0 +1,652 @@
+import Std.Internal.Http
+import Std.Internal.Async
+import Std.Internal.Async.Timer
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+
+def defaultConfig : Config :=
+ { lingeringTimeout := 1000, generateDate := false }
+
+
+def bad400 : String :=
+ "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def runWithTimeout {α : Type} (name : String) (timeoutMs : Nat := 15000) (action : IO α) : IO α := do
+ let task ← IO.asTask action
+ let ticks := (timeoutMs + 9) / 10
+
+ let rec loop (remaining : Nat) : IO α := do
+ if (← IO.getTaskState task) == .finished then
+ match (← IO.wait task) with
+ | .ok x => pure x
+ | .error err => throw err
+ else
+ match remaining with
+ | 0 =>
+ IO.cancel task
+ throw <| IO.userError s!"Test '{name}' timed out after {timeoutMs}ms (possible hang/regression)"
+ | n + 1 =>
+ IO.sleep 10
+ loop n
+
+ loop ticks
+
+def closeChannelIdempotent {α : Type} (ch : Std.CloseableChannel α) : IO Unit := do
+ match ← EIO.toBaseIO ch.close with
+ | .ok _ => pure ()
+ | .error .alreadyClosed => pure ()
+ | .error err => throw <| IO.userError (toString err)
+
+def sendRaw
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := defaultConfig) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+
+def sendRawAndClose
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := defaultConfig) : IO ByteArray := Async.block do
+ client.send raw
+ closeChannelIdempotent client.getSendChan
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+
+def sendFragmentedAndClose
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (parts : Array ByteArray)
+ (handler : TestHandler)
+ (config : Config := defaultConfig) : IO ByteArray := Async.block do
+ let serverTask ← async (t := AsyncTask) do
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+
+ for part in parts do
+ client.send part
+
+ closeChannelIdempotent client.getSendChan
+ await serverTask
+
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+
+def responseText (response : ByteArray) : String :=
+ String.fromUTF8! response
+
+
+def responseBody (response : ByteArray) : String :=
+ let parts := (responseText response).splitOn "\x0d\n\x0d\n"
+ match parts.drop 1 with
+ | [] => ""
+ | body :: _ => body
+
+
+def assertStatusPrefix (name : String) (response : ByteArray) (prefix_ : String) : IO Unit := do
+ let text := responseText response
+ unless text.startsWith prefix_ do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected status prefix {prefix_.quote}\nGot:\n{text.quote}"
+
+
+def assertExact (name : String) (response : ByteArray) (expected : String) : IO Unit := do
+ let text := responseText response
+ if text != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected:\n{expected.quote}\nGot:\n{text.quote}"
+
+
+def countOccurrences (s : String) (needle : String) : Nat :=
+ if needle.isEmpty then
+ 0
+ else
+ (s.splitOn needle).length - 1
+
+
+def assertStatusCount (name : String) (response : ByteArray) (expected : Nat) : IO Unit := do
+ let text := responseText response
+ let got := countOccurrences text "HTTP/1.1 "
+ if got != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {expected} responses but saw {got}\n{text.quote}"
+
+
+def nextSeed (seed : Nat) : Nat :=
+ (1664525 * seed + 1013904223) % 4294967296
+
+
+def randBelow (seed : Nat) (maxExclusive : Nat) : Nat × Nat :=
+ let seed' := nextSeed seed
+ if maxExclusive == 0 then
+ (0, seed')
+ else
+ (seed' % maxExclusive, seed')
+
+
+def randIn (seed : Nat) (low : Nat) (high : Nat) : Nat × Nat :=
+ if high < low then
+ (low, seed)
+ else
+ let (n, seed') := randBelow seed (high - low + 1)
+ (low + n, seed')
+
+
+def randomAsciiBytes (seed : Nat) (len : Nat) : ByteArray × Nat := Id.run do
+ let mut s := seed
+ let mut out := ByteArray.empty
+
+ for _ in [0:len] do
+ let (r, s') := randBelow s 38
+ s := s'
+
+ let code :=
+ if r < 26 then
+ 97 + r
+ else if r < 36 then
+ 48 + (r - 26)
+ else if r == 36 then
+ 45
+ else
+ 95
+
+ out := out.push (UInt8.ofNat code)
+
+ (out, s)
+
+
+def randomTokenBytes (seed : Nat) (len : Nat) : ByteArray × Nat := Id.run do
+ let mut s := seed
+ let mut out := ByteArray.empty
+
+ for _ in [0:len] do
+ let (r, s') := randBelow s 36
+ s := s'
+
+ let code :=
+ if r < 26 then
+ 97 + r
+ else
+ 48 + (r - 26)
+
+ out := out.push (UInt8.ofNat code)
+
+ (out, s)
+
+
+def randomSplit (seed : Nat) (data : ByteArray) (maxPart : Nat := 17) : Array ByteArray × Nat := Id.run do
+ let mut s := seed
+ let mut out : Array ByteArray := #[]
+ let mut i := 0
+
+ while i < data.size do
+ let remaining := data.size - i
+ let upper := Nat.min maxPart remaining
+ let (partLen, s') := randIn s 1 upper
+ s := s'
+
+ out := out.push (data.extract i (i + partLen))
+ i := i + partLen
+
+ (out, s)
+
+
+def randomChunkedPayload (seed : Nat) (body : ByteArray) : ByteArray × Nat := Id.run do
+ let mut s := seed
+ let mut out := ByteArray.empty
+ let mut i := 0
+
+ while i < body.size do
+ let remaining := body.size - i
+ let maxChunk := Nat.min 9 remaining
+ let (chunkLen, s') := randIn s 1 maxChunk
+ s := s'
+
+ out := out ++ s!"{chunkLen}\x0d\n".toUTF8
+ out := out ++ body.extract i (i + chunkLen)
+ out := out ++ "\x0d\n".toUTF8
+ i := i + chunkLen
+
+ out := out ++ "0\x0d\n\x0d\n".toUTF8
+ (out, s)
+
+
+def mkContentLengthHead (path : String) (bodySize : Nat) : ByteArray :=
+ s!"POST {path} HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: {bodySize}\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+
+
+def mkChunkedHead (path : String) : ByteArray :=
+ s!"POST {path} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+
+
+def randomChunkExtensionList (seed : Nat) (count : Nat) : String × Nat := Id.run do
+ let mut s := seed
+ let mut ext := ""
+
+ for _ in [0:count] do
+ let (nameLen, s1) := randIn s 1 3
+ s := s1
+ let (valueLen, s2) := randIn s 1 3
+ s := s2
+
+ let (nameBytes, s3) := randomTokenBytes s nameLen
+ s := s3
+ let (valueBytes, s4) := randomTokenBytes s valueLen
+ s := s4
+
+ let name := String.fromUTF8! nameBytes
+ let value := String.fromUTF8! valueBytes
+ ext := ext ++ s!";{name}={value}"
+
+ (ext, s)
+
+
+def randomTrailerLines (seed : Nat) (count : Nat) : String × Nat := Id.run do
+ let mut s := seed
+ let mut lines := ""
+
+ for i in [0:count] do
+ let (nameLen, s1) := randIn s 1 4
+ s := s1
+ let (valueLen, s2) := randIn s 1 6
+ s := s2
+
+ let (nameBytes, s3) := randomTokenBytes s nameLen
+ s := s3
+ let (valueBytes, s4) := randomTokenBytes s valueLen
+ s := s4
+
+ let name := String.fromUTF8! nameBytes
+ let value := String.fromUTF8! valueBytes
+ lines := lines ++ s!"X{i}-{name}: {value}\x0d\n"
+
+ (lines, s)
+
+
+def echoBodyHandler : TestHandler := fun req => do
+ let body : String ← req.body.readAll
+ Response.ok |>.text body
+
+
+def runPipelinedReadAll
+ (raw : ByteArray)
+ (config : Config := defaultConfig) : IO (ByteArray × Array String) := Async.block do
+ let (client, server) ← Mock.new
+ let seenRef ← IO.mkRef (#[] : Array String)
+
+ let handler : TestHandler := fun req => do
+ let uri := toString req.head.uri
+ seenRef.modify (·.push uri)
+ let _body : String ← req.body.readAll
+ Response.ok |>.text uri
+
+ client.send raw
+ closeChannelIdempotent client.getSendChan
+
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+
+ let response ← client.recv?
+ let seen ← seenRef.get
+ pure (response.getD .empty, seen)
+
+
+def fuzzContentLengthEcho (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (len, seed1) := randIn seed 0 128
+ seed := seed1
+
+ let (body, seed2) := randomAsciiBytes seed len
+ seed := seed2
+
+ let head := mkContentLengthHead s!"/fuzz-cl-{i}" body.size
+ let (bodyParts, seed3) := randomSplit seed body
+ seed := seed3
+ let parts := #[head] ++ bodyParts
+
+ let (client, server) ← Mock.new
+ let response ← sendFragmentedAndClose client server parts echoBodyHandler
+
+ let expectedBody := String.fromUTF8! body
+ assertStatusPrefix s!"fuzzContentLengthEcho case={i} seed={caseSeed}" response "HTTP/1.1 200"
+
+ let gotBody := responseBody response
+ if gotBody != expectedBody then
+ throw <| IO.userError s!"fuzzContentLengthEcho case={i} seed={caseSeed} failed:\nExpected body {expectedBody.quote}\nGot body {gotBody.quote}\nFull response:\n{(responseText response).quote}"
+
+
+def fuzzContentLengthLeadingZerosAccepted (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (len, seed1) := randIn seed 1 96
+ seed := seed1
+
+ let (leadingZeros, seed2) := randIn seed 1 5
+ seed := seed2
+
+ let (body, seed3) := randomAsciiBytes seed len
+ seed := seed3
+
+ let clToken := String.ofList (List.replicate leadingZeros '0') ++ toString len
+ let raw :=
+ s!"POST /cl-leading-zeros-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: {clToken}\x0d\nConnection: close\x0d\n\x0d\n".toUTF8 ++ body
+
+ let (client, server) ← Mock.new
+ let response ← sendRaw client server raw echoBodyHandler
+
+ let expectedBody := String.fromUTF8! body
+ assertStatusPrefix s!"fuzzContentLengthLeadingZerosAccepted case={i} seed={caseSeed} len={len} zeros={leadingZeros}" response "HTTP/1.1 200"
+
+ let gotBody := responseBody response
+ if gotBody != expectedBody then
+ throw <| IO.userError s!"fuzzContentLengthLeadingZerosAccepted case={i} seed={caseSeed} failed:\nExpected body {expectedBody.quote}\nGot body {gotBody.quote}\nFull response:\n{(responseText response).quote}"
+
+
+def fuzzChunkedEcho (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (len, seed1) := randIn seed 0 128
+ seed := seed1
+
+ let (body, seed2) := randomAsciiBytes seed len
+ seed := seed2
+
+ let (chunkedBody, seed3) := randomChunkedPayload seed body
+ seed := seed3
+
+ let head := mkChunkedHead s!"/fuzz-chunked-{i}"
+ let raw := head ++ chunkedBody
+
+ let (client, server) ← Mock.new
+ let response ← sendRaw client server raw echoBodyHandler
+
+ let expectedBody := String.fromUTF8! body
+ assertStatusPrefix s!"fuzzChunkedEcho case={i} seed={caseSeed}" response "HTTP/1.1 200"
+
+ let gotBody := responseBody response
+ if gotBody != expectedBody then
+ throw <| IO.userError s!"fuzzChunkedEcho case={i} seed={caseSeed} failed:\nExpected body {expectedBody.quote}\nGot body {gotBody.quote}\nFull response:\n{(responseText response).quote}"
+
+
+def fuzzMixedTransferEncodingAndContentLengthRejected (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (len, seed1) := randIn seed 0 96
+ seed := seed1
+
+ let (body, seed2) := randomAsciiBytes seed len
+ seed := seed2
+
+ let (chunkedBody, seed3) := randomChunkedPayload seed body
+ seed := seed3
+
+ let (declaredCl, seed4) := randIn seed 0 128
+ seed := seed4
+
+ let raw :=
+ s!"POST /te-cl-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nContent-Length: {declaredCl}\x0d\nConnection: close\x0d\n\x0d\n".toUTF8 ++ chunkedBody
+
+ let (client, server) ← Mock.new
+ let response ← sendRaw client server raw echoBodyHandler
+ assertExact s!"fuzzMixedTransferEncodingAndContentLengthRejected case={i} seed={caseSeed} declaredCl={declaredCl}" response bad400
+
+
+def fuzzInvalidChunkSizeRejected (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let badTokens : Array String := #["g", "G", "z", "Z", "@", "!", "x"]
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (idx, seed1) := randBelow seed badTokens.size
+ seed := seed1
+
+ let token := badTokens[idx]!
+ let raw :=
+ s!"POST /bad-size-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n{token}\x0d\nabc\x0d\n0\x0d\n\x0d\n".toUTF8
+
+ let (client, server) ← Mock.new
+ let response ← sendRaw client server raw echoBodyHandler
+
+ assertExact s!"fuzzInvalidChunkSizeRejected case={i} seed={caseSeed} token={token}" response bad400
+
+
+def fuzzDuplicateContentLengthRejected (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (cl1, seed1) := randIn seed 0 64
+ seed := seed1
+
+ let (same, seed2) := randBelow seed 2
+ seed := seed2
+
+ let (delta, seed3) := randIn seed 1 10
+ seed := seed3
+
+ let cl2 := if same == 0 then cl1 else cl1 + delta
+ let (body, seed4) := randomAsciiBytes seed cl1
+ seed := seed4
+
+ let raw :=
+ s!"POST /dup-cl-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: {cl1}\x0d\nContent-Length: {cl2}\x0d\nConnection: close\x0d\n\x0d\n".toUTF8 ++ body
+
+ let (client, server) ← Mock.new
+ let response ← sendRaw client server raw echoBodyHandler
+
+ assertExact s!"fuzzDuplicateContentLengthRejected case={i} seed={caseSeed} cl1={cl1} cl2={cl2}" response bad400
+
+
+def fuzzChunkExtensionLimits (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxChunkExtNameLength := 4
+ maxChunkExtValueLength := 4
+ }
+
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (nameLen, seed1) := randIn seed 1 8
+ seed := seed1
+
+ let (valueLen, seed2) := randIn seed 1 8
+ seed := seed2
+
+ let (nameBytes, seed3) := randomTokenBytes seed nameLen
+ seed := seed3
+
+ let (valueBytes, seed4) := randomTokenBytes seed valueLen
+ seed := seed4
+
+ let name := String.fromUTF8! nameBytes
+ let value := String.fromUTF8! valueBytes
+
+ let raw :=
+ s!"POST /ext-limit-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n1;{name}={value}\x0d\nx\x0d\n0\x0d\n\x0d\n".toUTF8
+
+ let expectOk := nameLen ≤ 4 ∧ valueLen ≤ 4
+
+ let (client, server) ← Mock.new
+ let response ← sendRaw client server raw echoBodyHandler (config := config)
+
+ if expectOk then
+ assertStatusPrefix s!"fuzzChunkExtensionLimits case={i} seed={caseSeed} nameLen={nameLen} valueLen={valueLen}" response "HTTP/1.1 200"
+ else
+ assertExact s!"fuzzChunkExtensionLimits case={i} seed={caseSeed} nameLen={nameLen} valueLen={valueLen}" response bad400
+
+
+def fuzzChunkExtensionCountLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxChunkExtensions := 2
+ }
+
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (extCount, seed1) := randIn seed 0 5
+ seed := seed1
+
+ let (extList, seed2) := randomChunkExtensionList seed extCount
+ seed := seed2
+
+ let raw :=
+ s!"POST /ext-count-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n1{extList}\x0d\nx\x0d\n0\x0d\n\x0d\n".toUTF8
+
+ let (client, server) ← Mock.new
+ let response ← sendRaw client server raw echoBodyHandler (config := config)
+
+ if extCount ≤ 2 then
+ assertStatusPrefix s!"fuzzChunkExtensionCountLimit case={i} seed={caseSeed} extCount={extCount}" response "HTTP/1.1 200"
+ else
+ assertExact s!"fuzzChunkExtensionCountLimit case={i} seed={caseSeed} extCount={extCount}" response bad400
+
+
+def fuzzTrailerHeaderCountLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxTrailerHeaders := 2
+ }
+
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (trailerCount, seed1) := randIn seed 0 5
+ seed := seed1
+
+ let (trailers, seed2) := randomTrailerLines seed trailerCount
+ seed := seed2
+
+ let raw :=
+ s!"POST /trailers-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n1\x0d\na\x0d\n0\x0d\n{trailers}\x0d\n".toUTF8
+
+ let (client, server) ← Mock.new
+ let response ← sendRaw client server raw echoBodyHandler (config := config)
+
+ if trailerCount ≤ 2 then
+ assertStatusPrefix s!"fuzzTrailerHeaderCountLimit case={i} seed={caseSeed} trailerCount={trailerCount}" response "HTTP/1.1 200"
+ else
+ assertExact s!"fuzzTrailerHeaderCountLimit case={i} seed={caseSeed} trailerCount={trailerCount}" response bad400
+
+def fuzzCompleteFirstBodyAllowsPipeline (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let mut seed := seed0
+
+ for i in [0:iterations] do
+ let caseSeed := seed
+
+ let (len, seed1) := randIn seed 0 32
+ seed := seed1
+
+ let (body, seed2) := randomAsciiBytes seed len
+ seed := seed2
+
+ let uri1 := s!"/first-complete-{i}"
+ let req1 :=
+ s!"POST {uri1} HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: {len}\x0d\n\x0d\n".toUTF8 ++ body
+ let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+
+ let (response, seen) ← runPipelinedReadAll (req1 ++ req2)
+
+ let text := responseText response
+ assertStatusCount s!"fuzzCompleteFirstBodyAllowsPipeline case={i} seed={caseSeed}" response 2
+
+ unless text.contains uri1 do
+ throw <| IO.userError s!"fuzzCompleteFirstBodyAllowsPipeline case={i} seed={caseSeed} failed:\nMissing first URI {uri1.quote}\n{text.quote}"
+
+ unless text.contains "/second" do
+ throw <| IO.userError s!"fuzzCompleteFirstBodyAllowsPipeline case={i} seed={caseSeed} failed:\nMissing second response\n{text.quote}"
+
+ if seen.size != 2 ∨ seen[0]! != uri1 ∨ seen[1]! != "/second" then
+ throw <| IO.userError s!"fuzzCompleteFirstBodyAllowsPipeline case={i} seed={caseSeed} failed:\nExpected seen=[{uri1.quote}, \"/second\"] got {seen}"
+
+
+-- Property: Content-Length framing is stable across random payloads and random transport splits.
+#eval runWithTimeout "fuzz_content_length_echo" 20000 do
+ fuzzContentLengthEcho 40 0x00C0FFEE
+
+-- Property: Content-Length with randomized leading zeros is accepted and decoded to exact body length.
+#eval runWithTimeout "fuzz_content_length_leading_zeros_accepted" 20000 do
+ fuzzContentLengthLeadingZerosAccepted 30 0x00CAB005
+
+-- Property: Chunked framing reconstructs exact bodies under random chunking and transport splits.
+#eval runWithTimeout "fuzz_chunked_echo" 20000 do
+ fuzzChunkedEcho 40 0x00123456
+
+-- Property: Mixing Transfer-Encoding with Content-Length is always rejected.
+#eval runWithTimeout "fuzz_te_cl_mixed_rejected" 20000 do
+ fuzzMixedTransferEncodingAndContentLengthRejected 30 0x0010CE11
+
+-- Property: Invalid chunk-size tokens are rejected deterministically with 400.
+#eval runWithTimeout "fuzz_invalid_chunk_size_rejected" 20000 do
+ fuzzInvalidChunkSizeRejected 30 0x00BAD001
+
+-- Property: Duplicate Content-Length headers are always rejected (same or different values).
+#eval runWithTimeout "fuzz_duplicate_content_length_rejected" 20000 do
+ fuzzDuplicateContentLengthRejected 30 0x00D0C1A7
+
+-- Property: Chunk extension name/value limits are enforced under randomized lengths.
+#eval runWithTimeout "fuzz_chunk_extension_limits" 20000 do
+ fuzzChunkExtensionLimits 40 0x00A11CE5
+
+-- Property: Chunk extension count limit is enforced under randomized extension lists.
+#eval runWithTimeout "fuzz_chunk_extension_count_limit" 20000 do
+ fuzzChunkExtensionCountLimit 35 0x00E77E11
+
+-- Property: Trailer header count limit is enforced under randomized trailer sections.
+#eval runWithTimeout "fuzz_trailer_header_count_limit" 20000 do
+ fuzzTrailerHeaderCountLimit 35 0x00A71A12
+
+-- Property: Complete first request body allows pipelined follow-up parsing.
+#eval runWithTimeout "fuzz_complete_first_body_allows_pipeline" 20000 do
+ fuzzCompleteFirstBodyAllowsPipeline 30 0x00777777
diff --git a/tests/lean/run/async_http_fuzz_limits.lean b/tests/lean/run/async_http_fuzz_limits.lean
new file mode 100644
index 000000000000..0dca9995ffeb
--- /dev/null
+++ b/tests/lean/run/async_http_fuzz_limits.lean
@@ -0,0 +1,472 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+
+/-!
+# Limit-enforcement fuzzing for the HTTP/1.1 server.
+
+Tests that every configurable limit in `H1.Config` and `Server.Config` is
+correctly enforced under randomized inputs. Inspired by hyper's fuzzing of
+size and count limits.
+-/
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+def closeChannelIdempotent {α : Type} (ch : Std.CloseableChannel α) : IO Unit := do
+ match ← EIO.toBaseIO ch.close with
+ | .ok _ => pure ()
+ | .error .alreadyClosed => pure ()
+ | .error err => throw <| IO.userError (toString err)
+
+def sendRaw
+ (client : Mock.Client) (server : Mock.Server) (raw : ByteArray)
+ (handler : TestHandler) (config : Config) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config |>.run
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+def sendRawAndClose
+ (client : Mock.Client) (server : Mock.Server) (raw : ByteArray)
+ (handler : TestHandler) (config : Config) : IO ByteArray := Async.block do
+ client.send raw
+ closeChannelIdempotent client.getSendChan
+ Std.Http.Server.serveConnection server handler config |>.run
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+def runWithTimeout {α : Type} (name : String) (timeoutMs : Nat := 20000) (action : IO α) : IO α := do
+ let task ← IO.asTask action
+ let ticks := (timeoutMs + 9) / 10
+ let rec loop (remaining : Nat) : IO α := do
+ if (← IO.getTaskState task) == .finished then
+ match (← IO.wait task) with
+ | .ok x => pure x
+ | .error err => throw err
+ else
+ match remaining with
+ | 0 => IO.cancel task; throw <| IO.userError s!"Test '{name}' timed out"
+ | n + 1 => IO.sleep 10; loop n
+ loop ticks
+
+-- PRNG
+def nextSeed (seed : Nat) : Nat := (1664525 * seed + 1013904223) % 4294967296
+def randBelow (seed : Nat) (n : Nat) : Nat × Nat :=
+ let s := nextSeed seed
+ (if n == 0 then 0 else s % n, s)
+def randIn (seed : Nat) (lo hi : Nat) : Nat × Nat :=
+ if hi < lo then (lo, seed) else
+ let (r, s) := randBelow seed (hi - lo + 1)
+ (lo + r, s)
+
+def randomTokenBytes (seed : Nat) (len : Nat) : ByteArray × Nat := Id.run do
+ let mut s := seed; let mut out := ByteArray.empty
+ for _ in [0:len] do
+ let (r, s') := randBelow s 36; s := s'
+ let code := if r < 26 then 97 + r else 48 + (r - 26)
+ out := out.push (UInt8.ofNat code)
+ (out, s)
+
+def randomAsciiBytes (seed : Nat) (len : Nat) : ByteArray × Nat := Id.run do
+ let mut s := seed; let mut out := ByteArray.empty
+ for _ in [0:len] do
+ let (r, s') := randBelow s 26; s := s'
+ out := out.push (UInt8.ofNat (97 + r))
+ (out, s)
+
+private def toHexAux : Nat → Nat → String → String
+ | 0, _, acc => acc
+ | fuel + 1, n, acc =>
+ if n == 0 then acc
+ else
+ let d := n % 16
+ let c : Char := if d < 10 then Char.ofNat (48 + d) else Char.ofNat (87 + d)
+ toHexAux fuel (n / 16) (String.ofList [c] ++ acc)
+
+def natToHex (n : Nat) : String :=
+ if n == 0 then "0" else toHexAux 16 n ""
+
+def assertStatusPrefix (name : String) (response : ByteArray) (pfx : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.startsWith pfx do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {pfx.quote}\nGot:\n{text.quote}"
+
+def assertExact (name : String) (response : ByteArray) (expected : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ if text != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected:\n{expected.quote}\nGot:\n{text.quote}"
+
+def countOccurrences (s needle : String) : Nat :=
+ if needle.isEmpty then 0 else (s.splitOn needle).length - 1
+
+def bad400 : String :=
+ "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def echoBodyHandler : TestHandler := fun req => do
+ let body : String ← req.body.readAll
+ Response.ok |>.text body
+
+def okHandler : TestHandler := fun _ => Response.ok |>.text "ok"
+
+-- ============================================================================
+-- maxBodySize — Content-Length framing
+-- ============================================================================
+
+-- Property: Content-Length body exactly at or below maxBodySize → 200.
+-- Content-Length body above maxBodySize → 413 (no body bytes needed).
+def fuzzBodySizeLimitContentLength (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let limit : Nat := 64
+ let config : Config := { lingeringTimeout := 1000, generateDate := false, maxBodySize := limit }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (bodySize, s1) := randIn seed 0 (limit + 20); seed := s1
+ let (bodyBytes, s2) := randomAsciiBytes seed bodySize; seed := s2
+ let raw :=
+ s!"POST /bl-cl-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: {bodySize}\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ ++ bodyBytes
+ 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 bodySize ≤ limit then
+ assertStatusPrefix s!"fuzzBodySizeLimitCL iter={i} seed={caseSeed} size={bodySize}" response "HTTP/1.1 200"
+ else
+ assertStatusPrefix s!"fuzzBodySizeLimitCL iter={i} seed={caseSeed} size={bodySize}" response "HTTP/1.1 413"
+
+-- ============================================================================
+-- maxBodySize — chunked framing
+-- ============================================================================
+
+-- Property: chunked bodies with total bytes 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 }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ -- Total body size across 1-4 chunks
+ let (totalSize, s1) := randIn seed 0 (limit + 16); seed := s1
+ let (numChunks, s2) := randIn seed 1 4; seed := s2
+
+ -- Build chunks that sum to totalSize
+ let chunkSize := (totalSize + numChunks - 1) / numChunks
+ let mut chunkedBody := ByteArray.empty
+ let mut remaining := totalSize
+ for _ in [0:numChunks] do
+ if remaining == 0 then break
+ let thisChunk := Nat.min chunkSize remaining
+ let (chunkBytes, s3) := randomAsciiBytes seed thisChunk; seed := s3
+ chunkedBody := chunkedBody ++ s!"{natToHex thisChunk}\x0d\n".toUTF8 ++ chunkBytes ++ "\x0d\n".toUTF8
+ remaining := remaining - thisChunk
+ chunkedBody := chunkedBody ++ "0\x0d\n\x0d\n".toUTF8
+
+ let raw :=
+ s!"POST /bl-ch-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ ++ chunkedBody
+ 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"
+ else
+ assertStatusPrefix s!"fuzzBodySizeLimitChunked iter={i} seed={caseSeed} total={totalSize}" response "HTTP/1.1 413"
+
+-- ============================================================================
+-- maxHeaders — header count limit
+-- ============================================================================
+
+-- Property: header count at or below maxHeaders → 200.
+-- header count above maxHeaders → 400.
+def fuzzHeaderCountLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let limit : Nat := 5
+ let config : Config := { lingeringTimeout := 1000, generateDate := false, maxHeaders := limit }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ -- Host counts as 1 header, Connection as 1, so extra headers = headerCount - 2
+ let (headerCount, s1) := randIn seed 2 (limit + 4); seed := s1
+ let extraCount := headerCount - 2 -- we always add Host + Connection
+
+ let mut extraHeaders := ""
+ let mut s := s1
+ for j in [0:extraCount] do
+ let (nameLen, s2) := randIn s 1 8; s := s2
+ let (nameBytes, s3) := randomTokenBytes s nameLen; s := s3
+ let name := String.fromUTF8! nameBytes
+ extraHeaders := extraHeaders ++ s!"X-Extra-{j}-{name}: value\x0d\n"
+ seed := s
+
+ let raw :=
+ s!"GET /hc-{i} HTTP/1.1\x0d\nHost: example.com\x0d\n{extraHeaders}Connection: close\x0d\n\x0d\n".toUTF8
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server raw okHandler config
+ -- headerCount includes Host and Connection (always present)
+ if headerCount ≤ limit then
+ assertStatusPrefix s!"fuzzHeaderCount iter={i} seed={caseSeed} count={headerCount}" response "HTTP/1.1 200"
+ else
+ assertStatusPrefix s!"fuzzHeaderCount iter={i} seed={caseSeed} count={headerCount}" response "HTTP/1.1 400"
+
+-- ============================================================================
+-- maxHeaderBytes — total header bytes limit
+-- ============================================================================
+
+-- Property: headers whose aggregate bytes (name + ": " + value + "\r\n") are at or
+-- below maxHeaderBytes are accepted; above it they are rejected with 400.
+def fuzzHeaderTotalBytesLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ -- Fixed baseline: "Host: example.com\r\n" + "Connection: close\r\n" = 20 + 20 = 40 bytes.
+ -- We'll add a single large X-Payload header to cross the boundary.
+ let limit : Nat := 200
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxHeaderBytes := limit
+ maxHeaderValueLength := limit + 100 -- allow value longer than total limit for testing
+ }
+ let baseline := ("Host: example.com\x0d\nConnection: close\x0d\n".toUTF8).size
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ -- Pick a value size that puts total bytes just under or over the limit
+ -- Each "X-Payload: " header = name(9) + ": "(2) + value + "\r\n"(2) = value + 13
+ let overhead := baseline + 13 -- "X-Payload" (9) + ": " (2) + "\r\n" (2) + baseline
+ -- We want value sizes that land on both sides of (limit - overhead)
+ let boundary := if limit > overhead then limit - overhead else 0
+ let (valueSize, s1) := randIn seed 0 (boundary + 20); seed := s1
+ let (valueBytes, s2) := randomAsciiBytes seed valueSize; seed := s2
+ let value := String.fromUTF8! valueBytes
+
+ let raw :=
+ s!"GET /hb-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nX-Payload: {value}\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server raw okHandler config
+ -- Total bytes = baseline + "X-Payload: " + value + "\r\n"
+ let totalBytes := baseline + 9 + 2 + valueSize + 2
+ if totalBytes ≤ limit then
+ assertStatusPrefix s!"fuzzHeaderBytes iter={i} seed={caseSeed} total={totalBytes}" response "HTTP/1.1 200"
+ else
+ assertStatusPrefix s!"fuzzHeaderBytes iter={i} seed={caseSeed} total={totalBytes}" response "HTTP/1.1 400"
+
+-- ============================================================================
+-- maxMessages — requests per connection
+-- ============================================================================
+
+-- Property: after maxMessages requests on a single connection, the server
+-- closes the connection (disables keep-alive). All maxMessages
+-- requests receive a valid response.
+def fuzzMaxMessagesPerConnection (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let limit : Nat := 3
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxRequests := limit
+ }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (reqCount, s1) := randIn seed 1 (limit + 3); seed := s1
+
+ -- Build reqCount keep-alive requests followed by close
+ let mut raw := ByteArray.empty
+ for j in [0:reqCount] do
+ let connHeader :=
+ if j + 1 == reqCount then "Connection: close\x0d\n" else "Connection: keep-alive\x0d\n"
+ raw := raw ++ s!"GET /msg-{i}-{j} HTTP/1.1\x0d\nHost: example.com\x0d\n{connHeader}\x0d\n".toUTF8
+
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server raw okHandler config
+ let text := String.fromUTF8! response
+ let seen := countOccurrences text "HTTP/1.1 200"
+ let expected := Nat.min reqCount limit
+ if seen != expected then
+ throw <| IO.userError
+ s!"fuzzMaxMessages iter={i} seed={caseSeed} reqCount={reqCount}: expected {expected} responses, got {seen}\n{text.quote}"
+
+-- ============================================================================
+-- maxLeadingEmptyLines — leading CRLF before request-line
+-- ============================================================================
+
+-- Property: at most maxLeadingEmptyLines bare CRLFs before the request-line are tolerated.
+-- More than that → 400.
+def fuzzLeadingEmptyLinesLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let limit : Nat := 4
+ let config : Config := { lingeringTimeout := 1000, generateDate := false, maxLeadingEmptyLines := limit }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (lineCount, s1) := randIn seed 0 (limit + 4); seed := s1
+ let leadingCRLF := (List.replicate lineCount "\x0d\n").foldl (· ++ ·) ""
+ let raw :=
+ (leadingCRLF ++ s!"GET /le-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n").toUTF8
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server raw okHandler config
+ if lineCount ≤ limit then
+ assertStatusPrefix s!"fuzzLeadingEmptyLines iter={i} seed={caseSeed} count={lineCount}" response "HTTP/1.1 200"
+ else
+ assertStatusPrefix s!"fuzzLeadingEmptyLines iter={i} seed={caseSeed} count={lineCount}" response "HTTP/1.1 400"
+
+-- ============================================================================
+-- maxSpaceSequence — OWS (optional whitespace) limit
+-- ============================================================================
+
+-- Property: OWS sequences at or below maxSpaceSequence are accepted.
+-- OWS sequences exceeding the limit → 400.
+def fuzzOWSSequenceLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let limit : Nat := 4
+ let config : Config := { lingeringTimeout := 1000, generateDate := false, maxSpaceSequence := limit }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (spaceCount, s1) := randIn seed 0 (limit + 4); seed := s1
+ let spaces := String.ofList (List.replicate spaceCount ' ')
+ -- OWS appears between ':' and value in header fields
+ let raw :=
+ s!"GET /ows-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nX-OWS:{spaces}value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server raw okHandler config
+ if spaceCount ≤ limit then
+ assertStatusPrefix s!"fuzzOWSLimit iter={i} seed={caseSeed} spaces={spaceCount}" response "HTTP/1.1 200"
+ else
+ assertStatusPrefix s!"fuzzOWSLimit iter={i} seed={caseSeed} spaces={spaceCount}" response "HTTP/1.1 400"
+
+-- ============================================================================
+-- maxStartLineLength — request-line length limit
+-- ============================================================================
+
+-- Property: request lines at or below maxStartLineLength → 200.
+-- Request lines above maxStartLineLength → 414 (URI too long) or 400.
+def fuzzStartLineLengthLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let limit : Nat := 64
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxStartLineLength := limit
+ maxUriLength := limit
+ }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ -- "GET " (4) + path + " HTTP/1.1\r\n" (12) → path can be up to (limit - 16)
+ let pathBudget := if limit > 16 then limit - 16 else 1
+ let (pathLen, s1) := randIn seed 1 (pathBudget + 10); seed := s1
+ let path := "/" ++ String.ofList (List.replicate (pathLen - 1) 'a')
+ let raw :=
+ s!"GET {path} HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server raw okHandler config
+ -- start-line = "GET " + path + " HTTP/1.1\r\n"
+ let lineLen := 4 + pathLen + 11
+ if lineLen ≤ limit then
+ assertStatusPrefix s!"fuzzStartLineLen iter={i} seed={caseSeed} len={lineLen}" response "HTTP/1.1 200"
+ else
+ -- Either 414 (URI too long) or 400
+ let text := String.fromUTF8! response
+ unless text.startsWith "HTTP/1.1 414" || text.startsWith "HTTP/1.1 400" do
+ throw <| IO.userError
+ s!"fuzzStartLineLen iter={i} seed={caseSeed} len={lineLen}: expected 414 or 400, got {text.quote}"
+
+-- ============================================================================
+-- maxHeaderNameLength and maxHeaderValueLength
+-- ============================================================================
+
+-- Property: header names exceeding maxHeaderNameLength → 400.
+def fuzzHeaderNameLengthLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let limit : Nat := 16
+ let config : Config := { lingeringTimeout := 1000, generateDate := false, maxHeaderNameLength := limit }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (nameLen, s1) := randIn seed 1 (limit + 8); seed := s1
+ let (nameBytes, s2) := randomTokenBytes seed nameLen; seed := s2
+ let name := String.fromUTF8! nameBytes
+ let raw :=
+ s!"GET /hnl-{i} HTTP/1.1\x0d\nHost: example.com\x0d\n{name}: value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server raw okHandler config
+ if nameLen ≤ limit then
+ assertStatusPrefix s!"fuzzHeaderNameLen iter={i} seed={caseSeed} len={nameLen}" response "HTTP/1.1 200"
+ else
+ assertStatusPrefix s!"fuzzHeaderNameLen iter={i} seed={caseSeed} len={nameLen}" response "HTTP/1.1 400"
+
+-- Property: header values exceeding maxHeaderValueLength → 400.
+def fuzzHeaderValueLengthLimit (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let limit : Nat := 32
+ let config : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxHeaderValueLength := limit
+ maxHeaderBytes := 65536 -- don't let total bytes limit interfere
+ }
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (valueLen, s1) := randIn seed 0 (limit + 8); seed := s1
+ let (valueBytes, s2) := randomAsciiBytes seed valueLen; seed := s2
+ let value := String.fromUTF8! valueBytes
+ let raw :=
+ s!"GET /hvl-{i} HTTP/1.1\x0d\nHost: example.com\x0d\nX-Long: {value}\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server raw okHandler config
+ if valueLen ≤ limit then
+ assertStatusPrefix s!"fuzzHeaderValueLen iter={i} seed={caseSeed} len={valueLen}" response "HTTP/1.1 200"
+ else
+ assertStatusPrefix s!"fuzzHeaderValueLen iter={i} seed={caseSeed} len={valueLen}" response "HTTP/1.1 400"
+
+-- ============================================================================
+-- Run all properties
+-- ============================================================================
+
+-- Property: maxBodySize enforced for Content-Length framing.
+#eval runWithTimeout "fuzz_body_limit_content_length" 30000 do
+ fuzzBodySizeLimitContentLength 50 0x00B0DEC0
+
+-- Property: maxBodySize enforced for chunked framing.
+#eval runWithTimeout "fuzz_body_limit_chunked" 30000 do
+ fuzzBodySizeLimitChunked 40 0x00C8BE11
+
+-- Property: maxHeaders count limit is enforced.
+#eval runWithTimeout "fuzz_header_count_limit" 30000 do
+ fuzzHeaderCountLimit 50 0x00AA55AA
+
+-- Property: maxHeaderBytes aggregate limit is enforced.
+#eval runWithTimeout "fuzz_header_bytes_limit" 30000 do
+ fuzzHeaderTotalBytesLimit 40 0x00FACE77
+
+-- Property: maxMessages per connection closes keep-alive after the configured count.
+#eval runWithTimeout "fuzz_max_messages_per_connection" 30000 do
+ fuzzMaxMessagesPerConnection 30 0x00123ABC
+
+-- Property: maxLeadingEmptyLines limit is enforced.
+#eval runWithTimeout "fuzz_leading_empty_lines_limit" 30000 do
+ fuzzLeadingEmptyLinesLimit 50 0x00EEF00D
+
+-- Property: maxSpaceSequence (OWS) limit is enforced.
+#eval runWithTimeout "fuzz_ows_sequence_limit" 30000 do
+ fuzzOWSSequenceLimit 50 0x00ABE5AB
+
+-- Property: maxStartLineLength / maxUriLength is enforced, returning 414 or 400.
+#eval runWithTimeout "fuzz_start_line_length_limit" 30000 do
+ fuzzStartLineLengthLimit 50 0x00C0FFEE
+
+-- Property: maxHeaderNameLength is enforced.
+#eval runWithTimeout "fuzz_header_name_length_limit" 30000 do
+ fuzzHeaderNameLengthLimit 50 0x00DEAD01
+
+-- Property: maxHeaderValueLength is enforced.
+#eval runWithTimeout "fuzz_header_value_length_limit" 30000 do
+ fuzzHeaderValueLengthLimit 50 0x00BEEF02
diff --git a/tests/lean/run/async_http_fuzz_random.lean b/tests/lean/run/async_http_fuzz_random.lean
new file mode 100644
index 000000000000..0ae4dfa14b9b
--- /dev/null
+++ b/tests/lean/run/async_http_fuzz_random.lean
@@ -0,0 +1,304 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+
+/-!
+# Random-byte fuzzing for the HTTP/1.1 parser.
+
+Inspired by hyper's `fuzz_h1_req` libFuzzer target. The core property: any byte
+sequence fed to the server must be handled without panicking, hanging, or
+producing a malformed response. The server must either:
+- Send no bytes (connection closed before a complete request arrives), or
+- Send a response that starts with "HTTP/1.1 ".
+-/
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+def defaultConfig : Config :=
+ { lingeringTimeout := 1000, generateDate := false }
+
+def closeChannelIdempotent {α : Type} (ch : Std.CloseableChannel α) : IO Unit := do
+ match ← EIO.toBaseIO ch.close with
+ | .ok _ => pure ()
+ | .error .alreadyClosed => pure ()
+ | .error err => throw <| IO.userError (toString err)
+
+def sendRawAndClose
+ (client : Mock.Client) (server : Mock.Server) (raw : ByteArray)
+ (handler : TestHandler) (config : Config := defaultConfig) : IO ByteArray := Async.block do
+ client.send raw
+ closeChannelIdempotent client.getSendChan
+ Std.Http.Server.serveConnection server handler config |>.run
+ let res ← client.recv?
+ pure (res.getD .empty)
+
+def runWithTimeout {α : Type} (name : String) (timeoutMs : Nat := 20000) (action : IO α) : IO α := do
+ let task ← IO.asTask action
+ let ticks := (timeoutMs + 9) / 10
+ let rec loop (remaining : Nat) : IO α := do
+ if (← IO.getTaskState task) == .finished then
+ match (← IO.wait task) with
+ | .ok x => pure x
+ | .error err => throw err
+ else
+ match remaining with
+ | 0 => IO.cancel task; throw <| IO.userError s!"Test '{name}' timed out"
+ | n + 1 => IO.sleep 10; loop n
+ loop ticks
+
+-- PRNG
+def nextSeed (seed : Nat) : Nat := (1664525 * seed + 1013904223) % 4294967296
+def randBelow (seed : Nat) (n : Nat) : Nat × Nat :=
+ let s := nextSeed seed
+ (if n == 0 then 0 else s % n, s)
+def randIn (seed : Nat) (lo hi : Nat) : Nat × Nat :=
+ if hi < lo then (lo, seed) else
+ let (r, s) := randBelow seed (hi - lo + 1)
+ (lo + r, s)
+
+-- All 256 byte values
+def randomFullBytes (seed : Nat) (len : Nat) : ByteArray × Nat := Id.run do
+ let mut s := seed; let mut out := ByteArray.empty
+ for _ in [0:len] do
+ let (r, s') := randBelow s 256; s := s'
+ out := out.push (UInt8.ofNat r)
+ (out, s)
+
+def okHandler : TestHandler := fun _ => Response.ok |>.text "ok"
+
+-- Server-generated responses are always valid ASCII. Verify the response is
+-- either empty or starts with the HTTP/1.1 status-line prefix.
+def assertValidHttpOrEmpty (name : String) (response : ByteArray) : IO Unit := do
+ if response.size == 0 then pure ()
+ else
+ let pfx := "HTTP/1.1 ".toUTF8
+ if response.size >= pfx.size && response.extract 0 pfx.size == pfx then pure ()
+ else
+ let display := match String.fromUTF8? (response.extract 0 (Nat.min 200 response.size)) with
+ | some s => s.quote | none => "(non-UTF-8 bytes)"
+ throw <| IO.userError
+ s!"Test '{name}' failed:\nResponse is neither empty nor valid HTTP/1.1:\n{display}"
+
+-- Property: any fully-random byte sequence never causes a panic or malformed response.
+-- Direct analogue of hyper's fuzz_h1_req libFuzzer target.
+def fuzzRandomBytesNoPanic (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (len, s1) := randIn seed 0 96; seed := s1
+ let (bytes, s2) := randomFullBytes seed len; seed := s2
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server bytes okHandler
+ assertValidHttpOrEmpty s!"fuzzRandomBytesNoPanic iter={i} seed={caseSeed} len={len}" response
+
+-- Property: flipping a single bit in any valid request must not cause a panic.
+def fuzzBitFlipOnValidRequests (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let corpus : Array ByteArray := #[
+ "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ "POST /submit HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8,
+ "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8,
+ "OPTIONS * HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ "CONNECT example.com:443 HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ "DELETE /resource HTTP/1.1\x0d\nHost: api.example.com\x0d\nAuthorization: Bearer token123\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ ]
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (idx, s1) := randBelow seed corpus.size; seed := s1
+ let req := corpus[idx]!
+ let (pos, s2) := randBelow seed req.size; seed := s2
+ let (bit, s3) := randBelow seed 8; seed := s3
+ let orig := req[pos]!
+ let mask : UInt8 := (1 : UInt8) <<< bit.toUInt8
+ let flipped := orig ^^^ mask
+ let mutated := (req.extract 0 pos).push flipped ++ req.extract (pos + 1) req.size
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server mutated okHandler
+ assertValidHttpOrEmpty
+ s!"fuzzBitFlip iter={i} seed={caseSeed} reqIdx={idx} pos={pos} bit={bit}" response
+
+-- Property: truncating a valid request at any byte boundary must not cause a panic.
+def fuzzTruncatedRequests (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let corpus : Array ByteArray := #[
+ "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ "POST /data HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 4\x0d\nConnection: close\x0d\n\x0d\ndata".toUTF8,
+ "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n4\x0d\ndata\x0d\n0\x0d\n\x0d\n".toUTF8,
+ "HEAD /resource HTTP/1.1\x0d\nHost: example.com\x0d\nAccept: application/json\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ ]
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (idx, s1) := randBelow seed corpus.size; seed := s1
+ let req := corpus[idx]!
+ let (truncLen, s2) := randBelow seed req.size; seed := s2
+ let truncated := req.extract 0 truncLen
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server truncated okHandler
+ assertValidHttpOrEmpty
+ s!"fuzzTruncated iter={i} seed={caseSeed} reqIdx={idx} truncLen={truncLen}" response
+
+-- Property: a valid HTTP method prefix followed by garbage must not cause a panic.
+def fuzzMethodPrefixWithGarbage (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let methods : Array ByteArray := #[
+ "GET ".toUTF8, "POST ".toUTF8, "PUT ".toUTF8, "DELETE ".toUTF8,
+ "HEAD ".toUTF8, "OPTIONS ".toUTF8, "PATCH ".toUTF8, "CONNECT ".toUTF8,
+ "HTTP/1.1 ".toUTF8,
+ ByteArray.empty,
+ ]
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (mIdx, s1) := randBelow seed methods.size; seed := s1
+ let pfx := methods[mIdx]!
+ let (gLen, s2) := randIn seed 0 64; seed := s2
+ let (garbage, s3) := randomFullBytes seed gLen; seed := s3
+ let request := pfx ++ garbage
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server request okHandler
+ assertValidHttpOrEmpty
+ s!"fuzzMethodPrefix iter={i} seed={caseSeed} mIdx={mIdx} gLen={gLen}" response
+
+-- Property: high-byte (0x80–0xFF, non-ASCII) sequences must not cause a panic.
+def fuzzHighByteValues (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (len, s1) := randIn seed 0 48; seed := s1
+ let mut out := ByteArray.empty
+ let mut s := s1
+ for _ in [0:len] do
+ let (r, s') := randBelow s 128; s := s'
+ out := out.push (UInt8.ofNat (r + 128))
+ seed := s
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server out okHandler
+ assertValidHttpOrEmpty s!"fuzzHighBytes iter={i} seed={caseSeed} len={len}" response
+
+-- Property: garbage appended after a complete request must not cause a panic.
+def fuzzGarbageAfterCompleteRequest (iterations : Nat) (seed0 : Nat) : IO Unit := do
+ let validReq :=
+ "GET /check HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let mut seed := seed0
+ for i in [0:iterations] do
+ let caseSeed := seed
+ let (gLen, s1) := randIn seed 0 32; seed := s1
+ let (garbage, s2) := randomFullBytes seed gLen; seed := s2
+ let request := validReq ++ garbage
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server request okHandler
+ assertValidHttpOrEmpty
+ s!"fuzzGarbageAfter iter={i} seed={caseSeed} gLen={gLen}" response
+
+-- Property: every single-byte input is handled safely (all 256 values).
+def fuzzSingleByteInputs : IO Unit := do
+ for b in List.range 256 do
+ let bytes := ByteArray.mk #[b.toUInt8]
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server bytes okHandler
+ assertValidHttpOrEmpty s!"fuzzSingleByte byte={b}" response
+
+-- Property: known attack patterns and real-world malformed inputs are handled safely.
+-- This is the Lean analogue of hyper's denial-of-service and smuggling corpus.
+def fuzzKnownMaliciousPatterns : IO Unit := do
+ let patterns : Array ByteArray := #[
+ -- TLS 1.2 client hello prefix
+ ByteArray.mk #[0x16, 0x03, 0x01, 0x00, 0xa5, 0x01, 0x00, 0x00],
+ -- TLS 1.3 client hello prefix
+ ByteArray.mk #[0x16, 0x03, 0x03, 0x00, 0x7c, 0x01, 0x00, 0x00],
+ -- HTTP/2 connection preface
+ "PRI * HTTP/2.0\x0d\n\x0d\nSM\x0d\n\x0d\n".toUTF8,
+ -- Bare LF line endings
+ "GET / HTTP/1.1\nHost: example.com\n\n".toUTF8,
+ -- CR-only line endings
+ "GET / HTTP/1.1\x0dHost: example.com\x0d\x0d".toUTF8,
+ -- Null bytes everywhere
+ ByteArray.mk #[0x00, 0x00, 0x00, 0x00],
+ -- CRLF injection attempt in request-line
+ "GET /path%0d%0aInjected: header HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n".toUTF8,
+ -- Unicode in path (raw multibyte UTF-8)
+ "GET /caf\xc3\xa9 HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n".toUTF8,
+ -- HTTP response sent as a request (should fail, not panic)
+ "HTTP/1.1 200 OK\x0d\nContent-Length: 2\x0d\n\x0d\nok".toUTF8,
+ -- Request smuggling: CL.TE
+ "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 6\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\n0\x0d\n\x0d\nX".toUTF8,
+ -- Request smuggling: TE.CL
+ "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nContent-Length: 3\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8,
+ -- Duplicate chunked coding
+ "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8,
+ -- TE with tab (whitespace obfuscation)
+ "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding:\x09chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8,
+ -- TE with null byte injection
+ "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunk\x00ed\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8,
+ -- Extremely long method token
+ (String.ofList (List.replicate 8192 'A') ++ " / HTTP/1.1\x0d\nHost: h\x0d\n\x0d\n").toUTF8,
+ -- SSRF-like absolute-form URI targeting internal host
+ "GET http://169.254.169.254/latest/meta-data/ HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n".toUTF8,
+ -- Chunk size with non-hex chars
+ "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\nGG\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8,
+ -- Chunk size overflow attempt (16+ hex digits)
+ "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\nffffffffffffffff1\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8,
+ -- Header with embedded CRLF in value
+ "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nX-Inject: foo\x0d\nEvil: injected\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ -- Multiple Host headers (smuggling attempt)
+ "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nHost: evil.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ -- Absolute-form URI with bad host overrides Host header
+ "GET http://evil.internal/steal HTTP/1.1\x0d\nHost: public.example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ -- Folded header (obs-fold, rejected per RFC 9112)
+ "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nX-Folded: value\x0d\n continuation\x0d\nConnection: close\x0d\n\x0d\n".toUTF8,
+ ]
+ for i in [:patterns.size] do
+ let pattern := patterns[i]!
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server pattern okHandler
+ assertValidHttpOrEmpty s!"fuzzKnownMalicious pattern={i}" response
+
+-- ============================================================================
+-- Run all properties
+-- ============================================================================
+
+-- Property: any random byte sequence is handled safely (core libFuzzer equivalent).
+#eval runWithTimeout "fuzz_random_bytes_no_panic" 30000 do
+ fuzzRandomBytesNoPanic 200 0x00FACADE
+
+-- Property: single bit mutations on valid requests are handled safely.
+#eval runWithTimeout "fuzz_bit_flip_valid_requests" 30000 do
+ fuzzBitFlipOnValidRequests 150 0x00B1FF10
+
+-- Property: truncation at any byte boundary is handled safely.
+#eval runWithTimeout "fuzz_truncated_requests" 30000 do
+ fuzzTruncatedRequests 150 0x00DEAD42
+
+-- Property: HTTP method prefix followed by random garbage is handled safely.
+#eval runWithTimeout "fuzz_method_prefix_with_garbage" 30000 do
+ fuzzMethodPrefixWithGarbage 100 0x00CA7500
+
+-- Property: high-byte (non-ASCII) sequences are handled safely.
+#eval runWithTimeout "fuzz_high_byte_values" 30000 do
+ fuzzHighByteValues 120 0x00FF8000
+
+-- Property: garbage appended after a complete request is handled safely.
+#eval runWithTimeout "fuzz_garbage_after_complete_request" 30000 do
+ fuzzGarbageAfterCompleteRequest 100 0x00A1B2C3
+
+-- Property: every single-byte input is handled safely (all 256 cases).
+#eval runWithTimeout "fuzz_single_byte_inputs" 30000 do
+ fuzzSingleByteInputs
+
+-- Property: known attack patterns and malformed inputs are handled safely.
+#eval runWithTimeout "fuzz_known_malicious_patterns" 30000 do
+ fuzzKnownMaliciousPatterns
diff --git a/tests/lean/run/async_http_hang_regressions.lean b/tests/lean/run/async_http_hang_regressions.lean
new file mode 100644
index 000000000000..940de7210b28
--- /dev/null
+++ b/tests/lean/run/async_http_hang_regressions.lean
@@ -0,0 +1,376 @@
+import Std.Internal.Http
+import Std.Internal.Async
+import Std.Internal.Async.Timer
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+def defaultConfig : Config :=
+ { lingeringTimeout := 500, generateDate := false }
+
+def runWithTimeout {α : Type} (name : String) (timeoutMs : Nat := 2000) (action : IO α) : IO α := do
+ let task ← IO.asTask action
+ let ticks := (timeoutMs + 9) / 10
+
+ let rec loop (remaining : Nat) : IO α := do
+ if (← IO.getTaskState task) == .finished then
+ match (← IO.wait task) with
+ | .ok x => pure x
+ | .error err => throw err
+ else
+ match remaining with
+ | 0 =>
+ IO.cancel task
+ throw <| IO.userError s!"Test '{name}' timed out after {timeoutMs}ms (possible hang/loop)"
+ | n + 1 =>
+ IO.sleep 10
+ loop n
+
+ loop ticks
+
+def sendRaw (client : Mock.Client) (server : Mock.Server) (raw : ByteArray)
+ (handler : TestHandler) (config : Config := defaultConfig) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+def sendRawTimed (name : String) (raw : ByteArray)
+ (handler : TestHandler) (config : Config := defaultConfig) : IO ByteArray :=
+ runWithTimeout name 2000 do
+ let (client, server) ← Mock.new
+ sendRaw client server raw handler config
+
+def runClosedClientTimed (name : String) (raw : ByteArray)
+ (handler : TestHandler) (config : Config := defaultConfig) : IO Unit :=
+ runWithTimeout name 2000 do
+ Async.block do
+ let (client, server) ← Mock.new
+ client.send raw
+ client.close
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+
+def countOccurrences (s : String) (needle : String) : Nat :=
+ if needle.isEmpty then 0 else (s.splitOn needle).length - 1
+
+def assertStatusPrefix (name : String) (response : ByteArray) (prefix_ : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.startsWith prefix_ do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected prefix: {prefix_.quote}\nGot:\n{text.quote}"
+
+def assertContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.contains needle do
+ throw <| IO.userError s!"Test '{name}' failed:\nMissing: {needle.quote}\nGot:\n{text.quote}"
+
+def assertNotContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ if text.contains needle then
+ throw <| IO.userError s!"Test '{name}' failed:\nDid not expect {needle.quote}\nGot:\n{text.quote}"
+
+def assertEndsWith (name : String) (response : ByteArray) (suffix_ : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.endsWith suffix_ do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected suffix: {suffix_.quote}\nGot:\n{text.quote}"
+
+def assertStatusCount (name : String) (response : ByteArray) (expected : Nat) : IO Unit := do
+ let text := String.fromUTF8! response
+ let got := countOccurrences text "HTTP/1.1 "
+ unless got == expected do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {expected} HTTP responses, got {got}\n{text.quote}"
+
+def onesChunked (n : Nat) : String := Id.run do
+ let mut body := ""
+ for i in [0:n] do
+ body := body ++ s!"{toString i |>.length}\x0d\n{toString i}\x0d\n"
+ body ++ "0\x0d\n\x0d\n"
+
+def ignoreHandler : TestHandler := fun _ => Response.ok |>.text "ok"
+
+def uriHandler : TestHandler := fun req => Response.ok |>.text (toString req.head.uri)
+
+def echoBodyHandler : TestHandler := fun req => do
+ let mut body := ByteArray.empty
+ for chunk in req.body do
+ body := body ++ chunk.data
+ Response.ok |>.text (String.fromUTF8! body)
+
+def firstChunkHandler : TestHandler := fun req => do
+ let first ← req.body.recv
+ let text :=
+ match first with
+ | some chunk => String.fromUTF8! chunk.data
+ | none => "none"
+ Response.ok |>.text text
+
+def streamPiecesHandler (n : Nat) : TestHandler := fun _ => do
+ let (outgoing, _incoming) ← Body.mkChannel
+ background do
+ for i in [0:n] do
+ outgoing.send <| Chunk.ofByteArray s!"piece-{i};".toUTF8
+ outgoing.close
+ return Response.ok
+ |>.body outgoing
+
+def stressResponseHandler (n : Nat) : TestHandler := fun _ => do
+ let (outgoing, _incoming) ← Body.mkChannel
+ background do
+ for i in [0:n] do
+ outgoing.send <| Chunk.ofByteArray s!"x{i},".toUTF8
+ outgoing.close
+ return Response.ok
+ |>.body outgoing
+
+-- 01: Ignore fixed-size request body and respond immediately.
+#eval runWithTimeout "01_ignore_fixed_length_body" 2000 do
+ let raw := "POST /fixed HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 10\x0d\nConnection: close\x0d\n\x0d\n0123456789".toUTF8
+ let response ← sendRawTimed "01_ignore_fixed_length_body/send" raw ignoreHandler
+ assertStatusPrefix "01_ignore_fixed_length_body" response "HTTP/1.1 200"
+
+-- 02: Ignore chunked request body and respond immediately.
+#eval runWithTimeout "02_ignore_chunked_body" 2000 do
+ let raw := "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n6\x0d\n world\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRawTimed "02_ignore_chunked_body/send" raw ignoreHandler
+ assertStatusPrefix "02_ignore_chunked_body" response "HTTP/1.1 200"
+
+-- 03: Large fixed-size body ignored by handler (regression for stalled body transfer).
+#eval runWithTimeout "03_ignore_large_fixed_body" 2000 do
+ let body := String.ofList (List.replicate 8192 'A')
+ let raw := s!"POST /large HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 8192\x0d\nConnection: close\x0d\n\x0d\n{body}".toUTF8
+ let response ← sendRawTimed "03_ignore_large_fixed_body/send" raw ignoreHandler
+ assertStatusPrefix "03_ignore_large_fixed_body" response "HTTP/1.1 200"
+
+-- 04: Read full request body and echo it.
+#eval runWithTimeout "04_echo_full_body" 2000 do
+ let raw := "POST /echo HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 11\x0d\nConnection: close\x0d\n\x0d\nhello world".toUTF8
+ let response ← sendRawTimed "04_echo_full_body/send" raw echoBodyHandler
+ assertContains "04_echo_full_body" response "hello world"
+
+-- 05: Read only first chunk and reply (should not deadlock connection).
+#eval runWithTimeout "05_read_first_chunk_only" 2000 do
+ let raw := "POST /first HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 11\x0d\nConnection: close\x0d\n\x0d\nhello world".toUTF8
+ let response ← sendRawTimed "05_read_first_chunk_only/send" raw firstChunkHandler
+ assertStatusPrefix "05_read_first_chunk_only" response "HTTP/1.1 200"
+ assertContains "05_read_first_chunk_only" response "hello world"
+
+-- 06: Stream many response chunks.
+#eval runWithTimeout "06_stream_many_response_chunks" 2000 do
+ let raw := "GET /stream HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let response ← sendRawTimed "06_stream_many_response_chunks/send" raw (streamPiecesHandler 40)
+ assertStatusPrefix "06_stream_many_response_chunks" response "HTTP/1.1 200"
+ assertContains "06_stream_many_response_chunks" response "piece-0;"
+ assertContains "06_stream_many_response_chunks" response "piece-39;"
+
+-- 07: Stream response with known fixed size.
+#eval runWithTimeout "07_stream_known_size" 2000 do
+ let raw := "GET /known HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let response ← sendRawTimed "07_stream_known_size/send" raw (fun _ => do
+ let (outgoing, _incoming) ← Body.mkChannel
+ outgoing.setKnownSize (some (.fixed 8))
+ background do
+ outgoing.send <| Chunk.ofByteArray "abcd".toUTF8
+ outgoing.send <| Chunk.ofByteArray "efgh".toUTF8
+ outgoing.close
+ return Response.ok
+ |>.body outgoing)
+ assertStatusPrefix "07_stream_known_size" response "HTTP/1.1 200"
+ assertContains "07_stream_known_size" response "Content-Length: 8"
+ assertContains "07_stream_known_size" response "abcdefgh"
+
+-- 08: Use interestSelector before sending response data.
+#eval runWithTimeout "08_interest_selector_gating" 2000 do
+ let raw := "GET /interest HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let response ← sendRawTimed "08_interest_selector_gating/send" raw (fun _ => do
+ let (outgoing, _incoming) ← Body.mkChannel
+ background do
+ let interested ← Selectable.one #[
+ .case outgoing.interestSelector pure
+ ]
+ if interested then
+ outgoing.send <| Chunk.ofByteArray "interest-ok".toUTF8
+ outgoing.close
+ return Response.ok
+ |>.body outgoing)
+ assertStatusPrefix "08_interest_selector_gating" response "HTTP/1.1 200"
+ assertContains "08_interest_selector_gating" response "interest-ok"
+
+-- 09: Incomplete sends collapse into one payload.
+#eval runWithTimeout "09_incomplete_send_collapse" 2000 do
+ let raw := "GET /collapse HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let response ← sendRawTimed "09_incomplete_send_collapse/send" raw (fun _ => do
+ let (outgoing, _incoming) ← Body.mkChannel
+ background do
+ outgoing.send ({ data := "hello ".toUTF8, extensions := #[] } : Chunk) (incomplete := true)
+ outgoing.send ({ data := "wor".toUTF8, extensions := #[] } : Chunk) (incomplete := true)
+ outgoing.send ({ data := "ld".toUTF8, extensions := #[] } : Chunk)
+ outgoing.close
+ return Response.ok
+ |>.body outgoing)
+ assertStatusPrefix "09_incomplete_send_collapse" response "HTTP/1.1 200"
+ assertContains "09_incomplete_send_collapse" response "hello world"
+
+-- 10: Pipeline fixed-body POST then GET.
+#eval runWithTimeout "10_pipeline_fixed_then_get" 2000 do
+ let raw := ("POST /one HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\n\x0d\nhello" ++
+ "GET /two HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n").toUTF8
+ let response ← sendRawTimed "10_pipeline_fixed_then_get/send" raw uriHandler
+ assertStatusCount "10_pipeline_fixed_then_get" response 2
+ assertContains "10_pipeline_fixed_then_get" response "/one"
+ assertContains "10_pipeline_fixed_then_get" response "/two"
+
+-- 11: Pipeline chunked-body POST then GET.
+#eval runWithTimeout "11_pipeline_chunked_then_get" 2000 do
+ let raw := ("POST /chunk HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n" ++
+ "GET /two HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n").toUTF8
+ let response ← sendRawTimed "11_pipeline_chunked_then_get/send" raw uriHandler
+ assertStatusCount "11_pipeline_chunked_then_get" response 2
+ assertContains "11_pipeline_chunked_then_get" response "/chunk"
+ assertContains "11_pipeline_chunked_then_get" response "/two"
+
+-- 12: Malformed first request should not loop into second.
+#eval runWithTimeout "12_malformed_closes_connection" 2000 do
+ let raw := ("GET / HTTP/1.1\x0d\nHost: example.com\x0d\nBadHeader value\x0d\n\x0d\n" ++
+ "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n").toUTF8
+ let response ← sendRawTimed "12_malformed_closes_connection/send" raw uriHandler
+ assertStatusPrefix "12_malformed_closes_connection" response "HTTP/1.1 400"
+ assertStatusCount "12_malformed_closes_connection" response 1
+
+-- 13: Client closes while server is streaming response.
+#eval runWithTimeout "13_client_close_while_streaming" 2000 do
+ let raw := "GET /close-stream HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ runClosedClientTimed "13_client_close_while_streaming/run" raw (stressResponseHandler 600)
+
+-- 14: Client closes before sending full body.
+#eval runWithTimeout "14_client_close_mid_body" 2000 do
+ let raw := "POST /mid-body HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 100\x0d\nConnection: close\x0d\n\x0d\nabcde".toUTF8
+ runClosedClientTimed "14_client_close_mid_body/run" raw ignoreHandler
+
+-- 15: Handler throws while request body is present.
+#eval runWithTimeout "15_handler_throw_unread_body" 2000 do
+ let raw := "POST /throw HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let response ← sendRawTimed "15_handler_throw_unread_body/send" raw (fun _ => throw <| IO.userError "boom")
+ assertStatusPrefix "15_handler_throw_unread_body" response "HTTP/1.1 500"
+
+-- 16: Many tiny chunked request chunks ignored by handler.
+#eval runWithTimeout "16_many_tiny_chunked_ignored" 2000 do
+ let body := onesChunked 80
+ let raw := s!"POST /tiny HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n{body}".toUTF8
+ let response ← sendRawTimed "16_many_tiny_chunked_ignored/send" raw ignoreHandler
+ assertStatusPrefix "16_many_tiny_chunked_ignored" response "HTTP/1.1 200"
+
+-- 17: Many tiny chunked request chunks consumed and counted.
+#eval runWithTimeout "17_many_tiny_chunked_consumed" 2000 do
+ let body := onesChunked 25
+ let raw := s!"POST /count HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n{body}".toUTF8
+ let response ← sendRawTimed "17_many_tiny_chunked_consumed/send" raw (fun req => do
+ let mut count := 0
+ for _ in req.body do
+ count := count + 1
+ Response.ok |>.text (toString count))
+ assertStatusPrefix "17_many_tiny_chunked_consumed" response "HTTP/1.1 200"
+ assertEndsWith "17_many_tiny_chunked_consumed" response "25"
+
+ pure ()
+
+-- 18: Stress response streaming with many chunks and active client.
+#eval runWithTimeout "18_stress_streaming_active_client" 2000 do
+ let raw := "GET /stress HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let response ← sendRawTimed "18_stress_streaming_active_client/send" raw (stressResponseHandler 120)
+ assertStatusPrefix "18_stress_streaming_active_client" response "HTTP/1.1 200"
+ assertContains "18_stress_streaming_active_client" response "x0,"
+ assertContains "18_stress_streaming_active_client" response "x119,"
+
+-- 19: Pipeline with large unread first body still processes second request.
+#eval runWithTimeout "19_pipeline_large_unread_then_get" 2000 do
+ let body := String.ofList (List.replicate 5000 'b')
+ let raw := (s!"POST /big HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5000\x0d\n\x0d\n{body}" ++
+ "GET /after HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n").toUTF8
+ let response ← sendRawTimed "19_pipeline_large_unread_then_get/send" raw uriHandler
+ assertStatusCount "19_pipeline_large_unread_then_get" response 2
+ assertContains "19_pipeline_large_unread_then_get" response "/big"
+ assertContains "19_pipeline_large_unread_then_get" response "/after"
+
+-- 20: Triple pipeline mixed body styles.
+#eval runWithTimeout "20_triple_pipeline_mixed" 2000 do
+ let raw := ("POST /a HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 4\x0d\n\x0d\ndata" ++
+ "POST /b HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\n3\x0d\nhey\x0d\n0\x0d\n\x0d\n" ++
+ "GET /c HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n").toUTF8
+ let response ← sendRawTimed "20_triple_pipeline_mixed/send" raw uriHandler
+ assertStatusCount "20_triple_pipeline_mixed" response 3
+ assertContains "20_triple_pipeline_mixed" response "/a"
+ assertContains "20_triple_pipeline_mixed" response "/b"
+ assertContains "20_triple_pipeline_mixed" response "/c"
+
+-- 21: Slow/incomplete active body transfer must time out (no connection pinning).
+#eval runWithTimeout "21_incomplete_slow_post_times_out" 2000 do
+ let raw := "POST /slow HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 100\x0d\nConnection: close\x0d\n\x0d\nabcde".toUTF8
+ let response ← sendRawTimed
+ "21_incomplete_slow_post_times_out/send"
+ raw
+ (fun req => do
+ let _s : String ← req.body.readAll
+ Response.ok |>.text "unreachable")
+ (config := { lingeringTimeout := 200, generateDate := false })
+ assertStatusPrefix "21_incomplete_slow_post_times_out" response "HTTP/1.1 408"
+
+-- 22: Keep-alive + unknown-size stream flushes once first chunk is available.
+#eval runWithTimeout "22_keepalive_unknown_size_flushes_early" 3000 do
+ Async.block do
+ let (client, server) ← Mock.new
+ let handler : TestHandler := fun _ => do
+ let (outgoing, _incoming) ← Body.mkChannel
+ background do
+ outgoing.send <| Chunk.ofByteArray "aaa".toUTF8
+ let sleep ← Sleep.mk 300
+ sleep.wait
+ outgoing.send <| Chunk.ofByteArray "bbb".toUTF8
+ outgoing.close
+ return Response.ok
+ |>.body outgoing
+
+ background <| (Std.Http.Server.serveConnection server handler {
+ lingeringTimeout := 800
+ keepAliveTimeout := ⟨1500, by decide⟩
+ generateDate := false
+ }).run
+
+ client.send "GET /stream HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n".toUTF8
+
+ let mut early : Option ByteArray := none
+ for _ in [0:5] do
+ if early.isNone then
+ let sleep ← Sleep.mk 40
+ sleep.wait
+ early ← client.tryRecv?
+
+ let earlyBytes := early.getD ByteArray.empty
+ if earlyBytes.isEmpty then
+ throw <| IO.userError "Test '22_keepalive_unknown_size_flushes_early' failed:\nExpected early streamed bytes before producer EOF"
+
+ assertContains "22_keepalive_unknown_size_flushes_early header" earlyBytes "Transfer-Encoding: chunked"
+ assertContains "22_keepalive_unknown_size_flushes_early first chunk" earlyBytes "aaa"
+ assertNotContains "22_keepalive_unknown_size_flushes_early no second chunk yet" earlyBytes "bbb"
+
+ let sleep ← Sleep.mk 420
+ sleep.wait
+ let later := (← client.tryRecv?).getD ByteArray.empty
+ assertContains "22_keepalive_unknown_size_flushes_early second chunk later" later "bbb"
+
+ client.close
diff --git a/tests/lean/run/async_http_keepalive.lean b/tests/lean/run/async_http_keepalive.lean
new file mode 100644
index 000000000000..3f8a0cc89907
--- /dev/null
+++ b/tests/lean/run/async_http_keepalive.lean
@@ -0,0 +1,224 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+
+def sendRaw
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 3000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+
+def runPipelined
+ (raw : String)
+ (readBody : Bool)
+ (config : Config := { lingeringTimeout := 1000, generateDate := false }) : IO (ByteArray × Array String) := Async.block do
+ let (client, server) ← Mock.new
+ let seenRef ← IO.mkRef (#[] : Array String)
+
+ let handler : TestHandler := fun req => do
+ let uri := toString req.head.uri
+ seenRef.modify (·.push uri)
+
+ let body ←
+ if readBody then
+ req.body.readAll
+ else
+ pure ""
+
+ Response.ok |>.text s!"{uri}:{body}"
+
+ client.send raw.toUTF8
+ client.getSendChan.close
+
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+
+ let response ← client.recv?
+ let seen ← seenRef.get
+ pure (response.getD .empty, seen)
+
+
+def assertContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.contains needle do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected to contain {needle.quote}\nGot:\n{text.quote}"
+
+
+def assertNotContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ if text.contains needle then
+ throw <| IO.userError s!"Test '{name}' failed:\nDid not expect {needle.quote}\nGot:\n{text.quote}"
+
+
+def countOccurrences (s : String) (needle : String) : Nat :=
+ if needle.isEmpty then
+ 0
+ else
+ (s.splitOn needle).length - 1
+
+
+def assertStatusCount (name : String) (response : ByteArray) (expected : Nat) : IO Unit := do
+ let text := String.fromUTF8! response
+ let got := countOccurrences text "HTTP/1.1 "
+ if got != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {expected} responses, got {got}\n{text.quote}"
+
+
+def assertSeenCount (name : String) (seen : Array String) (expected : Nat) : IO Unit := do
+ if seen.size != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {expected} handler calls, got {seen.size}: {seen}"
+
+
+-- Two sequential requests on the same HTTP/1.1 connection.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let req1 := "GET /first HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n"
+ let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let response ← sendRaw client server (req1 ++ req2).toUTF8 (fun req =>
+ Response.ok |>.text (toString req.head.uri))
+
+ assertStatusCount "Two keep-alive responses" response 2
+ assertContains "Two keep-alive first" response "/first"
+ assertContains "Two keep-alive second" response "/second"
+
+-- Connection: close on first request blocks pipelined second request.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let req1 := "GET /first HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let response ← sendRaw client server (req1 ++ req2).toUTF8 (fun req =>
+ Response.ok |>.text (toString req.head.uri))
+
+ assertStatusCount "Connection close response count" response 1
+ assertContains "Connection close first served" response "/first"
+ assertNotContains "Connection close second blocked" response "/second"
+
+-- Disabling keep-alive via config forces one response.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let req1 := "GET /1 HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n"
+ let req2 := "GET /2 HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let response ← sendRaw client server (req1 ++ req2).toUTF8
+ (fun req => Response.ok |>.text (toString req.head.uri))
+ (config := { lingeringTimeout := 3000, enableKeepAlive := false, generateDate := false })
+
+ assertStatusCount "Keep-alive disabled response count" response 1
+ assertContains "Keep-alive disabled first served" response "/1"
+ assertNotContains "Keep-alive disabled second blocked" response "/2"
+
+-- maxRequests cap enforces hard limit on responses per connection.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let req0 := "GET /0 HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n"
+ let req1 := "GET /1 HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n"
+ let req2 := "GET /2 HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let response ← sendRaw client server (req0 ++ req1 ++ req2).toUTF8
+ (fun req => Response.ok |>.text (toString req.head.uri))
+ (config := { lingeringTimeout := 3000, maxRequests := 2, generateDate := false })
+
+ assertStatusCount "maxRequests response count" response 2
+ assertContains "maxRequests /0 served" response "/0"
+ assertContains "maxRequests /1 served" response "/1"
+ assertNotContains "maxRequests /2 blocked" response "/2"
+
+-- Handler that ignores a fixed-size body still allows next keep-alive request.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let req1 := "POST /ignore HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\n\x0d\nhello"
+ let req2 := "GET /after HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let response ← sendRaw client server (req1 ++ req2).toUTF8 (fun req =>
+ Response.ok |>.text (toString req.head.uri))
+
+ assertStatusCount "Unread CL body keep-alive responses" response 2
+ assertContains "Unread CL body first" response "/ignore"
+ assertContains "Unread CL body second" response "/after"
+
+-- Handler that ignores chunked body still allows next keep-alive request.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let req1 := "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n"
+ let req2 := "GET /next HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let response ← sendRaw client server (req1 ++ req2).toUTF8 (fun req =>
+ Response.ok |>.text (toString req.head.uri))
+
+ assertStatusCount "Unread chunked body keep-alive responses" response 2
+ assertContains "Unread chunked first" response "/chunked"
+ assertContains "Unread chunked second" response "/next"
+
+-- Exact first Content-Length allows pipelined second request.
+#eval show IO _ from do
+ let req1 := "POST /first HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 3\x0d\n\x0d\nabc"
+ let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let (response, seen) ← runPipelined (req1 ++ req2) true
+
+ assertStatusCount "Exact CL pipelined responses" response 2
+ assertContains "Exact CL first" response "/first"
+ assertContains "Exact CL second" response "/second"
+ assertSeenCount "Exact CL seen count" seen 2
+
+-- Incomplete first Content-Length blocks pipelined second request.
+#eval show IO _ from do
+ let req1 := "POST /first HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 10\x0d\n\x0d\nabc"
+ let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let (response, seen) ← runPipelined (req1 ++ req2) true
+
+ assertContains "Incomplete CL first served" response "/first"
+ assertNotContains "Incomplete CL second blocked" response "/second"
+ assertSeenCount "Incomplete CL seen count" seen 1
+
+-- Incomplete first chunked body blocks pipelined second request.
+#eval show IO _ from do
+ let req1 := "POST /chunked-first HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\nF\x0d\nhel"
+ let req2 := "GET /second HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let (response, seen) ← runPipelined (req1 ++ req2) true
+
+ assertNotContains "Incomplete chunked second blocked" response "/second"
+ if seen.contains "/second" then
+ throw <| IO.userError s!"Test 'Incomplete chunked seen list' failed: {seen}"
+
+-- Content-Length: 0 on first request allows immediate second request.
+#eval show IO _ from do
+ let req1 := "POST /empty HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 0\x0d\n\x0d\n"
+ let req2 := "GET /tail HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let (response, seen) ← runPipelined (req1 ++ req2) true
+
+ assertStatusCount "CL=0 pipelined responses" response 2
+ assertContains "CL=0 first" response "/empty"
+ assertContains "CL=0 second" response "/tail"
+ assertSeenCount "CL=0 seen count" seen 2
+
+-- Complete chunked first request allows second request.
+#eval show IO _ from do
+ let req1 := "POST /chunked HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n"
+ let req2 := "GET /tail HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n"
+ let (response, seen) ← runPipelined (req1 ++ req2) true
+
+ assertStatusCount "Complete chunked pipelined responses" response 2
+ assertContains "Complete chunked first" response "/chunked"
+ assertContains "Complete chunked second" response "/tail"
+ assertSeenCount "Complete chunked seen count" seen 2
diff --git a/tests/lean/run/async_http_malformed.lean b/tests/lean/run/async_http_malformed.lean
new file mode 100644
index 000000000000..d1e70eec8d55
--- /dev/null
+++ b/tests/lean/run/async_http_malformed.lean
@@ -0,0 +1,501 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+
+def sendRaw
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 1000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+
+def sendRawAndClose
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 1000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ client.getSendChan.close
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+
+def assertStatus (name : String) (response : ByteArray) (status : String) : IO Unit := do
+ let responseStr := String.fromUTF8! response
+ unless responseStr.startsWith status do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected status: {status}\nGot:\n{responseStr.quote}"
+
+
+def assertExact (name : String) (response : ByteArray) (expected : String) : IO Unit := do
+ let responseStr := String.fromUTF8! response
+ if responseStr != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected:\n{expected.quote}\nGot:\n{responseStr.quote}"
+
+
+def assertContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let responseStr := String.fromUTF8! response
+ unless responseStr.contains needle do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected to contain: {needle.quote}\nGot:\n{responseStr.quote}"
+
+
+def headerSection (response : ByteArray) : String :=
+ (String.fromUTF8! response).splitOn "\x0d\n\x0d\n" |>.headD ""
+
+
+def okHandler : TestHandler :=
+ fun _ => Response.ok |>.text "ok"
+
+
+def bad400 : String :=
+ "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def bad505 : String :=
+ "HTTP/1.1 505 HTTP Version Not Supported\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+
+def ok200 : String :=
+ "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 2\x0d\n\x0d\nok"
+
+
+def ok200Head : String :=
+ "HTTP/1.1 200 OK\x0d\nContent-Type: text/plain; charset=utf-8\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 2\x0d\n\x0d\n"
+
+
+def notImplemented : String :=
+ "HTTP/1.1 501 Not Implemented\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+
+-- Client-mode response parsing regressions.
+#eval show IO _ from do
+ let machineA : Protocol.H1.Machine .sending := { config := {} }
+ let rawA := "HTTP/1.1 200 OK\x0d\nContent-Length: 0\x0d\nConnection: close\x0d\n\x0d\n"
+ let (machineA, stepA) := (machineA.feed rawA.toUTF8).step
+ let failedA := stepA.events.any fun
+ | .failed _ => true
+ | _ => false
+ if failedA then
+ throw <| IO.userError s!"Test 'Client mode parses response status-line with headers' failed:\nUnexpected failure events: {repr stepA.events}"
+
+ let endedA := stepA.events.any fun
+ | .endHeaders _ => true
+ | _ => false
+ unless endedA do
+ throw <| IO.userError s!"Test 'Client mode parses response status-line with headers' failed:\nMissing endHeaders event: {repr stepA.events}"
+
+ unless machineA.reader.messageHead.status == .ok do
+ throw <| IO.userError s!"Test 'Client mode parses response status-line with headers' failed:\nUnexpected status: {repr machineA.reader.messageHead.status}"
+
+ unless machineA.reader.messageHead.headers.hasEntry Header.Name.contentLength (Header.Value.ofString! "0") do
+ throw <| IO.userError s!"Test 'Client mode parses response status-line with headers' failed:\nMissing Content-Length header in parsed response"
+
+ let machineB : Protocol.H1.Machine .sending := { config := {} }
+ let rawB := "HTTP/1.1 204 No Content\x0d\n\x0d\n"
+ let (_machineB, stepB) := (machineB.feed rawB.toUTF8).step
+ let failedB := stepB.events.any fun
+ | .failed _ => true
+ | _ => false
+ if failedB then
+ throw <| IO.userError s!"Test 'Client mode parses headerless response status-line' failed:\nUnexpected failure events: {repr stepB.events}"
+
+ let needMoreB := stepB.events.any fun
+ | .needMoreData _ => true
+ | _ => false
+ if needMoreB then
+ throw <| IO.userError s!"Test 'Client mode parses headerless response status-line' failed:\nUnexpected needMoreData event: {repr stepB.events}"
+
+ let endedB := stepB.events.any fun
+ | .endHeaders _ => true
+ | _ => false
+ unless endedB do
+ throw <| IO.userError s!"Test 'Client mode parses headerless response status-line' failed:\nMissing endHeaders event: {repr stepB.events}"
+
+ let machineC : Protocol.H1.Machine .sending := { config := {} }
+ let rawC := "HTTP/1.1 204 No Content\x0d\nContent-Length: 5\x0d\n\x0d\nHELLO"
+ let (machineC, stepC) := (machineC.feed rawC.toUTF8).step
+ let failedC := stepC.events.any fun
+ | .failed _ => true
+ | _ => false
+ if failedC then
+ throw <| IO.userError s!"Test 'Client mode ignores body framing on 204' failed:\nUnexpected failure events: {repr stepC.events}"
+
+ match machineC.reader.state with
+ | .readBody (.fixed 0) =>
+ pure ()
+ | .complete =>
+ pure ()
+ | .closed =>
+ pure ()
+ | _ =>
+ throw <| IO.userError s!"Test 'Client mode ignores body framing on 204' failed:\nUnexpected body-reading state: {repr machineC.reader.state}"
+
+ unless machineC.reader.input.remainingBytes == 5 do
+ throw <| IO.userError s!"Test 'Client mode ignores body framing on 204' failed:\nExpected 5 unread bytes, got {machineC.reader.input.remainingBytes}"
+
+-- Outgoing response framing regressions for bodyless statuses.
+#eval show IO _ from do
+ let request := "GET /cache HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let machine0 : Protocol.H1.Machine .receiving := { config := {} }
+ let (machine1, _step1) := (machine0.feed request).step
+
+ let headers304 := Headers.empty.insert Header.Name.contentLength (Header.Value.ofString! "5")
+ let machine304 := machine1.send ({ status := .notModified, headers := headers304 } : Response.Head)
+ let (_machine304, step304) := machine304.step
+ let text304 := String.fromUTF8! step304.output.toByteArray
+ unless text304.contains "HTTP/1.1 304 Not Modified" do
+ throw <| IO.userError s!"Test '304 preserves explicit Content-Length' failed:\n{text304.quote}"
+ unless text304.contains "Content-Length: 5" do
+ throw <| IO.userError s!"Test '304 preserves explicit Content-Length' failed:\n{text304.quote}"
+ if text304.contains "Content-Length: 0" then
+ throw <| IO.userError s!"Test '304 preserves explicit Content-Length' failed:\nUnexpected rewritten Content-Length: {text304.quote}"
+
+ let headers204 := Headers.empty
+ |>.insert Header.Name.contentLength (Header.Value.ofString! "9")
+ let machine204 := machine1.send ({ status := .noContent, headers := headers204 } : Response.Head)
+ let (_machine204, step204) := machine204.step
+ let text204 := String.fromUTF8! step204.output.toByteArray
+ unless step204.output.size > 0 do
+ throw <| IO.userError "Test '204 strips framing headers' failed:\nExpected serialized response output"
+ unless text204.contains "HTTP/1.1 204 No Content" do
+ throw <| IO.userError s!"Test '204 strips framing headers' failed:\n{text204.quote}"
+ if text204.contains "Content-Length:" ∨ text204.contains "Transfer-Encoding:" then
+ throw <| IO.userError s!"Test '204 strips framing headers' failed:\nUnexpected framing headers:\n{text204.quote}"
+
+-- Host header rules.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let missingHost := "GET / HTTP/1.1\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA missingHost okHandler
+ assertExact "Missing Host header" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let emptyHost := "GET / HTTP/1.1\x0d\nHost: \x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB emptyHost okHandler
+ -- RFC 9110 §7.2: for origin-form URIs (no authority), an empty Host field value is valid.
+ assertExact "Empty Host header allowed" responseB ok200
+
+ let (clientC, serverC) ← Mock.new
+ let multiHost := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nHost: other.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC multiHost okHandler
+ assertExact "Multiple Host headers" responseC bad400
+
+ let (clientD, serverD) ← Mock.new
+ let absoluteIgnoresHost := "GET http://good.example/path HTTP/1.1\x0d\nHost: good.example\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD absoluteIgnoresHost okHandler
+ assertExact "Absolute-form authority takes precedence over Host" responseD ok200
+
+-- HTTP version handling.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let rawA := "GET / HTTP/2.0\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA okHandler
+ assertExact "HTTP/2.0 rejected" responseA bad505
+
+ let (clientB, serverB) ← Mock.new
+ let rawB := "GET / HTTP/1.0\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB okHandler
+ assertExact "HTTP/1.0 rejected" responseB bad505
+
+-- Request-line parsing failures.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let missingVersion := "GET /\x0d\nHost: example.com\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA missingVersion okHandler
+ assertExact "Missing version in request-line" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let missingUri := "GET HTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB missingUri okHandler
+ assertExact "Missing URI in request-line" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let extraSpaces := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC extraSpaces okHandler
+ assertExact "Extra spaces in request-line" responseC bad400
+
+ let (clientD, serverD) ← Mock.new
+ let emptyLine := "\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD emptyLine okHandler
+ assertExact "Empty request-line" responseD ""
+
+ let (clientE, serverE) ← Mock.new
+ let whitespaceOnly := " \x0d\n\x0d\n".toUTF8
+ let responseE ← sendRaw clientE serverE whitespaceOnly okHandler
+ assertExact "Whitespace-only request-line" responseE bad400
+
+ let (clientF, serverF) ← Mock.new
+ let noSpaces := "GETHTTP/1.1\x0d\nHost: example.com\x0d\n\x0d\n".toUTF8
+ let responseF ← sendRaw clientF serverF noSpaces okHandler
+ assertExact "No spaces in request-line" responseF bad400
+
+ let (clientG, serverG) ← Mock.new
+ let leadingCRLF := "\x0d\nGET / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseG ← sendRaw clientG serverG leadingCRLF okHandler
+ assertExact "Leading CRLF before request-line" responseG ok200
+
+ let (clientH, serverH) ← Mock.new
+ let garbageAfterVersion := "GET / HTTP/1.1 xxxxxx\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseH ← sendRaw clientH serverH garbageAfterVersion okHandler
+ assertExact "Garbage after request-line version" responseH bad400
+
+-- Method rules.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let invalidMethod := "FOOBAR / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA invalidMethod okHandler
+ assertExact "Unknown method returns 200" responseA ok200
+
+ let (clientB, serverB) ← Mock.new
+ let lowercaseMethod := "get / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB lowercaseMethod okHandler
+ assertExact "Lowercase extension method returns 501" responseB notImplemented
+
+ let (clientC, serverC) ← Mock.new
+ let nonAsciiMethod := "GÉT / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC nonAsciiMethod okHandler
+ assertExact "Non-ASCII method rejected" responseC bad400
+
+ let (clientD, serverD) ← Mock.new
+ let longMethod := String.ofList (List.replicate 20 'G')
+ let rawD := s!"{longMethod} / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD rawD okHandler
+ assertExact "Long extension method returns 200" responseD ok200
+
+ let (clientE, serverE) ← Mock.new
+ let tokenMethod := "X-CUSTOM / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseE ← sendRaw clientE serverE tokenMethod okHandler
+ assertExact "Token method with hyphen forwarded to handler" responseE ok200
+
+-- HEAD framing and authority-form rules.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let headReq := "HEAD / HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA headReq okHandler
+ assertExact "HEAD omits body bytes" responseA ok200Head
+
+ let (clientB, serverB) ← Mock.new
+ let badAuthority := "GET example.com:443 HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB badAuthority okHandler
+ assertExact "GET authority-form rejected" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let okAuthority := "CONNECT example.com:443 HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC okAuthority okHandler
+ assertExact "CONNECT authority-form accepted" responseC ok200
+
+ let (clientD, serverD) ← Mock.new
+ let getAsterisk := "GET * HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD getAsterisk okHandler
+ assertExact "Asterisk-form rejected for non-OPTIONS" responseD bad400
+
+ let (clientE, serverE) ← Mock.new
+ let optionsAsterisk := "OPTIONS * HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseE ← sendRaw clientE serverE optionsAsterisk okHandler
+ assertExact "Asterisk-form accepted for OPTIONS" responseE ok200
+
+-- h11-inspired: GET and HEAD should use the same framing headers.
+#eval show IO _ from do
+ let handler : TestHandler := fun _ => Response.ok |>.text "hello"
+
+ let (clientA, serverA) ← Mock.new
+ let getReq := "GET /frame HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let getResponse ← sendRaw clientA serverA getReq handler
+
+ let (clientB, serverB) ← Mock.new
+ let headReq := "HEAD /frame HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let headResponse ← sendRaw clientB serverB headReq handler
+
+ let getHeaders := headerSection getResponse
+ let headHeaders := headerSection headResponse
+ if getHeaders != headHeaders then
+ throw <| IO.userError s!"Test 'HEAD framing headers parity' failed:\nGET headers:\n{getHeaders.quote}\nHEAD headers:\n{headHeaders.quote}"
+
+ assertContains "GET framing body present" getResponse "hello"
+ let headText := String.fromUTF8! headResponse
+ if headText.contains "hello" then
+ throw <| IO.userError s!"Test 'HEAD framing body omitted' failed:\n{headText.quote}"
+
+-- Header syntax and byte-level validation.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let noColon := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nBadHeader value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA noColon okHandler
+ assertExact "Header without colon" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let obsFold := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\n X-Bad: folded\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB obsFold okHandler
+ assertExact "Leading whitespace header" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let beforeName := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nX-Bad".toUTF8
+ let afterName := "Header: value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC (beforeName ++ ByteArray.mk #[0] ++ afterName) okHandler
+ assertExact "NUL in header name" responseC bad400
+
+ let (clientD, serverD) ← Mock.new
+ let beforeValue := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nX-Header: bad".toUTF8
+ let afterValue := "value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD (beforeValue ++ ByteArray.mk #[0] ++ afterValue) okHandler
+ assertExact "NUL in header value" responseD bad400
+
+ let (clientE, serverE) ← Mock.new
+ let beforeCtrl := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nX-Header: bad".toUTF8
+ let afterCtrl := "value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseE ← sendRaw clientE serverE (beforeCtrl ++ ByteArray.mk #[0x01] ++ afterCtrl) okHandler
+ assertExact "Control char in header value" responseE bad400
+
+ let (clientF, serverF) ← Mock.new
+ let spaceInName := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nBad Header: value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseF ← sendRaw clientF serverF spaceInName okHandler
+ assertExact "Space in header name" responseF bad400
+
+-- Lenient-but-supported parsing behavior.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let bareLF := "GET / HTTP/1.1\nHost: example.com\nConnection: close\n\n".toUTF8
+ let responseA ← sendRaw clientA serverA bareLF okHandler
+ assertExact "Bare LF line endings accepted" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let splitHeaders := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nX-Inject: value\x0d\nEvil: injected\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB splitHeaders okHandler
+ assertExact "CRLF split into two headers" responseB ok200
+
+ let (clientC, serverC) ← Mock.new
+ let tabValue := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nX-Tab: value\twith\ttabs\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC tabValue okHandler
+ assertExact "Tab in header value accepted" responseC ok200
+
+ let (clientD, serverD) ← Mock.new
+ let absoluteUri := "GET http://example.com/path HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD absoluteUri okHandler
+ assertExact "Absolute-form URI accepted" responseD ok200
+
+ let (clientE, serverE) ← Mock.new
+ let colonValue := "GET / HTTP/1.1\x0d\nHost: example.com\x0d\nBad:Name: value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseE ← sendRaw clientE serverE colonValue okHandler
+ assertExact "Additional colon remains in value" responseE ok200
+
+-- Content-Length validation.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let nonNumeric := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: abc\x0d\nConnection: close\x0d\n\x0d\nbody".toUTF8
+ let responseA ← sendRaw clientA serverA nonNumeric okHandler
+ assertExact "Non-numeric Content-Length" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let negative := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: -1\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB negative okHandler
+ assertExact "Negative Content-Length" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let duplicateCl := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nContent-Length: 5\x0d\nContent-Length: 10\x0d\nConnection: close\x0d\n\x0d\nhello".toUTF8
+ let responseC ← sendRaw clientC serverC duplicateCl okHandler
+ assertExact "Duplicate Content-Length mismatch" responseC bad400
+
+-- Transfer-Encoding normalization.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let mixedCase := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: Chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA mixedCase (fun req => do
+ let body : String ← req.body.readAll
+ Response.ok |>.text body)
+ assertStatus "Mixed-case chunked accepted" responseA "HTTP/1.1 200"
+ assertContains "Mixed-case chunked body" responseA "hello"
+
+ let (clientB, serverB) ← Mock.new
+ let teOWS := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked \x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB teOWS (fun req => do
+ let body : String ← req.body.readAll
+ Response.ok |>.text body)
+ assertStatus "Transfer-Encoding trailing OWS accepted" responseB "HTTP/1.1 200"
+ assertContains "Transfer-Encoding trailing OWS body" responseB "hello"
+
+ let (clientC, serverC) ← Mock.new
+ let doubleChunked := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC doubleChunked okHandler
+ assertExact "Double chunked rejected" responseC bad400
+
+ let (clientD, serverD) ← Mock.new
+ let unsupportedTe := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: gzip, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD unsupportedTe (fun req => do
+ let seenTe := match req.head.headers.getAll? Header.Name.transferEncoding with
+ | some values => String.intercalate "|" (values.map (·.value) |>.toList)
+ | none => ""
+ Response.ok |>.text seenTe)
+ assertStatus "Chunked transfer-coding chain accepted" responseD "HTTP/1.1 200"
+ assertContains "Transfer-coding chain is visible to handler" responseD "gzip, chunked"
+
+-- Size limits.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let longName := String.ofList (List.replicate 257 'X')
+ let rawA := s!"GET / HTTP/1.1\x0d\nHost: example.com\x0d\n{longName}: value\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA okHandler
+ assertExact "Header name too long" responseA bad400
+
+ let cfg : Config := {
+ lingeringTimeout := 1000
+ generateDate := false
+ maxStartLineLength := 16384
+ }
+
+ let (clientB, serverB) ← Mock.new
+ let segment := String.ofList (List.replicate 255 'a')
+ let maxUri := "/" ++ String.intercalate "/" (List.replicate 32 segment)
+ let rawB := s!"GET {maxUri} HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB okHandler (config := cfg)
+ assertExact "URI at limit accepted" responseB ok200
+
+ let (clientC, serverC) ← Mock.new
+ let longUri := maxUri ++ "/x"
+ let rawC := s!"GET {longUri} HTTP/1.1\x0d\nHost: example.com\x0d\nConnection: close\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC rawC okHandler (config := cfg)
+ assertStatus "URI too long returns 414" responseC "HTTP/1.1 414"
+
+-- Empty connection closes silently (no response bytes).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let response ← sendRawAndClose client server ByteArray.empty okHandler
+ assert! response.size == 0
+
+-- h11-inspired: early invalid-byte detection before CRLF.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let responseA ← sendRawAndClose clientA serverA (ByteArray.mk #[0x00]) okHandler
+ assertExact "Early invalid NUL" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let responseB ← sendRawAndClose clientB serverB (ByteArray.mk #[0x20]) okHandler
+ assertExact "Early invalid SP" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let responseC ← sendRawAndClose clientC serverC (ByteArray.mk #[0x16, 0x03, 0x01, 0x00, 0xa5]) okHandler
+ assertExact "Early invalid TLS prefix" responseC bad400
diff --git a/tests/lean/run/async_http_te_security.lean b/tests/lean/run/async_http_te_security.lean
new file mode 100644
index 000000000000..1291c8bdf4da
--- /dev/null
+++ b/tests/lean/run/async_http_te_security.lean
@@ -0,0 +1,184 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+
+def sendRaw
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 1000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+
+def assertStatus (name : String) (response : ByteArray) (status : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.startsWith status do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {status}\nGot:\n{text.quote}"
+
+
+def assertExact (name : String) (response : ByteArray) (expected : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ if text != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected:\n{expected.quote}\nGot:\n{text.quote}"
+
+
+def assertContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.contains needle do
+ throw <| IO.userError s!"Test '{name}' failed:\nMissing {needle.quote}\nGot:\n{text.quote}"
+
+
+def echoHandler : TestHandler :=
+ fun req => do
+ let body : String ← req.body.readAll
+ Response.ok |>.text body
+
+def okHandler : TestHandler :=
+ fun _ => Response.ok |>.text "ok"
+
+def bad400 : String :=
+ "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+def bad501 : String :=
+ "HTTP/1.1 501 Not Implemented\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+-- Baseline: normal chunked request is accepted and body is delivered.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "TE: chunked baseline" response "HTTP/1.1 200"
+ assertContains "TE: chunked body delivered" response "hello"
+
+
+-- TE: gzip alone (chunked not last) → 400.
+-- The server can only frame bodies with chunked; an unknown-only coding has no supported framing.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: gzip\x0d\nConnection: close\x0d\n\x0d\nbody".toUTF8
+ let response ← sendRaw client server raw okHandler
+ assertExact "TE: gzip alone → 400" response bad400
+
+
+-- TE: deflate alone → 400 (chunked not last).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: deflate\x0d\nConnection: close\x0d\n\x0d\nbody".toUTF8
+ let response ← sendRaw client server raw okHandler
+ assertExact "TE: deflate alone → 400" response bad400
+
+
+-- TE: identity alone → 400 (chunked not last).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: identity\x0d\nConnection: close\x0d\n\x0d\nbody".toUTF8
+ let response ← sendRaw client server raw okHandler
+ assertExact "TE: identity alone → 400" response bad400
+
+
+-- TE: chunked, gzip → 400. Chunked is not last; Validate rejects this.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked, gzip\x0d\nConnection: close\x0d\n\x0d\nbody".toUTF8
+ let response ← sendRaw client server raw okHandler
+ assertExact "TE: chunked not last → 400" response bad400
+
+
+-- TE: gzip, chunked → 200. Unknown coding before chunked is accepted; body is framed as chunked.
+-- The server reads the raw chunked bytes without applying the gzip layer.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: gzip, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "TE: gzip, chunked → 200" response "HTTP/1.1 200"
+ assertContains "TE: gzip, chunked body delivered" response "hello"
+
+
+-- TE: br, chunked → 200. Same as above with a different preceding coding.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: br, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "TE: br, chunked → 200" response "HTTP/1.1 200"
+
+
+-- TE + Content-Length → 400 (request smuggling prevention, RFC 9112 §6.1).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nContent-Length: 5\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw okHandler
+ assertExact "TE + Content-Length → 400 (smuggling)" response bad400
+
+
+-- TE: chunked, chunked → 400 (duplicate chunked, Validate rejects).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked, chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw okHandler
+ assertExact "TE: chunked, chunked → 400" response bad400
+
+
+-- Mixed case: Chunked (capital C) is accepted (codings are lowercased when parsed).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: Chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "TE: Chunked (mixed case) → 200" response "HTTP/1.1 200"
+ assertContains "TE: Chunked body delivered" response "hello"
+
+
+-- NUL byte inside TE value → 400 (non-token character).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let before := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunk".toUTF8
+ let after := "ed\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server (before ++ ByteArray.mk #[0x00] ++ after) okHandler
+ assertExact "NUL in TE value → 400" response bad400
+
+
+-- Control character (0x01) inside TE value → 400.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let before := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunk".toUTF8
+ let after := "ed\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server (before ++ ByteArray.mk #[0x01] ++ after) okHandler
+ assertExact "Control char in TE value → 400" response bad400
+
+
+-- Empty TE value → 400 (empty coding list is invalid per TransferEncoding.Validate).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: \x0d\nConnection: close\x0d\n\x0d\nbody".toUTF8
+ let response ← sendRaw client server raw okHandler
+ assertStatus "TE: empty value → error" response "HTTP/1.1 4"
+
+
+-- TE: chunked with trailing OWS is accepted (OWS is stripped before parsing).
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked \x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw echoHandler
+ assertStatus "TE: chunked with trailing OWS → 200" response "HTTP/1.1 200"
diff --git a/tests/lean/run/async_http_trailers.lean b/tests/lean/run/async_http_trailers.lean
new file mode 100644
index 000000000000..94a0599c8cfb
--- /dev/null
+++ b/tests/lean/run/async_http_trailers.lean
@@ -0,0 +1,282 @@
+import Std.Internal.Http
+import Std.Internal.Async
+
+open Std.Internal.IO Async
+open Std Http
+open Std.Http.Internal
+
+abbrev TestHandler := Request Body.Incoming → ContextAsync (Response Body.AnyBody)
+
+instance : Std.Http.Server.Handler TestHandler where
+ onRequest handler request := handler request
+
+instance : Coe (ContextAsync (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+instance : Coe (Async (Response Body.Incoming)) (ContextAsync (Response Body.AnyBody)) where
+ coe action := do
+ let response ← action
+ pure { response with body := Body.Internal.incomingToOutgoing response.body }
+
+def sendRaw
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 3000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+
+def sendRawAndClose
+ (client : Mock.Client)
+ (server : Mock.Server)
+ (raw : ByteArray)
+ (handler : TestHandler)
+ (config : Config := { lingeringTimeout := 1000, generateDate := false }) : IO ByteArray := Async.block do
+ client.send raw
+ client.close
+ Std.Http.Server.serveConnection server handler config
+ |>.run
+ let res ← client.recv?
+ pure <| res.getD .empty
+
+
+def assertStatus (name : String) (response : ByteArray) (status : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.startsWith status do
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected {status}\nGot:\n{text.quote}"
+
+
+def assertContains (name : String) (response : ByteArray) (needle : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ unless text.contains needle do
+ throw <| IO.userError s!"Test '{name}' failed:\nMissing {needle.quote}\nGot:\n{text.quote}"
+
+
+def assertExact (name : String) (response : ByteArray) (expected : String) : IO Unit := do
+ let text := String.fromUTF8! response
+ if text != expected then
+ throw <| IO.userError s!"Test '{name}' failed:\nExpected:\n{expected.quote}\nGot:\n{text.quote}"
+
+def bodyHandler : TestHandler :=
+ fun req => do
+ let body : String ← req.body.readAll
+ Response.ok |>.text body
+
+def bad400 : String :=
+ "HTTP/1.1 400 Bad Request\x0d\nServer: LeanHTTP/1.1\x0d\nConnection: close\x0d\nContent-Length: 0\x0d\n\x0d\n"
+
+-- Chunked body without trailers.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw bodyHandler
+ assertStatus "Chunked no trailers" response "HTTP/1.1 200"
+ assertContains "Chunked no trailers body" response "hello"
+
+-- Single trailer header.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nChecksum: abc123\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw bodyHandler
+ assertStatus "Single trailer" response "HTTP/1.1 200"
+ assertContains "Single trailer body" response "hello"
+
+-- Multiple trailer headers.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nChecksum: abc123\x0d\nExpires: Thu, 01 Dec 1994 16:00:00 GMT\x0d\nX-Custom: value\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw bodyHandler
+ assertStatus "Multiple trailers" response "HTTP/1.1 200"
+ assertContains "Multiple trailers body" response "hello"
+
+-- Terminal chunk extensions can precede trailers.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0;ext=val\x0d\nX-Trailer: yes\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw bodyHandler
+ assertStatus "Terminal chunk extensions + trailers" response "HTTP/1.1 200"
+ assertContains "Terminal chunk extensions + trailers body" response "hello"
+
+-- Trailer name and value limits.
+#eval show IO _ from do
+ let exactName := String.ofList (List.replicate 256 'X')
+ let longName := String.ofList (List.replicate 257 'X')
+ let exactValue := String.ofList (List.replicate 8192 'v')
+ let longValue := String.ofList (List.replicate 8193 'v')
+
+ let (clientA, serverA) ← Mock.new
+ let rawA := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\n{exactName}: value\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA bodyHandler
+ assertStatus "Trailer name at 256" responseA "HTTP/1.1 200"
+
+ let (clientB, serverB) ← Mock.new
+ let rawB := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\n{longName}: value\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB bodyHandler
+ assertExact "Trailer name exceeds 256" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let rawC := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nX-Exact: {exactValue}\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC rawC bodyHandler
+ assertStatus "Trailer value at 8192" responseC "HTTP/1.1 200"
+
+ let (clientD, serverD) ← Mock.new
+ let rawD := s!"POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nX-Too-Long: {longValue}\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD rawD bodyHandler
+ assertExact "Trailer value exceeds 8192" responseD bad400
+
+-- maxTrailerHeaders enforcement.
+#eval show IO _ from do
+ let config2 : Config := { lingeringTimeout := 3000, maxTrailerHeaders := 2, generateDate := false }
+
+ let (clientA, serverA) ← Mock.new
+ let okRaw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nT1: a\x0d\nT2: b\x0d\n\x0d\n".toUTF8
+ let okResponse ← sendRaw clientA serverA okRaw bodyHandler (config := config2)
+ assertStatus "maxTrailerHeaders exact limit" okResponse "HTTP/1.1 200"
+
+ let (clientB, serverB) ← Mock.new
+ let badRaw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nT1: a\x0d\nT2: b\x0d\nT3: c\x0d\n\x0d\n".toUTF8
+ let badResponse ← sendRaw clientB serverB badRaw bodyHandler (config := config2)
+ assertExact "maxTrailerHeaders overflow" badResponse bad400
+
+ let config0 : Config := { lingeringTimeout := 3000, maxTrailerHeaders := 0, generateDate := false }
+
+ let (clientC, serverC) ← Mock.new
+ let rejectAny := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nX-Trailer: rejected\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC rejectAny bodyHandler (config := config0)
+ assertExact "maxTrailerHeaders=0 rejects trailers" responseC bad400
+
+ let (clientD, serverD) ← Mock.new
+ let noTrailer := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD noTrailer bodyHandler (config := config0)
+ assertStatus "maxTrailerHeaders=0 no trailers" responseD "HTTP/1.1 200"
+
+-- Trailer syntax validation.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let noColon := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nBadTrailer value\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA noColon bodyHandler
+ assertExact "Trailer without colon" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let leadingWS := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\n X-Bad: folded\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB leadingWS bodyHandler
+ assertExact "Trailer leading whitespace" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let spaceName := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nBad Name: value\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC spaceName bodyHandler
+ assertExact "Trailer name contains space" responseC bad400
+
+-- Trailer byte-level validation.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let beforeName := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nX-Bad".toUTF8
+ let afterName := "Name: value\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA (beforeName ++ ByteArray.mk #[0] ++ afterName) bodyHandler
+ assertExact "NUL in trailer name" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let beforeValue := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nX-Header: bad".toUTF8
+ let afterValue := "value\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB (beforeValue ++ ByteArray.mk #[0] ++ afterValue) bodyHandler
+ assertExact "NUL in trailer value" responseB bad400
+
+ let (clientC, serverC) ← Mock.new
+ let responseC ← sendRaw clientC serverC (beforeValue ++ ByteArray.mk #[0x01] ++ afterValue) bodyHandler
+ assertExact "Control char in trailer value" responseC bad400
+
+-- Incomplete trailer section with client close yields no response bytes.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n3\x0d\nabc\x0d\n0\x0d\nX-Trailer: value\x0d\n".toUTF8
+ let response ← sendRawAndClose client server raw bodyHandler
+ assert! response.size == 0
+
+-- Trailer encoding emits terminal chunk plus trailer headers.
+#eval show IO _ from Async.block do
+ let trailer := Trailer.empty
+ |>.insert (.mk "checksum") (.mk "abc123")
+ |>.insert (.mk "expires") (.mk "Thu, 01 Dec 1994")
+ let encoded := (Encode.encode (v := .v11) ChunkedBuffer.empty trailer).toByteArray
+ let text := String.fromUTF8! encoded
+ assert! text.contains "0\x0d\n"
+ assert! text.contains "Checksum: abc123\x0d\n"
+ assert! text.contains "Expires: Thu, 01 Dec 1994\x0d\n"
+
+-- Empty trailer encoding is exactly terminal chunk CRLF CRLF.
+#eval show IO _ from Async.block do
+ let encoded := (Encode.encode (v := .v11) ChunkedBuffer.empty Trailer.empty).toByteArray
+ let text := String.fromUTF8! encoded
+ assert! text == "0\x0d\n\x0d\n"
+
+-- Trailer injection: forbidden field names must be rejected (RFC 9112 §6.5).
+-- A client injecting framing or routing fields via trailers could confuse proxies.
+#eval show IO _ from do
+ -- content-length in trailer must be rejected
+ let (clientA, serverA) ← Mock.new
+ let rawA := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nContent-Length: 1000\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA bodyHandler
+ assertExact "content-length in trailer rejected" responseA bad400
+
+ -- transfer-encoding in trailer must be rejected
+ let (clientB, serverB) ← Mock.new
+ let rawB := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nTransfer-Encoding: chunked\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB bodyHandler
+ assertExact "transfer-encoding in trailer rejected" responseB bad400
+
+ -- host in trailer must be rejected
+ let (clientC, serverC) ← Mock.new
+ let rawC := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nHost: evil.example\x0d\n\x0d\n".toUTF8
+ let responseC ← sendRaw clientC serverC rawC bodyHandler
+ assertExact "host in trailer rejected" responseC bad400
+
+ -- connection in trailer must be rejected
+ let (clientD, serverD) ← Mock.new
+ let rawD := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nConnection: keep-alive\x0d\n\x0d\n".toUTF8
+ let responseD ← sendRaw clientD serverD rawD bodyHandler
+ assertExact "connection in trailer rejected" responseD bad400
+
+ -- authorization in trailer must be rejected
+ let (clientE, serverE) ← Mock.new
+ let rawE := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nAuthorization: Bearer token\x0d\n\x0d\n".toUTF8
+ let responseE ← sendRaw clientE serverE rawE bodyHandler
+ assertExact "authorization in trailer rejected" responseE bad400
+
+ -- cache-control in trailer must be rejected
+ let (clientF, serverF) ← Mock.new
+ let rawF := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nCache-Control: no-cache\x0d\n\x0d\n".toUTF8
+ let responseF ← sendRaw clientF serverF rawF bodyHandler
+ assertExact "cache-control in trailer rejected" responseF bad400
+
+ -- te in trailer must be rejected
+ let (clientG, serverG) ← Mock.new
+ let rawG := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nTE: trailers\x0d\n\x0d\n".toUTF8
+ let responseG ← sendRaw clientG serverG rawG bodyHandler
+ assertExact "te in trailer rejected" responseG bad400
+
+-- Forbidden trailer field names are rejected regardless of case.
+#eval show IO _ from do
+ let (clientA, serverA) ← Mock.new
+ let rawA := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nCONTENT-LENGTH: 0\x0d\n\x0d\n".toUTF8
+ let responseA ← sendRaw clientA serverA rawA bodyHandler
+ assertExact "CONTENT-LENGTH in trailer rejected (uppercase)" responseA bad400
+
+ let (clientB, serverB) ← Mock.new
+ let rawB := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nContent-Length: 0\x0d\nChecksum: abc\x0d\n\x0d\n".toUTF8
+ let responseB ← sendRaw clientB serverB rawB bodyHandler
+ assertExact "forbidden trailer among others rejected" responseB bad400
+
+-- Non-forbidden custom trailers are still allowed after the fix.
+#eval show IO _ from do
+ let (client, server) ← Mock.new
+ let raw := "POST / HTTP/1.1\x0d\nHost: example.com\x0d\nTransfer-Encoding: chunked\x0d\nConnection: close\x0d\n\x0d\n5\x0d\nhello\x0d\n0\x0d\nChecksum: deadbeef\x0d\nX-Timing: 12ms\x0d\n\x0d\n".toUTF8
+ let response ← sendRaw client server raw bodyHandler
+ assertStatus "non-forbidden trailers accepted" response "HTTP/1.1 200"
+ assertContains "body delivered with custom trailers" response "hello"
diff --git a/tests/lean/run/async_http_uri.lean b/tests/lean/run/async_http_uri.lean
index 7d5942292f0e..91aa77027b3d 100644
--- a/tests/lean/run/async_http_uri.lean
+++ b/tests/lean/run/async_http_uri.lean
@@ -212,6 +212,7 @@ info: some " "
#eval parseCheck "https://user:pass@secure.example.com/private"
#eval parseCheck "/double//slash//path"
#eval parseCheck "http://user%40example:pass%3Aword@host.com"
+#eval parseCheck "http://[::ffff:192.168.1.1]/path"
#guard
match (parseRequestTarget <* Std.Internal.Parsec.eof).run "http:80".toUTF8 with
@@ -226,6 +227,8 @@ info: some " "
#eval parseCheckFail ""
#eval parseCheckFail "[::1"
#eval parseCheckFail "[:::1]:80"
+#eval parseCheckFail "http://exa_mple.com/path"
+#eval parseCheckFail "http://[fe80::1%25eth0]/path"
#eval parseCheckFail "#frag"
#eval parseCheckFail "/path/\n"
#eval parseCheckFail "/path/\u0000"