zstd's decoder

We proved 44 C specs of zstd's decoder. Each spec states a property, and each has a theorem in Rocq (formerly Coq). Twenty-five are short specs that quote the text they come from: RFC 8878, zstd.h or the xxHash specification. On any input the decoder is safe and keeps within its buffers, valid frames decode to exactly their content, invalid frames are refused, and memory stays within zstd's own estimates and is all given back. The other 19 are the longer specs of our first zstd proof, which draw compliant frames, compressed blocks and dictionaries included, within stated bounds. AI agents wrote the proof, about 430,000 lines of Rocq, and Rocq checks it. The specs, the proof and every change to the code are in genproof/zstd-auto-proofs-public.

The short specs#

Each spec links to its page, which shows the spec whole, as it is in the repository, with its theorem. A short spec is 10 to 78 lines of C. In a spec, nondet_*, upto(max), any_bytes(n) and pick(x) stand for any value, 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.

The valid frames of these specs hold only Raw and RLE blocks, which harness/frames.h (115 lines) writes field by field as RFC 8878 lays them out. zstd's compressor is not part of the code under test, so valid frames are written by hand. In the short specs, compressed blocks (Huffman literals, FSE sequences) appear only as any bytes.

The standard on valid input#

Frames as RFC 8878 lays them out decode to exactly their content. 3 specs

• rfc_frameC file · 24 lines

  A frame of Raw and RLE blocks in any header form, with or without a checksum, decodes with ZSTD_decompress, given room for its content, to exactly its content.

• rfc_concatC file · 35 lines

  Any number of such frames one after the other decode to their contents one after the other.

• rfc_skippableC file · 40 lines

  Skippable frames (any magic of the 16, any user data up to 2^32 - 1 bytes) anywhere among them add nothing.

Rejecting bad input#

Any input is safe, and invalid frames are refused. 8 specs

• rj_any_inputC file · 29 lines

  On any bytes, with any capacity, ZSTD_decompress and a reused context's ZSTD_decompressDCtx return an error or a size at most the capacity. With the theorem's "no undefined behaviour", no input makes these calls access memory outside their objects.

• rj_any_streamC file · 41 lines

  On any bytes in any pieces, with any buffers and start positions, the stream reset after each error, ZSTD_decompressStream keeps both positions within their buffers and never moves them back.

• rj_any_dictC file · 30 lines

  On any dictionary bytes and any input, ZSTD_decompress_usingDict returns an error or a size at most the capacity. The dictionary and the output are one object (the spec explains why).

• rj_bad_checksumC file · 30 lines

  A frame whose checksum is changed to any other value is refused: ZSTD_error_checksum_wrong one-shot, never complete when streamed.

• rj_content_sizeC file · 31 lines

  A frame whose Frame_Content_Size declares any other size than its content's (2^64 - 1, which means "unknown", is left out) is refused, one-shot and streamed.

• rj_reserved_bitC file · 28 lines

  A frame with the header's Reserved_bit set is refused, one-shot and streamed.

• rj_reserved_blockC file · 35 lines

  A frame where any one block's type is changed to 3 (Reserved) is refused, one-shot and streamed.

• rj_truncatedC file · 29 lines

  Any part of a frame that stops before its end is never taken for a complete frame, one-shot or streamed.

The interface#

The functions of zstd.h return and write what zstd.h says. 10 specs

• api_split_invariantC file · 49 lines

  For any accepted ZSTD_d_windowLogMax, a series of frames streamed in any pieces with any output room ends as one-shot decoding ends: when one-shot decoding fails, the stream never completes after reading everything; when it succeeds, the stream completes with exactly the same bytes.

• api_untouched_outputC file · 44 lines

  On any input in any pieces, the stream reset after each error, a stream call never changes the output before the position it is given, and a call that returns no error writes nothing after the position it returns.

• api_resetC file · 77 lines

  A context used for one-shot and streaming decoding of any inputs, with dictionaries loaded by copy and any ZSTD_d_windowLogMax, then reset with ZSTD_reset_session_and_parameters, behaves like a new one on any input (same results, positions and bytes; both fail or neither).

• api_short_outputC file · 24 lines

  A frame given less capacity than its content is refused with ZSTD_error_dstSize_tooSmall. The spec checks the error code only, not what is in dst.

• api_flush_boundC file · 34 lines

  On any input, the stream reset after each error, a stream call given no input writes at most ZSTD_BLOCKSIZE_MAX (128 KiB).

• api_content_sizeC file · 32 lines

  ZSTD_getFrameContentSize returns the declared size (any 64-bit value), ZSTD_CONTENTSIZE_UNKNOWN without the field, 0 for a skippable frame.

• api_frame_sizeC file · 27 lines

  ZSTD_findFrameCompressedSize returns exactly the size of the first frame, Zstandard or skippable, whatever follows.

• api_dict_idC file · 26 lines

  ZSTD_getDictID_fromFrame returns the frame's Dictionary_ID (any value, any field size), 0 for a skippable frame.

• api_ignore_checksumC file · 27 lines

  With ZSTD_d_forceIgnoreChecksum, a frame with any checksum decodes to exactly its content.

• api_free_nullC file · 10 lines

  ZSTD_freeDCtx, ZSTD_freeDStream, ZSTD_freeDDict accept NULL.

Memory#

Counted through the context's allocator: bounded, and all given back. 3 specs

• res_freeC file · 78 lines

  After any use (one-shot and streaming decoding, dictionaries loaded by copy, one referenced dictionary with or without ZSTD_d_refMultipleDDicts, any ZSTD_d_windowLogMax, resets), ZSTD_freeDCtx gives back every byte.

• res_memory_oneshotC file · 57 lines

  Decoding any inputs one-shot never holds more than ZSTD_estimateDCtxSize().

• res_memory_streamC file · 69 lines

  With any accepted ZSTD_d_windowLogMax, streaming any input, the stream reset after each error, never holds more than ZSTD_estimateDStreamSize(2^windowLogMax).

Checksum#

zstd's XXH64 is the xxHash specification's. 1 spec

• ck_xxh64C file · 60 lines

  ZSTD_XXH64 equals XXH64 as the xxHash specification defines it, written out in the spec, for any bytes and seed.

Earlier, longer properties#

These are the 19 specs of our first zstd proof, renamed x_<name> with their statements unchanged. Ten draw compliant frames, compressed blocks and dictionaries included, from the frame writer harness/writer.h; eight take any bytes; x_bound is about a macro. They are bounded: on any bytes, for example, input of at most 4096 bytes and output of at most 65536. The repository's SPECS.md gives every bound.

• x_any_oneshotC file · 52 lines

  One-shot decompression of any bytes into any capacity: an error or at most the capacity; ZSTD_freeDCtx accepts NULL.

• x_any_streamC file · 82 lines

  Streaming any bytes over any chunking: 0 <= pos <= size for input and output; at most ZSTD_BLOCKSIZE_MAX flushed without new input; resets after errors.

• x_any_dictC file · 78 lines

  Any dictionary bytes and any frame bytes through the by-reference dictionary APIs: an error or at most the capacity.

• x_any_dict_copyC file · 66 lines

  The same through the APIs that copy the dictionary.

• x_any_infoC file · 67 lines

  The frame-inspection functions on any bytes return what zstd.h documents (sizes within the input, "wanted" sizes, magic tests).

• x_any_info_extraC file · 55 lines

  ZSTD_getDecompressedSize and ZSTD_getFrameHeader_advanced on any bytes, as documented.

• x_any_paramsC file · 123 lines

  Any values of the decoding parameters (window limit, format, checksum, several dictionaries, block size): one-shot and streaming stay safe and within their buffers.

• x_any_bufferlessC file · 94 lines

  Buffer-less streaming (ZSTD_decompressContinue) on any bytes in any pieces, with or without a dictionary: an error or at most the capacity.

• x_boundC file · 16 lines

  ZSTD_COMPRESSBOUND(A) + ZSTD_COMPRESSBOUND(B) <= ZSTD_COMPRESSBOUND(A + B) for A, B of at least 128 KB with A + B < ZSTD_MAX_INPUT_SIZE.

• x_valid_oneshotC file · 62 lines

  Any series of compliant frames (every block, literal and table mode, header form, checksum, skippable frames) decodes one-shot to exactly its content; with room for it, it succeeds unless zlimits.h allows a refusal.

• x_valid_streamC file · 92 lines

  The same streamed in any pieces with any output room; the hint never asks for more than the frame holds.

• x_valid_dictC file · 79 lines

  Any dictionary (raw or formatted) and frames written with it, through the by-reference dictionary APIs: exactly the content.

• x_valid_dict_copyC file · 66 lines

  The same through the APIs that copy the dictionary.

• x_valid_dict_apiC file · 213 lines

  Several dictionaries selected by their ID (ZSTD_d_refMultipleDDicts), the _advanced loaders, the deprecated stream initialisation: exactly the content.

• x_valid_infoC file · 112 lines

  On compliant frames, the inspection functions report exactly the frames' sizes, content sizes and IDs.

• x_valid_paramsC file · 208 lines

  Compliant frames under any accepted decoding parameters decode to exactly their content.

• x_valid_bufferlessC file · 106 lines

  Buffer-less streaming of compliant frames, each call given exactly what it asks for: exactly the content, 0 through skippable frames.

• x_detectC file · 78 lines

  A compliant series with one frame's checksum changed or reserved bit set is refused, one-shot and streamed.

• x_stable_outC file · 89 lines

  ZSTD_d_stableOutBuffer: memory safe on any bytes; on compliant frames, every byte written is the content.

Limits#

Each theorem is harness_safe whole_prog, where whole_prog is the spec linked with the decoder. 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. An access outside an object or a use after free is undefined behaviour, so memory safety is part of every theorem. 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 covered.
• Any malloc may return NULL. When zstd reports ZSTD_error_memory_allocation, or the spec cannot allocate, the spec claims nothing more about that run.
• In the short specs, data has any length the allocator provides. Only frame windows are limited, to zstd's documented limits: 2 GiB in one call, 128 MiB for a stream by default.
• Error codes are not checked, except where a spec names one.
• The configuration has no assembly, no BMI2 and no legacy formats, and uses the plain Huffman loops. In-place decoding is left out, and so are four public functions that take a struct by value. The compressor is not covered.
• The theorems are about the decoder with the edits listed below. Nothing is proved about the unmodified code.
• Each theorem rests on 14 axioms: eight standard axioms of Rocq and six declarations of VST's malloc library. The result also trusts Rocq, VST, CompCert's semantics of C, clightgen, QuickProof's translation scripts, its model of the environment and qp verify (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:

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

The code under test#

The code is zstd's decoder at commit 01b7154f1172 on the dev branch (2026-09-18), after release v1.5.7: lib/common and lib/decompress, compiled as one unit. The repository's patch/GENPROOF-PATCH.md describes every edit, and every changed line carries a comment with the original. Idiom edits rewrite C that CompCert's semantics or VST cannot handle; differential tests against the original check most of them. Other edits fix places where the code differed from zstd's documentation, or where it reached expressions that CompCert's semantics leaves undefined. One added function passes the allocator by pointer for the memory specs. The edits are tested, not proved.

Bugs found#

Some specs were false on zstd's decoder at 01b7154f; the edits that make them hold are in the repository's patch/GENPROOF-PATCH.md. Reported upstream so far, on 2026-11-01:

• ZSTD_getDictID_fromFrame returns the magic variant (0-15) of a skippable frame as its dictionary ID, not 0 (api_dict_id; meta/zstd#4881).
• One-shot decoding refuses skippable frames whose Frame_Size is 2^32 - 8 or more, which RFC 8878 allows; streaming decoding skips them (rfc_skippable; meta/zstd#4882).
• Streaming decoding does not compare the decoded size with Frame_Content_Size when a frame ends with an empty last block, so it reports success on a frame shorter than it declares (rj_content_size; meta/zstd#4880).

Maintained by Vladimir Kukharenko.