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

Http2 – HTTP/2 Protocol

Lean: Hale.Http2 | Haskell: http2

HTTP/2 framing, HPACK header compression, flow control, and server implementation per RFC 9113. Stream IDs carry a 31-bit bound proof. Settings carry RFC 9113 value constraint proofs.

Key Types

TypeDescription
StreamId31-bit bounded stream identifier
FrameTypeInductive of all RFC 9113 frame types
ErrorCodeConnection/stream error codes
SettingsRFC 9113 settings with proof-carrying value constraints
ConnectionErrorError code + message for GOAWAY
StreamErrorStream ID + error code + message for RST_STREAM

Modules

ModuleDescription
Frame.TypesFrame type definitions and flags
Frame.EncodeBinary frame serialization
Frame.DecodeBinary frame deserialization
HPACK.TableDynamic/static header table
HPACK.HuffmanHuffman coding
HPACK.EncodeHPACK header compression
HPACK.DecodeHPACK header decompression
FlowControlWindow-based flow control
StreamStream lifecycle management
ServerHTTP/2 server implementation

Files

  • Hale/Http2/Network/HTTP2/Types.lean – Core types
  • Hale/Http2/Network/HTTP2/Frame/Types.lean – Frame definitions
  • Hale/Http2/Network/HTTP2/Frame/Encode.lean – Frame encoding
  • Hale/Http2/Network/HTTP2/Frame/Decode.lean – Frame decoding
  • Hale/Http2/Network/HTTP2/HPACK/Table.lean – HPACK tables
  • Hale/Http2/Network/HTTP2/HPACK/Huffman.lean – Huffman coding
  • Hale/Http2/Network/HTTP2/HPACK/Encode.lean – HPACK encoding
  • Hale/Http2/Network/HTTP2/HPACK/Decode.lean – HPACK decoding
  • Hale/Http2/Network/HTTP2/FlowControl.lean – Flow control
  • Hale/Http2/Network/HTTP2/Stream.lean – Stream management
  • Hale/Http2/Network/HTTP2/Server.lean – Server