Std.Http: a request with an overlong request-target gets 400 or 414 depending on where a read ends #16035

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)
• When reporting a perceived soundness bug: Does it affect lake check --paranoid?
  (Not a soundness bug.)

Description

Std.Http's HTTP/1.1 receiver answers a request whose request-target is longer than maxUriLength (default 8192) with 414 URI Too Long when the request line arrives in one read, but with 400 Bad Request when a read ends between byte maxStartLineLength (default 8192) and the byte at which the request-line parser checks maxUriLength. RFC 9112 §3: "A server that receives a request-target longer than any URI it wishes to parse MUST respond with a 414 (URI Too Long) status code".

The server asks for at most 8192 bytes per read (defaultPayloadBytes and maximumRecvSize in Std/Http/Server/Config.lean), so the first read of such a request can end exactly in that window: in a local test with Std.Http.Server.serve, a GET with an 8194-byte target sent in one write got 400 Bad Request.

Cause: processReceivingStartLine (Std/Http/Protocol/H1.lean) runs parseRequestLineRawVersion through parseWith with limit := some machine.config.maxStartLineLength. On .eof, parseWith fails the message with .badMessage once usedBytesUntilFailure ≥ limit, so the start-line limit is also applied to an incomplete line. parseURI (Std/Http/Protocol/H1/Parser.lean) decides "uri too long" only after it has read maxUriLength target bytes and seen the next byte, i.e. at byte 4 + 8192 + 1 for a GET. A read that ends before that byte but at or after byte 8192 hits the start-line limit first. With the default configuration such a request line is also longer than maxStartLineLength, so the request is rejected either way; only the status code depends on the split.

Steps to Reproduce

import Std.Http
open Std.Http Std.Http.Protocol.H1

/-- Feed the pieces in order, stepping after each, and return the first line of the output. -/
def statusLine (pieces : List String) : String := Id.run do
  let mut m : Machine .receiving := { config := {} }
  let mut out := ByteArray.empty
  for p in pieces do
    m := m.feed p.toUTF8
    let (m', r) := m.step
    m := m'
    out := out ++ r.output.toByteArray
  for _ in [0:3] do
    let (m', r) := m.step
    m := m'
    out := out ++ r.output.toByteArray
  return ((String.fromUTF8! out).splitOn "\r\n").head!

#eval show IO Unit from do
  -- a request-target of 8194 bytes, longer than the default `maxUriLength` (8192)
  let req := "GET /" ++ String.ofList (List.replicate 8193 'a') ++ " HTTP/1.1\r\nHost: a\r\n\r\n"
  IO.println s!"one read:           {statusLine [req]}"
  for k in [8191, 8192, 8196, 8197] do
    IO.println s!"split at byte {k}: {statusLine [(req.take k).toString, (req.drop k).toString]}"

Output:

one read:           HTTP/1.1 414 URI Too Long
split at byte 8191: HTTP/1.1 414 URI Too Long
split at byte 8192: HTTP/1.1 400 Bad Request
split at byte 8196: HTTP/1.1 400 Bad Request
split at byte 8197: HTTP/1.1 414 URI Too Long

Expected behavior: 414 URI Too Long for every split.

Actual behavior: 400 Bad Request when a read ends at bytes 8192–8196.

Versions

4.37.0-nightly-2026-10-20; macOS 27.0.1 (arm64). src/Std/Http is unchanged on master since then.

Additional Information

Found while proving, for a copy of Std.Http with the fix for #15840, that how the input is split into reads does not change what the receiving machine does (https://github.com/eumemic/stdhttp-verify, FINDINGS.md §7): a differential test of the machine, one read against every split, turned up this case.

Possible fix, tested in that copy: check maxStartLineLength on the complete line only. In processReceivingStartLine, call parseWith with limit := none, and when the parse succeeds but consumed more than maxStartLineLength bytes, return machine.setFailure .badMessage (what parseWith returns for an over-long complete line today). An incomplete line is then bounded by the request-line parser's own limits (leading empty lines, the method token, maxUriLength) rather than by maxStartLineLength; with the defaults that is under 100 bytes more. With this change the request above gets 414 for every split, and results for complete requests are unchanged (the tests/elab/async_http_*.lean files pass, and 150 test requests plus 4,987 mutations sent in one write get the same responses as before).

Disclosure: the testing, diagnosis and patch were done with AI assistance (Claude).