def Network.HTTP2.HPACK.encodeInteger (value prefixBits : Nat) : ByteArray

Encode an integer with the given prefix size (1-8 bits). The first byte has 8 - prefixBits high bits already set by the caller.

$$I < 2^N - 1 \Rightarrow \text{one byte: } I$$ $$I \geq 2^N - 1 \Rightarrow \text{prefix } 2^N - 1, \text{ then } I - (2^N-1) \text{ in 7-bit chunks}$$

$$\text{encodeInteger} : \text{Nat} \to \text{Nat} \to \text{ByteArray}$$

Equations

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

def Network.HTTP2.HPACK.encodeInteger.go (v : Nat) (acc : ByteArray) (fuel : Nat) : ByteArray

Equations

• One or more equations did not get rendered due to their size.
• Network.HTTP2.HPACK.encodeInteger.go v acc 0 = acc

def Network.HTTP2.HPACK.encodeString (s : String) : ByteArray

Encode a string literal in HPACK format. The first byte's high bit indicates Huffman coding (0 = raw).

$$\text{encodeString} : \text{String} \to \text{ByteArray}$$

Equations

• Network.HTTP2.HPACK.encodeString s = Network.HTTP2.HPACK.encodeInteger s.toUTF8.size 7 ++ s.toUTF8

inductive Network.HTTP2.HPACK.HeaderRep : Type

HPACK header representation types.

• indexed (index : Nat) : HeaderRep

  Indexed Header Field Representation (Section 6.1). References a complete (name, value) pair from the table.

• literalIndexed (nameIndex : Option Nat) (name value : String) : HeaderRep

  Literal Header Field with Incremental Indexing (Section 6.2.1). The field is added to the dynamic table.

• literalNotIndexed (nameIndex : Option Nat) (name value : String) : HeaderRep

  Literal Header Field without Indexing (Section 6.2.2). The field is NOT added to the dynamic table.

• literalNeverIndexed (nameIndex : Option Nat) (name value : String) : HeaderRep

  Literal Header Field Never Indexed (Section 6.2.3). Sensitive value that must never be indexed.

• tableSizeUpdate (newSize : Nat) : HeaderRep

  Dynamic Table Size Update (Section 6.3).

@[implicit_reducible]

instance Network.HTTP2.HPACK.instReprHeaderRep : Repr HeaderRep

Equations

• Network.HTTP2.HPACK.instReprHeaderRep = { reprPrec := Network.HTTP2.HPACK.instReprHeaderRep.repr }

def Network.HTTP2.HPACK.instReprHeaderRep.repr : HeaderRep → Nat → Std.Format

Equations

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

def Network.HTTP2.HPACK.encodeHeaderRep : HeaderRep → ByteArray

Encode a single header representation to HPACK wire format. $$\text{encodeHeaderRep} : \text{HeaderRep} \to \text{ByteArray}$$

Equations

• One or more equations did not get rendered due to their size.
• Network.HTTP2.HPACK.encodeHeaderRep (Network.HTTP2.HPACK.HeaderRep.indexed a) = Network.HTTP2.HPACK.orFirstByte✝ (Network.HTTP2.HPACK.encodeInteger a 7) 128
• Network.HTTP2.HPACK.encodeHeaderRep (Network.HTTP2.HPACK.HeaderRep.literalNotIndexed (some idx) a_1 a_2) = Network.HTTP2.HPACK.encodeInteger idx 4 ++ Network.HTTP2.HPACK.encodeString a_2
• Network.HTTP2.HPACK.encodeHeaderRep (Network.HTTP2.HPACK.HeaderRep.tableSizeUpdate a) = Network.HTTP2.HPACK.orFirstByte✝ (Network.HTTP2.HPACK.encodeInteger a 5) 32

def Network.HTTP2.HPACK.encodeHeaders (dt : DynamicTable) (headers : List HeaderField) : ByteArray × DynamicTable

Encode a list of header fields using HPACK. Uses incremental indexing for all fields (the simplest strategy). Returns the encoded header block and the updated dynamic table.

$$\text{encodeHeaders} : \text{DynamicTable} \to \text{List}(\text{HeaderField}) \to \text{ByteArray} \times \text{DynamicTable}$$

Equations

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