fix: complete bodyless HTTP responses on the client instead of stalling

src/Std/Http/Protocol/H1.lean

@@ -670,6 +670,17 @@ private def advanceAfterHeaders (machine : Machine dir) (state : Reader.State di
   | .receiving, nextState, machine => machine.setReaderState nextState |>.setWriterState .waitingHeaders |>.addEvent .needAnswer
   | .sending, nextState, machine => machine.setReaderState nextState
 
+/--
+HEAD responses have no body, regardless of any framing headers. Override the
+framing mode to `.fixed 0` so the reader doesn't block waiting for body bytes.
+-/
+@[inline]
+private def suppressIncomingBodyIfHead (machine : Machine dir) (mode : BodyMode) : BodyMode :=
+  match dir with
+  | .sending =>
+    if machine.writer.messageHead.method == .head then .fixed 0 else mode
+  | .receiving => mode
+
 /--
 Processes a finished header block:
 1. updates keep-alive policy from config and headers,
@@ -684,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
@@ -1541,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

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