Skip to content

stdlib.encoding

Encoding Utilities

Generated from v0.65.7. 9 source files, 95 documented symbols.

ascii85.xi

fn ascii85_encode(data: &Vec[UInt8]) -> Str

Encodes bytes as an Ascii85 string ('!'..'u'; runs of four zero bytes collapse to 'z'). Empty input yields "". Complexity: O(n).

  • Postcondition: (data.len() == 0) => (result.len() == 0)
  • Postcondition: result.len() <= ((data.len() + 3) / 4) * 5
fn ascii85_decode(s: Str) -> Result[Vec[UInt8], Str]

Decodes an Ascii85 string back into bytes. Accepts 'z' for zero runs. Returns Err on an invalid character, a 'z' inside a group, an out-of-range group value, or a degenerate tail group. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= 4 * s.len()
fn ascii85_encode_str(s: Str) -> Str

Encodes a string's UTF-8 bytes as Ascii85. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.len() == 0)
fn ascii85_decode_str(s: Str) -> Result[Str, Str]

Decodes Ascii85 into a UTF-8 string (bytes copied verbatim; the caller is responsible for the UTF-8 validity of the decoded content). Returns Err on invalid Ascii85. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= 4 * s.len()
fn ascii85_encode_with_delim(data: &Vec[UInt8]) -> Str

Encodes bytes as Ascii85 wrapped in the Adobe delimiters "<~" and "~>". Complexity: O(n).

  • Postcondition: result.len() >= 4
  • Postcondition: result.len() <= ((data.len() + 3) / 4) * 5 + 4
fn ascii85_decode_with_delim(s: Str) -> Result[Vec[UInt8], Str]

Decodes an Ascii85 string that is wrapped in the Adobe delimiters "<~" and "~>". Returns Err if the delimiters are missing or the payload is invalid. Complexity: O(n).

  • Postcondition: (s.len() < 4) => (result.is_err)
  • Postcondition: result is Ok(_) => result.len() <= 4 * s.len()

base32.xi

fn base32_encode(data: &Vec[UInt8]) -> Str

Encodes bytes as an RFC 4648 base32 string (alphabet A-Z, 2-7), padded with '=' to a multiple of 8 characters. Complexity: O(n).

  • Postcondition: result.len() == ((data.len() + 4) / 5) * 8
fn base32_decode(s: Str) -> Result[Vec[UInt8], Str]

Decodes an RFC 4648 base32 string to bytes. Returns Err on invalid input. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= (s.len() * 5) / 8
fn base32hex_encode(data: &Vec[UInt8]) -> Str

Encodes bytes as a base32hex string (RFC 4648 section 7, alphabet 0-9, A-V), padded with '='. Complexity: O(n).

  • Postcondition: result.len() == ((data.len() + 4) / 5) * 8
fn base32_encode_lower_nopad(data: &Vec[UInt8]) -> Str

Encodes bytes as a canonical unpadded LOWERCASE RFC 4648 base32 string (alphabet a-z, 2-7; wave 166 row 46, i2p "b32" addresses / GCS object names). The output length is ceil(n * 8 / 5) with no '=' padding: ((n / 5) * 8) + (2, 4, 5, 7 for n % 5 = 1, 2, 3, 4). Decode with base32_decode (padding optional, either case). Complexity: O(n).

  • Postcondition: (data.len() == 0) => (result.len() == 0)
fn base32hex_decode(s: Str) -> Result[Vec[UInt8], Str]

Decodes a base32hex string to bytes (both digit cases accepted). Returns Err on invalid input. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= (s.len() * 5) / 8
fn base32_encode_str(s: Str) -> Str

Encodes a string's UTF-8 bytes as base32. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.len() == 0)
  • Postcondition: result.len() % 8 == 0
fn base32_decode_str(s: Str) -> Result[Str, Str]

Decodes base32 into a UTF-8 string (bytes copied verbatim; callers are responsible for UTF-8 validity). Returns Err on invalid base32. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= (s.len() * 5) / 8

base64.xi

fn base64_encode(data: &Vec[UInt8]) -> Str

Encodes bytes as a standard base64 string with mandatory '=' padding. Empty input yields "". Complexity: O(n).

  • Postcondition: result.len() == ((data.len() + 2) / 3) * 4
fn base64_decode(s: Str) -> Result[Vec[UInt8], Str]

Decodes a standard base64 string to bytes. Accepts optional '=' padding. Returns Err on a non-multiple-of-4 length or an invalid character. Complexity: O(n).

  • Postcondition: result is Ok(_) => result.len() <= (s.len() / 4) * 3
  • Postcondition: (s.len() == 0) => (result.is_ok)
fn base64_encode_str(s: Str) -> Str

Encodes a string's UTF-8 bytes as standard base64. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.len() == 0)
  • Postcondition: (s.len() > 0) => (result.len() % 4 == 0)
fn base64_decode_str(s: Str) -> Result[Str, Str]

Decodes base64 into a UTF-8 string (bytes copied verbatim; callers are responsible for UTF-8 validity). Returns Err on invalid base64. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= (s.len() / 4) * 3
fn base64_encode_padded(data: &Vec[UInt8]) -> Str

Encodes bytes as base64 with mandatory padding. Standard base64 always pads, so this is equivalent to base64_encode. Complexity: O(n).

  • Postcondition: result.len() == ((data.len() + 2) / 3) * 4
fn base64_decode_padded(s: Str) -> Result[Vec[UInt8], Str]

Decodes a base64 string that MUST carry correct padding: the string length must be a multiple of 4 and the number of trailing '=' characters must match the data length (0, 1 or 2 for full, 2- and 1-byte tails). Returns Err on malformed padding or an invalid character. Complexity: O(n).

  • Postcondition: (s.len() % 4 != 0) => (result.is_err)
  • Postcondition: (s.len() == 0) => (result.is_err)
  • Postcondition: result is Ok(_) => result.len() <= (s.len() / 4) * 3
fn base64url_encode(data: &Vec[UInt8]) -> Str

Encodes bytes as an unpadded URL-safe base64 string (alphabet A-Za-z0-9-_). Empty input yields "". Complexity: O(n).

  • Postcondition: (data.len() % 3 == 0) => (result.len() == ((data.len() + 2) / 3) * 4)
  • Postcondition: (data.len() % 3 == 1) => (result.len() == ((data.len() + 2) / 3) * 4 - 2)
  • Postcondition: (data.len() % 3 == 2) => (result.len() == ((data.len() + 2) / 3) * 4 - 1)
fn base64url_decode(s: Str) -> Result[Vec[UInt8], Str]

Decodes an unpadded URL-safe base64 string to bytes. Optional '=' padding is tolerated. Returns Err on an invalid character. Complexity: O(n).

  • Postcondition: (s.len() % 4 == 1) => (result.is_err)
  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= (s.len() * 3) / 4

encoding.xi

fn base64_encode(data: &Vec[UInt8]) -> Str

=== Base64 ===

  • Postcondition: result.len() == ((data.len() + 2) / 3) * 4

fn base64_decode(encoded: Str) -> Result[Vec[UInt8], Str]

Decode standard base64; Err on invalid input.

  • Precondition: encoded.len() % 4 == 0
  • Postcondition: result is Ok(_) => result.len() <= (encoded.len() / 4) * 3
  • Postcondition: (encoded.len() == 0) => (result.is_ok)

fn base64url_encode(data: &Vec[UInt8]) -> Str

URL-safe base64 encoding (no padding).

  • Postcondition: (data.len() % 3 == 0) => (result.len() == ((data.len() + 2) / 3) * 4)
  • Postcondition: (data.len() % 3 == 1) => (result.len() == ((data.len() + 2) / 3) * 4 - 2)
  • Postcondition: (data.len() % 3 == 2) => (result.len() == ((data.len() + 2) / 3) * 4 - 1)

fn base64url_decode(encoded: Str) -> Result[Vec[UInt8], Str]

Decode URL-safe base64; Err on invalid input.

  • Postcondition: result is Ok(_) => result.len() <= (encoded.len() * 3) / 4
  • Postcondition: (encoded.len() % 4 == 1) => (result.is_err)
  • Postcondition: (encoded.len() == 0) => (result.is_ok)

fn hex_encode(data: &Vec[UInt8]) -> Str

=== Hex ===

  • Postcondition: result.len() == data.len() * 2

fn hex_decode(encoded: Str) -> Result[Vec[UInt8], Str]

Decode hex (either case); Err on bad input.

  • Precondition: encoded.len() % 2 == 0
  • Postcondition: result is Ok(_) => result.len() == encoded.len() / 2
  • Postcondition: (encoded.len() == 0) => (result.is_ok)

fn hex_encode_upper(data: &Vec[UInt8]) -> Str

Uppercase hex encoding.

  • Postcondition: result.len() == data.len() * 2

fn url_encode(data: Str) -> Str

=== URL encoding ===

  • Postcondition: result.len() >= data.len()
  • Postcondition: result.len() <= 3 * data.len()

fn url_decode(encoded: Str) -> Result[Str, Str]

Percent-decode a URL component; Err on malformed escapes.

  • Postcondition: result is Ok(_) => result.len() <= encoded.len()
  • Postcondition: (encoded.len() == 0) => (result.is_ok)

fn percent_encode(data: Str) -> Str

=== Percent encoding ===

  • Postcondition: result.len() >= data.len()
  • Postcondition: result.len() <= 3 * data.len()

fn percent_decode(encoded: Str) -> Result[Str, Str]

Alias of url_decode (form-style percent-decoding: '+' becomes a space). The strict RFC 3986 surface that keeps '+' literal is xiom.encoding.percent.percent_decode.

  • Postcondition: result is Ok(_) => result.len() <= encoded.len()
  • Postcondition: (encoded.len() == 0) => (result.is_ok)

fn utf8_encode(s: Str) -> Vec[UInt8]

=== UTF-8 ===

  • Postcondition: result.len() >= s.len()

fn utf8_decode(data: &Vec[UInt8]) -> Result[Str, Str]

Decode UTF-8 bytes to a Str; Err on invalid sequences.

  • Postcondition: result is Ok(_) => result.len() <= data.len()
  • Postcondition: (data.len() == 0) => (result.is_ok)

fn utf8_valid(data: &Vec[UInt8]) -> Bool

True when the bytes are valid UTF-8.

  • Postcondition: result == true => utf8_decode(data) is Ok(_)
  • Postcondition: (data.len() == 0) => (result == true)

fn utf8_char_len(first_byte: UInt8) -> Int

UTF-8 sequence length implied by the first byte (0 when invalid).

  • Postcondition: result >= 1 && result <= 4
  • Postcondition: (first_byte >= 248) => (result == 1)

fn binary_to_text(data: &Vec[UInt8], format: Int) -> Str

=== Binary to text ===

  • Precondition: format >= 0 && format <= 2
  • Postcondition: format == 0 => result.len() == ((data.len() + 2) / 3) * 4
  • Postcondition: format == 1 => result.len() == data.len() * 2
  • Postcondition: format == 2 && data.len() % 3 == 0 => result.len() == ((data.len() + 2) / 3) * 4
  • Postcondition: format == 2 && data.len() % 3 == 1 => result.len() == ((data.len() + 2) / 3) * 4 - 2
  • Postcondition: format == 2 && data.len() % 3 == 2 => result.len() == ((data.len() + 2) / 3) * 4 - 1

fn text_to_binary(text: Str, format: Int) -> Result[Vec[UInt8], Str]

Encode text into bytes using the given format code; Err on unknown format.

  • Precondition: format >= 0 && format <= 2
  • Postcondition: format == 0 => (result is Ok(_) => result.len() <= (text.len() / 4) * 3)
  • Postcondition: format == 1 => (result is Ok(_) => result.len() == text.len() / 2)
  • Postcondition: format == 2 => (result is Ok(_) => result.len() <= (text.len() / 4) * 3)

fn base32_encode(data: &Vec[UInt8]) -> Str

Encodes bytes to a Base32 string using RFC 4648 alphabet (A-Z, 2-7). Processes 5-byte blocks into 8 Base32 characters. Padding with '=' to multiple of 8. Complexity: O(n), n = data length.

  • Postcondition: result.len() == ((data.len() + 4) / 5) * 8

fn base32_decode(encoded: Str) -> Result[Vec[UInt8], Str]

Decodes a Base32 string (RFC 4648, with optional '=' padding). Returns the decoded bytes or an error string. Complexity: O(n), n = encoded string length.

  • Postcondition: (encoded.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= (encoded.len() * 5) / 8

fn base16_encode(data: &Vec[UInt8]) -> Str

Alias for hex_encode. Converts bytes to lowercase hex string.

  • Postcondition: result.len() == data.len() * 2

fn int_to_hex(n: Int) -> Str

Converts an integer to a lowercase hexadecimal string. Complexity: O(log16(n)).

  • Postcondition: (n == 0) => (result.len() == 1)
  • Postcondition: result.len() <= 16
  • Postcondition: (n > 0) => (result.len() >= 1)
  • Postcondition: (n < 0 && 0 - n > 0) => (result.len() >= 1)

fn hex_to_int(s: Str) -> Option[Int]

Converts a hexadecimal string to an integer. Returns None if the string contains invalid hex characters. Complexity: O(n), n = string length.

  • Postcondition: (s.len() == 0) => (result.is_none)
  • Postcondition: result.is_some => (s.len() > 0)

fn base64_encode_str(s: Str) -> Str

Encodes a string to Base64 by first converting to UTF-8 bytes. Complexity: O(n), n = string length.

  • Precondition: true
  • Postcondition: (s.len() == 0) => (result.len() == 0)
  • Postcondition: (s.len() > 0) => (result.len() % 4 == 0)

fn base64_decode_str(encoded: Str) -> Result[Str, Str]

Decodes a Base64 string and returns the original string. Complexity: O(n), n = encoded string length.

  • Postcondition: (encoded.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= (encoded.len() / 4) * 3

hex.xi

fn hex_encode(data: &Vec[UInt8]) -> Str

Encodes a byte vector as a lowercase hexadecimal string (two digits per byte). Empty input yields "". Complexity: O(n).

  • Postcondition: result.len() == data.len() * 2
fn hex_decode(s: Str) -> Result[Vec[UInt8], Str]

Decodes a hexadecimal string into bytes. Accepts both digit cases. Returns Err on an odd length or an invalid hex character. Complexity: O(n).

  • Postcondition: (s.len() % 2 != 0) => (result.is_err)
  • Postcondition: result is Ok(_) => result.len() == s.len() / 2
fn hex_encode_upper(data: &Vec[UInt8]) -> Str

Encodes a byte vector as an uppercase hexadecimal string. Complexity: O(n).

  • Postcondition: result.len() == data.len() * 2
fn hex_encode_str(s: Str) -> Str

Encodes the UTF-8 bytes of a string as lowercase hex. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.len() == 0)
  • Postcondition: result.len() % 2 == 0
fn hex_decode_str(s: Str) -> Result[Str, Str]

Decodes a hex string back into a string (decoded bytes copied verbatim; callers are responsible for UTF-8 validity). Returns Err on invalid hex. Complexity: O(n).

  • Postcondition: (s.len() % 2 != 0) => (result.is_err)
  • Postcondition: result is Ok(_) => result.len() <= s.len() / 2
fn hex_encode_int(n: Int) -> Str

Encodes an integer as a lowercase hex string (no sign, no prefix; 0 -> "0"). Complexity: O(log16(n)).

  • Postcondition: (n == 0) => (result.len() == 1)
  • Postcondition: result.len() <= 16
  • Postcondition: (n > 0) => (result.len() >= 1)
  • Postcondition: (n < 0 && 0 - n > 0) => (result.len() >= 1)
fn hex_decode_int(s: Str) -> Result[Int, Str]

Parses a hex string into an integer. Returns Err on an empty string or an invalid hex character. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_err)
  • Postcondition: result is Ok(_) => s.len() > 0
fn hex_nibble_to_int(c: Char) -> Option[Int]

The numeric value of a hex digit character (0-15), or None if c is not a hex digit. Complexity: O(1).

  • Postcondition: (c == '') => (result.is_none)
fn hex_int_to_nibble(n: Int) -> Char

The hex digit character for a 0-15 value (lowercase). Returns '\0' for a value outside that range. Complexity: O(1).

  • Postcondition: (n < 0 || n > 15) => (result == '')
  • Postcondition: (n >= 0 && n <= 15) => (result != '')

idna.xi

fn idna_split_labels(domain: Str) -> Vec[Str]

Splits a domain at the dot separators. Empty labels (e.g. a trailing dot) are preserved. Complexity: O(n).

  • Postcondition: result.len() >= 1
fn idna_join_labels(labels: &Vec[Str]) -> Str

Joins labels back into a domain with '.' separators. Complexity: O(n * total length).

  • Postcondition: (labels.len() == 0) => (result.len() == 0)
  • Postcondition: (labels.len() > 0) => (result.len() >= labels.len() - 1)
fn idna_to_ascii(s: Str) -> Result[Str, Str]

Converts a Unicode domain to its ASCII A-label form: ASCII labels are lowercased and kept; non-ASCII labels are Punycode-encoded with the "xn--" prefix. Returns Err on an empty domain, an oversized label/domain, or a punycode failure. Complexity: O(sum of label^2).

  • Postcondition: (s.len() == 0) => (result.is_err)
  • Postcondition: result is Ok(_) => result.len() >= 1 && result.len() <= 253
fn idna_to_unicode(s: Str) -> Result[Str, Str]

Converts an A-label domain to Unicode: labels with the "xn--" prefix are Punycode-decoded, all others pass through. Returns Err on a punycode failure. Complexity: O(sum of label^2).

  • Postcondition: (s.len() == 0) => (result.is_ok)
fn idna_is_valid(s: Str) -> Bool

Reports whether a domain conforms to IDNA requirements: total length at most 253 bytes, every label 1..63 bytes, ASCII-only, LDH-shaped (or a valid "xn--" A-label whose payload decodes), and neither starting nor ending with a hyphen. Returns false for any violation. Complexity: O(total length + sum of label^2).

  • Postcondition: (s.len() == 0) => (result == false)
  • Postcondition: (result == true) => (s.len() >= 1 && s.len() <= 253)
fn idna_uts46_normalize(s: Str) -> Result[Str, Str]

Applies the simplified UTS-46 mapping to a domain string: ASCII uppercasing, fullwidth-to-ASCII and ideographic-space mapping, and rejection of control/surrogate characters. (NFC normalization is omitted; the code points are otherwise preserved.) Returns Err on a disallowed character. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= s.len()
fn idna_nameprep(s: Str) -> Result[Str, Str]

Applies the older Nameprep profile (RFC 3491 subset) to a domain string: case folding (ASCII lowercase), rejection of whitespace, control and surrogate characters. Returns Err on a disallowed character. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result.is_ok)
  • Postcondition: result is Ok(_) => result.len() <= s.len()
fn idna_is_bidi_valid(s: Str) -> Bool

Reports whether s satisfies the IDNA bidi rule (RFC 5893 subset): a label containing an RTL code point must start with an RTL code point, end with an RTL code point or a digit, and contain no LTR letters; labels with no RTL code point are always acceptable. Applies to every dot-separated label. Complexity: O(n).

  • Postcondition: (s.len() == 0) => (result == true)

le.xi

fn write_u16_le(out: &mut Vec[UInt8], v: Int) -> Result[Unit, Str]

Append v as a little-endian UInt16; Err when v < 0 or v > 0xFFFF.

  • Postcondition: (v < 0 || v > 65535) => (result.is_err)
  • Postcondition: (v >= 0 && v <= 65535) => (result.is_ok)
  • Postcondition: (v >= 0 && v <= 65535) => (out.len() == out.len()@pre + 2)
fn write_u24_le(out: &mut Vec[UInt8], v: Int) -> Result[Unit, Str]

Append v as a little-endian 24-bit value; Err when v < 0 or v > 0xFFFFFF.

  • Postcondition: (v < 0 || v > 16777215) => (result.is_err)
  • Postcondition: (v >= 0 && v <= 16777215) => (result.is_ok)
  • Postcondition: (v >= 0 && v <= 16777215) => (out.len() == out.len()@pre + 3)
fn write_u32_le(out: &mut Vec[UInt8], v: Int) -> Result[Unit, Str]

Append v as a little-endian UInt32; Err when v < 0 or v > 0xFFFFFFFF.

  • Postcondition: (v < 0 || v > 4294967295) => (result.is_err)
  • Postcondition: (v >= 0 && v <= 4294967295) => (result.is_ok)
  • Postcondition: (v >= 0 && v <= 4294967295) => (out.len() == out.len()@pre + 4)
fn write_u64_le(out: &mut Vec[UInt8], v: Int) -> Result[Unit, Str]

Append v as a little-endian UInt64 (accepted domain 0..=INT64_MAX); Err when v < 0.

  • Postcondition: (v < 0) => (result.is_err)
fn write_u16_be(out: &mut Vec[UInt8], v: Int) -> Result[Unit, Str]

Append v as a big-endian UInt16; Err when v < 0 or v > 0xFFFF.

  • Postcondition: (v < 0 || v > 65535) => (result.is_err)
  • Postcondition: (v >= 0 && v <= 65535) => (result.is_ok)
  • Postcondition: (v >= 0 && v <= 65535) => (out.len() == out.len()@pre + 2)
fn write_u24_be(out: &mut Vec[UInt8], v: Int) -> Result[Unit, Str]

Append v as a big-endian 24-bit value; Err when v < 0 or v > 0xFFFFFF.

  • Postcondition: (v < 0 || v > 16777215) => (result.is_err)
  • Postcondition: (v >= 0 && v <= 16777215) => (result.is_ok)
  • Postcondition: (v >= 0 && v <= 16777215) => (out.len() == out.len()@pre + 3)
fn write_u32_be(out: &mut Vec[UInt8], v: Int) -> Result[Unit, Str]

Append v as a big-endian UInt32; Err when v < 0 or v > 0xFFFFFFFF.

  • Postcondition: (v < 0 || v > 4294967295) => (result.is_err)
fn write_u64_be(out: &mut Vec[UInt8], v: Int) -> Result[Unit, Str]

Append v as a big-endian UInt64 (accepted domain 0..=INT64_MAX); Err when v < 0.

  • Postcondition: (v < 0) => (result.is_err)
  • Postcondition: (v >= 0) => (result.is_ok)
  • Postcondition: (v >= 0) => (out.len() == out.len()@pre + 8)
fn read_u16_le(data: &Vec[UInt8], pos: Int) -> Result[Int, Str]

Read a little-endian UInt16 at pos; Err when pos < 0 or fewer than two bytes remain.

  • Postcondition: (pos < 0 || pos + 2 > data.len()) => (result.is_err)
  • Postcondition: (pos >= 0 && pos + 2 <= data.len()) => (result.is_ok)
fn read_u24_le(data: &Vec[UInt8], pos: Int) -> Result[Int, Str]

Read a little-endian 24-bit value at pos; Err when pos < 0 or fewer than three bytes remain.

  • Postcondition: (pos < 0 || pos + 3 > data.len()) => (result.is_err)
  • Postcondition: (pos >= 0 && pos + 3 <= data.len()) => (result.is_ok)
fn read_u32_le(data: &Vec[UInt8], pos: Int) -> Result[Int, Str]

Read a little-endian UInt32 at pos; Err when pos < 0 or fewer than four bytes remain.

  • Postcondition: (pos < 0) => (result.is_err)
fn read_u64_le(data: &Vec[UInt8], pos: Int) -> Result[Int, Str]

Read a little-endian UInt64 at pos; Err when pos < 0 or fewer than eight bytes remain. The return carries the raw 64-bit pattern (two's complement when the top bit is set), which write_u64_le reproduces for the accepted domain.

  • Postcondition: (pos < 0) => (result.is_err)
fn read_u16_be(data: &Vec[UInt8], pos: Int) -> Result[Int, Str]

Read a big-endian UInt16 at pos; Err when pos < 0 or fewer than two bytes remain.

  • Postcondition: (pos < 0 || pos + 2 > data.len()) => (result.is_err)
  • Postcondition: (pos >= 0 && pos + 2 <= data.len()) => (result.is_ok)
fn read_u24_be(data: &Vec[UInt8], pos: Int) -> Result[Int, Str]

Read a big-endian 24-bit value at pos; Err when pos < 0 or fewer than three bytes remain.

  • Postcondition: (pos < 0 || pos + 3 > data.len()) => (result.is_err)
  • Postcondition: (pos >= 0 && pos + 3 <= data.len()) => (result.is_ok)
fn read_u32_be(data: &Vec[UInt8], pos: Int) -> Result[Int, Str]

Read a big-endian UInt32 at pos; Err when pos < 0 or fewer than four bytes remain.

  • Postcondition: (pos < 0) => (result.is_err)
fn read_u64_be(data: &Vec[UInt8], pos: Int) -> Result[Int, Str]

Read a big-endian UInt64 at pos; Err when pos < 0 or fewer than eight bytes remain. The return carries the raw 64-bit pattern (two's complement when the top bit is set).

  • Postcondition: (pos < 0 || pos + 8 > data.len()) => (result.is_err)
  • Postcondition: (pos >= 0 && pos + 8 <= data.len()) => (result.is_ok)

percent.xi

fn percent_encode(s: Str) -> Str

Percent-encodes every non-unreserved character of s per its UTF-8 bytes; spaces become '%20'. Unreserved characters (A-Z a-z 0-9 - _ . ~) pass through. Complexity: O(n).

  • Postcondition: result.len() >= s.len()
  • Postcondition: result.len() <= 3 * s.len()
fn percent_decode(s: Str) -> Result[Str, Str]

Decodes percent-escapes in s. '+' is left as a literal '+'. Returns Err on a truncated or malformed escape. Complexity: O(n).

  • Postcondition: result is Ok(_) => result.len() <= 2 * s.len()
  • Postcondition: (s.len() == 0) => (result.is_ok)
fn percent_encode_component(s: Str) -> Str

Percent-encodes a single URL path or query component: only unreserved characters pass through; everything else -- including '/', '?', '&', '=' -- is percent-encoded per UTF-8 byte. Complexity: O(n).

  • Postcondition: result.len() >= s.len()
  • Postcondition: result.len() <= 3 * s.len()
fn percent_decode_component(s: Str) -> Result[Str, Str]

Decodes a URL component: '%XX' escapes are decoded; '+' is left as a literal '+'. Returns Err on a truncated or malformed escape. Complexity: O(n).

  • Postcondition: result is Ok(_) => result.len() <= 2 * s.len()
  • Postcondition: (s.len() == 0) => (result.is_ok)
fn percent_encode_bytes(data: &Vec[UInt8]) -> Str

Percent-encodes raw bytes: unreserved ASCII bytes pass through, all other bytes become '%XX'. Complexity: O(n).

  • Postcondition: result.len() >= data.len()
  • Postcondition: result.len() <= 3 * data.len()
fn percent_decode_bytes(s: Str) -> Result[Vec[UInt8], Str]

Decodes percent-escapes into bytes; '+' is left as a literal '+'. Returns Err on a truncated or malformed escape. Complexity: O(n).

  • Postcondition: result is Ok(_) => result.len() <= 2 * s.len()
  • Postcondition: (s.len() == 0) => (result.is_ok)
fn percent_encode_www_form(s: Str) -> Str

Encodes as application/x-www-form-urlencoded: spaces become '+', all other non-unreserved characters are percent-encoded per UTF-8 byte. Complexity: O(n).

  • Postcondition: result.len() >= s.len()
  • Postcondition: result.len() <= 3 * s.len()
fn percent_encode_keep(s: Str, keep: Str) -> Str

Percent-encodes s but keeps every single-byte character of the keep byte set literal (uppercase hex escapes; wave 166 row 46). For example percent_encode_keep("/a b", "/") encodes the space only. Multi-byte characters are always encoded. Complexity: O(n * |keep|).

  • Postcondition: result.len() >= s.len()
  • Postcondition: result.len() <= 3 * s.len()
fn percent_encode_path(s: Str) -> Str

Path-segment-aware percent-encoder (wave 166 row 46; requester gcp -- GCS object paths): unreserved characters and '/' pass through, everything else is percent-encoded per UTF-8 byte with UPPERCASE hex. Complexity: O(n).

  • Postcondition: result.len() >= s.len()
  • Postcondition: result.len() <= 3 * s.len()
fn percent_decode_www_form(s: Str) -> Result[Str, Str]

Decodes a form body: '+' becomes a space and '%XX' escapes are decoded. Returns Err on a truncated or malformed escape. Complexity: O(n).

  • Postcondition: result is Ok(_) => result.len() <= 2 * s.len()
  • Postcondition: (s.len() == 0) => (result.is_ok)

punycode.xi

fn punycode_adapt(delta: Int, numpoints: Int, firsttime: Bool) -> Int

The RFC-3492 bias adaptation function. Maps a delta to a new bias value. Complexity: O(log delta).

  • Precondition: numpoints > 0
  • Precondition: delta >= 0
  • Postcondition: result >= 0
fn punycode_encode_digit(d: Int) -> Char

Maps a 0-35 value to its Punycode digit character (a-z, then 0-9). Returns '\0' for a value outside 0..35. Complexity: O(1).

  • Postcondition: (d < 0 || d > 35) => (result == '')
  • Postcondition: (d >= 0 && d <= 35) => (result != '')
fn punycode_decode_digit(c: Char) -> Int

Maps a Punycode digit character back to a 0-35 value; -1 for invalid. Complexity: O(1).

  • Postcondition: result >= -1 && result <= 35
fn punycode_encode(s: Str) -> Result[Str, Str]

Encodes a single Unicode label to Punycode (RFC 3492 section 6.3). Returns Err on an invalid code point or an arithmetic overflow. Complexity: O(n^2), n = label length in code points.

  • Postcondition: (s.len() == 0) => (result.is_ok)
fn punycode_decode(s: Str) -> Result[Str, Str]

Decodes a Punycode label to Unicode (RFC 3492 section 6.2). Returns Err on an invalid digit, a truncated sequence, an overflow, a basic decoded code point, or an invalid code point. Complexity: O(n^2), n = encoded length.

  • Postcondition: (s.len() == 0) => (result.is_ok)
fn punycode_encode_domain(domain: Str) -> Result[Str, Str]

Encodes every label of a full domain: ASCII labels pass through unchanged, non-ASCII labels are Punycode-encoded and prefixed with "xn--" (RFC 3490 A-label form). Empty labels are preserved. Returns Err on a punycode failure. Complexity: O(sum of label^2).

  • Postcondition: (domain.len() == 0) => (result.is_ok)
fn punycode_decode_domain(domain: Str) -> Result[Str, Str]

Decodes every label of an A-label domain: labels starting with "xn--" (case-insensitive) are Punycode-decoded, all others pass through. Empty labels are preserved. Returns Err on a punycode failure. Complexity: O(sum of label^2).

  • Postcondition: (domain.len() == 0) => (result.is_ok)