def Network.HTTP2.decodeUInt16BE (bs : ByteArray) (offset : Nat := 0) : Option UInt16

Equations

• Network.HTTP2.decodeUInt16BE bs offset = if offset + 2 > bs.size then none else have b0 := bs[offset]!; have b1 := bs[offset + 1]!; some (b0.toUInt16 <<< 8 ||| b1.toUInt16)

def Network.HTTP2.decodeUInt32BE (bs : ByteArray) (offset : Nat := 0) : Option UInt32

Equations

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

def Network.HTTP2.decodeFrameHeader (bs : ByteArray) (offset : Nat := 0) : Option FrameHeader

Equations

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

def Network.HTTP2.decodeSettingsParam (bs : ByteArray) (offset : Nat := 0) : Option (SettingsKeyId × UInt32)

Equations

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

def Network.HTTP2.decodeSettingsPayload (bs : ByteArray) : Option (List (SettingsKeyId × UInt32))

Equations

• Network.HTTP2.decodeSettingsPayload bs = if (bs.size % 6 != 0) = true then none else have count := bs.size / 6; Network.HTTP2.decodeSettingsPayload.go bs 0 [] count

def Network.HTTP2.decodeSettingsPayload.go (bs : ByteArray) (i : Nat) (acc : List (SettingsKeyId × UInt32)) (fuel : Nat) : Option (List (SettingsKeyId × UInt32))

Equations

• One or more equations did not get rendered due to their size.
• Network.HTTP2.decodeSettingsPayload.go bs i acc 0 = some acc.reverse

def Network.HTTP2.applySettings (s : Settings) (params : List (SettingsKeyId × UInt32)) : Settings

Equations

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

def Network.HTTP2.decodeGoaway (bs : ByteArray) : Option (StreamId × ErrorCode × ByteArray)

Equations

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

def Network.HTTP2.decodeWindowUpdate (bs : ByteArray) : Option UInt32

Equations

• Network.HTTP2.decodeWindowUpdate bs = if bs.size < 4 then none else do let inc ← Network.HTTP2.decodeUInt32BE bs some (inc &&& 2147483647)

def Network.HTTP2.decodeRstStream (bs : ByteArray) : Option ErrorCode

Equations

• Network.HTTP2.decodeRstStream bs = if bs.size < 4 then none else do let code ← Network.HTTP2.decodeUInt32BE bs some (Network.HTTP2.ErrorCode.fromUInt32 code)

def Network.HTTP2.decodePriority (bs : ByteArray) (offset : Nat := 0) : Option (Bool × StreamId × UInt8)

Equations

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

def Network.HTTP2.decodePadding (bs : ByteArray) : Option (ByteArray × Nat)

Equations

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

def Network.HTTP2.validateFrameSize (h : FrameHeader) (s : Settings) : Option ErrorCode

Equations

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