From 521565ebcdb4c2846dd84ab729c859a14931f2ef Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Mon, 15 Jun 2026 19:43:57 -0300 Subject: [PATCH 1/5] fix: close error on recv --- src/Std/Http/Data/Body/Stream.lean | 10 ++++++++- tests/elab/async_http_body.lean | 36 ++++++++++++++++++++++++++++++ 2 files changed, 45 insertions(+), 1 deletion(-) diff --git a/src/Std/Http/Data/Body/Stream.lean b/src/Std/Http/Data/Body/Stream.lean index ec4409c9903e..41495b662a48 100644 --- a/src/Std/Http/Data/Body/Stream.lean +++ b/src/Std/Http/Data/Body/Stream.lean @@ -436,7 +436,15 @@ def checkCloseError (stream : Stream) : Async Unit := do | none => pure () instance : NextChunk Async where - nextChunk := Stream.recv + nextChunk stream := do + match ← Stream.recv stream with + | some chunk => return some chunk + | none => + -- A consumer that was already blocked in `recv` when `closeWithError` fired is woken with + -- EOF (`none`); re-check the recorded terminal error so it surfaces as a thrown exception + -- rather than a silent short read, matching the `ContextAsync` instance below. + checkCloseError stream + return none instance : NextChunk ContextAsync where nextChunk stream := do diff --git a/tests/elab/async_http_body.lean b/tests/elab/async_http_body.lean index 78a5aa80fc8b..dbac86a0ed34 100644 --- a/tests/elab/async_http_body.lean +++ b/tests/elab/async_http_body.lean @@ -791,3 +791,39 @@ def responseBuilderNoBodyAlwaysClosed : Async Unit := do assert! result.isNone #eval responseBuilderNoBodyAlwaysClosed.block + +-- Test closeWithError: a recv issued *after* the stream is closed with an error surfaces it. + +def recvAfterCloseWithErrorThrows : Async Unit := do + let stream ← Body.mkStream + stream.closeWithError (IO.userError "boom") + let threw ← + try + let _ ← stream.recv + pure false + catch _ => + pure true + assert! threw + +#eval recvAfterCloseWithErrorThrows.block + +-- Test closeWithError: a consumer already blocked in `readAll` (Async) when the stream is closed +-- with an error must observe a thrown exception, not a silent EOF / short read. This is the path +-- the client's `abortState` relies on (e.g. response body limit exceeded, mid-stream failure). + +def asyncReadAllSurfacesCloseError : Async Unit := do + let stream ← Body.mkStream + -- `readAll` in `Async` goes through the `NextChunk Async` instance; the consumer blocks in `recv`. + let readTask ← async (t := AsyncTask) <| (stream.readAll (α := ByteArray) : Async ByteArray) + -- Yield so the consumer occupies the single pending-consumer slot before we fail the stream. + let _ ← Selectable.one #[ .case (← Selector.sleep 50) pure ] + stream.closeWithError (IO.userError "mid-stream failure") + let threw ← + try + let _ ← await readTask + pure false + catch _ => + pure true + assert! threw + +#eval asyncReadAllSurfacesCloseError.block From 7d2ac8e4a5b7c1396d18134147f2e2a5b41f7f26 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Mon, 15 Jun 2026 20:10:07 -0300 Subject: [PATCH 2/5] fix: complete bodyless HTTP responses on the client instead of stalling --- src/Std/Http/Protocol/H1.lean | 35 ++++++++++++++------ tests/elab/async_http_h1_rfc_compliance.lean | 24 ++++++++++++++ 2 files changed, 49 insertions(+), 10 deletions(-) diff --git a/src/Std/Http/Protocol/H1.lean b/src/Std/Http/Protocol/H1.lean index ebfa37bf07bb..32dfe6a7aa66 100644 --- a/src/Std/Http/Protocol/H1.lean +++ b/src/Std/Http/Protocol/H1.lean @@ -669,6 +669,18 @@ private def advanceAfterHeaders (machine : Machine dir) (state : Reader.State di | .receiving, nextState, machine => machine.setReaderState nextState |>.setWriterState .waitingHeaders |>.addEvent .needAnswer | .sending, nextState, machine => machine.setReaderState nextState +/-- +Client side, reading a response to a HEAD request: RFC 9110 §8.6 specifies that +HEAD responses have no body, regardless of any framing headers. Override the +framing mode to `.fixed 0` so the reader doesn't block waiting for body bytes. +-/ +@[inline] +private def suppressIncomingBodyIfHead (machine : Machine dir) (mode : BodyMode) : BodyMode := + match dir with + | .sending => + if machine.writer.messageHead.method == .head then .fixed 0 else mode + | .receiving => mode + /-- Processes a finished header block: 1. updates keep-alive policy from config and headers, @@ -683,6 +695,7 @@ private def processHeaders (machine : Machine dir) : Machine dir := match checkMessageHead machine.reader.messageHead with | .error err => machine.setFailure err | .ok mode => + let mode := suppressIncomingBodyIfHead machine mode if exceedsBodyLimitForMode machine mode then machine.setFailure .entityTooLarge else @@ -1540,7 +1553,15 @@ When upper layers are not pulling body chunks, the machine drains body bytes internally to keep parsing/connection progress moving. -/ private partial def processReadBodyState (machine : Machine dir) (bodyState : Reader.BodyState) : Machine dir := - if drainBodyInternally machine then + -- Auto-drain when the body is internal (1xx responses on the client), or + -- when the client is reading a response with known zero length: `.fixed 0` + -- has no bytes to expose, so waiting for a caller `pullBody` would stall the + -- connection indefinitely on responses that must not carry a body (204, + -- 304, HEAD responses). Server-side (`.receiving`) keeps the existing + -- semantics so handlers can observe the body stream explicitly. + let autoDrain := drainBodyInternally machine || (dir matches .sending ∧ bodyState matches .fixed 0) + + if autoDrain then let (machine, _pulledChunk, shouldContinue) := parseBody machine bodyState if shouldContinue then processRead machine else machine else @@ -1629,15 +1650,9 @@ private partial def pullNextChunk (machine : Machine dir) : Machine dir × Optio | .readBody bodyState => let (machine, pulledChunk, shouldContinue) := parseBody machine bodyState match pulledChunk with - | some _ => - (machine, pulledChunk) - | none => - if shouldContinue then - pullNextChunk machine - else - (machine, none) - | _ => - (machine, none) + | some _ => (machine, pulledChunk) + | none => if shouldContinue then pullNextChunk machine else (machine, none) + | _ => (machine, none) /-- Pulls at most one body chunk from the reader. diff --git a/tests/elab/async_http_h1_rfc_compliance.lean b/tests/elab/async_http_h1_rfc_compliance.lean index 7969f778dacd..32e67847081e 100644 --- a/tests/elab/async_http_h1_rfc_compliance.lean +++ b/tests/elab/async_http_h1_rfc_compliance.lean @@ -755,3 +755,27 @@ private def minimalGetRequest : Request.Head := |>.step |>.step |>.assertOutputContains "Connection: keep-alive" "RFC 2616 §19.7.1: HTTP/1.0 keep-alive response must include Connection: keep-alive" |>.run + +#eval runGroup "RFC 9110 §8.6 / §6.3: client-side bodyless response framing" do + -- §8.6: a HEAD response has no body regardless of framing headers. The client reader must treat + -- it as zero-length and finish without blocking, even though Content-Length advertises bytes that + -- never arrive on the wire. + MachineTester.sending "§8.6: client HEAD response — body suppressed despite Content-Length" + |>.send { minimalGetRequest with method := .head } |>.step + |>.feed "HTTP/1.1 200 OK\r\nContent-Length: 100\r\n\r\n" + |>.step + |>.assertNoError + |>.assert (fun m => !m.canPullBody) + "HEAD response must expose no body to pull (reader must not block on absent body bytes)" + |>.assertReaderComplete |>.run + + -- §6.3: a client response with a known zero-length body (e.g. 204) must auto-complete; otherwise + -- the connection would stall waiting for a `pullBody` that never produces bytes. + MachineTester.sending "§6.3: client zero-length response auto-completes without pullBody" + |>.send minimalGetRequest |>.step + |>.feed "HTTP/1.1 204 No Content\r\nContent-Length: 0\r\n\r\n" + |>.step + |>.assertNoError + |>.assert (fun m => !m.canPullBody) + "zero-length response body must not require a caller pullBody to advance" + |>.assertReaderComplete |>.run From d56b83ccb63f7fc3410c649bfc9deaa8a2978b2e Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Mon, 15 Jun 2026 20:11:35 -0300 Subject: [PATCH 3/5] chore: shorten comment --- src/Std/Http/Protocol/H1.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Std/Http/Protocol/H1.lean b/src/Std/Http/Protocol/H1.lean index 32dfe6a7aa66..18e0757ec742 100644 --- a/src/Std/Http/Protocol/H1.lean +++ b/src/Std/Http/Protocol/H1.lean @@ -670,7 +670,6 @@ private def advanceAfterHeaders (machine : Machine dir) (state : Reader.State di | .sending, nextState, machine => machine.setReaderState nextState /-- -Client side, reading a response to a HEAD request: RFC 9110 §8.6 specifies that HEAD responses have no body, regardless of any framing headers. Override the framing mode to `.fixed 0` so the reader doesn't block waiting for body bytes. -/ From 6b6b14600437da7ce5819a03e1714b5811a70692 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 16 Jun 2026 00:54:11 -0300 Subject: [PATCH 4/5] style: use doc comment for resourceSpecificHeaders Co-Authored-By: Claude Opus 4.8 --- src/Std/Http/Protocol/H1/Redirect.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Http/Protocol/H1/Redirect.lean b/src/Std/Http/Protocol/H1/Redirect.lean index f7e2f673e76a..5e6352010d3f 100644 --- a/src/Std/Http/Protocol/H1/Redirect.lean +++ b/src/Std/Http/Protocol/H1/Redirect.lean @@ -198,7 +198,7 @@ request. private def validatingHeaders : Array Header.Name := #[.ifNoneMatch, .ifModifiedSince] -/- +/-- Resource-specific headers that become meaningless when the method changes to GET/HEAD and no body is sent. -/ From f38aa14367fc75c69e84c08115257d57fbfc7336 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 16 Jun 2026 01:03:53 -0300 Subject: [PATCH 5/5] feat: add autodrain again --- src/Std/Http/Protocol/H1.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Std/Http/Protocol/H1.lean b/src/Std/Http/Protocol/H1.lean index 53e44ddb1e0b..0f48d9f36acf 100644 --- a/src/Std/Http/Protocol/H1.lean +++ b/src/Std/Http/Protocol/H1.lean @@ -695,6 +695,7 @@ private def processHeaders (machine : Machine dir) : Machine dir := match checkMessageHead machine.reader.messageHead with | .error err => machine.setFailure err | .ok mode => + let mode := suppressIncomingBodyIfHead machine mode if exceedsBodyLimitForMode machine mode then machine.setFailure .entityTooLarge else @@ -1552,7 +1553,15 @@ When upper layers are not pulling body chunks, the machine drains body bytes internally to keep parsing/connection progress moving. -/ private partial def processReadBodyState (machine : Machine dir) (bodyState : Reader.BodyState) : Machine dir := - if drainBodyInternally machine then + -- Auto-drain when the body is internal (1xx responses on the client), or + -- when the client is reading a response with known zero length: `.fixed 0` + -- has no bytes to expose, so waiting for a caller `pullBody` would stall the + -- connection indefinitely on responses that must not carry a body (204, + -- 304, HEAD responses). Server-side (`.receiving`) keeps the existing + -- semantics so handlers can observe the body stream explicitly. + let autoDrain := drainBodyInternally machine || (dir matches .sending ∧ bodyState matches .fixed 0) + + if autoDrain then let (machine, _pulledChunk, shouldContinue) := parseBody machine bodyState if shouldContinue then processRead machine else machine else