Proof details
Start with an engine’s full argument, then follow lookup, copying, coding, and memory components in detail. Each route connects to concrete function contracts and definitions.
Decompression engine
Window contents, actual modes, supporting bits, lookup, exits, and call sequences.
Full proof details →Public contract and exact target →Compression engine
Windows, hash chains, matching, strategy loops, symbol ledgers, block output, and the default wrapper.
Full proof details →Public contract and exact target →Exact targets for call sequences and initialization domains →
Reading the actual proofs
Follow key lemmas in implementation order. Read the problem and premises for each step, then open its derivation. Whole-interface proofs connect these steps.
inflate
- Dynamic-table contents
The dynamic-block lengths must become entries the decoder can actually read. Actual inflate_table execution yields both the original safety/return classification and TableConstruction. Successful runs retain canonical leaves, links, and returned extents; empty tables, singleton tables, and constructor error returns are included.
CallPre describes the internal call’s readable input, writable table storage, and separation. CallPre supplies the length input, writable capacities, separation, and other internal call conditions. The constructed contents must still be connected to the decoder's consumer predicates and actual call state; this is not whole-stream decoding correctness.inflate_table_construction - State and window release
End must release the stream’s state and history without changing unrelated caller objects. The actual end execution for Goal.inflateEnd returns Z_OK, clears the stream's state pointer, removes live blocks exactly according to InflateOwned, and supplies the unrelated-object Frame and unchanged allocation counters.
Good is the state-validity condition used by this entry. Goal.inflateEnd explicitly requires Good and the default zcfree. This theorem uses that state condition; it does not independently establish Good for every public call history. Acceptance status requires separate audit and commit evidence.inflate_end_public
deflate
- Default initialization and allocation failure
Initialization must create a usable compressor or clean up a failed allocation attempt. Expands the fixed-parameter deflateInit_ call to establish Goal.deflateInit_: arbitrary level arguments, version and parameter refusals, five allocation outcomes, failure cleanup, ownership, and the initialized invariant are included.
Fresh and Uniq protect allocation identities and existing object representations. The public contract retains Fresh, Uniq, library globals, caller storage, version, and default-or-null allocator premises. Window 15, memory level 8, and strategy 0 are fixed; the general Goal.deflateInit2_ is neither assumed nor established.deflateInit_proof