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

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

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

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

@[implicit_reducible]

instance Std.Http.Chunk.instDecidableEqExtensionName : DecidableEq ExtensionName

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

@[implicit_reducible]

instance Std.Http.Chunk.instBEqExtensionName : BEq ExtensionName

@[implicit_reducible]

instance Std.Http.Chunk.instHashableExtensionName : Hashable ExtensionName

@[implicit_reducible]

instance Std.Http.Chunk.instInhabitedExtensionName : Inhabited ExtensionName

@[implicit_reducible]

instance Std.Http.Chunk.instToStringExtensionName : ToString ExtensionName

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.

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.

@[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

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

@[implicit_reducible]

instance Std.Http.Chunk.instReprExtensionValue : Repr ExtensionValue

@[implicit_reducible]

instance Std.Http.Chunk.instDecidableEqExtensionValue : DecidableEq ExtensionValue

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

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

@[implicit_reducible]

instance Std.Http.Chunk.instBEqExtensionValue : BEq ExtensionValue

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

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.

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.

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

def Std.Http.instInhabitedChunk.default : Chunk

def Std.Http.Chunk.empty : Chunk

An empty chunk with no data and no extensions.

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

Creates a simple chunk without extensions.

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

Adds an extension to a chunk.

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

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

@[implicit_reducible]

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

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

def Std.Http.instInhabitedTrailer.default : Trailer

def Std.Http.Trailer.empty : Trailer

Creates an empty trailer with no headers.

@[inline]

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

Inserts a trailer header field.

@[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.

@[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.

@[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.

@[inline]

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

Checks if a trailer header with the given name exists.

@[inline]

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

Removes a trailer header with the given name.

@[inline]

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

Gets the number of trailer headers.

@[inline]

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

Checks if the trailer has no headers.

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

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

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

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

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

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

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.

@[implicit_reducible]

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