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

QUIC – QUIC Transport Protocol

Lean: Hale.QUIC | Haskell: quic

QUIC transport protocol types per RFC 9000. Connection IDs carry a bounded-length proof (≤ 20 bytes). Stream IDs encode directionality (client/server, bidi/uni) in the type.

Key Types

TypeDescription
ConnectionIdVariable-length up to 20 bytes (bounded proof)
StreamIdUInt64 with 2-bit type encoding
TransportParamsRFC 9000 Section 18 defaults

Modules

ModuleDescription
TypesCore protocol types
ConfigConfiguration
ConnectionConnection management
StreamStream management
ServerQUIC server
ClientQUIC client

Files

  • Hale/QUIC/Network/QUIC/Types.lean – ConnectionId, StreamId, TransportParams
  • Hale/QUIC/Network/QUIC/Config.lean – Configuration
  • Hale/QUIC/Network/QUIC/Connection.lean – Connection management
  • Hale/QUIC/Network/QUIC/Stream.lean – Stream management
  • Hale/QUIC/Network/QUIC/Server.lean – Server
  • Hale/QUIC/Network/QUIC/Client.lean – Client