feat: introduce HTTP/1.1 protocol state machine

[algebraic-dev]

This PR introduces the H1 module, a pure HTTP/1.1 state machine that incrementally parses incoming byte streams and emits response bytes without side effects.

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:

[ghost]

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 01:04:26)

[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 01:04:28)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0a0323734b2d10c3f9355659f8e44b67bd36f644 --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-10 02:06:08)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-10 21:31:27)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-18 14:14:43)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-21 02:23:09)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b4f768b67f4d9a1573055a8a7d1d4bee5773326d --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-28 19:24:49)

[kim-em]

Not a blocker, but worth noting for future consideration:

When feed appends data (reader.input.array ++ data), the already-parsed bytes before input.pos are retained. Since resetForNextMessage preserves the input buffer across keep-alive requests, parsed bytes accumulate over the connection lifetime.

Rough impact estimate:

• Typical HTTP headers: 500 bytes - 2KB per request
• Default maxMessages = 100 per connection
• Worst case: ~100-200KB accumulated per connection
• At scale (10K connections): 1-2GB of wasted memory

How Rust handles this:

Rust's BytesMut does automatic compaction:

"Before allocating new buffer space, the reserve function will attempt to reclaim space in the existing buffer. If the current handle references a view into a larger original buffer, and all other handles have been dropped, then the current view can be copied/shifted to the front of the buffer."

A similar compaction strategy (shift unread bytes to front when parsed portion exceeds a threshold) could be added as a future optimization.

[mathlib-lean-pr-testing]

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 39c26fce1da321b24eaf949d0d7d028ba589e4e1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-10 02:06:06)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-10 21:31:25)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 6ca23a7b8bee57152110ce500ce795148707d4ed. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-13 14:51:24)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 91bd6e19a7b7aca769f9720e1127c768df0cd2a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-18 14:14:41)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 309f44d00757482e1c5a2b2427fdca818a24615a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-19 21:28:35)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-21 02:23:07)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 23:48:19)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a6ba7312cc7c8a95b258353325d34ff36b24babe --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-25 03:11:05)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b4f768b67f4d9a1573055a8a7d1d4bee5773326d --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-28 19:24:47)