Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Http3 – HTTP/3 Protocol

Lean: Hale.Http3 | Haskell: http3

HTTP/3 framing and QPACK header compression per RFC 9114. Uses QUIC variable-length integer encoding (RFC 9000 Section 16) with proven roundtrip properties.

Key Types

TypeDescription
FrameTypeInductive of HTTP/3 frame types (DATA, HEADERS, SETTINGS, GOAWAY, etc.)

Proven Properties

  • decodeVarInt (encodeVarInt n) = some n (roundtrip)

Modules

ModuleDescription
FrameFrame types + varint encoding/decoding
ErrorHTTP/3 error codes
QPACK.TableQPACK static/dynamic tables
QPACK.EncodeQPACK header compression
QPACK.DecodeQPACK header decompression
ServerHTTP/3 server

Files

  • Hale/Http3/Network/HTTP3/Frame.lean – Frame types, varint codec
  • Hale/Http3/Network/HTTP3/Error.lean – Error codes
  • Hale/Http3/Network/HTTP3/QPACK/Table.lean – QPACK tables
  • Hale/Http3/Network/HTTP3/QPACK/Encode.lean – QPACK encoding
  • Hale/Http3/Network/HTTP3/QPACK/Decode.lean – QPACK decoding
  • Hale/Http3/Network/HTTP3/Server.lean – Server