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

Equations

• Std.Http.URI.isEncodedChar rule c = decide (Std.Http.Internal.Char.isAsciiByte c = true ∧ (rule c = true ∨ Std.Http.Internal.Char.isHexDigitByte c = true ∨ c = '%'.toUInt8))

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.

Equations

• Std.Http.URI.isEncodedQueryChar rule c = decide (Std.Http.URI.isEncodedChar rule c = true ∨ c = '+'.toUInt8)

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

Equations

• Std.Http.URI.IsAllowedEncodedChars rule s = (s.data.all (Std.Http.URI.isEncodedChar rule) = true)

@[implicit_reducible]

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

Equations

• Std.Http.URI.instDecidableIsAllowedEncodedChars = (s.data.all (Std.Http.URI.isEncodedChar r)).decEq true

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

Equations

• Std.Http.URI.IsAllowedEncodedQueryChars rule s = (s.data.all (Std.Http.URI.isEncodedQueryChar rule) = true)

@[implicit_reducible]

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

Equations

• Std.Http.URI.instDecidableIsAllowedEncodedQueryChars = (s.data.all (Std.Http.URI.isEncodedQueryChar r)).decEq true

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)

Equations

• Std.Http.URI.isValidPercentEncoding ba = Std.Http.URI.isValidPercentEncoding.loop✝ ba 0

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.

Equations

• Std.Http.URI.hexDigit n = if n < 10 then n + '0'.toUInt8 else n - 10 + 'A'.toUInt8

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.

Equations

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

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.

Equations

• Std.Http.URI.EncodedString.empty = { toByteArray := ByteArray.empty, valid := ⋯ }

@[implicit_reducible]

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

Equations

• Std.Http.URI.EncodedString.instInhabited = { default := Std.Http.URI.EncodedString.empty }

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• Std.Http.URI.EncodedString.ofString? s = Std.Http.URI.EncodedString.ofByteArray? s.toUTF8

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.

Equations

• Std.Http.URI.EncodedString.ofString! s = Std.Http.URI.EncodedString.ofByteArray! s.toUTF8

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.

Equations

• Std.Http.URI.EncodedString.new ba valid _validEncoding = { toByteArray := ba, valid := valid }

@[implicit_reducible]

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

Equations

• Std.Http.URI.EncodedString.instToString = { toString := fun (es : Std.Http.URI.EncodedString r) => { toByteArray := es.toByteArray, isValidUTF8 := ⋯ } }

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.

Equations

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

@[implicit_reducible]

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

Equations

• Std.Http.URI.EncodedString.instRepr = { reprPrec := fun (es : Std.Http.URI.EncodedString r) (n : Nat) => reprPrec (toString es) n }

@[implicit_reducible]

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

Equations

• Std.Http.URI.EncodedString.instBEq = { beq := fun (x y : Std.Http.URI.EncodedString r) => decide (x.toByteArray = y.toByteArray) }

@[implicit_reducible]

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

Equations

• Std.Http.URI.EncodedString.instHashable = { hash := fun (x : Std.Http.URI.EncodedString r) => hash x.toByteArray }

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.

Equations

• Std.Http.URI.EncodedQueryString.empty = { toByteArray := ByteArray.empty, valid := ⋯ }

@[implicit_reducible]

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

Equations

• Std.Http.URI.EncodedQueryString.instInhabited = { default := Std.Http.URI.EncodedQueryString.empty }

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.

Equations

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

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.

Equations

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

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.

Equations

• Std.Http.URI.EncodedQueryString.ofString? s r = Std.Http.URI.EncodedQueryString.ofByteArray? s.toUTF8 r

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.

Equations

• Std.Http.URI.EncodedQueryString.ofString! s r = Std.Http.URI.EncodedQueryString.ofByteArray! s.toUTF8 r

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.

Equations

• Std.Http.URI.EncodedQueryString.new ba valid _validEncoding = { toByteArray := ba, valid := 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.

Equations

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

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.

Equations

• es.toString = { toByteArray := es.toByteArray, isValidUTF8 := ⋯ }

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.

Equations

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

@[implicit_reducible]

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

Equations

• Std.Http.URI.instToStringEncodedQueryString = { toString := Std.Http.URI.EncodedQueryString.toString }

@[implicit_reducible]

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

Equations

• Std.Http.URI.instReprEncodedQueryString = { reprPrec := fun (es : Std.Http.URI.EncodedQueryString r) (n : Nat) => reprPrec (toString es) n }

@[implicit_reducible]

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

Equations

• Std.Http.URI.instBEqEncodedQueryString = { beq := fun (x y : Std.Http.URI.EncodedQueryString r) => decide (x.toByteArray = y.toByteArray) }

@[implicit_reducible]

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

Equations

• Std.Http.URI.instHashableEncodedQueryString = { hash := fun (x : Std.Http.URI.EncodedQueryString r) => hash x.toByteArray }

@[implicit_reducible]

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

Equations

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

@[reducible, inline]

abbrev Std.Http.URI.EncodedSegment : Type

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

Equations

• Std.Http.URI.EncodedSegment = Std.Http.URI.EncodedString Std.Http.Internal.Char.isPChar

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

Encodes a raw string into an encoded path segment.

Equations

• Std.Http.URI.EncodedSegment.encode s = Std.Http.URI.EncodedString.encode s

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

Attempts to create an encoded path segment from raw bytes.

Equations

• Std.Http.URI.EncodedSegment.ofByteArray? ba = Std.Http.URI.EncodedString.ofByteArray? ba

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

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

Equations

• Std.Http.URI.EncodedSegment.ofByteArray! ba = Std.Http.URI.EncodedString.ofByteArray! ba

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

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

Equations

• segment.decode = Std.Http.URI.EncodedString.decode segment

@[reducible, inline]

abbrev Std.Http.URI.EncodedFragment : Type

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

Equations

• Std.Http.URI.EncodedFragment = Std.Http.URI.EncodedString Std.Http.Internal.Char.isFragmentChar

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

Encodes a raw string into an encoded fragment component.

Equations

• Std.Http.URI.EncodedFragment.encode s = Std.Http.URI.EncodedString.encode s

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

Attempts to create an encoded fragment component from raw bytes.

Equations

• Std.Http.URI.EncodedFragment.ofByteArray? ba = Std.Http.URI.EncodedString.ofByteArray? ba

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

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

Equations

• Std.Http.URI.EncodedFragment.ofByteArray! ba = Std.Http.URI.EncodedString.ofByteArray! ba

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

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

Equations

• fragment.decode = Std.Http.URI.EncodedString.decode fragment

@[reducible, inline]

abbrev Std.Http.URI.EncodedUserInfo : Type

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

Equations

• Std.Http.URI.EncodedUserInfo = Std.Http.URI.EncodedString Std.Http.Internal.Char.isUserInfoChar

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

Encodes a raw string into an encoded userinfo component.

Equations

• Std.Http.URI.EncodedUserInfo.encode s = Std.Http.URI.EncodedString.encode s

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

Attempts to create an encoded userinfo component from raw bytes.

Equations

• Std.Http.URI.EncodedUserInfo.ofByteArray? ba = Std.Http.URI.EncodedString.ofByteArray? ba

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

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

Equations

• Std.Http.URI.EncodedUserInfo.ofByteArray! ba = Std.Http.URI.EncodedString.ofByteArray! ba

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

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

Equations

• userInfo.decode = Std.Http.URI.EncodedString.decode userInfo

@[reducible, inline]

abbrev Std.Http.URI.EncodedQueryParam : Type

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

Equations

• Std.Http.URI.EncodedQueryParam = Std.Http.URI.EncodedQueryString Std.Http.Internal.Char.isQueryDataChar

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

Encodes a raw string into an encoded query parameter.

Equations

• Std.Http.URI.EncodedQueryParam.encode s = Std.Http.URI.EncodedQueryString.encode s Std.Http.Internal.Char.isQueryDataChar

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

Attempts to create an encoded query parameter from raw bytes.

Equations

• Std.Http.URI.EncodedQueryParam.ofByteArray? ba = Std.Http.URI.EncodedQueryString.ofByteArray? ba Std.Http.Internal.Char.isQueryDataChar

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

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

Equations

• Std.Http.URI.EncodedQueryParam.ofByteArray! ba = Std.Http.URI.EncodedQueryString.ofByteArray! ba Std.Http.Internal.Char.isQueryDataChar

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

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

Equations

• Std.Http.URI.EncodedQueryParam.fromString? s = Std.Http.URI.EncodedQueryString.ofString? s Std.Http.Internal.Char.isQueryDataChar

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

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

Equations

• param.decode = Std.Http.URI.EncodedQueryString.decode param