structure Network.HTTP2.ConnectionError : Type

A connection-level error that results in sending GOAWAY and closing the connection.

$$\text{ConnectionError} = \text{ErrorCode} \times \text{String}$$

• errorCode : ErrorCode

  The error code to send in the GOAWAY frame.

• message : String

  Human-readable description for debugging.

def Network.HTTP2.instReprConnectionError.repr : ConnectionError → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP2.instReprConnectionError : Repr ConnectionError

Equations

• Network.HTTP2.instReprConnectionError = { reprPrec := Network.HTTP2.instReprConnectionError.repr }

def Network.HTTP2.instInhabitedConnectionError.default : ConnectionError

Equations

• Network.HTTP2.instInhabitedConnectionError.default = { errorCode := default, message := default }

@[implicit_reducible]

instance Network.HTTP2.instInhabitedConnectionError : Inhabited ConnectionError

Equations

• Network.HTTP2.instInhabitedConnectionError = { default := Network.HTTP2.instInhabitedConnectionError.default }

@[implicit_reducible]

instance Network.HTTP2.instBEqConnectionError : BEq ConnectionError

Equations

• Network.HTTP2.instBEqConnectionError = { beq := fun (a b : Network.HTTP2.ConnectionError) => a.errorCode == b.errorCode && a.message == b.message }

@[implicit_reducible]

instance Network.HTTP2.instToStringConnectionError : ToString ConnectionError

Equations

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

structure Network.HTTP2.StreamError : Type

A stream-level error that results in sending RST_STREAM for that stream only.

$$\text{StreamError} = \text{StreamId} \times \text{ErrorCode} \times \text{String}$$

• streamId : StreamId

  The stream that experienced the error.

• errorCode : ErrorCode

  The error code to send in the RST_STREAM frame.

• message : String

  Human-readable description for debugging.

def Network.HTTP2.instReprStreamError.repr : StreamError → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP2.instReprStreamError : Repr StreamError

Equations

• Network.HTTP2.instReprStreamError = { reprPrec := Network.HTTP2.instReprStreamError.repr }

@[implicit_reducible]

instance Network.HTTP2.instInhabitedStreamError : Inhabited StreamError

Equations

• Network.HTTP2.instInhabitedStreamError = { default := Network.HTTP2.instInhabitedStreamError.default }

def Network.HTTP2.instInhabitedStreamError.default : StreamError

Equations

• Network.HTTP2.instInhabitedStreamError.default = { streamId := default, errorCode := default, message := default }

@[implicit_reducible]

instance Network.HTTP2.instBEqStreamError : BEq StreamError

Equations

• Network.HTTP2.instBEqStreamError = { beq := fun (a b : Network.HTTP2.StreamError) => a.streamId == b.streamId && a.errorCode == b.errorCode && a.message == b.message }

@[implicit_reducible]

instance Network.HTTP2.instToStringStreamError : ToString StreamError

Equations

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

inductive Network.HTTP2.HeaderBlockState : Type

State for tracking header block assembly across HEADERS + CONTINUATION frames.

RFC 9113 Section 4.3: A header block that does not fit within a single HEADERS or PUSH_PROMISE frame is continued in one or more CONTINUATION frames. The header block ends when END_HEADERS is set.

$$\text{HeaderBlockState} = \text{Idle} \mid \text{Assembling}(\text{StreamId}, \text{ByteArray})$$

• idle : HeaderBlockState

  No header block is being assembled.

• assembling (streamId : StreamId) (fragments : ByteArray) : HeaderBlockState

  A header block is being assembled for the given stream. The ByteArray accumulates the header block fragment bytes.

def Network.HTTP2.instInhabitedHeaderBlockState.default : HeaderBlockState

Equations

• Network.HTTP2.instInhabitedHeaderBlockState.default = Network.HTTP2.HeaderBlockState.idle

@[implicit_reducible]

instance Network.HTTP2.instInhabitedHeaderBlockState : Inhabited HeaderBlockState

Equations

• Network.HTTP2.instInhabitedHeaderBlockState = { default := Network.HTTP2.instInhabitedHeaderBlockState.default }

@[implicit_reducible]

instance Network.HTTP2.instBEqHeaderBlockState : BEq HeaderBlockState

Equations

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

@[inline]

def Network.HTTP2.HeaderBlockState.isAssembling : HeaderBlockState → Bool

Check if we are currently assembling a header block.

Equations

• Network.HTTP2.HeaderBlockState.idle.isAssembling = false
• (Network.HTTP2.HeaderBlockState.assembling streamId fragments).isAssembling = true

@[inline]

def Network.HTTP2.HeaderBlockState.streamId? : HeaderBlockState → Option StreamId

Get the stream ID being assembled, if any.

Equations

• Network.HTTP2.HeaderBlockState.idle.streamId? = none
• (Network.HTTP2.HeaderBlockState.assembling streamId fragments).streamId? = some streamId

def Network.HTTP2.HeaderBlockState.appendFragment (state : HeaderBlockState) (fragment : ByteArray) : Option HeaderBlockState

Append a fragment to the header block being assembled. Returns none if not currently assembling.

Equations

• Network.HTTP2.HeaderBlockState.idle.appendFragment fragment = none
• (Network.HTTP2.HeaderBlockState.assembling streamId fragments).appendFragment fragment = some (Network.HTTP2.HeaderBlockState.assembling streamId (fragments ++ fragment))

def Network.HTTP2.HeaderBlockState.complete : HeaderBlockState → Option (StreamId × ByteArray)

Get the complete assembled header block and reset to idle. Returns none if not currently assembling.

Equations

• Network.HTTP2.HeaderBlockState.idle.complete = none
• (Network.HTTP2.HeaderBlockState.assembling streamId fragments).complete = some (streamId, fragments)

inductive Network.HTTP2.HTTP2Result (α : Type) : Type

HTTP/2 connection-level protocol result.

• ok {α : Type} (value : α) : HTTP2Result α

  Success with a value.

• connectionError {α : Type} (error : ConnectionError) : HTTP2Result α

  Connection error requiring GOAWAY.

• streamError {α : Type} (error : StreamError) : HTTP2Result α

  Stream error requiring RST_STREAM.

def Network.HTTP2.instReprHTTP2Result.repr {α✝ : Type} [Repr α✝] : HTTP2Result α✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP2.instReprHTTP2Result {α✝ : Type} [Repr α✝] : Repr (HTTP2Result α✝)

Equations

• Network.HTTP2.instReprHTTP2Result = { reprPrec := Network.HTTP2.instReprHTTP2Result.repr }

def Network.HTTP2.HTTP2Result.map {α β : Type} (f : α → β) : HTTP2Result α → HTTP2Result β

Map a function over the success value.

Equations

• Network.HTTP2.HTTP2Result.map f (Network.HTTP2.HTTP2Result.ok a) = Network.HTTP2.HTTP2Result.ok (f a)
• Network.HTTP2.HTTP2Result.map f (Network.HTTP2.HTTP2Result.connectionError a) = Network.HTTP2.HTTP2Result.connectionError a
• Network.HTTP2.HTTP2Result.map f (Network.HTTP2.HTTP2Result.streamError a) = Network.HTTP2.HTTP2Result.streamError a

def Network.HTTP2.HTTP2Result.bind {α β : Type} (r : HTTP2Result α) (f : α → HTTP2Result β) : HTTP2Result β

Bind operation for chaining HTTP2Results.

Equations

• (Network.HTTP2.HTTP2Result.ok a).bind f = f a
• (Network.HTTP2.HTTP2Result.connectionError a).bind f = Network.HTTP2.HTTP2Result.connectionError a
• (Network.HTTP2.HTTP2Result.streamError a).bind f = Network.HTTP2.HTTP2Result.streamError a