Chunk

This module defines the Chunk type, which represents a chunk of data from a request or response.

Reference: https://www.rfc-editor.org/rfc/rfc9112.html#section-7.1

@[reducible, inline]

abbrev Std.Http.Chunk.IsValidExtensionName (s : String) : Prop

A proposition stating that s is a valid chunk-extension name: every character in s is an HTTP token character and s is non-empty.

Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension

Equations

• Std.Http.Chunk.IsValidExtensionName s = (Std.Http.Internal.isToken s = true)

structure Std.Http.Chunk.ExtensionName : Type

A validated chunk extension name that ensures all characters conform to HTTP standards per RFC 9112 §7.1.1. Extension names appear in chunked transfer encoding as key-value metadata.

Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension

• value : String

  The extension name string.

• isValidExtensionName : IsValidExtensionName self.value

  The proof that it's a valid extension name.

@[implicit_reducible]

instance Std.Http.Chunk.instReprExtensionName : Repr ExtensionName

Equations

• Std.Http.Chunk.instReprExtensionName = { reprPrec := Std.Http.Chunk.instReprExtensionName.repr }

def Std.Http.Chunk.instReprExtensionName.repr : ExtensionName → Nat → Format

Equations

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

def Std.Http.Chunk.instDecidableEqExtensionName.decEq (x✝ x✝¹ : ExtensionName) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Std.Http.Chunk.instDecidableEqExtensionName : DecidableEq ExtensionName

Equations

• Std.Http.Chunk.instDecidableEqExtensionName = Std.Http.Chunk.instDecidableEqExtensionName.decEq

def Std.Http.Chunk.instBEqExtensionName.beq : ExtensionName → ExtensionName → Bool

Equations

• One or more equations did not get rendered due to their size.
• Std.Http.Chunk.instBEqExtensionName.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.Chunk.instBEqExtensionName : BEq ExtensionName

Equations

• Std.Http.Chunk.instBEqExtensionName = { beq := Std.Http.Chunk.instBEqExtensionName.beq }

@[implicit_reducible]

instance Std.Http.Chunk.instHashableExtensionName : Hashable ExtensionName

Equations

• Std.Http.Chunk.instHashableExtensionName = { hash := fun (x : Std.Http.Chunk.ExtensionName) => hash x.value }

@[implicit_reducible]

instance Std.Http.Chunk.instInhabitedExtensionName : Inhabited ExtensionName

Equations

• Std.Http.Chunk.instInhabitedExtensionName = { default := { value := "_", isValidExtensionName := Std.Http.Chunk.instInhabitedExtensionName._proof_1 } }

@[implicit_reducible]

instance Std.Http.Chunk.instToStringExtensionName : ToString ExtensionName

Equations

• Std.Http.Chunk.instToStringExtensionName = { toString := fun (name : Std.Http.Chunk.ExtensionName) => name.value }

def Std.Http.Chunk.ExtensionName.ofString? (s : String) : Option ExtensionName

Attempts to create an ExtensionName from a String, returning none if the string contains invalid characters or is empty.

Equations

• Std.Http.Chunk.ExtensionName.ofString? s = if h : Std.Http.Chunk.IsValidExtensionName s then some { value := s, isValidExtensionName := h } else none

def Std.Http.Chunk.ExtensionName.ofString! (s : String) : ExtensionName

Creates an ExtensionName from a string, panicking with an error message if the string contains invalid characters or is empty.

Equations

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

@[reducible, inline]

abbrev Std.Http.Chunk.IsValidExtensionValue (s : String) : Prop

A proposition asserting that s is a valid extension value, meaning every character passes Char.quotedStringChar (i.e. is qdtext or a valid quoted-pair payload).

Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension

Equations

• Std.Http.Chunk.IsValidExtensionValue s = (s.toList.all Std.Http.Internal.Char.quotedStringChar = true)

structure Std.Http.Chunk.ExtensionValue : Type

A validated chunk extension value that ensures all characters conform to HTTP standards per RFC 9112 §7.1.1. Extension values appear in chunked transfer encoding as metadata associated with extension names.

Note: UTF-8 encoding is not supported. The quoting mechanism is strict and only permits escaping specific values. Additionally, the library does not support obs-text, which means certain UTF-8 characters or values outside of token, qdtext, and the limited set of escapable characters cannot be encoded.

Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension

• value : String

  The extension value string.

• isValidExtensionValue : IsValidExtensionValue self.value

  The proof that it's a valid extension value.

def Std.Http.Chunk.instReprExtensionValue.repr : ExtensionValue → Nat → Format

Equations

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

@[implicit_reducible]

instance Std.Http.Chunk.instReprExtensionValue : Repr ExtensionValue

Equations

• Std.Http.Chunk.instReprExtensionValue = { reprPrec := Std.Http.Chunk.instReprExtensionValue.repr }

@[implicit_reducible]

instance Std.Http.Chunk.instDecidableEqExtensionValue : DecidableEq ExtensionValue

Equations

• Std.Http.Chunk.instDecidableEqExtensionValue = Std.Http.Chunk.instDecidableEqExtensionValue.decEq

def Std.Http.Chunk.instDecidableEqExtensionValue.decEq (x✝ x✝¹ : ExtensionValue) : Decidable (x✝ = x✝¹)

Equations

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

def Std.Http.Chunk.instBEqExtensionValue.beq : ExtensionValue → ExtensionValue → Bool

Equations

• One or more equations did not get rendered due to their size.
• Std.Http.Chunk.instBEqExtensionValue.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.Chunk.instBEqExtensionValue : BEq ExtensionValue

Equations

• Std.Http.Chunk.instBEqExtensionValue = { beq := Std.Http.Chunk.instBEqExtensionValue.beq }

@[implicit_reducible]

instance Std.Http.Chunk.ExtensionValue.instInhabited : Inhabited ExtensionValue

Equations

• Std.Http.Chunk.ExtensionValue.instInhabited = { default := { value := "", isValidExtensionValue := Std.Http.Chunk.ExtensionValue.instInhabited._proof_1 } }

@[implicit_reducible]

instance Std.Http.Chunk.ExtensionValue.instToString : ToString ExtensionValue

Equations

• Std.Http.Chunk.ExtensionValue.instToString = { toString := fun (v : Std.Http.Chunk.ExtensionValue) => v.value }

def Std.Http.Chunk.ExtensionValue.quote (s : ExtensionValue) : String

Quotes an extension value if it contains non-token characters, otherwise returns it as-is.

Equations

• s.quote = Std.Http.Internal.quoteHttpString s.value ⋯

def Std.Http.Chunk.ExtensionValue.ofString? (s : String) : Option ExtensionValue

Attempts to create an ExtensionValue from a String, returning none if the string contains characters that cannot be encoded as an HTTP quoted-string.

Equations

• Std.Http.Chunk.ExtensionValue.ofString? s = if h : Std.Http.Chunk.IsValidExtensionValue s then some { value := s, isValidExtensionValue := h } else none

def Std.Http.Chunk.ExtensionValue.ofString! (s : String) : ExtensionValue

Creates an ExtensionValue from a string, panicking with an error message if the string contains characters that cannot be encoded as an HTTP quoted-string.

Equations

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

structure Std.Http.Chunk : Type

Represents a chunk of data with optional extensions (key-value pairs).

Reference: https://httpwg.org/specs/rfc9112.html#rfc.section.7.1

• data : ByteArray

  The byte data contained in this chunk.

• extensions : Array (ExtensionName × Option ExtensionValue)

  Optional metadata associated with this chunk as key-value pairs. Keys are validated Chunk.ExtensionName values, values are optional strings.

@[implicit_reducible]

instance Std.Http.instInhabitedChunk : Inhabited Chunk

Equations

• Std.Http.instInhabitedChunk = { default := Std.Http.instInhabitedChunk.default }

def Std.Http.instInhabitedChunk.default : Chunk

Equations

• Std.Http.instInhabitedChunk.default = { data := default, extensions := default }

def Std.Http.Chunk.empty : Chunk

An empty chunk with no data and no extensions.

Equations

• Std.Http.Chunk.empty = { data := ByteArray.empty }

def Std.Http.Chunk.ofByteArray (data : ByteArray) : Chunk

Creates a simple chunk without extensions.

Equations

• Std.Http.Chunk.ofByteArray data = { data := data }

def Std.Http.Chunk.insertExtension (chunk : Chunk) (key : ExtensionName) (value : ExtensionValue) : Chunk

Adds an extension to a chunk.

Equations

• chunk.insertExtension key value = { data := chunk.data, extensions := chunk.extensions.push (key, some value) }

def Std.Http.Chunk.toString? (chunk : Chunk) : Option String

Interprets the chunk data as a UTF-8 encoded string.

Equations

• chunk.toString? = String.fromUTF8? chunk.data

@[implicit_reducible]

instance Std.Http.Chunk.instEncodeV11 : Internal.Encode Version.v11 Chunk

Equations

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

structure Std.Http.Trailer : Type

Trailer headers sent after the final chunk in HTTP/1.1 chunked transfer encoding. Per RFC 9112 §7.1.2, trailers allow the sender to include additional metadata after the message body, such as message integrity checks or digital signatures.

• headers : Headers

  The trailer header fields as key-value pairs.

@[implicit_reducible]

instance Std.Http.instInhabitedTrailer : Inhabited Trailer

Equations

• Std.Http.instInhabitedTrailer = { default := Std.Http.instInhabitedTrailer.default }

def Std.Http.instInhabitedTrailer.default : Trailer

Equations

• Std.Http.instInhabitedTrailer.default = { headers := default }

def Std.Http.Trailer.empty : Trailer

Creates an empty trailer with no headers.

Equations

• Std.Http.Trailer.empty = { headers := Std.Http.Headers.empty }

@[inline]

def Std.Http.Trailer.insert (trailer : Trailer) (name : Header.Name) (value : Header.Value) : Trailer

Inserts a trailer header field.

Equations

• trailer.insert name value = { headers := trailer.headers.insert name value }

@[inline]

def Std.Http.Trailer.insert! (trailer : Trailer) (name value : String) : Trailer

Inserts a trailer header field from string name and value, panicking if either is invalid.

Equations

• trailer.insert! name value = { headers := trailer.headers.insert! name value }

@[inline]

def Std.Http.Trailer.get? (trailer : Trailer) (name : Header.Name) : Option Header.Value

Retrieves the first value for the given trailer header name. Returns none if absent.

Equations

• trailer.get? name = trailer.headers.get? name

@[inline]

def Std.Http.Trailer.getAll? (trailer : Trailer) (name : Header.Name) : Option (Array Header.Value)

Retrieves all values for the given trailer header name. Returns none if absent.

Equations

• trailer.getAll? name = trailer.headers.getAll? name

@[inline]

def Std.Http.Trailer.contains (trailer : Trailer) (name : Header.Name) : Bool

Checks if a trailer header with the given name exists.

Equations

• trailer.contains name = trailer.headers.contains name

@[inline]

def Std.Http.Trailer.erase (trailer : Trailer) (name : Header.Name) : Trailer

Removes a trailer header with the given name.

Equations

• trailer.erase name = { headers := trailer.headers.erase name }

@[inline]

def Std.Http.Trailer.size (trailer : Trailer) : Nat

Gets the number of trailer headers.

Equations

• trailer.size = trailer.headers.size

@[inline]

def Std.Http.Trailer.isEmpty (trailer : Trailer) : Bool

Checks if the trailer has no headers.

Equations

• trailer.isEmpty = trailer.headers.isEmpty

def Std.Http.Trailer.merge (t1 t2 : Trailer) : Trailer

Merges two trailers, accumulating values for duplicate keys from both.

Equations

• t1.merge t2 = { headers := t1.headers.merge t2.headers }

def Std.Http.Trailer.toList (trailer : Trailer) : List (Header.Name × Header.Value)

Converts the trailer headers to a list of key-value pairs.

Equations

• trailer.toList = trailer.headers.toList

def Std.Http.Trailer.toArray (trailer : Trailer) : Array (Header.Name × Header.Value)

Converts the trailer headers to an array of key-value pairs.

Equations

• trailer.toArray = trailer.headers.toArray

def Std.Http.Trailer.fold {α : Type u_1} (trailer : Trailer) (init : α) (f : α → Header.Name → Header.Value → α) : α

Folds over all key-value pairs in the trailer headers.

Equations

• trailer.fold init f = trailer.headers.fold init f

@[implicit_reducible]

instance Std.Http.Trailer.instEncodeV11 : Internal.Encode Version.v11 Trailer

Equations

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