inductive Network.HTTP3.FrameType : Type

HTTP/3 frame types (RFC 9114 Section 7). $$\text{FrameType}$$ enumerates the standard frame type identifiers.

• data : FrameType

  DATA frame (0x0). Carries request or response body data.

• headers : FrameType

  HEADERS frame (0x1). Carries an encoded header block.

• cancelPush : FrameType

  CANCEL_PUSH frame (0x3). Cancels a server push.

• settings : FrameType

  SETTINGS frame (0x4). Conveys configuration parameters.

• pushPromise : FrameType

  PUSH_PROMISE frame (0x5). Server push initiation.

• goaway : FrameType

  GOAWAY frame (0x7). Initiates graceful shutdown.

• maxPushId : FrameType

  MAX_PUSH_ID frame (0xD). Controls server push.

• unknown (id : UInt64) : FrameType

  Unknown/extension frame type.

def Network.HTTP3.instReprFrameType.repr : FrameType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Network.HTTP3.instReprFrameType : Repr FrameType

Equations

• Network.HTTP3.instReprFrameType = { reprPrec := Network.HTTP3.instReprFrameType.repr }

def Network.HTTP3.instBEqFrameType.beq : FrameType → FrameType → Bool

Equations

• Network.HTTP3.instBEqFrameType.beq Network.HTTP3.FrameType.data Network.HTTP3.FrameType.data = true
• Network.HTTP3.instBEqFrameType.beq Network.HTTP3.FrameType.headers Network.HTTP3.FrameType.headers = true
• Network.HTTP3.instBEqFrameType.beq Network.HTTP3.FrameType.cancelPush Network.HTTP3.FrameType.cancelPush = true
• Network.HTTP3.instBEqFrameType.beq Network.HTTP3.FrameType.settings Network.HTTP3.FrameType.settings = true
• Network.HTTP3.instBEqFrameType.beq Network.HTTP3.FrameType.pushPromise Network.HTTP3.FrameType.pushPromise = true
• Network.HTTP3.instBEqFrameType.beq Network.HTTP3.FrameType.goaway Network.HTTP3.FrameType.goaway = true
• Network.HTTP3.instBEqFrameType.beq Network.HTTP3.FrameType.maxPushId Network.HTTP3.FrameType.maxPushId = true
• Network.HTTP3.instBEqFrameType.beq (Network.HTTP3.FrameType.unknown a) (Network.HTTP3.FrameType.unknown b) = (a == b)
• Network.HTTP3.instBEqFrameType.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Network.HTTP3.instBEqFrameType : BEq FrameType

Equations

• Network.HTTP3.instBEqFrameType = { beq := Network.HTTP3.instBEqFrameType.beq }

def Network.HTTP3.FrameType.toId : FrameType → UInt64

Convert a frame type to its numeric identifier. $$\text{toId} : \text{FrameType} \to \text{UInt64}$$

Equations

• Network.HTTP3.FrameType.data.toId = 0
• Network.HTTP3.FrameType.headers.toId = 1
• Network.HTTP3.FrameType.cancelPush.toId = 3
• Network.HTTP3.FrameType.settings.toId = 4
• Network.HTTP3.FrameType.pushPromise.toId = 5
• Network.HTTP3.FrameType.goaway.toId = 7
• Network.HTTP3.FrameType.maxPushId.toId = 13
• (Network.HTTP3.FrameType.unknown a).toId = a

def Network.HTTP3.FrameType.fromId : UInt64 → FrameType

Parse a frame type from its numeric identifier. $$\text{fromId} : \text{UInt64} \to \text{FrameType}$$

Equations

• Network.HTTP3.FrameType.fromId 0 = Network.HTTP3.FrameType.data
• Network.HTTP3.FrameType.fromId 1 = Network.HTTP3.FrameType.headers
• Network.HTTP3.FrameType.fromId 3 = Network.HTTP3.FrameType.cancelPush
• Network.HTTP3.FrameType.fromId 4 = Network.HTTP3.FrameType.settings
• Network.HTTP3.FrameType.fromId 5 = Network.HTTP3.FrameType.pushPromise
• Network.HTTP3.FrameType.fromId 7 = Network.HTTP3.FrameType.goaway
• Network.HTTP3.FrameType.fromId 13 = Network.HTTP3.FrameType.maxPushId
• Network.HTTP3.FrameType.fromId x✝ = Network.HTTP3.FrameType.unknown x✝

@[implicit_reducible]

instance Network.HTTP3.instToStringFrameType : ToString FrameType

Equations

• One or more equations did not get rendered due to their size.

theorem Network.HTTP3.FrameType.roundtrip_data : fromId data.toId = data

Roundtrip theorems for FrameType fromId/toId.

theorem Network.HTTP3.FrameType.roundtrip_headers : fromId headers.toId = headers

theorem Network.HTTP3.FrameType.roundtrip_cancelPush : fromId cancelPush.toId = cancelPush

theorem Network.HTTP3.FrameType.roundtrip_settings : fromId settings.toId = settings

theorem Network.HTTP3.FrameType.roundtrip_pushPromise : fromId pushPromise.toId = pushPromise

theorem Network.HTTP3.FrameType.roundtrip_goaway : fromId goaway.toId = goaway

theorem Network.HTTP3.FrameType.roundtrip_maxPushId : fromId maxPushId.toId = maxPushId

def Network.HTTP3.maxVarInt : UInt64

The maximum value encodable as a QUIC variable-length integer. $$2^{62} - 1 = 4611686018427387903$$

Equations

• Network.HTTP3.maxVarInt = 4611686018427387903

def Network.HTTP3.encodeVarInt (val : UInt64) : ByteArray

Encode a value as a QUIC variable-length integer (RFC 9000 Section 16). Uses the minimum number of bytes for the given value. $$\text{encodeVarInt} : \text{UInt64} \to \text{ByteArray}$$

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP3.decodeVarInt (buf : ByteArray) (offset : Nat := 0) : Option (UInt64 × Nat)

Decode a QUIC variable-length integer from a ByteArray at the given offset. $$\text{decodeVarInt} : \text{ByteArray} \to \mathbb{N} \to \text{Option}(\text{UInt64} \times \mathbb{N})$$ Returns the decoded value and the number of bytes consumed, or none on error.

Equations

• One or more equations did not get rendered due to their size.

structure Network.HTTP3.Frame : Type

An HTTP/3 frame: type + payload. $$\text{Frame} = \text{FrameType} \times \text{ByteArray}$$

• frameType : FrameType

  The frame type.

• payload : ByteArray

  The frame payload (raw bytes).

def Network.HTTP3.Frame.encode (f : Frame) : ByteArray

Encode an HTTP/3 frame to wire format: varint(type) ++ varint(length) ++ payload. $$\text{encode} : \text{Frame} \to \text{ByteArray}$$

Equations

• f.encode = Network.HTTP3.encodeVarInt f.frameType.toId ++ Network.HTTP3.encodeVarInt f.payload.size.toUInt64 ++ f.payload

def Network.HTTP3.Frame.decode (buf : ByteArray) (offset : Nat := 0) : Option (Frame × Nat)

Decode an HTTP/3 frame from wire format at the given offset. $$\text{decode} : \text{ByteArray} \to \mathbb{N} \to \text{Option}(\text{Frame} \times \mathbb{N})$$ Returns the decoded frame and total bytes consumed, or none on error.

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP3.settingsQpackMaxTableCapacity : UInt64

HTTP/3 settings identifiers.

Equations

• Network.HTTP3.settingsQpackMaxTableCapacity = 1

def Network.HTTP3.settingsMaxFieldSectionSize : UInt64

Equations

• Network.HTTP3.settingsMaxFieldSectionSize = 6

def Network.HTTP3.settingsQpackBlockedStreams : UInt64

Equations

• Network.HTTP3.settingsQpackBlockedStreams = 7

structure Network.HTTP3.H3Settings : Type

HTTP/3 settings values. $$\text{H3Settings} = \{ \text{maxFieldSectionSize} : \mathbb{N},\; \ldots \}$$

• maxFieldSectionSize : Nat

  Maximum size of a header section (SETTINGS_MAX_FIELD_SECTION_SIZE, 0x6).

• qpackMaxTableCapacity : Nat

  Maximum QPACK dynamic table capacity (SETTINGS_QPACK_MAX_TABLE_CAPACITY, 0x1).

• qpackBlockedStreams : Nat

  Maximum number of blocked QPACK streams (SETTINGS_QPACK_BLOCKED_STREAMS, 0x7).

def Network.HTTP3.instReprH3Settings.repr : H3Settings → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Network.HTTP3.instReprH3Settings : Repr H3Settings

Equations

• Network.HTTP3.instReprH3Settings = { reprPrec := Network.HTTP3.instReprH3Settings.repr }

def Network.HTTP3.instBEqH3Settings.beq : H3Settings → H3Settings → Bool

Equations

• One or more equations did not get rendered due to their size.
• Network.HTTP3.instBEqH3Settings.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Network.HTTP3.instBEqH3Settings : BEq H3Settings

Equations

• Network.HTTP3.instBEqH3Settings = { beq := Network.HTTP3.instBEqH3Settings.beq }

def Network.HTTP3.H3Settings.default : H3Settings

Default HTTP/3 settings. $$\text{defaultH3Settings} = \text{H3Settings}\{\}$$

Equations

• Network.HTTP3.H3Settings.default = { }

def Network.HTTP3.H3Settings.encode (s : H3Settings) : ByteArray

Encode HTTP/3 settings as a sequence of varint(id) ++ varint(value) pairs. Only non-zero settings are included. $$\text{encode} : \text{H3Settings} \to \text{ByteArray}$$

Equations

• One or more equations did not get rendered due to their size.

def Network.HTTP3.H3Settings.decode (buf : ByteArray) : Option H3Settings

Decode HTTP/3 settings from a byte buffer. $$\text{decode} : \text{ByteArray} \to \text{Option}(\text{H3Settings})$$

Equations

• Network.HTTP3.H3Settings.decode buf = Network.HTTP3.decodeSettingsPairs✝ buf