@[reducible, inline]

abbrev Network.HTTP2.HPACK.HeaderField : Type

A header field is a name-value pair of strings. $$\text{HeaderField} = \text{String} \times \text{String}$$

Equations

• Network.HTTP2.HPACK.HeaderField = (String × String)

def Network.HTTP2.HPACK.staticTable : Array HeaderField

The HPACK static table as defined in RFC 7541 Appendix A. Index 1-based, containing 61 pre-defined header fields.

Equations

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

def Network.HTTP2.HPACK.staticTableSize : Nat

Size of the static table. Always 61.

Equations

• Network.HTTP2.HPACK.staticTableSize = 61

def Network.HTTP2.HPACK.staticLookup (index : Nat) : Option HeaderField

Look up an entry in the static table by 1-based index. $$\text{staticLookup}(i) = \text{staticTable}[i-1]$$ for $1 \leq i \leq 61$. Returns none for out-of-range indices.

Equations

• Network.HTTP2.HPACK.staticLookup index = if (decide (index ≥ 1) && decide (index ≤ Network.HTTP2.HPACK.staticTableSize)) = true then Network.HTTP2.HPACK.staticTable[index - 1]? else none

structure Network.HTTP2.HPACK.DynamicTable : Type

The HPACK dynamic table. Entries are stored most-recent-first. The table has a maximum size in octets, and entries are evicted from the end (oldest) when the size would exceed the maximum.

Size of an entry: name.length + value.length + 32 (RFC 7541 Section 4.1).

• entries : Array HeaderField

  Entries stored most-recent-first.

• currentSize : Nat

  Current size in octets.

• maxSize : Nat

  Maximum size in octets (from SETTINGS_HEADER_TABLE_SIZE).

def Network.HTTP2.HPACK.instReprDynamicTable.repr : DynamicTable → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP2.HPACK.instReprDynamicTable : Repr DynamicTable

Equations

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

@[inline]

def Network.HTTP2.HPACK.entrySize (name value : String) : Nat

Calculate the HPACK entry size per RFC 7541 Section 4.1. $$\text{entrySize}(n, v) = |n| + |v| + 32$$

Equations

• Network.HTTP2.HPACK.entrySize name value = name.length + value.length + 32

def Network.HTTP2.HPACK.DynamicTable.empty (maxSize : Nat) : DynamicTable

Create an empty dynamic table with the given maximum size. $$\text{empty}(m) = \{ \text{entries} = [], \text{currentSize} = 0, \text{maxSize} = m \}$$

Equations

• Network.HTTP2.HPACK.DynamicTable.empty maxSize = { entries := #[], currentSize := 0, maxSize := maxSize }

@[implicit_reducible]

instance Network.HTTP2.HPACK.DynamicTable.instInhabited : Inhabited DynamicTable

Equations

• Network.HTTP2.HPACK.DynamicTable.instInhabited = { default := Network.HTTP2.HPACK.DynamicTable.empty 4096 }

@[inline]

def Network.HTTP2.HPACK.DynamicTable.size (dt : DynamicTable) : Nat

Get the number of entries in the dynamic table.

Equations

• dt.size = dt.entries.size

def Network.HTTP2.HPACK.DynamicTable.lookup (dt : DynamicTable) (index : Nat) : Option HeaderField

Look up an entry by 0-based index (0 = most recent). $$\text{lookup}(dt, i) = dt.\text{entries}[i]$$

Equations

• dt.lookup index = dt.entries[index]?

def Network.HTTP2.HPACK.DynamicTable.insert (dt : DynamicTable) (name value : String) : DynamicTable

Insert a new entry at the front of the dynamic table. Evicts old entries as needed to maintain the size invariant. If the entry itself is larger than maxSize, the table is emptied.

$$\text{insert}(dt, n, v) = \text{evict}(\{n:v\} :: dt.\text{entries})$$

Equations

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

def Network.HTTP2.HPACK.DynamicTable.resize (dt : DynamicTable) (newMaxSize : Nat) : DynamicTable

Resize the dynamic table to a new maximum size. Evicts entries if needed. $$\text{resize}(dt, m) = \text{evict}(dt, m)$$ with updated maxSize.

Equations

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

def Network.HTTP2.HPACK.DynamicTable.find (dt : DynamicTable) (name value : String) : Option (Nat × Bool)

Find a header field in the dynamic table. Returns the 0-based index if found. Searches for exact (name, value) match first, then name-only match.

Equations

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

def Network.HTTP2.HPACK.indexLookup (dt : DynamicTable) (index : Nat) : Option HeaderField

Look up a header field by HPACK index (1-based, static table first, then dynamic). $$\text{indexLookup}(dt, i) = \begin{cases} \text{staticTable}[i-1] & \text{if } 1 \leq i \leq 61 \\ \text{dt.entries}[i-62] & \text{if } i > 61 \end{cases}$$

Equations

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

def Network.HTTP2.HPACK.findInTables (dt : DynamicTable) (name value : String) : Option (Nat × Bool)

Find a header field in the combined static + dynamic tables. Returns (index, exactMatch) where index is 1-based HPACK index.

Equations

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