Browse zlib specs

Proofs / zlib

zlib 1.3.2, the core library

specs
62
zlib 1.3.2
da607da7
lines of Rocq
~590,000
qp verify
PASS
On this page

We proved 62 C specs of the core of zlib 1.3.2: compression, decompression and the checksums. A spec is a small C program that states a property and that you can compile and run, and each spec has a theorem in Rocq (formerly Coq). AI agents wrote the proof, about 590,000 lines of Rocq, and Rocq checks it. The specs, the proof and every change to the code are in genproof/zlib-full-auto-proofs-public.

Ten properties

These are the properties a user of zlib relies on, with the specs that prove each. Every spec links to its page, which shows the spec whole, as it is in the repository. The numbers are for x86_64 (LP64), the platform of the theorems.

  1. Compression is deterministic. Two streams made by deflateInit2 with the same parameters, given the same calls, return the same codes and write the same bytes. The calls cut the data into any pieces, use any flush from Z_NO_FLUSH to Z_BLOCK (Z_FINISH only with all the rest of the data), and may call deflateParams before each deflate.

    Proved by api_deterministic.

  2. The compressed size is bounded. For any level -1..9, compress2_z into compressBound_z(n) = n + n/4096 + n/16384 + n/2^25 + 13 bytes returns Z_OK unless it reports Z_MEM_ERROR, and the length it reports is at most that. For deflateBound, with a dictionary, a gzip header or neither, data under 4 GiB and a bound below 2^32, one deflate(Z_FINISH) into exactly that many bytes returns Z_STREAM_END.

    Proved by res_compress_bound and res_bound. The first needs the fix for issue #1348 (below).

  3. Compression memory is bounded. Counted through the zalloc and zfree it is given, deflate never holds more than (1 << (w + 2)) + (1 << (memLevel + 9)) + 5968 bytes. Here w is windowBits without the minus sign of raw deflate or the 16 of gzip, and 9 for 8. The bound is checked after every call, over any number of deflate calls with any data, output space and flush.

    Proved by res_memory_deflate.

  4. Compression is memory-safe and returns only documented codes. For any parameters that deflateInit2 accepts, any data in any pieces, any output space and any flush value (any int), with deflateParams (any level and strategy) before any call until the first Z_FINISH, and calls that follow zlib.h's rule for Z_FINISH: every call returns a code that zlib.h documents (Z_STREAM_ERROR exactly for an invalid flush, level or strategy) and leaves the output space it did not write as it was.

    Proved by api_deflate_any. The round trip rt_stream drives deflate with any parameters, pieces and flush values up to Z_BLOCK, without deflateParams.

  5. Decompression is deterministic. With the 32 KiB window (windowBits -15, 15, 31 or 47) and input and output space under 4 GiB, one inflate call (any flush but Z_BLOCK and Z_TREES) and any split of the same input write the same bytes. When the one call returns Z_STREAM_END, Z_NEED_DICT or Z_DATA_ERROR, the split ends with the same code, and otherwise with none of the three. Two new streams with the same windowBits, fed any input in the same pieces with the same output space and flush, return the same codes and write the same bytes.

    Proved by api_split_invariant and api_inflate_deterministic.

  6. Decompression does not consume what follows the stream. Take a stream that zlib's deflate made, with any parameters it accepts, followed by any bytes. When inflate returns Z_STREAM_END, next_in points just past the stream: none of the bytes after it were consumed.

    Proved by rt_stream_trailing, with the stream in any pieces and any output space, and also by rt_session and rfc_trailing_bytes; for uncompress2 by rt_roundtrip; for streams of up to 2^19 bytes that a reference encoder builds from RFC 1951, followed by up to 16 bytes, by x_inflate_decode.

  7. Round trip. For any data and any level -1..9, compress2 into compressBound bytes returns Z_OK. Then uncompress2 of its output, followed by any bytes, into an output of at least the data's length returns Z_OK, gives back exactly the data, writes nothing after it and reports the stream's length as read.

    Proved by rt_roundtrip; with streams, any parameters, any split and any bytes after the stream, by rt_stream_trailing; in one session with a dictionary or a gzip header as well, by rt_session.

  8. Too little room gives Z_BUF_ERROR and the start of the data. For what compress2 made from one byte or more (any level -1..9), uncompress2 with less output space than the data (even none, also with a NULL buffer) returns Z_BUF_ERROR, writes exactly the first bytes of the data and reads less than the whole stream.

    Proved by api_short_output.

  9. Decompression memory is bounded. Counted through the zalloc and zfree it is given, inflate never holds more than (1 << w) + 7160 bytes. Here w is windowBits without the minus sign of raw inflate or the 16 or 32 added for gzip or header detection, and 15 when that leaves 0. The bound is checked after every call, over any number of inflate calls with any input, output space and flush.

    Proved by res_memory_inflate.

  10. Decompression is memory-safe on any input. For any windowBits that inflateInit2 accepts, inflate runs on any bytes of any length, in any pieces, with any output space and any flush, and inflateSetDictionary with any bytes between calls. Every inflate call returns a code that zlib.h documents, leaves the input and the output space it did not write as they were, and moves its pointers and counters by exactly what it read and wrote. The same holds for uncompress2.

    Proved by api_inflate_any; rj_any_input and api_untouched_output state parts of it on their own, and rj_uncompress_any covers uncompress2. x_inflate_buffers shows the same buffer discipline for the rest of the inflate API, with at most 16 MiB of input in all and 1 MiB of output space per call, and x_inflate_header for the buffers of inflateGetHeader, up to 64 KiB each.

Memory safety is part of every theorem, not only of 4 and 10. For its spec, each theorem rules out a read or write outside an object, a use after free, a double free, a null dereference, the use of an uninitialised value, a signed overflow and a division by zero. 5968 and 7160 bytes, in 3 and 9, are the sizes of deflate_state and struct inflate_state on x86_64.

All the specs

The 45 short specs, by what they promise, and then the 17 longer ones. A short spec is 14 to 204 lines of C, 54 to 296 with its shared headers, and most of them bound neither their data nor the number of calls. In a spec, nondet_* and upto(max) stand for any value, gp_assume restricts the inputs and gp_assert states what must hold. The first comment of each file states the property in full; it starts with Law, the older word for a spec.

Round trips

What goes in comes back. 7 specs

  • rt_roundtripC file · 65 lines

    Any data, any level -1..9: compress2 succeeds, and uncompress2 of its output followed by any bytes reads exactly the compressed bytes and gives back exactly the data.

  • rt_streamC file · 93 lines

    The same with streams: any compression parameters, the data given in any pieces, any output room and any flush from Z_NO_FLUSH to Z_BLOCK on every call, decompressed in any pieces with any flush: exactly the data comes back.

  • rt_stream_trailingC file · 106 lines

    rt_stream with any bytes after the stream: every call moves next_in and next_out exactly as far as it lowers avail_in and avail_out, a call offered no room (deflate) or neither input nor room (inflate) moves nothing, and decompression stops exactly at the end of the stream, reads none of the bytes after it and gives back exactly the data.

  • rt_sessionC file · 204 lines

    One session with everything at once: any wrapper, a preset dictionary or a full gzip header, the data in any pieces with any flush and output room, any bytes after the stream: every call accounts for its pointers, the dictionary is asked for exactly when it should be, and the data and every header field come back exactly.

  • rt_dictionaryC file · 86 lines

    Compressed with any preset dictionary (zlib wrapper, windowBits 8..15): decompression asks for it, and once given it, returns exactly the data.

  • rt_gzip_headerC file · 110 lines

    Every field of a gzip header (text flag, OS, time, extra field, name, comment; each present or not) comes back as it was given.

  • rt_partialC file · 68 lines

    Given any unfinished prefix of a compressed stream, decompression only ever writes the start of the data.

Rejecting bad input

Bad parameters and bad streams are refused, and any input is safe. 12 specs

  • rj_any_inputC file · 60 lines

    Any bytes given to decompression, in any pieces, with any flush and dictionaries in between: every call returns one of the documented codes.

  • rj_uncompress_anyC file · 38 lines

    The same for uncompress2: any bytes, any output size: only documented codes, and the output space after what it reports written is left as it was.

  • rj_far_backC file · 103 lines

    In a raw stream whose first block is a fixed-Huffman block of fewer than 32768 literals, a back-reference to before the start of the output is an error (Z_DATA_ERROR), and nothing beyond the literals is output.

  • rj_bad_headerC file · 45 lines

    A zlib header that breaks RFC 1950 (check bits, method, window size) is refused before any output.

  • rj_bad_blockC file · 91 lines

    A first block of a raw stream that breaks RFC 1951 is refused: a stored block whose length check fails, the reserved block type, forbidden codes.

  • rj_bad_checksumC file · 79 lines

    If the checksum or length at the end of the stream is changed, decompression never reports success.

  • rj_bad_dictionaryC file · 42 lines

    A zlib stream whose header asks for a dictionary makes inflate return Z_NEED_DICT, and a dictionary whose checksum is not the one the header names is refused.

  • rj_truncatedC file · 67 lines

    A truncated stream never reports success.

  • rj_bad_levelC file · 22 lines

    A level outside -1..9 makes compress2 fail with Z_STREAM_ERROR.

  • rj_deflate_paramsC file · 34 lines

    deflateInit2 accepts its parameters exactly when all are in the ranges of zlib.h.

  • rj_inflate_paramsC file · 26 lines

    inflateInit2 accepts exactly the window sizes of zlib.h.

  • rj_crc32_negativeC file · 15 lines

    Combining CRCs with a negative length returns 0.

The standard on valid input

Streams built by the RFCs decode, and level 0 writes exactly what RFC 1951 says. 4 specs

  • rfc_storedC file · 103 lines

    A stream of stored blocks built by hand from the RFCs (any data, any block sizes, any wrapper, any bytes after it) decompresses to exactly the data.

  • rfc_trailing_bytesC file · 82 lines

    For a stream that zlib's deflate made, followed by any bytes: when decompression returns Z_STREAM_END, it has consumed exactly the stream and none of the bytes after it.

  • rfc_level0_sizeC file · 59 lines

    At level 0 the output size is exactly the data plus 5 bytes per block plus the wrapper (the data given in pieces of whole 65535-byte blocks, one call or many).

  • rfc_level0_blocksC file · 77 lines

    At level 0 the output is exactly stored blocks as RFC 1951 defines them, holding the data in order.

The stream interface

Counters are exact, unwritten output stays as it was, and the same calls give the same results. 10 specs

  • api_deterministicC file · 73 lines

    Two streams with the same parameters, driven by the same calls, produce the same output.

  • api_inflate_deterministicC file · 58 lines

    Two new decompression streams with the same windowBits, fed the same input (any bytes) in the same pieces with the same flush, return the same codes and write the same bytes.

  • api_split_invariantC file · 76 lines

    For any input under 4 GiB, one call or any pieces give the same bytes and the same end result (32 KiB window).

  • api_deflate_anyC file · 82 lines

    Any accepted compression parameters, any data in any pieces, any flush and deflateParams between calls: deflate returns only the codes of zlib.h (Z_STREAM_ERROR exactly for an invalid flush), deflateParams returns Z_STREAM_ERROR exactly for an invalid level or strategy, and the output room not written is left as it was.

  • api_inflate_anyC file · 71 lines

    Any accepted windowBits, any input in any pieces (empty ones too), any flush, any output room (none too), dictionaries in between: only documented codes, the input and the unwritten output untouched, next_* and total_* move by exactly what was read and written, and no Z_OK when nothing could be done.

  • api_untouched_outputC file · 65 lines

    Decompression leaves the part of the output room it did not write as it was.

  • api_short_outputC file · 55 lines

    Given less room than the data needs (any amount, even none), uncompress2 says so (Z_BUF_ERROR), gives exactly the first bytes and has not read all of the compressed bytes (any bytes follow them).

  • api_countersC file · 50 lines

    The stream's pointers and counters move by exactly the bytes read and written.

  • api_dict_idC file · 66 lines

    For data compressed with a preset dictionary (zlib wrapper), decompression asks for it and reports the dictionary's Adler-32.

  • api_resetC file · 67 lines

    After any use and inflateReset, a stream behaves exactly like a new one.

Sizes and memory

The documented size bounds hold, memory stays within exact bounds, and the end functions give it all back. 6 specs

  • res_compress_boundC file · 29 lines

    compress2_z at any level -1..9 into compressBound_z bytes never runs out of room, and the output is at most that. zlib 1.3.2 as released fails it at level 0 for some inputs over 51 TiB (issue #1348, fixed upstream).

  • res_boundC file · 77 lines

    One deflate(Z_FINISH) into exactly deflateBound bytes returns Z_STREAM_END, with a dictionary, a gzip header or neither, for data under 4 GiB and a bound below 2^32.

  • res_memory_deflateC file · 93 lines

    Compression, over any number of calls, never holds more memory than the formula of zconf.h plus the exact size of its state (5968 bytes); Z_MEM_ERROR only when the allocator failed.

  • res_memory_inflateC file · 87 lines

    Nor does decompression: at most the window plus the exact size of its state (7160 bytes).

  • res_free_deflateC file · 69 lines

    After one deflate call and deflateEnd (and after a failed deflateInit2) all memory is given back.

  • res_free_inflateC file · 66 lines

    The same for decompression, after one inflate call.

Checksums

Adler-32 and CRC-32 are the RFCs' definitions, and combining them works for any cut. 6 specs

  • ck_adler32C file · 23 lines

    adler32_z equals the Adler-32 definition of RFC 1950, written out in the spec, for any bytes and any starting value whose halves are below 65521.

  • ck_adler32_combineC file · 23 lines

    The checksum of the whole equals adler32_combine of the checksums of its two parts, for any cut and any starting value whose halves are below 65521.

  • ck_adler32_nullC file · 14 lines

    With no buffer (Z_NULL), adler32_z returns the initial value 1.

  • ck_crc32C file · 29 lines

    crc32_z equals the bit-by-bit CRC-32 of RFC 1952, written out in the spec, for any bytes and any starting value.

  • ck_crc32_combineC file · 26 lines

    The same for CRC-32, with each of zlib's three combine functions.

  • ck_crc32_nullC file · 14 lines

    With no buffer, crc32_z returns the initial value 0.

Earlier, longer properties

The 17 specs whose names start with x_ come from our first proof of zlib's core, with their statements unchanged. They are bounded, most to 1 MiB of data or 16 MiB of input. x_inflate_decode checks inflate against a reference encoder written from RFC 1951 for all three kinds of block, which no short spec covers.

  • x_inflate_decodeC file · 289 lines

    inflate decodes every stream that a reference encoder written from RFC 1951 builds from stored, fixed and dynamic Huffman blocks (data up to 256 KiB, stream up to 512 KiB; raw, zlib or gzip wrapper; up to 16 bytes after it): only Z_OK, Z_BUF_ERROR or Z_STREAM_END, the output is always the start of the data, and at the end exactly the stream was consumed.

  • x_inflate_buffersC file · 167 lines

    Any sequence of calls of the inflate API (inflate with any flush, inflateSync, inflateGetDictionary, inflateSetDictionary, inflatePrime, inflateReset, inflateReset2, inflateValidate, inflateMark, inflateCodesUsed, inflateSyncPoint), any windowBits, input up to 16 MiB and output space up to 1 MiB per call: every call reads and writes only its buffers, pointers and counters move by exactly what was consumed and produced, and inflate leaves the output space it did not write unchanged.

  • x_inflate_codesC file · 172 lines

    inflateInit2_, inflate, inflateSetDictionary, inflateEnd, and every entry point after inflateEnd, return exactly the documented codes, for any input up to 16 MiB and any calls of inflate and inflateSetDictionary; the first comment gives each code's conditions.

  • x_inflate_checkC file · 103 lines

    With a zlib or gzip wrapper, once inflate has produced output, the stream's header is valid and after every call adler is the checksum of the output so far; inflate returns Z_STREAM_END only when the trailer matches it (input up to 16 MiB).

  • x_inflate_dictC file · 219 lines

    Preset dictionaries of up to 64 KiB: a zlib stream asks for the dictionary and reports its Adler-32, a wrong one gives Z_DATA_ERROR, the right one decodes the data, back-references into the dictionary included; inflateGetDictionary returns the window (data up to 256 KiB).

  • x_inflate_headerC file · 229 lines

    inflateGetHeader with buffers of any size up to 64 KiB, on a gzip member with any header fields: inflate writes the buffers only within their sizes, reports every field once the header is complete, and never accepts a reserved flag bit or a wrong header CRC.

  • x_inflate_resetC file · 110 lines

    After any use, inflateReset, or inflateReset2 with any windowBits, gives a stream that behaves like a new one from inflateInit2 on the same input (up to 16 MiB).

  • x_uncompress_anyC file · 51 lines

    uncompress and uncompress2 on any input of up to 16 MiB, with any output size up to 1 MiB: only documented codes, no write beyond the size they report, and on Z_OK a valid zlib header and a trailer that matches the output.

  • x_deflate_apiC file · 69 lines

    deflate's documented interface for any parameters, tuning, dictionary and gzip header, data of up to 1 MiB, and any sequence of deflate and deflateParams calls with any split: documented codes (Z_STREAM_ERROR exactly for invalid parameters), exact pointers and counters, the output space beyond what was produced unchanged, the right header and trailer at Z_STREAM_END, and Z_STREAM_ERROR from every call after deflateEnd.

  • x_deflate_roundtripC file · 84 lines

    One inflate call gives back exactly what deflate compressed, for any parameters, tuning, dictionary and gzip header (which comes back too) and any sequence of deflate (flush up to Z_BLOCK) and deflateParams calls with any split (data up to 1 MiB, output space up to 1 MiB per call, 4 MiB of compressed output).

  • x_deflate_boundC file · 97 lines

    One deflate(Z_FINISH) into exactly deflateBound bytes returns Z_STREAM_END, for any accepted parameters, dictionary (up to 32 KiB) and gzip header (fields up to 4 KiB) and data of up to 1 MiB; compressBound(n) is at least n, and at the default parameters deflateBound is at most compressBound.

  • x_deflate_bound_splitC file · 112 lines

    With the data given in any pieces with Z_NO_FLUSH, then Z_FINISH, and any output space per call (up to 1 MiB), the total output never exceeds deflateBound (same bounds as x_deflate_bound).

  • x_compress_roundtripC file · 77 lines

    For data of up to 1 MiB and any level: compress2 into compressBound bytes returns Z_STREAM_ERROR exactly for a level outside -1..9, else Z_OK with at most that many bytes; uncompress and uncompress2 give back exactly the data; with one byte too little room uncompress returns Z_BUF_ERROR, and a truncated stream is never accepted.

  • x_adler32_refC file · 49 lines

    adler32 and adler32_z equal the Adler-32 of RFC 1950 for any valid starting value and any buffer of up to 1 MiB, also when split into two calls; with a Z_NULL buffer they return 1.

  • x_adler32_combine_refC file · 53 lines

    adler32_combine gives the Adler-32 of a concatenation (two buffers of up to 1 MiB each), equals RFC 1950's algebraic combination for any valid checksums and any length of 0 or more, and returns 0xffffffff for a negative length.

  • x_crc32_refC file · 47 lines

    crc32 and crc32_z equal the bit-by-bit CRC-32 of RFC 1952 for any starting value and any buffer of up to 1 MiB, also when split into two calls; with a Z_NULL buffer they return 0; get_crc_table returns the CRC of every byte value.

  • x_crc32_combine_refC file · 51 lines

    crc32_combine, and crc32_combine_op with crc32_combine_gen, give the CRC-32 of a concatenation (two buffers of up to 1 MiB each); for a negative length they return 0.

Limits

Each theorem is harness_safe whole_prog, where whole_prog is the spec linked with the zlib files it uses. By VST's adequacy theorem it means that for every value the spec draws, no run has undefined behaviour in CompCert's semantics of C and every check in the spec holds. That adequacy theorem is not yet instantiated in Rocq for QuickProof's environment.

  • Termination is not proved. A run that never returns is not a counterexample.
  • The theorems are about the C code as CompCert 3.15 defines it for x86_64-linux, in one thread. A binary built by another compiler is outside them. Running out of stack is not ruled out.
  • crc32 is proved for its byte-at-a-time loop. A default build on x86_64 uses the braided loop, which is not covered.
  • Any malloc may return NULL, and the theorems cover those runs. After a failed allocation or Z_MEM_ERROR, most specs stop and claim nothing more about that run.
  • Memory leaks are ruled out only where a spec counts allocations: res_free_deflate and res_free_inflate.
  • The gz* file API and infback.c are not covered.
  • The theorems are about zlib 1.3.2 with the edits listed in the repository (below). Nothing is proved about the unmodified code.
  • The result trusts Rocq, VST, CompCert's semantics of C, clightgen, QuickProof's translation scripts, its model of the environment and qp verify, and the text of each spec (What a proof means).

How to check it

You need 64-bit x86 Linux with Coq 8.20.1, CompCert 3.15 and VST 2.15 (Install), or QuickProof's Docker image. Check the proof with a QuickProof checkout of your own at v0.1.0, the release the repository pins:

shell
git clone --branch v0.1.0 https://github.com/genproof/quickproof-public.git quickproof
git clone --recursive https://github.com/genproof/zlib-full-auto-proofs-public.git
quickproof/tools/qp verify zlib-full-auto-proofs-public --base contract

The tag contract holds the specs, the code and the 62 theorems before any proof. qp verify rebuilds every proof from a fresh clone. It checks that the statements are those of that tag and that nothing is admitted, and it lists the axioms each theorem uses.

A run of qp verify takes about 8 hours with 8 build jobs on 16 CPUs.

The code under test

The code is zlib 1.3.2, upstream commit da607da739fa: the core library without the gz* file API and without infback.c. The repository's patch/PATCH.md describes every edit, and every changed line keeps the original in a comment. Idiom edits and two deviations adapt the code to VST and CompCert and are meant to change no behaviour; a differential test compares the edited and the original zlib on random streams. The other edits fix bugs that the specs found, and each changes zlib's behaviour only in the case its bug describes. The edits are tested, not proved.

Bugs found

Some properties were false on zlib 1.3.2 as released:

  • Raw deflate(Z_FINISH) returned Z_OK when the last block exactly filled the output (issue #1300, fixed upstream by #1326).
  • A 32-bit sum in deflate_stored() could end a level-0 stream with input unread. Through compress2_z() this happened for some inputs over 51 TiB (issue #1348, fixed upstream in 2bed3d61). res_compress_bound needs this fix.
  • inflate() missed header bytes in total_in on Z_NEED_DICT (pull request #1297; fixed upstream in 066e0b68).
  • After inflatePrime(), inflate()'s fast path could rewind next_in before the input (fixed upstream in e7bb9788).
  • After inflateSync() and inflateReset2(), inflate() could write into a 1-byte window (fixed upstream in 8179479c).
  • inflateReset() kept the previous stream's window size (fixed upstream in c0424159).
  • inflate() stored a header's window size before checking it; upstream documented the behaviour instead (dfa96642).
  • deflateBound() is not an upper bound for Z_FIXED at levels 1-3 (reported; not fixed upstream yet).
  • adler32(x, Z_NULL, 1) reads buf[0]. That issue (#1283) was closed without a change.

We report every bug to its maintainers before we publish anything about it.

Maintained by Vladimir Kukharenko.