Browse zstd specs (13 of 44)

Proofs / zstd / The interface

api_untouched_output

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.

spec
44 lines of C
with its headers
77 lines
status
Proved
13 of 44
On this page

The spec

The spec is the C program harness/api_untouched_output.c, 44 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 api_untouched_output: For any input (any bytes, any length the allocator provides) given to
// ZSTD_decompressStream in any pieces, each call with any output space and start position (each piece and each output
// space an object of exactly its size), the stream reset after an error, no call changes the output space before the
// position it is given, and every call that returns no error writes only up to the position it returns: the bytes
// after it are as they were (an error leaves pos where it was, and the stream "in undefined state", zstd.h).
#include "laws_common.h"

int main(void) {
	size_t n = upto(PTRDIFF_MAX), read = 0;
	unsigned char *input = any_bytes(n);
	ZSTD_DStream *zds = ZSTD_createDStream();
	if (input == NULL || zds == NULL)
		return 0;
	do {
		// Each call: the next piece of the input and any output space with any start, as objects of their own
		size_t take = upto(n - read), room = upto(PTRDIFF_MAX);
		unsigned char *piece = copy_of(input + read, take), *out = any_bytes(room);
		unsigned char *before = out == NULL ? NULL : copy_of(out, room);
		if ((piece == NULL && take != 0) || (before == NULL && room != 0))
			return 0;
		ZSTD_inBuffer in;
		ZSTD_outBuffer output;
		in.src = piece;
		in.size = take;
		in.pos = 0;
		output.dst = out;
		output.size = room;
		output.pos = upto(room);
		size_t start = output.pos;
		size_t result = ZSTD_decompressStream(zds, &output, &in);
		// Check. zstd.h, ZSTD_outBuffer: pos is the "position where writing stopped"
		if (room != 0)
			gp_assert(bytes_eq(out, before, start) &&
			          (ZSTD_isError(result) || bytes_eq(out + output.pos, before + output.pos, room - output.pos)));
		read += in.pos;
		free(piece);
		free(out);
		free(before);
		if (ZSTD_isError(result))                    // zstd.h: after an error "it must be first reset"
			ZSTD_DCtx_reset(zds, ZSTD_reset_session_only);
	} while (nondet_u8() != 0);
	ZSTD_freeDStream(zds);
	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/api_untouched_output.v:

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