structure Network.HTTP2.FlowWindow : Type

Flow control window state for a connection or stream.

$$\text{FlowWindow} = \{ \text{size} : \mathbb{Z} \mid \text{size} \leq 2^{31} - 1 \}$$

Window sizes can go negative when the peer changes SETTINGS_INITIAL_WINDOW_SIZE.

• size : Int

  Current window size. Can be negative.

def Network.HTTP2.instReprFlowWindow.repr : FlowWindow → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP2.instReprFlowWindow : Repr FlowWindow

Equations

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

@[implicit_reducible]

instance Network.HTTP2.instInhabitedFlowWindow : Inhabited FlowWindow

Equations

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

def Network.HTTP2.instInhabitedFlowWindow.default : FlowWindow

Equations

• Network.HTTP2.instInhabitedFlowWindow.default = { size := default }

@[implicit_reducible]

instance Network.HTTP2.instBEqFlowWindow : BEq FlowWindow

Equations

• Network.HTTP2.instBEqFlowWindow = { beq := Network.HTTP2.instBEqFlowWindow.beq }

def Network.HTTP2.instBEqFlowWindow.beq : FlowWindow → FlowWindow → Bool

Equations

• Network.HTTP2.instBEqFlowWindow.beq { size := a } { size := b } = (a == b)
• Network.HTTP2.instBEqFlowWindow.beq x✝¹ x✝ = false

def Network.HTTP2.FlowWindow.default : FlowWindow

Create a flow window with the default initial size (65535).

Equations

• Network.HTTP2.FlowWindow.default = { size := 65535 }

def Network.HTTP2.FlowWindow.ofSize (n : Int) : FlowWindow

Create a flow window with a specific initial size.

Equations

• Network.HTTP2.FlowWindow.ofSize n = { size := n }

def Network.HTTP2.FlowWindow.increment (w : FlowWindow) (inc : UInt32) : Except ErrorCode FlowWindow

Apply a WINDOW_UPDATE increment. Returns an error if the result would exceed the maximum window size (2^31 - 1).

$$\text{increment}(w, i) = \begin{cases} \text{ok}(w + i) & \text{if } w + i \leq 2^{31} - 1 \\ \text{error} & \text{otherwise} \end{cases}$$

Equations

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

def Network.HTTP2.FlowWindow.consume (w : FlowWindow) (bytes : Nat) : FlowWindow

Consume bytes from the window (when sending data). $$\text{consume}(w, n) = w - n$$

Equations

• w.consume bytes = { size := w.size - ↑bytes }

def Network.HTTP2.FlowWindow.available (w : FlowWindow) : Nat

Check if there is any space in the window for sending. $$\text{available}(w) = \max(0, w.\text{size})$$

Equations

• w.available = if w.size > 0 then w.size.toNat else 0

def Network.HTTP2.FlowWindow.adjust (w : FlowWindow) (oldInitial newInitial : UInt32) : Except ErrorCode FlowWindow

Adjust the window when SETTINGS_INITIAL_WINDOW_SIZE changes. Per RFC 9113 Section 6.9.2: the difference between new and old initial window size is applied to all existing streams.

$$\text{adjust}(w, \text{old}, \text{new}) = w + (\text{new} - \text{old})$$

Equations

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

structure Network.HTTP2.ConnectionFlowControl : Type

Connection-level flow control state.

• sendWindow : FlowWindow

  Send window (how much we can send).

• recvWindow : FlowWindow

  Receive window (how much peer can send to us).

@[implicit_reducible]

instance Network.HTTP2.instReprConnectionFlowControl : Repr ConnectionFlowControl

Equations

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

def Network.HTTP2.instReprConnectionFlowControl.repr : ConnectionFlowControl → Nat → Std.Format

Equations

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

def Network.HTTP2.instInhabitedConnectionFlowControl.default : ConnectionFlowControl

Equations

• Network.HTTP2.instInhabitedConnectionFlowControl.default = { sendWindow := default, recvWindow := default }

@[implicit_reducible]

instance Network.HTTP2.instInhabitedConnectionFlowControl : Inhabited ConnectionFlowControl

Equations

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

def Network.HTTP2.ConnectionFlowControl.default : ConnectionFlowControl

Create default connection flow control.

Equations

• Network.HTTP2.ConnectionFlowControl.default = { sendWindow := Network.HTTP2.FlowWindow.default, recvWindow := Network.HTTP2.FlowWindow.default }

def Network.HTTP2.ConnectionFlowControl.processWindowUpdate (fc : ConnectionFlowControl) (increment : UInt32) : Except ErrorCode ConnectionFlowControl

Process a received WINDOW_UPDATE for the connection (stream 0). $$\text{processWindowUpdate} : \text{ConnectionFlowControl} \to \text{UInt32} \to \text{Except}(\text{ErrorCode}, \text{ConnectionFlowControl})$$

Equations

• fc.processWindowUpdate increment = match fc.sendWindow.increment increment with | Except.ok w => Except.ok { sendWindow := w, recvWindow := fc.recvWindow } | Except.error e => Except.error e

def Network.HTTP2.ConnectionFlowControl.consumeRecv (fc : ConnectionFlowControl) (bytes : Nat) : ConnectionFlowControl

Record that we received data from the peer. Decrements the receive window.

Equations

• fc.consumeRecv bytes = { sendWindow := fc.sendWindow, recvWindow := fc.recvWindow.consume bytes }

def Network.HTTP2.ConnectionFlowControl.consumeSend (fc : ConnectionFlowControl) (bytes : Nat) : ConnectionFlowControl

Record that we sent data. Decrements the send window.

Equations

• fc.consumeSend bytes = { sendWindow := fc.sendWindow.consume bytes, recvWindow := fc.recvWindow }

def Network.HTTP2.processStreamWindowUpdate (info : StreamInfo) (inc : UInt32) : Except ErrorCode StreamInfo

Process a WINDOW_UPDATE for a specific stream. Updates the stream's send window in the given StreamInfo.

Equations

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