structure Network.HTTP2.ConnectionState : Type

Mutable state for an HTTP/2 connection.

• localSettings : Settings

  Local settings (what we advertise).

• peerSettings : Settings

  Remote peer's settings.

• peerSettingsReceived : Bool

  Whether we have received the peer's initial SETTINGS.

• streams : StreamTable

  Stream table.

• flowControl : ConnectionFlowControl

  Connection-level flow control.

• decoderTable : HPACK.DynamicTable

  HPACK decoder dynamic table.

• encoderTable : HPACK.DynamicTable

  HPACK encoder dynamic table.

• headerBlockState : HeaderBlockState

  Header block assembly state.

• goawayReceived : Bool

  Whether a GOAWAY has been sent or received.

• lastGoodStreamId : StreamId

  Last stream ID we will process (set when sending GOAWAY).

def Network.HTTP2.instInhabitedConnectionState.default : ConnectionState

Equations

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

@[implicit_reducible]

instance Network.HTTP2.instInhabitedConnectionState : Inhabited ConnectionState

Equations

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

def Network.HTTP2.ConnectionState.initial : ConnectionState

Create initial connection state with default settings.

Equations

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

def Network.HTTP2.sendGoaway (send : ByteArray → IO Unit) (lastStreamId : StreamId) (errorCode : ErrorCode) (msg : String := "") : IO Unit

Send a GOAWAY frame with the given error code and close the connection. $$\text{sendGoaway} : (\text{ByteArray} \to \text{IO Unit}) \to \text{StreamId} \to \text{ErrorCode} \to \text{String} \to \text{IO Unit}$$

Equations

• Network.HTTP2.sendGoaway send lastStreamId errorCode msg = send (Network.HTTP2.encodeFrame (Network.HTTP2.buildGoawayFrame lastStreamId errorCode msg.toUTF8))

def Network.HTTP2.sendRstStream (send : ByteArray → IO Unit) (streamId : StreamId) (errorCode : ErrorCode) : IO Unit

Send a RST_STREAM frame for a specific stream. $$\text{sendRstStream} : (\text{ByteArray} \to \text{IO Unit}) \to \text{StreamId} \to \text{ErrorCode} \to \text{IO Unit}$$

Equations

• Network.HTTP2.sendRstStream send streamId errorCode = send (Network.HTTP2.encodeFrame (Network.HTTP2.buildRstStreamFrame streamId errorCode))

def Network.HTTP2.processSettings (state : ConnectionState) (payload : ByteArray) (send : ByteArray → IO Unit) : IO (Except ConnectionError ConnectionState)

Process a received SETTINGS frame (non-ACK). Updates the peer settings and sends an ACK.

$$\text{processSettings} : \text{ConnectionState} \to \text{ByteArray} \to (\text{ByteArray} \to \text{IO Unit}) \to \text{IO}(\text{Except}(\text{ConnectionError}, \text{ConnectionState}))$$

Equations

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

def Network.HTTP2.processPing (payload : ByteArray) (send : ByteArray → IO Unit) : IO Unit

Process a received PING frame. Echo back with ACK flag. $$\text{processPing} : \text{ByteArray} \to (\text{ByteArray} \to \text{IO Unit}) \to \text{IO Unit}$$

Equations

• Network.HTTP2.processPing payload send = send (Network.HTTP2.encodeFrame (Network.HTTP2.buildPingFrame payload true))

def Network.HTTP2.processWindowUpdateFrame (state : ConnectionState) (header : FrameHeader) (payload : ByteArray) : Except (ConnectionError ⊕ StreamError) ConnectionState

Process a received WINDOW_UPDATE frame. $$\text{processWindowUpdate} : \text{ConnectionState} \to \text{FrameHeader} \to \text{ByteArray} \to \text{Except}(\text{ConnectionError} \oplus \text{StreamError}, \text{ConnectionState})$$

Equations

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

def Network.HTTP2.sendResponse (state : ConnectionState) (send : ByteArray → IO Unit) (streamId : StreamId) (headers : List (String × String)) (body : ByteArray) : IO ConnectionState

Send a response: encode headers with HPACK, split into HEADERS + CONTINUATION frames if needed, then send DATA frame with the body.

$$\text{sendResponse} : \text{ConnectionState} \to (\text{ByteArray} \to \text{IO Unit}) \to \text{StreamId} \to \text{List}(\text{HeaderField}) \to \text{ByteArray} \to \text{IO}(\text{ConnectionState})$$

Equations

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

def Network.HTTP2.sendResponse.sendCont (send : ByteArray → IO Unit) (streamId : StreamId) (remaining : List ByteArray) : IO Unit

Equations

• One or more equations did not get rendered due to their size.
• Network.HTTP2.sendResponse.sendCont send streamId [] = pure ()
• Network.HTTP2.sendResponse.sendCont send streamId [last] = send (Network.HTTP2.encodeFrame (Network.HTTP2.buildContinuationFrame streamId last true))

def Network.HTTP2.runHTTP2Connection (recv : IO ByteArray) (send : ByteArray → IO Unit) (onRequest : List (String × String) → StreamId → IO (List (String × String) × ByteArray)) : IO (Except ConnectionError Unit)

Run an HTTP/2 connection as a server.

Takes IO callbacks for reading and writing bytes, plus a request handler that receives decoded headers and a stream ID and returns response headers and a body.

$$\text{runHTTP2Connection} : \text{IO ByteArray} \to (\text{ByteArray} \to \text{IO Unit}) \to (\text{List}(\text{String} \times \text{String}) \to \text{StreamId} \to \text{IO}(\text{List}(\text{String} \times \text{String}) \times \text{ByteArray})) \to \text{IO}(\text{Except}(\text{ConnectionError}, \text{Unit}))$$

Equations

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