Skip to content

stdlib.compress

Compression

Generated from v0.65.7. 12 source files, 113 documented symbols.

accept_encoding.xi

fn accept_encoding_q(header: Str, encoding: Str) -> Int

Effective q-value of encoding in header, in per-mille (0..1000). Returns -1 when the field neither names the coding nor carries a * wildcard. x-gzip counts as gzip; matching is case-insensitive. O(|h|).

  • Postcondition: result >= -1
  • Postcondition: result <= 1000
fn accept_encoding_choose(header: Str, supported: &Vec[Str]) -> Str

Choose a content coding against supported: highest q wins; ties prefer a non-identity coding, then the earlier header entry, then the earlier entry in supported. Returns the supported entry itself, "identity" when that is the only acceptable option (including the empty header), or "" when nothing is acceptable. O(|header| * |supported|).

  • Postcondition: result.len() >= 0

brotli.xi

fn brotli_is_rfc7932() -> Bool

Always false: this module does NOT implement RFC 7932 brotli (it uses a custom frame; see the module header). Real brotli: registry package xiom.brotli 0.1.0. O(1).

  • Postcondition: result == false
fn brotli_compress(data: &Vec[UInt8]) -> Vec[UInt8]

Compress at the default quality (11) and window exponent (20) into the custom NOT-RFC-7932 frame (see the module header; use the registry package xiom.brotli for real brotli). O(n * window).

  • Postcondition: result.len() >= 12
fn brotli_compress_quality(data: &Vec[UInt8], quality: Int) -> Vec[UInt8]

Compress with an explicit quality (0-11, clamped) into the custom NOT-RFC-7932 frame. The quality is recorded in the header and does not change the payload shape. Real brotli: registry package xiom.brotli.

  • Postcondition: result.len() >= 12
fn brotli_compress_window(data: &Vec[UInt8], window: Int) -> Vec[UInt8]

Compress with an explicit window size in bytes into the custom NOT-RFC-7932 frame. The base-2 logarithm is stored in the header, clamped to 10..24 (window 1KiB..16MiB). Real brotli: registry package xiom.brotli.

  • Postcondition: result.len() >= 12
fn brotli_decompress(data: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Decompress a custom NOT-RFC-7932 frame (see the module header; this does NOT read real brotli streams -- use the registry package xiom.brotli). Validates magic and the length trailer, then decompresses the payload. Returns Err on malformed input or a size mismatch.

  • Postcondition: (data.len() < 10) => (result.is_err)
fn brotli_decompress_stream(reader: Int, writer: Int) -> Result[Int, Str]

Stream-decompress between two file descriptors: reads all bytes from reader, decompresses them (custom NOT-RFC-7932 frame; real brotli: registry package xiom.brotli), writes the result to writer, and returns the number of bytes written. Errors surface as Err.

  • Postcondition: result is Ok(_) => result.value >= 0

compress.xi

type GzipCompressor

=== Gzip ===

Field Type
level Int

fn new() -> GzipCompressor

Streaming gzip compressor with the default level.

  • Postcondition: result.level == 6

fn with_level(level: Int) -> GzipCompressor

Streaming gzip compressor with a level 0..9.

  • Postcondition: result.level >= 0 && result.level <= 9

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

=== Gzip functions === Aggregate facade: delegate to the real sublib implementations (xiom.compress.gzip). The earlier RLE-based duplicates trapped on empty input (requires: data.len() > 0) and were not gzip-compatible.

  • Postcondition: result is Ok(_) => result.len() >= 18

fn gzip_compress_level(data: &Vec[UInt8], level: Int) -> Result[Vec[UInt8], Str]

Gzip-compress with a level 0..9; Err on failure.

  • Postcondition: result is Ok(_) => result.len() >= 18

fn gzip_decompress_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[UInt8], Str]

Capped variant: hard ceiling on decompressed size (bomb guard).

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

fn deflate_decompress_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[UInt8], Str]

Capped variant: hard ceiling on decompressed size (bomb guard).

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

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

Decompress gzip data; Err on malformed input.

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

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

=== Deflate / Raw ===

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

fn deflate_compress_level(data: &Vec[UInt8], level: Int) -> Result[Vec[UInt8], Str]

Deflate-compress with a level 0..9; Err on failure.

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

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

Decompress raw deflate data; Err on malformed input.

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

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

=== Zlib ===

  • Postcondition: result is Ok(_) => result.len() >= 6

fn zlib_compress_level(data: &Vec[UInt8], level: Int) -> Result[Vec[UInt8], Str]

Zlib-compress with a level 0..9; Err on failure.

  • Postcondition: result is Ok(_) => result.len() >= 6

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

Decompress zlib data; Err on malformed input.

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

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

=== Brotli === NOT RFC 7932: brotli_compress below writes the custom CE B2 CF 81 frame (see xiom.compress.brotli). Content-Encoding: br cannot be served from this module; use the registry package xiom.brotli 0.1.0 for real brotli.

  • Postcondition: result is Ok(_) => result.len() >= 8

fn brotli_compress_level(data: &Vec[UInt8], quality: Int) -> Result[Vec[UInt8], Str]

Brotli-compress with a quality 0..11 (clamped) into the custom NOT-RFC-7932 frame; Err on failure. Real brotli: registry xiom.brotli.

  • Postcondition: result is Ok(_) => result.len() >= 8

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

Decompress only the custom NOT-RFC-7932 frame (not real brotli streams); Err on malformed input. Real brotli: registry package xiom.brotli.

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

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

=== LZ4 === Checked wrapper (Result) around the raw block compressor. Renamed from lz4_compress so the umbrella leaf is unique: a bare lz4_compress resolved to the Vec variant in the checker but bound the Result wrapper in codegen (compiler-lane root cause, 2026-10-05).

  • Postcondition: result is Ok(_) => result.len() >= 1

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

Decompress an LZ4 block; Err on malformed input. Renamed from lz4_decompress for the same unique-leaf reason.

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

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

=== Snappy ===

  • Postcondition: result is Ok(_) => result.len() >= 1

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

Decompress Snappy data; Err on malformed input.

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

fn compression_ratio(original: Int, compressed: Int) -> Float64

compressed/original ratio (0 when original is 0).

  • Precondition: original >= 0
  • Precondition: compressed >= 0
  • Postcondition: result >= 0

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

True when the bytes start with a recognized compression header.

  • Precondition: data.len() >= 0

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

Name of the detected compression format, or "" when unrecognized. NOTE: "brotli" here means the custom CE B2 CF 81 frame of xiom.compress.brotli (real brotli streams have no magic and are NOT detected); zstd is not implemented in stdlib (registry xiom.zstd).

  • Precondition: data.len() >= 0

fn lz77_compress(data: &Vec[UInt8], window: Int) -> Vec[Int]

LZ77 compression using a simple sliding-window search. Emits tokens as flat triples in a Vec[Int]: [literal_len, match_offset, match_length, ...]. A match_offset of 0 means no match found; literal_len bytes follow directly. Window size limits the backward search distance. Complexity: O(n * window), n = data length.

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

fn lz77_decompress(tokens: &Vec[Int]) -> Result[Vec[UInt8], Str]

LZ77 decompression of token triples produced by lz77_compress. Each triple: [literal_len, data, match_length_or_zero]. If literal_len == 0: data = match_offset, third = match_length. If literal_len == 1: data = literal byte, third = 0. Complexity: O(t), t = number of tokens.

  • Postcondition: tokens.len() == 0 => result is Ok(_)

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

Simple byte-level run-length encoding. Format: [count: UInt8, byte: UInt8] for runs of identical bytes. Count represents the number of repetitions (1 means 1 byte). Differs from rle_encode which uses control-byte format with bit 7 markers. Complexity: O(n), n = data length.

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

fn huffman_freqs(data: &Vec[UInt8]) -> Vec[Int]

Builds a 256-slot frequency table for Huffman coding. Each slot i contains the count of byte value i in the input. Complexity: O(n), n = data length.

  • Postcondition: result.len() == 256

fn compress_gzip_str(s: Str) -> Result[Vec[UInt8], Str]

Compresses a UTF-8 string using gzip. Converts Str to bytes, then wraps gzip_compress. Complexity: O(n), n = string length.

  • Postcondition: s.len() == 0 => result is Err(_)

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

Decompresses gzip data to a UTF-8 string. Wraps gzip_decompress and converts the result to Str. Complexity: O(n), n = compressed data length.

  • Postcondition: result is Ok(_) => data.len() >= 18

fn compress_ratio(original: Int, compressed: Int) -> Float64

Alias for compression_ratio. Returns original / compressed as Float64. Complexity: O(1).

  • Postcondition: original >= 0 => result >= 0

crc32.xi

fn crc32(data: &Vec[UInt8]) -> Int

Compute the CRC-32 checksum (reflected 0xEDB88320) of data as an Int. Known answer: crc32("123456789") == 0xCBF43926 (3421780262). O(n*8).

  • Postcondition: (data.len() == 0) => (result == 0)

deflate.xi

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

Compress with the RFC 1951 encoding (matching the deterministic reference behavior shapes of zlib for greedy matchers). Default level 6 picks the smallest of stored/fixed/dynamic per input; for compressible data that is a dynamic-Huffman block.

  • Postcondition: result.len() >= 2
fn deflate_compress_level(data: &Vec[UInt8], level: Int) -> Vec[UInt8]

level 0 => STORED blocks (real, uncompressed); levels 1-3 => FIXED Huffman blocks; levels 4-9 => the smallest of STORED, FIXED and DYNAMIC Huffman blocks (dynamic is what wins on compressible inputs).

  • Postcondition: result.len() >= 2
  • Postcondition: (level <= 0) => (result.len() >= data.len() + 5)
  • Postcondition: (level <= 0 && data.len() == 0) => (result.len() == 5)
fn deflate_decompress(data: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Decompress raw deflate data; Err on malformed input.

  • Postcondition: (data.len() == 0) => (result.is_err)
fn deflate_decompress_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[UInt8], Str]

Decompress a real RFC 1951 stream with a hard output ceiling.

  • Postcondition: (data.len() == 0) => (result.is_err)
fn deflate_bound(len: Int) -> Int

Worst-case compressed size for len input bytes under the fixed-Huffman encoder: per byte at most 9 code bits + headers + match overhead is always below this bound. O(1).

  • Postcondition: (len < 0) => (result == 512)
  • Postcondition: (len >= 0) => (result == len * 5 + 512)
fn deflate_compress_stream(reader: Int, writer: Int) -> Result[Int, Str]

Stream-compress between two file descriptors: reads all bytes from reader, compresses them, writes the container to writer, and returns the number of bytes written. Errors (empty input, read/write failures) are returned as Err.

  • Postcondition: result is Ok(_) => result.value >= 0
fn deflate_length_base_table() -> Vec[Int]

RFC 1951 3.2.5 literal/length base values; index i is code 257 + i (29 entries covering codes 257..285). O(29).

  • Postcondition: result.len() == 29
fn deflate_length_extra_table() -> Vec[Int]

RFC 1951 3.2.5 extra-bit counts for length codes 257..285 (29 entries). O(29).

  • Postcondition: result.len() == 29
fn deflate_distance_base_table() -> Vec[Int]

RFC 1951 3.2.5 distance base values; index i is distance code i (30 entries covering codes 0..29). O(30).

  • Postcondition: result.len() == 30
fn deflate_distance_extra_table() -> Vec[Int]

RFC 1951 3.2.5 extra-bit counts for distance codes 0..29 (30 entries). O(30).

  • Postcondition: result.len() == 30
fn deflate_fixed_lit_lengths() -> Vec[Int]

RFC 1951 3.2.6 fixed literal/length code lengths (288 entries; symbol index, code 256 is the end-of-block symbol). O(288).

  • Postcondition: result.len() == 288
fn deflate_fixed_dist_lengths() -> Vec[Int]

RFC 1951 3.2.6 fixed distance code lengths: 30 codes of 5 bits (the fixed table defines 32; only codes 0..29 can appear in a stream). O(30).

  • Postcondition: result.len() == 30

gzip.xi

fn gzip_crc32(data: &Vec[UInt8]) -> UInt32

Compute the CRC-32 checksum (IEEE 802.3 polynomial) of data. O(n).

  • Postcondition: (data.len() == 0) => (result == 0)
fn gzip_header_new(mtime: Int, os: Int) -> Vec[UInt8]

Build a bare gzip header: magic (1F 8B), method (08), flags (00), MTIME (mtime, LE, may be 0), XFL (00) and OS (os, masked to 8 bits; use 255 for unknown, 3 for Unix). Returns 10 bytes.

  • Postcondition: result.len() == 10
fn gzip_compress(data: &Vec[UInt8]) -> Vec[UInt8]

Wrap data in a gzip stream: header (mtime 0, OS 255) + DEFLATE payload + CRC32 trailer + ISIZE trailer.

  • Postcondition: result.len() >= 20
fn gzip_decompress(data: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Unwrap and validate a gzip stream. Parses the optional header fields, decompresses the payload, and verifies the CRC32 and ISIZE trailer values. Returns Err on any mismatch or malformed input.

  • Postcondition: (data.len() < 18) => (result.is_err)
fn gzip_decompress_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[UInt8], Str]

Decompress with a hard ceiling on output size (decompression-bomb guard). The header's declared ISIZE is rejected up-front when it exceeds the cap; the payload cap is enforced inside the deflate stages.

  • Postcondition: (data.len() < 18) => (result.is_err)
  • Postcondition: (max_out < 0) => (result.is_err)
fn gzip_compress_file(path: Str) -> Result[Unit, Str]

Gzip a file to <path>.gz. Returns Err when the source cannot be read or the target cannot be written.

  • Postcondition: result is Ok(_) => io.file_exists(path + ".gz")
fn gzip_decompress_file(path: Str) -> Result[Vec[UInt8], Str]

Gunzip a file into raw bytes. Returns Err on read failures or invalid gzip data.

  • Postcondition: result is Err(_) => result.value.len() > 0
fn gzip_validate(data: &Vec[UInt8]) -> Bool

Sanity-check magic, method, and the minimum trailer footprint. O(1).

  • Postcondition: (data.len() < 18) => (result == false)

huffman.xi

type HuffmanTree

Huffman tree: per-symbol code lengths and canonical codes (index = byte value).

Field Type
code_lengths Vec[Int]
codes Vec[Int]
max_len Int
fn huffman_canonical(codelengths: &Vec[Int]) -> Vec[Int]

Derive the canonical prefix-free codes from per-symbol code lengths. Canonical order: shorter codes first, ties by symbol index. O(256).

  • Postcondition: result.len() == 256
fn huffman_build(frequencies: &Vec[Int]) -> HuffmanTree

Build a Huffman tree from a 256-slot frequency table (index = byte value). The tree holds per-symbol code lengths and canonical codes. Empty or single-symbol inputs are handled (single symbol gets length 1). Complexity: O(n^2) in the number of distinct symbols (<= 256).

  • Postcondition: result.code_lengths.len() == 256
  • Postcondition: result.max_len >= 0
fn huffman_code_lengths(tree: HuffmanTree) -> Vec[Int]

Extract the per-symbol code lengths as a fresh 256-slot Vec[Int].

  • Postcondition: result.len() == 256
fn huffman_table_new(codelengths: &Vec[Int]) -> Vec[Int]

Pack a flat canonical decode table: entries [0..255] are the canonical codes, entries [256..511] are the matching code lengths. O(512).

  • Postcondition: result.len() == 512
fn huffman_encode_symbol(tree: HuffmanTree, sym: Int) -> Vec[Bool]

Return the code bits of one symbol as booleans, MSB first. An uncovered symbol yields an empty Vec (documented).

  • Postcondition: (sym < 0 || sym > 255) => result.len() == 0
fn huffman_encode(tree: HuffmanTree, data: &Vec[UInt8]) -> Vec[UInt8]

Pack data into an MSB-first bit stream using the tree's codes. O(n * avg code length). Requires the tree to cover every input byte.

  • Postcondition: data.len() == 0 => result.len() == 0
fn huffman_decode(tree: HuffmanTree, bits: &Vec[UInt8], len: Int) -> Result[Vec[UInt8], Str]

Decode exactly len bits of the MSB-first stream back into bytes. Returns Err on invalid bit patterns or stream exhaustion.

  • Postcondition: result is Ok(_) => len <= 0 || result.len() <= len
fn huffman_compress(data: &Vec[UInt8]) -> Vec[UInt8]

One-shot Huffman compression: builds the frequency table and tree, packs the bits, and emits the self-describing container (header documented at the top of this module). Empty input yields a valid empty container.

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

Decompress Huffman-coded data; Err on malformed input.

  • Postcondition: result is Ok(_) => result.len() <= _HUFF_DEFAULT_CAP
fn huffman_decompress_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[UInt8], Str]

Decompress with a hard ceiling on output size. The container's declared length is rejected up-front when it exceeds the cap; the decode loop re-checks per symbol, so a lying header cannot allocate past the cap.

  • Postcondition: result is Ok(_) => result.len() <= max_out
fn rle_compress(data: &Vec[UInt8]) -> Vec[UInt8]

Byte-level run-length encoding: [count: UInt8, byte: UInt8] pairs for runs of identical bytes (count 1..255; runs longer than 255 split). Complexity: O(n), n = data length.

  • Postcondition: result.len() % 2 == 0
  • Postcondition: result.len() <= 2 * data.len()
fn rle_decompress(data: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Undo byte-level run-length encoding (rle_compress format). Returns Err on a truncated pair (odd trailing byte) or a zero count.

  • Postcondition: result is Ok(_) => result.len() >= data.len() / 2

lz4.xi

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

Compress data into a full frame (magic, FLG/BD, block size, payload).

  • Postcondition: result.len() >= 11
fn lz4_compress_frame(data: &Vec[UInt8]) -> Vec[UInt8]

Alias for lz4_compress: the frame IS the full container in this module.

  • Postcondition: result.len() >= 11
fn lz4_compress_hc(data: &Vec[UInt8]) -> Vec[UInt8]

Compress data into a frame using the high-compression block encoder.

  • Postcondition: result.len() >= 11
fn lz4_bound(len: Int) -> Int

Worst-case compressed size for len input bytes (literals expand by at most 1 byte per 255 input bytes plus token/header overhead). O(1).

  • Postcondition: (len < 0) => (result == 32)
  • Postcondition: (len >= 0) => (result == len + (len >> 8) + 32)
fn lz4_decompress(data: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Decompress an LZ4 block; Err on malformed input.

  • Postcondition: (data.len() < 11) => (result.is_err)
fn lz4_decompress_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[UInt8], Str]

Decompress with a hard ceiling on total output size (bomb guard). Checked after each block's expansion.

  • Postcondition: (data.len() < 11) => (result.is_err)
  • Postcondition: (max_out < 0) => (result.is_err)
fn lz4_decompress_frame(data: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Alias for lz4_decompress: parses and decompresses an lz4_compress frame.

  • Postcondition: (data.len() < 11) => (result.is_err)
fn lz4_compress_block(data: &Vec[UInt8]) -> Vec[UInt8]

Compress a raw block payload (no frame header) using the LZ4 block format. Greedy search with a 4KiB window; matches need length >= 4. Complexity: O(n * 4096).

  • Postcondition: (data.len() == 0) => (result.len() == 1)
fn lz4_compress_hc_block(data: &Vec[UInt8]) -> Vec[UInt8]

High-compression block variant: 64KiB search window, longer match scan. Uses the same block format, so lz4_decompress_block decodes either output.

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

Decompress a raw LZ4 block. Returns Err on truncation, an invalid offset, or malformed extended lengths.

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

lz77.xi

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

Compress data with a greedy 32KiB sliding-window search into the control-byte token stream documented above. O(n * 32768).

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

Decompress LZ77 data; Err on malformed input.

  • Postcondition: result is Ok(_) => result.len() <= _LZ77_DEFAULT_CAP
fn lz77_decompress_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[UInt8], Str]

Decompress with a hard ceiling on output size. Every expansion step is checked BEFORE writing, so a hostile token stream cannot allocate beyond the cap even momentarily. Returns Err("lz77: output exceeds cap") when exceeded.

  • Postcondition: result is Ok(_) => max_out < 0 || result.len() <= max_out
fn lz77_find_longest_match(data: &Vec[UInt8], pos: Int, window: Int) -> (Int, Int)

Locate the longest match for the byte at pos searching back at most window positions. Returns (length, distance); (0, 0) when no match of length >= 3 exists. Out-of-range positions yield (0, 0). Complexity: O(window * match_length).

  • Postcondition: result._0 >= 0 && result._0 <= 258
  • Postcondition: result._0 == 0 => result._1 == 0
fn lz77_token_encode(length: Int, distance: Int) -> Int

Pack a (length, distance) pair into a single token: (length << 16) | distance. Both fields are clamped to 16 bits (0..65535). Pure-Int token.

  • Postcondition: result >= 0 && result <= 4294967295
fn lz77_token_decode(token: Int) -> (Int, Int)

Unpack a token produced by lz77_token_encode into (length, distance).

  • Postcondition: result._0 >= 0 && result._0 <= 65535
  • Postcondition: result._1 >= 0 && result._1 <= 65535

snappy.xi

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

Read the varint uncompressed length that opens a raw snappy stream. Returns Err on a malformed header.

  • Postcondition: (data.len() == 0) => (result.is_err)
fn snappy_validate(data: &Vec[UInt8]) -> Bool

Sanity-check the varint header of a raw snappy stream. O(1)..O(10).

  • Postcondition: (data.len() == 0) => (result == false)
fn snappy_max_compressed_len(len: Int) -> Int

Upper bound on the compressed size of len input bytes (varint + up to 1/6 expansion for incompressible data). O(1).

  • Postcondition: (len < 0) => (result == 32)
  • Postcondition: (len >= 0) => (result == 32 + len + len / 6)
fn snappy_compress(data: &Vec[UInt8]) -> Vec[UInt8]

Compress data into a raw snappy stream (varint length + elements). Greedy matches with a 4KiB window; literals batch until a match is found. Complexity: O(n * 4096).

  • Postcondition: (data.len() == 0) => (result.len() == 1)
  • Postcondition: (data.len() > 0) => (result.len() >= 2)
fn snappy_decompress(data: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Decompress Snappy data; Err on malformed input.

  • Postcondition: (data.len() == 0) => (result.is_err)
fn snappy_decompress_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[UInt8], Str]

Decompress with a hard ceiling on output size (bomb guard). The varint-declared length is rejected up-front when it exceeds the cap; every literal/copy element re-checks before writing.

  • Postcondition: (data.len() == 0) => (result.is_err)
  • Postcondition: (max_out < 0) => (result.is_err)
fn snappy_compress_frame(data: &Vec[UInt8]) -> Vec[UInt8]

Compress data into a framed stream: varint(compressed payload length) followed by the raw snappy stream (which itself starts with the varint uncompressed length). The frame is self-delimiting.

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

Decompress a snappy_compress_frame stream. Validates the outer varint against the remaining bytes. Returns Err on any mismatch or malformed data.

  • Postcondition: (data.len() == 0) => (result.is_err)
  • Postcondition: (data.len() == 1) => (result.is_err)

zip.xi

type ZipEntry

One extracted archive member (reader side). crc, compressed_size and uncompressed_size come from the central directory; data is the verified content.

Field Type
name Str
method Int
crc Int
compressed_size Int
uncompressed_size Int
data Vec[UInt8]
type ZipWriter

Incremental archive builder (writer side). out holds local headers + payloads, central holds central-directory records as they are added.

Field Type
out Vec[UInt8]
central Vec[UInt8]
count Int
fn zip_list(data: &Vec[UInt8]) -> Result[Vec[Str], Str]

Parse the central directory and return the member names in archive order. Err on any malformed structure (truncation, bad signatures, zip64, multi-disk).

  • Postcondition: (data.len() < 22) => (result.is_err)
fn zip_extract_capped(data: &Vec[UInt8], max_out: Int) -> Result[Vec[ZipEntry], Str]

Extract every member with a per-entry output ceiling (decompression-bomb guard). Verifies each entry's CRC-32 and uncompressed size against the central directory; Err on the first mismatch.

  • Postcondition: (data.len() < 22) => (result.is_err)
  • Postcondition: (max_out < 0) => (result.is_err)
fn zip_extract(data: &Vec[UInt8]) -> Result[Vec[ZipEntry], Str]

Extract every member with the default 1 GiB per-entry ceiling.

  • Postcondition: (data.len() < 22) => (result.is_err)
fn zip_read(data: &Vec[UInt8], name: Str) -> Result[Vec[UInt8], Str]

Extract a single member by exact name (raw UTF-8 byte equality). Scanning stops at the first match; Err when the name is absent or the entry is malformed.

  • Postcondition: (data.len() < 22) => (result.is_err)
fn zip_writer_new() -> ZipWriter

New empty archive builder. finish on a fresh writer emits a valid 22-byte empty archive.

  • Postcondition: result.count == 0
  • Postcondition: result.out.len() == 0
  • Postcondition: result.central.len() == 0
fn zip_writer_add(w: &mut ZipWriter, name: Str, data: &Vec[UInt8], method: Int) -> Result[Unit, Str]

Append one member: local header + payload, then its central-directory record. method is ZIP_METHOD_STORED or ZIP_METHOD_DEFLATE; deflate uses the default level 6. Err on ids the zip32 format cannot express.

  • Postcondition: (name.len() == 0) => (result.is_err)
  • Postcondition: (name.len() > 65535) => (result.is_err)
fn zip_writer_add_level(w: &mut ZipWriter, name: Str, data: &Vec[UInt8], method: Int, level: Int) -> Result[Unit, Str]

zip_writer_add with an explicit deflate level (0..9; ignored for stored).

  • Postcondition: (name.len() == 0) => (result.is_err)
  • Postcondition: (name.len() > 65535) => (result.is_err)
fn zip_writer_finish(w: &mut ZipWriter) -> Result[Vec[UInt8], Str]

Close the archive: append the central directory and the EOCD and return the full byte stream. The writer stays usable for a new archive.

  • Postcondition: (result.is_ok) => (w.out.len() == w.out.len()@pre + w.central.len() + 22)

zlib.xi

fn zlib_header_new(level: Int) -> Vec[UInt8]

Build the CMF/FLG header bytes for a level (0-9, clamped). Returns 2 bytes.

  • Postcondition: result.len() == 2
fn zlib_adler32(data: &Vec[UInt8]) -> UInt32

Compute the Adler-32 checksum of data. O(n).

  • Postcondition: (data.len() == 0) => (result == 1)
fn zlib_compress(data: &Vec[UInt8]) -> Vec[UInt8]

Wrap data in a zlib stream at the default level (6).

  • Postcondition: result.len() >= 8
fn zlib_compress_level(data: &Vec[UInt8], level: Int) -> Vec[UInt8]

Wrap data in a zlib stream with an explicit level (0-9, clamped).

  • Postcondition: result.len() >= 8
fn zlib_decompress(data: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Unwrap and validate a zlib stream: header method/checksum, payload decompression, and Adler32 trailer verification. Returns Err on any mismatch or malformed input.

  • Postcondition: (data.len() < 6) => (result.is_err)
fn zlib_validate(data: &Vec[UInt8]) -> Bool

Sanity-check the zlib header (method and CMF/FLG checksum). O(1).

  • Postcondition: (data.len() < 6) => (result == false)