feat: introduce HTTP/1.1 server

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,13 +233,16 @@ 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 ()))
           | some res =>
             let async : Async _ := do
               let mainPromise := waiter.promise
 
+              await barrier
               for selectable in selectables do
                 selectable.selector.unregisterFn
 

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 "<h1>Hello!</h1>"
+
+-- 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`
+-/

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 :=