Browse zstd specs (37 of 44)

Proofs / zstd / Earlier, longer properties

x_valid_dict

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

spec
79 lines of C
with its headers
1,373 lines
status
Proved
37 of 44
On this page

The spec

The spec is the C program harness/x_valid_dict.c, 79 lines, shown whole as it is in the repository at 2e46017. It includes harness/writer.h (1,231 lines) and harness/zlimits.h (63 lines). Its first comment states the property in full, with every bound.

C
// Law valid_dict (PROMISES.md: V8, V9, V1-V4): ANY dictionary (harness/writer.h: raw content, or formatted with entropy
// tables and repeat offsets) and ANY series of compliant frames written with it, decoded through the dictionary APIs
// that use the caller's dictionary by reference.
//
// Claim (QuickProof.Contract.harness_safe of this program): no execution has undefined behaviour, and every gp_assert
// holds: a success returns exactly the series' content; with a capacity that holds it, decoding succeeds unless a
// frame's window is beyond zstd's range or memory cannot be allocated (zlimits.h).  The APIs: 0
// ZSTD_decompress_usingDict; 1 ZSTD_createDDict_byReference + ZSTD_decompress_usingDDict; 2
// ZSTD_DCtx_loadDictionary_byReference, sticky ("they remain valid when same context is reused"): the series is decoded
// twice; 3 ZSTD_createDDict_byReference + ZSTD_DCtx_refDDict; 4 ZSTD_DCtx_refPrefix, "only used once" and "treated as
// raw content": a raw dictionary and a single frame.  The output and the dictionary are two regions of one allocation
// [dst | 1 byte | dict] (any_dict explains why); the APIs that copy the dictionary are in valid_dict_copy.
#include <stdlib.h>
#include "quickproof.h"
#include "writer.h"
#include "zlimits.h"

static wdict_t wd;
static wseries_t sr;

int main(void)
{
	size_t cap, r, i;
	unsigned char *src, *buf, *dst, *dict;
	unsigned api = choose(5), rounds, k;
	ZSTD_DCtx *dctx;
	ZSTD_DDict *ddict = NULL;
	w_dict(&wd);
	w_series(&sr, &wd);
	if (api == 4)
		gp_assume(!wd.formatted && sr.nframes == 1 && !sr.f[0].skippable);
	cap = choose_in(0, sr.content_n + 16);
	src = exact_copy(sr.bytes, sr.n);
	buf = malloc(cap + 1 + wd.n);
	dctx = ZSTD_createDCtx();
	rounds = (src != NULL && buf != NULL && dctx != NULL) ? (api == 2 ? 2 : 1) : 0;
	dst = buf;
	dict = NULL;
	if (buf != NULL)
		dict = buf + cap + 1;     /* not on NULL: NULL + n is undefined (C11 6.5.6p8) */
	if (rounds > 0) {
		for (i = 0; i < wd.n; i++)
			dict[i] = wd.bytes[i];
		if (api == 1 || api == 3) {
			ddict = ZSTD_createDDict_byReference(dict, wd.n);
			if (ddict == NULL)
				rounds = 0;             /* out of memory: end the run */
		}
	}
	for (k = 0; k < rounds; k++) {
		if (api == 0) {
			r = ZSTD_decompress_usingDict(dctx, dst, cap, src, sr.n, dict, wd.n);
		} else if (api == 1) {
			r = ZSTD_decompress_usingDDict(dctx, dst, cap, src, sr.n, ddict);
		} else {
			r = 0;
			if (k == 0) {
				r = api == 2 ? ZSTD_DCtx_loadDictionary_byReference(dctx, dict, wd.n)
				    : api == 3 ? ZSTD_DCtx_refDDict(dctx, ddict) : ZSTD_DCtx_refPrefix(dctx, dict, wd.n);
				if (ZSTD_isError(r))
					rounds = 1;         /* no dictionary loaded (e.g. out of memory): no second round */
			}
			if (!ZSTD_isError(r))
				r = ZSTD_decompressDCtx(dctx, dst, cap, src, sr.n);
		}
		if (!ZSTD_isError(r)) {
			gp_assert(r == sr.content_n);
			for (i = 0; i < r; i++)
				gp_assert(dst[i] == sr.content[i]);
		} else if (cap >= sr.content_n && within_oneshot(&sr)) {
			gp_assert(ZSTD_getErrorCode(r) == ZSTD_error_memory_allocation);
		}
	}
	ZSTD_freeDDict(ddict);
	ZSTD_freeDCtx(dctx);
	free(src);
	free(buf);
	return 0;
}

harness/writer.h (1,231 lines) is too long to show here; it is in the repository.

harness/zlimits.h, 63 lines
C
// The limits under which zstd may refuse a compliant frame, as its documents state them (PROMISES.md V4): "a decoder
// is allowed to reject a compressed frame which requests a memory size beyond decoder's authorized range"
// (format), zstd's range being ZSTD_WINDOWLOG_MAX (31 on 64-bit: zstd.h) for any decoding and, for streaming,
// "By default, a decompression context accepts window sizes <= (1 << ZSTD_WINDOWLOG_LIMIT_DEFAULT)" (zstd.h);
// the memory allocation of its contexts; and, for streaming, zstd's deliberate busy-loop guard (stall_error).
#ifndef ZSTD_HARNESS_ZLIMITS_H
#define ZSTD_HARNESS_ZLIMITS_H
#include "writer.h"
#ifndef ZSTD_STATIC_LINKING_ONLY
#define ZSTD_STATIC_LINKING_ONLY   /* ZSTD_WINDOWLOG_MAX, ZSTD_WINDOWLOG_LIMIT_DEFAULT */
#endif
#include "zstd.h"
#include "zstd_errors.h"

/* every Zstandard frame of the series is within zstd's window range (single-segment: Window_Size = content size) */
static int within_oneshot(const wseries_t *sr)
{
	unsigned k;
	for (k = 0; k < sr->nframes; k++)
		if (!sr->f[k].skippable && !sr->f[k].single && sr->f[k].window_log > ZSTD_WINDOWLOG_MAX)
			return 0;
	return 1;
}

/* ... and within the streaming default */
static int within_stream(const wseries_t *sr)
{
	unsigned k;
	for (k = 0; k < sr->nframes; k++)
		if (!sr->f[k].skippable && sr->f[k].window > (1ULL << ZSTD_WINDOWLOG_LIMIT_DEFAULT))
			return 0;
	return within_oneshot(sr);
}

/* zstd's busy-loop guard, deliberate (commit 31769ce70 "error on no forward progress": a caller "may be caught in an
   infinite loop, calling the streaming decompression function again and again, without making any progress";
   db18a62f8 gave it its error codes): ZSTD_decompressStream fails on the ZSTD_NO_FORWARD_PROGRESS_MAX-th (16 by
   default) call in a row that reads no input and writes no output, with noForwardProgress_destFull if the output is
   full, else noForwardProgress_inputEmpty (the input is then empty).  zstd.h does not document it.  True iff error
   code e is that error, legitimately: this call (fresh input, output position opos0 before it) read and wrote
   nothing, and so did the `stalled` calls in a row before it. */
#define NO_PROGRESS_MAX 16
static int stall_error(ZSTD_ErrorCode e, size_t stalled, const ZSTD_inBuffer *in, const ZSTD_outBuffer *out,
                       size_t opos0)
{
	if (stalled + 1 < NO_PROGRESS_MAX || in->pos != 0 || out->pos != opos0)
		return 0;
	if (e == ZSTD_error_noForwardProgress_destFull)
		return out->pos == out->size;
	return e == ZSTD_error_noForwardProgress_inputEmpty && out->pos < out->size && in->pos == in->size;
}

/* a copy of b[0..n) in a buffer of exactly n bytes (NULL: out of memory) */
static unsigned char *exact_copy(const unsigned char *b, size_t n)
{
	unsigned char *p = malloc(n > 0 ? n : 1);
	size_t i;
	if (p != NULL)
		for (i = 0; i < n; i++)
			p[i] = b[i];
	return p;
}
#endif

The theorem

QuickProof generated this statement from the spec, in src/contracts/x_valid_dict.v:

Rocq
Theorem x_valid_dict : harness_safe whole_prog.

src/contracts/laws.v states it on the spec's own program, whole_prog (the spec linked with the code under test), with its proof:

Rocq
Theorem x_valid_dict : harness_safe Zstd.contracts.x_valid_dict.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 Zstd.contracts.suite.suite_x))))))))))))). Qed.

Read as a statement about runs, it says that no run of the program has undefined behaviour or a failing check, for every value the spec can draw. That reading rests on VST's adequacy theorem, which is not yet instantiated in Rocq (formerly Coq) for QuickProof's environment.

The C files (units) its program links
  • patch/decoder.c
  • quickproof/libc/libc.c
  • quickproof/libc/malloc_unit.c

What it leaves out

  • What the first comment of the spec excludes, and its bounds.
  • Like every spec of this proof: termination (a run that never returns is not a counterexample), one thread, and binaries built by a compiler (the theorem is about the code as CompCert defines C for x86_64, LP64).
  • Other configurations of zstd (flags, legacy formats, assembly) and the compressor.
  • The edits to zstd's code, listed in the repository, are checked against the original by testing, not proved.

The summary page says what the proof as a whole covers.

How it was proved

AI agents wrote the proof, and Rocq checks it. qp verify passes on this repository: this statement is the one generated from the spec at the contract commit, and its proof uses only Rocq's standard axioms and VST's abstract malloc library.