HTTP Character Predicates

This module provides shared character validation predicates used across the HTTP library. All predicates in this module are ASCII-only by design (isAscii c where applicable), and intentionally exclude obs-text and all non-ASCII code points.

@[inline]

def Std.Http.Internal.Char.isAscii (c : Char) : Bool

Checks if a character is ASCII (Unicode code point < 128).

@[inline]

def Std.Http.Internal.Char.isAsciiByte (c : UInt8) : Bool

Checks if a byte represents an ASCII character (value < 128).

@[inline]

def Std.Http.Internal.Char.isDigitByte (c : UInt8) : Bool

Checks if a byte is a decimal digit (0-9).

@[inline]

def Std.Http.Internal.Char.isAlphaByte (c : UInt8) : Bool

Checks if a byte is an alphabetic character (a-z or A-Z).

@[inline]

def Std.Http.Internal.Char.tchar (c : Char) : Bool

tchar = "!" / "#" / "$" / "%" / "&" / "'" / "*" / "+" / "-" / "." / "^" / "_" / "" / "|" / "~" / DIGIT / ALPHA ; Visible token characters used to build token`.

@[inline]

def Std.Http.Internal.Char.vchar (c : Char) : Bool

vchar = %x21-7E ; Visible (printing) ASCII characters.

@[inline]

def Std.Http.Internal.Char.qdtext (c : Char) : Bool

qdtext = HTAB / SP / %x21 / %x23-5B / %x5D-7E ; ASCII-only variant (no obs-text).

@[inline]

def Std.Http.Internal.Char.quotedPairChar (c : Char) : Bool

quoted-pair = "\" ( HTAB / SP / VCHAR ) ; ASCII-only variant (no obs-text).

@[inline]

def Std.Http.Internal.Char.quotedStringChar (c : Char) : Bool

quoted-string body character class: ( qdtext / quoted-pair payload ) in ASCII-only mode.

theorem Std.Http.Internal.Char.quotedStringChar_lt_0x80 {c : Char} : quotedStringChar c = true → c < '€'

theorem Std.Http.Internal.Char.not_quotedStringChar_of_not_qdtext_not_dquote_backslash (c : Char) : c < '€' → ¬qdtext c = true ∧ ¬(decide (c = '\"') || decide (c = '\\')) = true → ¬quotedStringChar c = true

@[inline]

def Std.Http.Internal.Char.fieldVchar (c : Char) : Bool

field-vchar = VCHAR ; ASCII-only variant (no obs-text).

@[inline]

def Std.Http.Internal.Char.fieldContent (c : Char) : Bool

field-content character class: field-vchar / SP / HTAB ; ASCII-only variant (no obs-text).

@[inline]

def Std.Http.Internal.Char.ctext (c : Char) : Bool

ctext = HTAB / SP / %x21-27 / %x2A-5B / %x5D-7E ; ASCII-only variant (no obs-text).

@[inline]

def Std.Http.Internal.Char.etagc (c : Char) : Bool

etagc = "!" / %x23-7E ; ASCII-only variant (no obs-text).

@[inline]

def Std.Http.Internal.Char.ows (c : Char) : Bool

OWS = *( SP / HTAB ) (character class only)

@[inline]

def Std.Http.Internal.Char.bws (c : Char) : Bool

BWS = OWS (character class alias)

@[inline]

def Std.Http.Internal.Char.rws (c : Char) : Bool

RWS = 1*( SP / HTAB ) (character class is identical to ows)

@[inline]

def Std.Http.Internal.Char.obsText (c : Char) : Bool

obs-text = %x80-FF (and higher Unicode scalar values in this library's Char model).

@[inline]

def Std.Http.Internal.Char.reasonPhraseChar (c : Char) : Bool

reason-phrase character class: HTAB / SP / VCHAR ; ASCII-only variant (no obs-text).

Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase

@[inline]

def Std.Http.Internal.Char.isHexDigit (c : Char) : Bool

Checks if a character is a hexadecimal digit (0-9, a-f, or A-F).

@[inline]

def Std.Http.Internal.Char.isHexDigitByte (c : UInt8) : Bool

Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F).

@[inline]

def Std.Http.Internal.Char.isAlphaNum (c : UInt8) : Bool

Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z).

@[inline]

def Std.Http.Internal.Char.isAsciiAlphaNumChar (c : Char) : Bool

Checks whether c is an ASCII alphanumeric character.

@[inline]

def Std.Http.Internal.Char.isValidSchemeChar (c : Char) : Bool

Checks if a character is valid after the first character of a URI scheme. Valid characters are ASCII alphanumeric, +, -, and ..

@[inline]

def Std.Http.Internal.Char.isValidDomainNameChar (c : Char) : Bool

Checks if a character is valid for use in a domain name. Valid characters are ASCII alphanumeric, hyphens, and dots.

@[inline]

def Std.Http.Internal.Char.isUnreserved (c : UInt8) : Bool

Checks if a byte is an unreserved character according to RFC 3986. Unreserved characters are: alphanumeric, hyphen, period, underscore, and tilde.

@[inline]

def Std.Http.Internal.Char.isSubDelims (c : UInt8) : Bool

Checks if a byte is a sub-delimiter character according to RFC 3986. Sub-delimiters are: !, $, &, ', (, ), *, +, ,, ;, =.

@[inline]

def Std.Http.Internal.Char.isPChar (c : UInt8) : Bool

Checks if a byte is a valid path character (pchar) according to RFC 3986. pchar = unreserved / pct-encoded / sub-delims / ":" / "@"

Note: The percent-encoding (pct-encoded) is handled separately by isEncodedChar, so this predicate only covers the non-percent characters.

@[inline]

def Std.Http.Internal.Char.isQueryChar (c : UInt8) : Bool

Checks if a byte is a valid character in a URI query component according to RFC 3986. query = *( pchar / "/" / "?" )

@[inline]

def Std.Http.Internal.Char.isFragmentChar (c : UInt8) : Bool

Checks if a byte is a valid character in a URI fragment component according to RFC 3986. fragment = *( pchar / "/" / "?" )

@[inline]

def Std.Http.Internal.Char.isUserInfoChar (c : UInt8) : Bool

Checks if a byte is a valid character in a URI userinfo component according to RFC 3986. userinfo = *( unreserved/ sub-delims / ":" )

Note: It avoids the pct-encoded of the original grammar because it is used with Encoding.lean that provides it.

@[inline]

def Std.Http.Internal.Char.isQueryDataChar (c : UInt8) : Bool

Checks if a byte is a valid character in a URI query component, excluding the typical key/value separators & and =.

Inspired by query = *( pchar / "/" / "?" ) from RFC 3986, but disallows & and = so they can be treated as structural separators.