Hale.Http3.Network.HTTP3.Error

HTTP/3 error codes (RFC 9114 Section 8.1). $$\text{H3Error}$$ enumerates all standard error codes in the range $[0x100, 0x110]$.

noError : H3Error
No error (0x100). Used in GOAWAY or stream close without error.
generalProtocolError : H3Error
General protocol error (0x101).
internalError : H3Error
Internal error (0x102).
streamCreationError : H3Error
Stream creation error (0x103).
closedCriticalStream : H3Error
Critical stream was closed (0x104).
frameUnexpected : H3Error
Frame received in unexpected context (0x105).
frameError : H3Error
Frame violates layout or size rules (0x106).
excessiveLoad : H3Error
Peer generating excessive load (0x107).
idError : H3Error
Stream ID error (0x108).
settingsError : H3Error
SETTINGS frame error (0x109).
missingSettings : H3Error
No SETTINGS frame received (0x10A).
requestRejected : H3Error
Request rejected before processing (0x10B).
requestCancelled : H3Error
Request cancelled (0x10C).
requestIncomplete : H3Error
Request stream terminated prematurely (0x10D).
messageError : H3Error
Malformed HTTP message (0x10E).
connectError : H3Error
CONNECT request error (0x10F).
versionFallback : H3Error
Version fallback triggered (0x110).
unknown (code : UInt64) : H3Error
Unknown/unrecognised error code.

Instances For

source

@[implicit_reducible]

instance Network.HTTP3.instReprH3Error :

Repr H3Error

Equations

Network.HTTP3.instReprH3Error = { reprPrec := Network.HTTP3.instReprH3Error.repr }

source

def Network.HTTP3.instReprH3Error.repr :

H3Error → Nat → Std.Format

Equations

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

Instances For

source

def Network.HTTP3.instBEqH3Error.beq :

H3Error → H3Error → Bool

Equations

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

Instances For

source

@[implicit_reducible]

instance Network.HTTP3.instBEqH3Error :

BEq H3Error

Equations

Network.HTTP3.instBEqH3Error = { beq := Network.HTTP3.instBEqH3Error.beq }

source

def Network.HTTP3.H3Error.toCode :

H3Error → UInt64

Convert an HTTP/3 error to its numeric code. $$\text{toCode} : \text{H3Error} \to \text{UInt64}$$

Equations

Instances For

source

def Network.HTTP3.H3Error.fromCode :

UInt64 → H3Error

Parse an HTTP/3 error from its numeric code. $$\text{fromCode} : \text{UInt64} \to \text{H3Error}$$

Equations

Instances For

source

@[implicit_reducible]

instance Network.HTTP3.instToStringH3Error :

ToString H3Error

Equations

Network.HTTP3.instToStringH3Error = { toString := fun (e : Network.HTTP3.H3Error) => toString "H3Error(" ++ toString e.toCode ++ toString ")" }

source

theorem Network.HTTP3.H3Error.roundtrip_noError :

fromCode noError.toCode = noError

Roundtrip property: fromCode (toCode e) = e for all known error codes. This does not hold for unknown since the code may collide with a known code.

source

theorem Network.HTTP3.H3Error.roundtrip_generalProtocolError :

fromCode generalProtocolError.toCode = generalProtocolError

source

theorem Network.HTTP3.H3Error.roundtrip_internalError :

fromCode internalError.toCode = internalError

source

theorem Network.HTTP3.H3Error.roundtrip_streamCreationError :

fromCode streamCreationError.toCode = streamCreationError

source

theorem Network.HTTP3.H3Error.roundtrip_closedCriticalStream :

fromCode closedCriticalStream.toCode = closedCriticalStream