URI Encoding

This module provides utilities for percent-encoding URI components according to RFC 3986. It includes character validation, encoding/decoding functions, and types that maintain encoding invariants through Lean's dependent type system.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-2.1

def Std.Http.URI.isEncodedChar (rule : UInt8 → Bool) (c : UInt8) : Bool

Checks if a byte is a valid character in a percent-encoded URI component. Valid characters are unreserved characters or the percent sign (for escape sequences).

def Std.Http.URI.isEncodedQueryChar (rule : UInt8 → Bool) (c : UInt8) : Bool

Checks if a byte is valid in a percent-encoded query string component. Extends isEncodedChar to also allow '+' which represents space in application/x-www-form-urlencoded format.

@[reducible, inline]

abbrev Std.Http.URI.IsAllowedEncodedChars (rule : UInt8 → Bool) (s : ByteArray) : Prop

Checks if all characters in a ByteArray are allowed in an encoded URI component. This is a fast check that only verifies the character set, not full encoding validity.

@[implicit_reducible]

instance Std.Http.URI.instDecidableIsAllowedEncodedChars {r : UInt8 → Bool} {s : ByteArray} : Decidable (IsAllowedEncodedChars r s)

@[reducible, inline]

abbrev Std.Http.URI.IsAllowedEncodedQueryChars (rule : UInt8 → Bool) (s : ByteArray) : Prop

Checks if all characters in a ByteArray are allowed in an encoded query parameter. Allows '+' as an alternative encoding for space (application/x-www-form-urlencoded).

@[implicit_reducible]

instance Std.Http.URI.instDecidableIsAllowedEncodedQueryChars {r : UInt8 → Bool} {s : ByteArray} : Decidable (IsAllowedEncodedQueryChars r s)

def Std.Http.URI.isValidPercentEncoding (ba : ByteArray) : Bool

Validates that all percent signs in a byte array are followed by exactly two hexadecimal digits. This ensures proper percent-encoding according to RFC 3986.

For example:

• %20 is valid (percent followed by two hex digits)
• % is invalid (percent with no following digits)
• %2 is invalid (percent followed by only one digit)
• %GG is invalid (percent followed by non-hex characters)

def Std.Http.URI.hexDigit (n : UInt8) : UInt8

Converts a nibble (4-bit value, 0-15) to its hexadecimal digit representation. Returns '0'-'9' for values 0-9, and 'A'-'F' for values 10-15.

def Std.Http.URI.hexDigitToUInt8? (c : UInt8) : Option UInt8

Converts a hexadecimal digit character to its numeric value (0-15). Returns none if the character is not a valid hex digit.

theorem Std.Http.URI.all_of_all_of_imp {p q : UInt8 → Bool} {b : ByteArray} (h : b.data.all p = true) (imp : ∀ (c : UInt8), p c = true → q c = true) : b.data.all q = true

theorem Std.Http.URI.isValidUTF8_of_isAsciiByte (ba : ByteArray) (s : ba.data.all Internal.Char.isAsciiByte = true) : ba.IsValidUTF8

structure Std.Http.URI.EncodedString (r : UInt8 → Bool) : Type

A percent-encoded URI component with a compile-time proof that it contains only valid encoded characters. This provides type-safe URI encoding without runtime validation.

The invariant guarantees that the string contains only unreserved characters (alphanumeric, hyphen, period, underscore, tilde) and percent signs (for escape sequences).

• toByteArray : ByteArray

  The underlying byte array containing the percent-encoded data.

• valid : IsAllowedEncodedChars r self.toByteArray

  Proof that all characters in the byte array are valid encoded characters.

def Std.Http.URI.EncodedString.empty {r : UInt8 → Bool} : EncodedString r

Creates an empty encoded string.

@[implicit_reducible]

instance Std.Http.URI.EncodedString.instInhabited {r : UInt8 → Bool} : Inhabited (EncodedString r)

def Std.Http.URI.EncodedString.encode {r : UInt8 → Bool} (s : String) : EncodedString r

Encodes a raw string into an EncodedString with automatic proof construction. Unreserved characters (alphanumeric, hyphen, period, underscore, tilde) are kept as-is, while all other characters are percent-encoded.

def Std.Http.URI.EncodedString.ofByteArray? {r : UInt8 → Bool} (ba : ByteArray) : Option (EncodedString r)

Attempts to create an EncodedString from a ByteArray. Returns some if the byte array contains only valid encoded characters and all percent signs are followed by exactly two hex digits, none otherwise.

def Std.Http.URI.EncodedString.ofByteArray! {r : UInt8 → Bool} (ba : ByteArray) : EncodedString r

Creates an EncodedString from a ByteArray, panicking if the byte array is invalid.

def Std.Http.URI.EncodedString.ofString? {r : UInt8 → Bool} (s : String) : Option (EncodedString r)

Creates an EncodedString from a String by checking if it's already a valid percent-encoded string. Returns some if valid, none otherwise.

def Std.Http.URI.EncodedString.ofString! {r : UInt8 → Bool} (s : String) : EncodedString r

Creates an EncodedString from a String, panicking if the string is not a valid percent-encoded string.

def Std.Http.URI.EncodedString.new {r : UInt8 → Bool} (ba : ByteArray) (valid : IsAllowedEncodedChars r ba) (_validEncoding : isValidPercentEncoding ba = true) : EncodedString r

Creates an EncodedString from a ByteArray with compile-time proofs. Use this when you have proofs that the byte array is valid.

@[implicit_reducible]

instance Std.Http.URI.EncodedString.instToString {r : UInt8 → Bool} : ToString (EncodedString r)

def Std.Http.URI.EncodedString.decode {r : UInt8 → Bool} (es : EncodedString r) : Option String

Decodes an EncodedString back to a regular String. Converts percent-encoded sequences (e.g., "%20") back to their original characters. Returns none if the decoded bytes are not valid UTF-8.

@[implicit_reducible]

instance Std.Http.URI.EncodedString.instRepr {r : UInt8 → Bool} : Repr (EncodedString r)

@[implicit_reducible]

instance Std.Http.URI.EncodedString.instBEq {r : UInt8 → Bool} : BEq (EncodedString r)

@[implicit_reducible]

instance Std.Http.URI.EncodedString.instHashable {r : UInt8 → Bool} : Hashable (EncodedString r)

structure Std.Http.URI.EncodedQueryString (r : UInt8 → Bool) : Type

A percent-encoded query string component with a compile-time proof that it contains only valid encoded query characters. Extends EncodedString to support the '+' character for spaces, following the application/x-www-form-urlencoded format.

This type is specifically designed for encoding query parameters where spaces can be represented as '+' instead of "%20".

• toByteArray : ByteArray

  The underlying byte array containing the percent-encoded query data.

• valid : IsAllowedEncodedQueryChars r self.toByteArray

  Proof that all characters in the byte array are valid encoded query characters.

def Std.Http.URI.EncodedQueryString.empty {r : UInt8 → Bool} : EncodedQueryString r

Creates an empty encoded query string.

@[implicit_reducible]

instance Std.Http.URI.EncodedQueryString.instInhabited {r : UInt8 → Bool} : Inhabited (EncodedQueryString r)

def Std.Http.URI.EncodedQueryString.ofByteArray? (ba : ByteArray) (r : UInt8 → Bool := Internal.Char.isQueryChar) : Option (EncodedQueryString r)

Attempts to create an EncodedQueryString from a ByteArray. Returns some if the byte array contains only valid encoded query characters and all percent signs are followed by exactly two hex digits, none otherwise.

def Std.Http.URI.EncodedQueryString.ofByteArray! (ba : ByteArray) (r : UInt8 → Bool := Internal.Char.isQueryChar) : EncodedQueryString r

Creates an EncodedQueryString from a ByteArray, panicking if the byte array is invalid.

def Std.Http.URI.EncodedQueryString.ofString? (s : String) (r : UInt8 → Bool := Internal.Char.isQueryChar) : Option (EncodedQueryString r)

Creates an EncodedQueryString from a String by checking if it's already a valid percent-encoded string. Returns some if valid, none otherwise.

def Std.Http.URI.EncodedQueryString.ofString! (s : String) (r : UInt8 → Bool := Internal.Char.isQueryChar) : EncodedQueryString r

Creates an EncodedQueryString from a String, panicking if the string is not a valid percent-encoded string.

def Std.Http.URI.EncodedQueryString.new {r : UInt8 → Bool} (ba : ByteArray) (valid : IsAllowedEncodedQueryChars r ba) (_validEncoding : isValidPercentEncoding ba = true) : EncodedQueryString r

Creates an EncodedQueryString from a ByteArray with compile-time proofs. Use this when you have proofs that the byte array is valid.

def Std.Http.URI.EncodedQueryString.encode (s : String) (r : UInt8 → Bool := Internal.Char.isQueryChar) : EncodedQueryString r

Encodes a raw string into an EncodedQueryString with automatic proof construction. Unreserved characters are kept as-is, spaces are encoded as '+', and all other characters are percent-encoded.

def Std.Http.URI.EncodedQueryString.toString {r : UInt8 → Bool} (es : EncodedQueryString r) : String

Converts an EncodedQueryString to a String, given a proof that all characters satisfying r are ASCII.

def Std.Http.URI.EncodedQueryString.decode {r : UInt8 → Bool} (es : EncodedQueryString r) : Option String

Decodes an EncodedQueryString back to a regular String. Converts percent-encoded sequences and '+' signs back to their original characters. Returns none if the decoded bytes are not valid UTF-8.

This is almost the same code from System.Uri.UriEscape.decodeUri, but with Option instead.

@[implicit_reducible]

instance Std.Http.URI.instToStringEncodedQueryString {r : UInt8 → Bool} : ToString (EncodedQueryString r)

@[implicit_reducible]

instance Std.Http.URI.instReprEncodedQueryString {r : UInt8 → Bool} : Repr (EncodedQueryString r)

@[implicit_reducible]

instance Std.Http.URI.instBEqEncodedQueryString {r : UInt8 → Bool} : BEq (EncodedQueryString r)

@[implicit_reducible]

instance Std.Http.URI.instHashableEncodedQueryString {r : UInt8 → Bool} : Hashable (EncodedQueryString r)

@[implicit_reducible]

instance Std.Http.URI.instHashableOptionEncodedQueryString {r : UInt8 → Bool} : Hashable (Option (EncodedQueryString r))

@[reducible, inline]

abbrev Std.Http.URI.EncodedSegment : Type

A percent-encoded URI path segment. Valid characters are pchar (unreserved, sub-delims, ':', '@').

def Std.Http.URI.EncodedSegment.encode (s : String) : EncodedSegment

Encodes a raw string into an encoded path segment.

def Std.Http.URI.EncodedSegment.ofByteArray? (ba : ByteArray) : Option EncodedSegment

Attempts to create an encoded path segment from raw bytes.

def Std.Http.URI.EncodedSegment.ofByteArray! (ba : ByteArray) : EncodedSegment

Creates an encoded path segment from raw bytes, panicking on invalid encoding.

def Std.Http.URI.EncodedSegment.decode (segment : EncodedSegment) : Option String

Decodes an encoded path segment back to a UTF-8 string.

@[reducible, inline]

abbrev Std.Http.URI.EncodedFragment : Type

A percent-encoded URI fragment component. Valid characters are pchar / "/" / "?".

def Std.Http.URI.EncodedFragment.encode (s : String) : EncodedFragment

Encodes a raw string into an encoded fragment component.

def Std.Http.URI.EncodedFragment.ofByteArray? (ba : ByteArray) : Option EncodedFragment

Attempts to create an encoded fragment component from raw bytes.

def Std.Http.URI.EncodedFragment.ofByteArray! (ba : ByteArray) : EncodedFragment

Creates an encoded fragment component from raw bytes, panicking on invalid encoding.

def Std.Http.URI.EncodedFragment.decode (fragment : EncodedFragment) : Option String

Decodes an encoded fragment component back to a UTF-8 string.

@[reducible, inline]

abbrev Std.Http.URI.EncodedUserInfo : Type

A percent-encoded URI userinfo component. Valid characters are unreserved / sub-delims / ":".

def Std.Http.URI.EncodedUserInfo.encode (s : String) : EncodedUserInfo

Encodes a raw string into an encoded userinfo component.

def Std.Http.URI.EncodedUserInfo.ofByteArray? (ba : ByteArray) : Option EncodedUserInfo

Attempts to create an encoded userinfo component from raw bytes.

def Std.Http.URI.EncodedUserInfo.ofByteArray! (ba : ByteArray) : EncodedUserInfo

Creates an encoded userinfo component from raw bytes, panicking on invalid encoding.

def Std.Http.URI.EncodedUserInfo.decode (userInfo : EncodedUserInfo) : Option String

Decodes an encoded userinfo component back to a UTF-8 string.

@[reducible, inline]

abbrev Std.Http.URI.EncodedQueryParam : Type

A percent-encoded URI query parameter. Valid characters are pchar / "/" / "?" with '+' for spaces.

def Std.Http.URI.EncodedQueryParam.encode (s : String) : EncodedQueryParam

Encodes a raw string into an encoded query parameter.

def Std.Http.URI.EncodedQueryParam.ofByteArray? (ba : ByteArray) : Option EncodedQueryParam

Attempts to create an encoded query parameter from raw bytes.

def Std.Http.URI.EncodedQueryParam.ofByteArray! (ba : ByteArray) : EncodedQueryParam

Creates an encoded query parameter from raw bytes, panicking on invalid encoding.

def Std.Http.URI.EncodedQueryParam.fromString? (s : String) : Option EncodedQueryParam

Attempts to create an encoded query parameter from an encoded string.

def Std.Http.URI.EncodedQueryParam.decode (param : EncodedQueryParam) : Option String

Decodes an encoded query parameter back to a UTF-8 string.