x_valid_info

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

spec: 112 lines of C
with its headers: 1,406 lines
status: Proved; 40 of 44

On this page

The spec

The spec is the C program harness/x_valid_info.c, 112 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.

// Law valid_info (PROMISES.md: I1-I6): the frame-inspection functions on ANY series of compliant frames, with or
// without ANY dictionary (harness/writer.h).
//
// Claim (QuickProof.Contract.harness_safe of this program): no execution has undefined behaviour, and every gp_assert
// holds; at the start of each frame of the series (zstd.h):
//   ZSTD_findFrameCompressedSize = the frame's size (a skippable frame: "its content size + 8 bytes");
//   ZSTD_getFrameContentSize = its Frame_Content_Size, or ZSTD_CONTENTSIZE_UNKNOWN when absent; 0 for a skippable frame;
//   ZSTD_getDictID_fromFrame = its Dictionary_ID (0 when absent, and for a skippable frame);
//   ZSTD_isFrame = 1; ZSTD_isSkippableFrame = whether it is skippable;
//   ZSTD_getFrameHeader = 0, with the frame's frameContentSize, windowSize, blockSizeMax, frameType, headerSize,
//     dictID and checksumFlag (a skippable frame: its content size, type and "skippable magic variant");
//   ZSTD_frameHeaderSize = its header's size (Zstandard frames);
//   ZSTD_readSkippableFrame = its user data and magic variant, or an error when dstCapacity cannot hold them;
// for the whole series: ZSTD_findDecompressedSize = the content size when every Zstandard frame declares its size, else
// ZSTD_CONTENTSIZE_UNKNOWN; ZSTD_decompressBound = the sum per frame of the declared size, or "# blocks * min(128 KB,
// Window_Size)"; and ZSTD_getDictID_fromDict = the dictionary's ID (0 for a raw-content dictionary).  A frame whose
// window is beyond zstd's range may give an error instead (zlimits.h).
#include <stdlib.h>
#include "quickproof.h"
#include "writer.h"
#include "zlimits.h"

static wdict_t wd;
static wseries_t sr;

int main(void)
{
	int withdict = choose(2), anybig = 0, allfcs = 1;
	unsigned char *src, *dst;
	size_t cap, r, i;
	unsigned long long bound = 0;
	unsigned k;
	if (withdict) {
		w_dict(&wd);
		w_series(&sr, &wd);
		gp_assert(ZSTD_getDictID_fromDict(wd.bytes, wd.n) == (wd.formatted ? wd.id : 0));
	} else {
		w_series(&sr, 0);
	}
	cap = choose_in(0, W_SKIP_MAX + 4);
	src = exact_copy(sr.bytes, sr.n);
	dst = malloc(cap > 0 ? cap : 1);
	if (src == NULL || dst == NULL) {
		free(src);
		free(dst);
		return 0;                       /* harness out of memory: end the run */
	}
	for (k = 0; k < sr.nframes; k++) {
		const winfo_t *f = &sr.f[k];
		const unsigned char *p = src + f->start;
		size_t rest = sr.n - f->start;
		int big = !f->skippable && !f->single && f->window_log > ZSTD_WINDOWLOG_MAX;
		unsigned long long c;
		ZSTD_FrameHeader zfh;
		anybig |= big;
		if (!f->skippable) {
			if (f->fcs_present)
				bound += f->fcs;
			else {
				bound += (unsigned long long) f->blocks * (f->window < (1ULL << 17) ? f->window : (1ULL << 17));
				allfcs = 0;
			}
		}
		r = ZSTD_findFrameCompressedSize(p, rest);
		gp_assert(r == f->size || (big && ZSTD_isError(r)));
		c = ZSTD_getFrameContentSize(p, rest);
		if (f->skippable)
			gp_assert(c == 0);
		else
			gp_assert(c == (f->fcs_present ? f->fcs : ZSTD_CONTENTSIZE_UNKNOWN) || (big && c == ZSTD_CONTENTSIZE_ERROR));
		gp_assert(ZSTD_getDictID_fromFrame(p, rest) == (f->skippable ? 0 : f->did) || big);
		gp_assert(ZSTD_isFrame(p, rest) == 1);
		gp_assert(ZSTD_isSkippableFrame(p, rest) == f->skippable);
		r = ZSTD_getFrameHeader(&zfh, p, rest);
		gp_assert(r == 0 || (big && ZSTD_isError(r)));
		if (r == 0 && f->skippable) {
			gp_assert(zfh.frameType == ZSTD_skippableFrame);
			gp_assert(zfh.frameContentSize == f->skip_n);
			gp_assert(zfh.dictID == f->variant);
		} else if (r == 0) {
			gp_assert(zfh.frameType == ZSTD_frame);
			gp_assert(zfh.frameContentSize == (f->fcs_present ? f->fcs : ZSTD_CONTENTSIZE_UNKNOWN));
			gp_assert(zfh.windowSize == f->window);
			gp_assert(zfh.blockSizeMax == (f->window < (1ULL << 17) ? f->window : (1ULL << 17)));
			gp_assert(zfh.headerSize == f->hsize);
			gp_assert(zfh.dictID == f->did);
			gp_assert(zfh.checksumFlag == f->checksum);
		}
		if (!f->skippable)
			gp_assert(ZSTD_frameHeaderSize(p, rest) == f->hsize);
		if (f->skippable) {
			unsigned v = 0;
			r = ZSTD_readSkippableFrame(dst, cap, &v, p, rest);
			if (cap >= f->skip_n) {
				gp_assert(r == f->skip_n);
				gp_assert(v == f->variant);
				for (i = 0; i < r; i++)
					gp_assert(dst[i] == p[8 + i]);
			} else {
				gp_assert(ZSTD_isError(r));
			}
		}
	}
	{
		unsigned long long d = ZSTD_findDecompressedSize(src, sr.n), b = ZSTD_decompressBound(src, sr.n);
		gp_assert(d == (allfcs ? sr.content_n : ZSTD_CONTENTSIZE_UNKNOWN) || (anybig && d == ZSTD_CONTENTSIZE_ERROR));
		gp_assert(b == bound || (anybig && b == ZSTD_CONTENTSIZE_ERROR));
	}
	free(src);
	free(dst);
	return 0;
}

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

harness/zlimits.h, 63 lines

// 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_info.v:

Rocq

Theorem x_valid_info : 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_info : harness_safe Zstd.contracts.x_valid_info.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (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.

The spec#

The theorem#

What it leaves out#

How it was proved#

The spec

The theorem

What it leaves out

How it was proved