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).

Equations

• Std.Http.Internal.Char.isAscii c = decide (c.toNat < 128)

@[inline]

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

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

Equations

• Std.Http.Internal.Char.isAsciiByte c = decide (c < 128)

@[inline]

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

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

Equations

• Std.Http.Internal.Char.isDigitByte c = (decide (c ≥ '0'.toUInt8) && decide (c ≤ '9'.toUInt8))

@[inline]

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

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

Equations

• Std.Http.Internal.Char.isAlphaByte c = (decide (c ≥ 'A'.toUInt8) && decide (c ≤ 'Z'.toUInt8) || decide (c ≥ 'a'.toUInt8) && decide (c ≤ 'z'.toUInt8))

@[inline]

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

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

Equations

• Std.Http.Internal.Char.tchar '!' = (true || '!'.isDigit || '!'.isAlpha)
• Std.Http.Internal.Char.tchar '#' = (true || '#'.isDigit || '#'.isAlpha)
• Std.Http.Internal.Char.tchar '$' = (true || '$'.isDigit || '$'.isAlpha)
• Std.Http.Internal.Char.tchar '%' = (true || '%'.isDigit || '%'.isAlpha)
• Std.Http.Internal.Char.tchar '&' = (true || '&'.isDigit || '&'.isAlpha)
• Std.Http.Internal.Char.tchar '\'' = (true || '\''.isDigit || '\''.isAlpha)
• Std.Http.Internal.Char.tchar '*' = (true || '*'.isDigit || '*'.isAlpha)
• Std.Http.Internal.Char.tchar '+' = (true || '+'.isDigit || '+'.isAlpha)
• Std.Http.Internal.Char.tchar '-' = (true || '-'.isDigit || '-'.isAlpha)
• Std.Http.Internal.Char.tchar '.' = (true || '.'.isDigit || '.'.isAlpha)
• Std.Http.Internal.Char.tchar '^' = (true || '^'.isDigit || '^'.isAlpha)
• Std.Http.Internal.Char.tchar '_' = (true || '_'.isDigit || '_'.isAlpha)
• Std.Http.Internal.Char.tchar '`' = (true || '`'.isDigit || '`'.isAlpha)
• Std.Http.Internal.Char.tchar '|' = (true || '|'.isDigit || '|'.isAlpha)
• Std.Http.Internal.Char.tchar '~' = (true || '~'.isDigit || '~'.isAlpha)
• Std.Http.Internal.Char.tchar c = (false || c.isDigit || c.isAlpha)

@[inline]

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

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

Equations

• Std.Http.Internal.Char.vchar c = decide (c ≥ '!' ∧ c ≤ '~')

@[inline]

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

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

Equations

• Std.Http.Internal.Char.qdtext '\t' = (true || decide ('#' ≤ '\t' ∧ '\t' ≤ '[') || decide (']' ≤ '\t' ∧ '\t' ≤ '~'))
• Std.Http.Internal.Char.qdtext ' ' = (true || decide ('#' ≤ ' ' ∧ ' ' ≤ '[') || decide (']' ≤ ' ' ∧ ' ' ≤ '~'))
• Std.Http.Internal.Char.qdtext '!' = (true || decide ('#' ≤ '!' ∧ '!' ≤ '[') || decide (']' ≤ '!' ∧ '!' ≤ '~'))
• Std.Http.Internal.Char.qdtext c = (false || decide ('#' ≤ c ∧ c ≤ '[') || decide (']' ≤ c ∧ c ≤ '~'))

@[inline]

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

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

Equations

• Std.Http.Internal.Char.quotedPairChar '\t' = (true || Std.Http.Internal.Char.vchar '\t')
• Std.Http.Internal.Char.quotedPairChar ' ' = (true || Std.Http.Internal.Char.vchar ' ')
• Std.Http.Internal.Char.quotedPairChar c = (false || Std.Http.Internal.Char.vchar c)

@[inline]

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

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

Equations

• Std.Http.Internal.Char.quotedStringChar c = (Std.Http.Internal.Char.qdtext c || Std.Http.Internal.Char.quotedPairChar c)

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).

Equations

• Std.Http.Internal.Char.fieldVchar c = Std.Http.Internal.Char.vchar c

@[inline]

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

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

Equations

• Std.Http.Internal.Char.fieldContent ' ' = (Std.Http.Internal.Char.fieldVchar ' ' || true)
• Std.Http.Internal.Char.fieldContent '\t' = (Std.Http.Internal.Char.fieldVchar '\t' || true)
• Std.Http.Internal.Char.fieldContent c = (Std.Http.Internal.Char.fieldVchar c || false)

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

Equations

• Std.Http.Internal.Char.ctext '\t' = (true || decide ('!' ≤ '\t' ∧ '\t' ≤ '\'') || decide ('*' ≤ '\t' ∧ '\t' ≤ '[') || decide (']' ≤ '\t' ∧ '\t' ≤ '~'))
• Std.Http.Internal.Char.ctext ' ' = (true || decide ('!' ≤ ' ' ∧ ' ' ≤ '\'') || decide ('*' ≤ ' ' ∧ ' ' ≤ '[') || decide (']' ≤ ' ' ∧ ' ' ≤ '~'))
• Std.Http.Internal.Char.ctext c = (false || decide ('!' ≤ c ∧ c ≤ '\'') || decide ('*' ≤ c ∧ c ≤ '[') || decide (']' ≤ c ∧ c ≤ '~'))

@[inline]

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

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

Equations

• Std.Http.Internal.Char.etagc c = (decide (c = '!') || decide ('#' ≤ c ∧ c ≤ '~'))

@[inline]

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

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

Equations

• Std.Http.Internal.Char.ows ' ' = true
• Std.Http.Internal.Char.ows '\t' = true
• Std.Http.Internal.Char.ows c = false

@[inline]

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

BWS = OWS (character class alias)

Equations

• Std.Http.Internal.Char.bws c = Std.Http.Internal.Char.ows c

@[inline]

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

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

Equations

• Std.Http.Internal.Char.rws c = Std.Http.Internal.Char.ows c

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

Equations

• Std.Http.Internal.Char.obsText c = decide (128 ≤ c.toNat)

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

Equations

• Std.Http.Internal.Char.reasonPhraseChar '\t' = (true || Std.Http.Internal.Char.vchar '\t')
• Std.Http.Internal.Char.reasonPhraseChar ' ' = (true || Std.Http.Internal.Char.vchar ' ')
• Std.Http.Internal.Char.reasonPhraseChar c = (false || Std.Http.Internal.Char.vchar c)

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

Equations

• Std.Http.Internal.Char.isHexDigit 'a' = (true || 'a'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'b' = (true || 'b'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'c' = (true || 'c'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'd' = (true || 'd'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'e' = (true || 'e'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'f' = (true || 'f'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'A' = (true || 'A'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'B' = (true || 'B'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'C' = (true || 'C'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'D' = (true || 'D'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'E' = (true || 'E'.isDigit)
• Std.Http.Internal.Char.isHexDigit 'F' = (true || 'F'.isDigit)
• Std.Http.Internal.Char.isHexDigit c = (false || c.isDigit)

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

Equations

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

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

Equations

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

@[inline]

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

Checks whether c is an ASCII alphanumeric character.

Equations

• Std.Http.Internal.Char.isAsciiAlphaNumChar c = (Std.Http.Internal.Char.isAscii c && (c.isDigit || c.isAlpha))

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

Equations

• Std.Http.Internal.Char.isValidSchemeChar '+' = (Std.Http.Internal.Char.isAsciiAlphaNumChar '+' || true)
• Std.Http.Internal.Char.isValidSchemeChar '-' = (Std.Http.Internal.Char.isAsciiAlphaNumChar '-' || true)
• Std.Http.Internal.Char.isValidSchemeChar '.' = (Std.Http.Internal.Char.isAsciiAlphaNumChar '.' || true)
• Std.Http.Internal.Char.isValidSchemeChar c = (Std.Http.Internal.Char.isAsciiAlphaNumChar c || false)

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

Equations

• Std.Http.Internal.Char.isValidDomainNameChar '-' = (Std.Http.Internal.Char.isAsciiAlphaNumChar '-' || true)
• Std.Http.Internal.Char.isValidDomainNameChar '.' = (Std.Http.Internal.Char.isAsciiAlphaNumChar '.' || true)
• Std.Http.Internal.Char.isValidDomainNameChar c = (Std.Http.Internal.Char.isAsciiAlphaNumChar c || false)

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

Equations

• Std.Http.Internal.Char.isUnreserved c = (Std.Http.Internal.Char.isAlphaNum c || (decide (c = '-'.toUInt8) || decide (c = '.'.toUInt8) || decide (c = '_'.toUInt8) || decide (c = '~'.toUInt8)))

@[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: !, $, &, ', (, ), *, +, ,, ;, =.

Equations

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

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

Equations

• Std.Http.Internal.Char.isPChar c = (Std.Http.Internal.Char.isUnreserved c || Std.Http.Internal.Char.isSubDelims c || decide (c = ':'.toUInt8) || decide (c = '@'.toUInt8))

@[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 / "/" / "?" )

Equations

• Std.Http.Internal.Char.isQueryChar c = (Std.Http.Internal.Char.isPChar c || decide (c = '/'.toUInt8) || decide (c = '?'.toUInt8))

@[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 / "/" / "?" )

Equations

• Std.Http.Internal.Char.isFragmentChar c = (Std.Http.Internal.Char.isPChar c || decide (c = '/'.toUInt8) || decide (c = '?'.toUInt8))

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

Equations

• Std.Http.Internal.Char.isUserInfoChar c = (Std.Http.Internal.Char.isUnreserved c || Std.Http.Internal.Char.isSubDelims c || decide (c = ':'.toUInt8))

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

Equations

• Std.Http.Internal.Char.isQueryDataChar c = (Std.Http.Internal.Char.isQueryChar c && decide (c ≠ '&'.toUInt8) && decide (c ≠ '='.toUInt8))