fix: small issues with chunks and comments

Author: algebraic-dev

src/Std/Internal/Async/Basic.lean

@@ -137,7 +137,7 @@ protected def pure (x : α) : ETask ε α :=
   Task.pure <| .ok x
 
 /--
-Returns `true` if a `ETask` has finished it's execution
+Returns `true` if a `ETask` has finished its execution
 -/
 @[inline]
 protected def isFinished (x : ETask ε α) : BaseIO Bool := do

src/Std/Internal/Http.lean

@@ -20,7 +20,14 @@ A "low-level" HTTP 1.1 Server and Client implementation for Lean. It is designed
 # Overview
 
 This module of the standard library defines many concepts related to the HTTP protocol
-and its semantics in a SANS-IO format. The main function of this library is `Std.Http.Server.serve`,
+and its semantics in a sans I/O format.
+
+**sans I/O** means that the core logic of the library doesn’t perform any actual input/output itself,
+it just defines how data *should* be processed. This separation allows the protocol implementation
+to remain pure and testable, while different transports (like TCP sockets or mocks) can handle
+the actual reading and writing of bytes.
+
+The main function of this library is `Std.Http.Server.serve`,
 located in the module `Std.Internal.Http.Server`. It starts a simple HTTP/1.1 server that
 handles all requests and sends them to a simple handler function. It uses the default `Std.Internal.Async`
 library, but it can be customized to use whatever IO library you want, as the protocol implementation
@@ -29,14 +36,6 @@ is pure.
 If you want to customize how your server handles sockets, you can use `Std.Http.Server.serveConnection`,
 which is a simple function to bind a handler to a `Transport`.
 
-# Low-Level Protocol Implementation
-
-This library provides a low-level foundation that allows you to implement your own IO layer on top
-of it. The core protocol parsing and generation logic is available in `Std.Internal.Http.Protocol`,
-which provides pure functions for HTTP message parsing and serialization. This design allows you to
-integrate the HTTP protocol handling with any IO system or networking library of your choice, while
-reusing the robust protocol implementation.
-
 # Minimal Example
 
 ```lean
@@ -63,26 +62,19 @@ def main := mainAsync.block
 
 ## Transport
 
-`Std.Http.Server.Transport` is a type class used for describing a way of communication between a `Connection` and outside
-of the `Connection`. It can be a `Mock.Client` that sends and receives byte arrays so it can be used for
-deterministic testing a HTTP connection or a `TCP.Socket.Client` that is how usually it communicated with
-the internet.
+`Std.Http.Server.Transport` is a type class that defines how communication occurs between a `Connection`
+and the outside world. It can be implemented by, for example, a `Mock.Client`, which sends and receives
+byte arrays for deterministic HTTP connection testing, or by a `TCP.Socket.Client`, which is the
+standard way to communicate over the internet in HTTP/1.1.
 
 ## Connection
 
-`Std.Http.Server.Connection` is a structure that stores both a `Transport` and a `Machine`
-the machine right now is only a `Protocol.H1.Machine` that implements a State Machine for parsing request and responses for HTTP/1.1
+`Std.Http.Server.Connection` is a structure that holds both a `Transport` and a `Machine`. Currently,
+the machine is a `Protocol.H1.Machine`, which implements the state machine responsible for parsing HTTP/1.1
+requests and responses.
 
 If you want to customize how your server handles sockets, you can use `Std.Http.Server.serveConnection`,
-which is a simple function to bind a handler to a `ClientConnection`.
-
-# Low-Level Protocol Implementation
-
-This library provides a low-level foundation that allows you to implement your own IO layer on top
-of it. The core protocol parsing and generation logic is available in `Std.Internal.Http.Protocol`,
-which provides pure functions for HTTP message parsing and serialization. This design allows you to
-integrate the HTTP protocol handling with any IO system or networking library of your choice, while
-reusing the robust protocol implementation.
+a simple function that binds a handler to a `ClientConnection`.
 
 # Minimal Example
 
@@ -100,10 +92,9 @@ def handler (req : Request Body) : Async (Response Body) := do
   return Response.ok ("hi, " ++ data)
 
 def mainAsync : Async Unit := do
-  Server.serve (.v4 (.mk (.ofParts 0 0 0 0) 8080)) handler
+  let server ← Server.serve (.v4 (.mk (.ofParts 0 0 0 0) 8080)) handler
+  server.waitShutdown
 
 def main := mainAsync.block
 ```
 -/
-
-namespace Std.Http

src/Std/Internal/Http/Client/Config.lean

@@ -86,14 +86,13 @@ namespace Config
 /--
 Convert this client config into an HTTP/1.1 protocol configuration.
 -/
-def toH1Config (config : Config) : Protocol.H1.Config :=
-  { maxMessages := config.maxRequestsPerConnection
-    maxHeaders := config.maxResponseHeaders
-    maxHeaderSize := config.maxHeaderValueSize
-    enableKeepAlive := config.enableKeepAlive
-    highMark := config.writeBufferHighWatermark
-    identityHeader := config.userAgent
-  }
+def toH1Config (config : Config) : Protocol.H1.Config where
+  maxMessages := config.maxRequestsPerConnection
+  maxHeaders := config.maxResponseHeaders
+  maxHeaderSize := config.maxHeaderValueSize
+  enableKeepAlive := config.enableKeepAlive
+  highMark := config.writeBufferHighWatermark
+  identityHeader := config.userAgent
 
 end Config
 end Std.Http.Client

src/Std/Internal/Http/Client/Connection.lean

@@ -103,7 +103,7 @@ namespace PersistentConnection
 /--
 Send a request through the persistent connection.
 -/
-def send [Transport α] (pc : PersistentConnection α) (request : Request Body) : Async (Response Body) := do
+def send (pc : PersistentConnection α) (request : Request Body) : Async (Response Body) := do
   let responsePromise ← IO.Promise.new
   let cancellationToken ← Std.CancellationToken.new
 
@@ -278,22 +278,15 @@ Create a persistent connection that can handle multiple sequential requests.
 # Example
 
 ```lean
--- Connect to a server
-let socket ← Socket.mk
-socket.connect serverAddr
+let client ← TCP.Socket.Client.mk
+client.connect addr
 
--- Create persistent connection
-let pc ← createPersistentConnection socket config
+let persistent ← Client.createPersistentConnection client
 
--- Spawn the connection handler
-async (pc.connection.handlePersistent pc.config pc.requestChannel)
+let res1 ← persistent.send req1
+let res2 ← persistent.send req2
 
--- Send multiple requests
-pc.send request1 (fun response => IO.println s!"Response 1: {response.head.status}")
-pc.send request2 (fun response => IO.println s!"Response 2: {response.head.status}")
-
--- Close when done
-pc.close
+persistent.close
 ```
 -/
 def createPersistentConnection [Transport t] (client : t) (config : Client.Config := {}) : Async (PersistentConnection t) := do

src/Std/Internal/Http/Data/Body.lean

@@ -21,8 +21,6 @@ namespace Std.Http
 
 open Std Internal IO Async
 
-set_option linter.all true
-
 /--
 Type that represents the body of a request or response with streams of bytearrays or bytearrays of fixed
 size.

src/Std/Internal/Http/Data/Body/ByteStream.lean

@@ -164,38 +164,29 @@ partial def write (stream : ByteStream) (data : ByteArray) (extensions : Array (
 
     let availableSpace := state.maxBufferSize - state.bufferedSize
 
-    if availableSpace = 0 then
+    if availableSpace < data.size then
       let promise ← IO.Promise.new
       modify fun s => { s with backpressureWaiting := s.backpressureWaiting.enqueue promise }
       return Sum.inl (promise, data, extensions)
     else
-      let toWrite := min data.size availableSpace
-      let dataToAdd := data.extract 0 toWrite
-      let remaining := if toWrite < data.size then data.extract toWrite data.size else ByteArray.empty
-
-      let chunk : Chunk := {
-        data := dataToAdd,
-        extensions := extensions
-      }
+      let chunk : Chunk := { data := data, extensions := extensions }
 
       state := { state with
         pendingChunks := state.pendingChunks.push chunk,
         bufferedSize := state.bufferedSize + chunk.size
       }
 
-      -- Notify waiting consumers if we've reached highMark
       if state.bufferedSize >= state.highMark then
         if let some (consumer, rest) := state.waiting.dequeue? then
           discard <| consumer.resolve true
           state := { state with waiting := rest }
 
       set state
-      return Sum.inr (true, remaining, extensions)
+      return Sum.inr (true, ByteArray.empty, extensions)
 
   match result with
   | .inr (success, remaining, exts) =>
-    if remaining.isEmpty ∨ ¬ success
-     then
+    if remaining.isEmpty ∨ ¬ success then
       return success
     else
       write stream remaining exts
@@ -346,24 +337,23 @@ Iterate over the body content in chunks, processing each ByteArray chunk with th
 -/
 @[inline]
 protected partial def forIn
-  {β : Type} (stream : ByteStream) (acc : β)
-  (step : Chunk → β → Async (ForInStep β)) :
-  Async β := do
-    let rec @[specialize] loop (stream : ByteStream) (acc : β) : Async β := do
+    {β : Type} (stream : ByteStream) (acc : β)
+    (step : Chunk → β → Async (ForInStep β)) : Async β := do
 
-      if let some data ← stream.recv then
-        let mut acc := acc
+  let rec @[specialize] loop (stream : ByteStream) (acc : β) : Async β := do
+    if let some data ← stream.recv then
+      let mut acc := acc
 
-        for data in data do
-          match ← step data acc with
-          | .done res => return res
-          | .yield res => acc := res
+      for data in data do
+        match ← step data acc with
+        | .done res => return res
+        | .yield res => acc := res
 
-        loop stream acc
-      else
-        return acc
+      loop stream acc
+    else
+      return acc
 
-    loop stream acc
+  loop stream acc
 
 instance : ForIn Async ByteStream Chunk where
   forIn := Std.Http.Body.ByteStream.forIn

src/Std/Internal/Http/Data/Body/Length.lean

@@ -21,8 +21,6 @@ namespace Std.Http.Body
 
 set_option linter.all true
 
-set_option linter.all true
-
 /--
 Size of the body of a response or request.
 -/

src/Std/Internal/Http/Data/Chunk.lean

@@ -30,12 +30,13 @@ Represents a chunk of data with optional extensions (key-value pairs).
 structure Chunk where
 
   /--
-  ?
+  The byte data contained in this chunk.
   -/
   data : ByteArray
 
   /--
-  ?
+  Optional metadata associated with this chunk as key-value pairs. Keys are strings, values are
+  optional strings.
   -/
   extensions : Array (String × Option String) := #[]
   deriving Inhabited
@@ -59,14 +60,14 @@ Returns the total size of the chunk including data and formatted extensions. Ext
 as: ;name=value;name=value Plus 2 bytes for \r\n at the end.
 -/
 def size (chunk : Chunk) : Nat :=
-  let extensionsSize := chunk.extensions.foldl (fun acc (name, value) => acc + name.length + (value.get!).length + 2) 0
+  let extensionsSize := chunk.extensions.foldl (fun acc (name, value) => acc + name.length + (value.map (fun v => v.length + 1) |>.getD 0) + 1) 0
   chunk.data.size + extensionsSize + (if extensionsSize > 0 then 2 else 0)
 
 instance : Encode .v11 Chunk where
   encode buffer chunk :=
-  let chunkLen := chunk.data.size
-  let exts := chunk.extensions.foldl (fun acc (name, value)  => acc ++ ";" ++ name ++ (value.map (fun x => "=" ++ x) |>.getD "")) ""
-  let size := Nat.toDigits 16 chunkLen |>.toArray |>.map Char.toUInt8 |> ByteArray.mk
-  buffer.append #[size, exts.toUTF8, "\r\n".toUTF8, chunk.data, "\r\n".toUTF8]
+    let chunkLen := chunk.data.size
+    let exts := chunk.extensions.foldl (fun acc (name, value)  => acc ++ ";" ++ name ++ (value.map (fun x => "=" ++ x) |>.getD "")) ""
+    let size := Nat.toDigits 16 chunkLen |>.toArray |>.map Char.toUInt8 |> ByteArray.mk
+    buffer.append #[size, exts.toUTF8, "\r\n".toUTF8, chunk.data, "\r\n".toUTF8]
 
 end Chunk

src/Std/Internal/Http/Data/Headers.lean

@@ -106,11 +106,13 @@ Returns `true` if they match.
 def is (s : HeaderValue) (h : String) : Bool :=
   s.value.toLower == h.toLower
 
+
 /--
 Concatenates two `HeaderValue` instances, preserving the validity guarantee.
 -/
-def append (l : HeaderValue) (r : HeaderValue) : HeaderValue := by
-  refine ⟨l.value ++ r.value, ?_⟩
+def append (l : HeaderValue) (r : HeaderValue) : HeaderValue :=
+  ⟨l.value ++ r.value, ?_⟩
+where finally
   unfold isValidHeaderValue
   rw [String.data_append]
   rw [List.all_append]

src/Std/Internal/Http/Server.lean

@@ -109,9 +109,8 @@ private def frameCancellation (s : Server) (action : Async α) : Async α := do
   return result
 
 /--
-Start a new HTTP/1.1 server on the given socket address. This function uses the `Async` for handling
-tasks and TCP connections, it also returns a `Server` structure that can be used to the cancellation
-of the server.
+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
     (addr : Net.SocketAddress)