feat: introduce Body type class and some Body types for HTTP

[algebraic-dev]

This PR introduces the Body type class, the ChunkStream and Full types that are used to represent streaming bodies of Requests and Responses.

This contains the same code as #10478, divided into separate pieces to facilitate easier review.

The pieces of this feature are:

• Core data structures: feat: add core HTTP data types #12126
• Headers: feat: introduce Headers data type for HTTP #12127
• URI: feat: introduce URI data type for HTTP #12128
• Body: feat: introduce Body type class and some Body types for HTTP #12144
• H1: feat: introduce HTTP/1.1 protocol state machine #12146
• Server: feat: introduce HTTP/1.1 server #12151
• Client:

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto 4c1e4a77b4952098ea043f9b8c2d155c20b24523. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-25 00:53:54)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto e9a1c9ef63d8e53803c16077f03e2dacd4a890bd. You can force reference manual CI using the force-manual-ci label. (2026-01-25 00:53:55)

[kim-em]

The docstring says "Returns none" but the implementation returns some (.fixed 0).

[kim-em]

After let c := c.data.toArray, the name c is shadowed. Now c.size in .emptyWithCapacity c.size is the number of ByteArrays in the queue, not the total byte count. The original code used the struct's size field (total bytes) for pre-allocation.

Should this be something like:

def toByteArray (cb : ChunkedBuffer) : ByteArray :=
  let arr := cb.data.toArray
  if h : 1 = arr.size then
    arr[0]'(Nat.le_of_eq h)
  else
    arr.foldl (· ++ ·) (.emptyWithCapacity cb.size)

[kim-em]

The .reverse here is correct but non-obvious—I initially thought it was a bug. Queue.enqueueAll prepends to eList, so reversing is needed to maintain FIFO order after the internal reversal during toArray/dequeue?.

Would a brief comment help future readers? Something like:

-- Queue.enqueueAll prepends to eList, so reverse to maintain FIFO order