Browse zstd specs (24 of 44)

Proofs / zstd / Memory

res_memory_stream

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

spec
69 lines of C
with its headers
102 lines
status
Proved
24 of 44
On this page

The spec

The spec is the C program harness/res_memory_stream.c, 69 lines, shown whole as it is in the repository at 2e46017. It includes harness/laws_common.h (33 lines). Its first comment states the property in full, with every bound.

C
// Law res_memory_stream: Counted through the allocator it is given (ZSTD_customMem), a decompression context with
// ZSTD_d_windowLogMax set to any value zstd accepts (0: the default, 2^ZSTD_WINDOWLOG_LIMIT_DEFAULT bytes) never holds
// more than ZSTD_estimateDStreamSize(2^windowLogMax) bytes while it decodes any input (any bytes, any length the
// allocator provides) in any pieces with any output room, reset after errors: zstd.h, ZSTD_d_windowLogMax: "a size
// limit (in power of 2) beyond which the streaming API will refuse to allocate memory buffer"; ZSTD_estimate*(): "The
// ZSTD_DStream memory budget depends on frame's window Size. This information can be passed manually, using
// ZSTD_estimateDStreamSize".
#include "laws_common.h"
ZSTD_DCtx *ZSTD_createDCtx_advancedP(const ZSTD_customMem *mem);   // ZSTD_createDCtx_advanced(*mem) (patch/lawhooks.py)

// An allocator that counts the bytes zstd holds now and at most. Each block carries its size just in front of it;
// freeing anything else than a block from count_alloc, or one twice, is undefined behaviour here.
struct count {
	size_t now, peak;
};
static void *count_alloc(void *opaque, size_t size) {
	struct count *count = opaque;
	size_t *block = size <= PTRDIFF_MAX - sizeof (size_t) ? malloc(sizeof (size_t) + size) : NULL;
	if (block == NULL)
		return NULL;
	block[0] = size;
	count->now += size;
	if (count->now > count->peak)
		count->peak = count->now;
	return block + 1;
}
static void count_free(void *opaque, void *address) {
	struct count *count = opaque;
	size_t *block = (size_t *) address - 1;
	if (address == NULL)
		return;
	count->now -= block[0];
	free(block);
}

int main(void) {
	struct count count;
	ZSTD_customMem mem;
	count.now = count.peak = 0;
	mem.customAlloc = count_alloc;
	mem.customFree = count_free;
	mem.opaque = &count;
	int window_log = (int) nondet_u32();
	ZSTD_DCtx *dctx = ZSTD_createDCtx_advancedP(&mem);
	if (dctx == NULL || ZSTD_isError(ZSTD_DCtx_setParameter(dctx, ZSTD_d_windowLogMax, window_log)))
		return 0;
	size_t n = upto(PTRDIFF_MAX), cap = upto(PTRDIFF_MAX);
	unsigned char *src = any_bytes(n), *dst = malloc(cap);
	if (src == NULL || dst == NULL)
		return 0;
	ZSTD_inBuffer in;
	ZSTD_outBuffer out;
	in.src = src;
	in.size = 0;
	in.pos = 0;
	out.dst = dst;
	out.pos = 0;
	do {   // Each call: the input so far and any more of it, any room after the output so far
		in.size += upto(n - in.size);
		out.size = out.pos + upto(cap - out.pos);
		if (ZSTD_isError(ZSTD_decompressStream(dctx, &out, &in)))   // zstd.h, after an error: "it must be first
			ZSTD_DCtx_reset(dctx, ZSTD_reset_session_only);     // reset"
	} while (nondet_u8() != 0);
	// Check
	size_t max_window = (size_t) 1 << (window_log == 0 ? ZSTD_WINDOWLOG_LIMIT_DEFAULT : window_log);
	gp_assert(count.peak <= ZSTD_estimateDStreamSize(max_window));
	ZSTD_freeDCtx(dctx);
	return 0;
}
harness/laws_common.h, 33 lines
C
// laws_common.h: trivial helpers shared by the zstd laws (each law includes it once). No models, no algorithms.
#define ZSTD_STATIC_LINKING_ONLY                     // zstd.h's experimental part (ZSTD_WINDOWLOG_MAX, ...)
#include <stdint.h>
#include <stdlib.h>
#include "quickproof.h"
#include "zstd.h"
#include "zstd_errors.h"
uint64_t ZSTD_XXH64(const void *input, size_t length, uint64_t seed);   // zstd's XXH64 (law ck_xxh64 checks it)
static size_t upto(size_t max) {                    // any value from 0 to max
	size_t value = nondet_size();
	return value < max ? value : max;
}
static unsigned char *any_bytes(size_t n) {         // a new object of n arbitrary bytes (NULL if malloc fails)
	unsigned char *bytes = malloc(n);
	if (bytes != NULL && n != 0)
		nondet_bytes(bytes, n);
	return bytes;
}
static unsigned char *copy_of(const unsigned char *source, size_t n) {   // a new object holding source[0..n-1]
	unsigned char *copy = malloc(n);
	for (size_t i = 0; copy != NULL && i < n; i++)
		copy[i] = source[i];
	return copy;
}
static int bytes_eq(const unsigned char *a, const unsigned char *b, size_t n) {   // a[0..n-1] == b[0..n-1]
	for (size_t i = 0; i < n; i++)
		if (a[i] != b[i])
			return 0;
	return 1;
}
static int out_of_memory(size_t result) {           // zstd could not allocate (this ends a run: no claim)
	return ZSTD_getErrorCode(result) == ZSTD_error_memory_allocation;
}

The theorem

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

Rocq
Theorem res_memory_stream : 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 res_memory_stream : harness_safe Zstd.contracts.res_memory_stream.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 Zstd.contracts.suite.suite)))))))))))))). 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.