Header Names

This module defines the Name type, which represents validated HTTP header names that conform to HTTP standards.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5

@[reducible, inline]

abbrev Std.Http.Header.IsValidHeaderName (s : String) : Prop

Proposition asserting that a string is a valid HTTP header name: all characters are valid token characters and the string is non-empty.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-names

Equations

• Std.Http.Header.IsValidHeaderName s = (Std.Http.Internal.isToken s = true)

structure Std.Http.Header.Name : Type

A validated HTTP header name that ensures all characters conform to HTTP standards. Header names are case-insensitive according to HTTP specifications.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-names

• value : String

  The lowercased normalized header name string.

• isValidHeaderValue : IsValidHeaderName self.value

  The proof that it's a valid header name.

• isLowerCase : Internal.IsLowerCase self.value

  The proof that we stored the header name in stored as a lower case string.

theorem Std.Http.Header.Name.ext {x y : Name} (value : x.value = y.value) : x = y

theorem Std.Http.Header.Name.ext_iff {x y : Name} : x = y ↔ x.value = y.value

@[implicit_reducible]

instance Std.Http.Header.instReprName : Repr Name

Equations

• Std.Http.Header.instReprName = { reprPrec := Std.Http.Header.instReprName.repr }

def Std.Http.Header.instReprName.repr : Name → Nat → Format

Equations

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

@[implicit_reducible]

instance Std.Http.Header.instDecidableEqName : DecidableEq Name

Equations

• Std.Http.Header.instDecidableEqName = Std.Http.Header.instDecidableEqName.decEq

def Std.Http.Header.instDecidableEqName.decEq (x✝ x✝¹ : Name) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Std.Http.Header.Name.instBEq : BEq Name

Equations

• Std.Http.Header.Name.instBEq = { beq := fun (a b : Std.Http.Header.Name) => decide (a.value = b.value) }

@[implicit_reducible]

instance Std.Http.Header.Name.instHashable : Hashable Name

Equations

• Std.Http.Header.Name.instHashable = { hash := fun (x : Std.Http.Header.Name) => hash x.value }

theorem Std.Http.Header.Name.Name.beq_eq {x y : Name} : (x == y) = (x.value == y.value)

instance Std.Http.Header.Name.instLawfulBEq : LawfulBEq Name

instance Std.Http.Header.Name.instLawfulHashable : LawfulHashable Name

@[implicit_reducible]

instance Std.Http.Header.Name.instInhabited : Inhabited Name

Equations

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

def Std.Http.Header.Name.ofString? (s : String) : Option Name

Attempts to create a Name from a String, returning none if the string contains invalid characters for HTTP header names or is empty.

Equations

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

def Std.Http.Header.Name.ofString! (s : String) : Name

Creates a Name from a string, panicking with an error message if the string contains invalid characters for HTTP header names or is empty.

Equations

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

@[inline]

def Std.Http.Header.Name.toCanonical (name : Name) : String

Converts the header name to title case (e.g., "Content-Type").

Note: some well-known headers have unconventional casing (e.g., "WWW-Authenticate"), but since HTTP header names are case-insensitive, this always uses simple capitalization.

Equations

• name.toCanonical = "-".intercalate (List.map (fun (x : String) => x.capitalize) (name.value.splitOn "-"))

def Std.Http.Header.Name.is (name : Name) (s : String) : Bool

Performs a case-insensitive comparison between a Name and a String. Returns true if they match.

Equations

• name.is s = (name.value == s.toLower)

@[implicit_reducible]

instance Std.Http.Header.Name.instToString : ToString Name

Equations

• Std.Http.Header.Name.instToString = { toString := fun (name : Std.Http.Header.Name) => name.toCanonical }

def Std.Http.Header.Name.contentType : Name

Standard Content-Type header name

Equations

• Std.Http.Header.Name.contentType = { value := "content-type", isValidHeaderValue := Std.Http.Header.Name.contentType._proof_1✝, isLowerCase := Std.Http.Header.Name.contentType._proof_2✝ }

def Std.Http.Header.Name.contentLength : Name

Standard Content-Length header name

Equations

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

def Std.Http.Header.Name.host : Name

Standard Host header name

Equations

• Std.Http.Header.Name.host = { value := "host", isValidHeaderValue := Std.Http.Header.Name.host._proof_1✝, isLowerCase := Std.Http.Header.Name.host._proof_2✝ }

def Std.Http.Header.Name.authorization : Name

Standard Authorization header name

Equations

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

def Std.Http.Header.Name.userAgent : Name

Standard User-Agent header name

Equations

• Std.Http.Header.Name.userAgent = { value := "user-agent", isValidHeaderValue := Std.Http.Header.Name.userAgent._proof_1✝, isLowerCase := Std.Http.Header.Name.userAgent._proof_2✝ }

def Std.Http.Header.Name.accept : Name

Standard Accept header name

Equations

• Std.Http.Header.Name.accept = { value := "accept", isValidHeaderValue := Std.Http.Header.Name.accept._proof_1✝, isLowerCase := Std.Http.Header.Name.accept._proof_2✝ }

def Std.Http.Header.Name.connection : Name

Standard Connection header name

Equations

• Std.Http.Header.Name.connection = { value := "connection", isValidHeaderValue := Std.Http.Header.Name.connection._proof_1✝, isLowerCase := Std.Http.Header.Name.connection._proof_2✝ }

def Std.Http.Header.Name.transferEncoding : Name

Standard Transfer-Encoding header name

Equations

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

def Std.Http.Header.Name.server : Name

Standard Server header name

Equations

• Std.Http.Header.Name.server = { value := "server", isValidHeaderValue := Std.Http.Header.Name.server._proof_1✝, isLowerCase := Std.Http.Header.Name.server._proof_2✝ }

def Std.Http.Header.Name.date : Name

Standard Date header name

Equations

• Std.Http.Header.Name.date = { value := "date", isValidHeaderValue := Std.Http.Header.Name.date._proof_1✝, isLowerCase := Std.Http.Header.Name.date._proof_2✝ }

def Std.Http.Header.Name.expect : Name

Standard Expect header name

Equations

• Std.Http.Header.Name.expect = { value := "expect", isValidHeaderValue := Std.Http.Header.Name.expect._proof_1✝, isLowerCase := Std.Http.Header.Name.expect._proof_2✝ }