Browse zlib specs (4 of 62)

Proofs / zlib / Round trips

rt_session

One session with everything at once: any wrapper, a preset dictionary or a full gzip header, the data in any pieces with any flush and output room, any bytes after the stream: every call accounts for its pointers, the dictionary is asked for exactly when it should be, and the data and every header field come back exactly.

spec
204 lines of C
with its headers
296 lines
status
Proved
4 of 62
On this page

The spec

The spec is the C program harness/rt_session.c, 204 lines, shown whole as it is in the repository at 37189f4. It includes harness/laws_common.h (40 lines) and harness/laws_session.h (52 lines). Its first comment states the property in full, with every bound.

C
// Law rt_session: For any level, windowBits, memLevel and strategy in zlib.h's ranges for deflateInit2 (raw, zlib or
// gzip wrapper), with or without, after it, deflateSetDictionary of any dictionary (1 to 2^32 - 1 bytes; zlib or raw
// wrapper) or deflateSetHeader of any gzip header (text, os, hcrc: any ints; time below 2^32; an extra field of up to
// 65535 bytes, a name and a comment of up to 2^32 - 2 nonzero bytes, each present or not; gzip wrapper), and any data
// (any length the allocator provides) given to deflate() in any pieces (at most 2^32 - 1 bytes per call), with any
// output space (at most 2^32 - 1 bytes per call, none included, from a buffer of any size; running out of it ends the
// run) and any flush Z_NO_FLUSH..Z_BLOCK per call (Z_FINISH coming with the rest of the data once one call can take it,
// and repeated until Z_STREAM_END), then inflateInit2 with the matching windowBits, inflateGetHeader with buffers of
// exactly the fields' sizes (if a header was set), inflateSetDictionary of a copy of the dictionary (raw wrapper: after
// inflateInit2; zlib wrapper: when inflate() returns Z_NEED_DICT), and inflate() fed the compressed bytes followed by
// any bytes (any number up to PTRDIFF_MAX minus the stream's length) in any pieces, empty ones included, with any
// output space, none included, and any flush: deflateInit2, deflateSetDictionary, deflateSetHeader, inflateInit2,
// inflateGetHeader and inflateSetDictionary return Z_OK; every call moves next_in and next_out exactly as far as it
// lowers avail_in and avail_out; a deflate() call offered no output space returns Z_BUF_ERROR and moves no pointer and
// no counter; inflate() returns only Z_OK, Z_BUF_ERROR or Z_NEED_DICT until Z_STREAM_END, Z_NEED_DICT exactly once when
// a dictionary was set with the zlib wrapper and never otherwise, a call offered neither input nor output space does
// not return Z_OK and moves no pointer and no counter, and at Z_STREAM_END it has read exactly the compressed bytes,
// none of the bytes after them, written exactly the data, as a copy made before compression holds it, and reported the
// header complete with the fields that copies made before compression hold, and Z_NULL for an absent one (Z_MEM_ERROR
// ends the run).
#include "laws_common.h"
#include "laws_session.h"

static unsigned char *any_string(size_t len) {
	unsigned char *string = alloc_any_bytes(len + 1);
	if (string == NULL)
		return NULL;
	for (size_t i = 0; i < len; i++)
		gp_assume(string[i] != 0);
	string[len] = 0;
	return string;
}

static int same_field(int present, unsigned char *got, unsigned char *given, size_t len) {
	if (!present)
		return got == Z_NULL;                        // zlib.h: absent fields are "set to Z_NULL"
	return got != Z_NULL && bytes_eq(got, given, len);
}

int main(void) {
	int level = (int) nondet_u32();
	int window_bits = (int) nondet_u32();
	int mem_level = (int) nondet_u32();
	int strategy = (int) nondet_u32();
	gp_assume(deflate_params_ok(level, window_bits, mem_level, strategy));
	unsigned char choice = nondet_u8();
	int with_dict = window_bits <= 15 && (choice & 1);
	int with_head = window_bits > 15 && (choice & 1);
	// RFC 1952 2.3: MTIME is 4 bytes, OS 1, XLEN 2; the name and the comment are "zero-terminated"
	size_t dict_len = 1 + upto(UINT_MAX - 1);
	size_t extra_len = upto(65535);
	size_t name_len = upto(UINT_MAX - 1);
	size_t comment_len = upto(UINT_MAX - 1);
	size_t data_len = upto(PTRDIFF_MAX);
	size_t out_size = upto(PTRDIFF_MAX);
	int text = (int) nondet_u32();
	uLong time = nondet_u32();
	int os = (int) nondet_u32();
	int hcrc = (int) nondet_u32();
	unsigned char *dict = alloc_any_bytes(dict_len);
	unsigned char *extra = alloc_any_bytes(extra_len);
	unsigned char *name = any_string(name_len);
	unsigned char *comment = any_string(comment_len);
	unsigned char *data = alloc_any_bytes(data_len);
	if (!dict || !extra || !name || !comment || !data)
		return 0;
	unsigned char *dict_copy = copy_of(dict, dict_len);
	unsigned char *extra_copy = copy_of(extra, extra_len);
	unsigned char *name_copy = copy_of(name, name_len + 1);
	unsigned char *comment_copy = copy_of(comment, comment_len + 1);
	unsigned char *expected = copy_of(data, data_len);
	unsigned char *compressed = malloc(out_size);
	unsigned char *out = malloc(data_len);
	gz_header head;
	head.text = text;
	head.time = time;
	head.os = os;
	head.hcrc = hcrc;
	head.extra = (choice & 2) ? extra : Z_NULL;
	head.extra_len = (uInt) extra_len;
	head.name = (choice & 4) ? name : Z_NULL;
	head.comment = (choice & 8) ? comment : Z_NULL;
	gz_header got;
	got.extra = malloc(extra_len);
	got.extra_max = (uInt) extra_len;
	got.name = malloc(name_len + 1);
	got.name_max = (uInt) (name_len + 1);
	got.comment = malloc(comment_len + 1);
	got.comm_max = (uInt) (comment_len + 1);
	if (!dict_copy || !extra_copy || !name_copy || !comment_copy || !expected || !compressed || !out)
		return 0;
	if (!got.extra || !got.name || !got.comment)
		return 0;
	z_stream compressor;
	new_stream(&compressor);
	int code = deflateInit2(&compressor, level, Z_DEFLATED, window_bits, mem_level, strategy);
	if (code == Z_MEM_ERROR)
		return 0;
	gp_assert(code == Z_OK);
	// zlib.h, deflateSetDictionary and deflateSetHeader: "returns Z_OK if success"
	if (with_dict)
		gp_assert(deflateSetDictionary(&compressor, dict, (uInt) dict_len) == Z_OK);
	if (with_head)
		gp_assert(deflateSetHeader(&compressor, &head) == Z_OK);
	compressor.next_in = data;
	compressor.next_out = compressed;
	size_t offered = 0;
	int flush = Z_NO_FLUSH;
	struct position at;
	do {
		size_t read = (size_t) (compressor.next_in - data);
		if (flush != Z_FINISH) {
			offered += upto(data_len - offered);
			flush = (int) upto(Z_BLOCK);
			if (flush == Z_FINISH && data_len - read > UINT_MAX)
				flush = Z_NO_FLUSH;
			if (flush == Z_FINISH)
				offered = data_len;
		}
		compressor.avail_in = clip(offered - read);
		compressor.avail_out = clip(upto(out_size - (size_t) (compressor.next_out - compressed)));
		position_of(&compressor, &at);

		code = deflate(&compressor, flush);

		// zlib.h, deflate: "Compress more input starting at next_in and update next_in and avail_in accordingly";
		// "Z_BUF_ERROR if no progress is possible (for example avail_in or avail_out was zero)"
		gp_assert(accounted(&compressor, &at));
		if (at.avail_out == 0)
			gp_assert(code == Z_BUF_ERROR && unmoved(&compressor, &at));
		if (code != Z_STREAM_END && compressor.next_out == compressed + out_size)
			return 0;
	} while (code != Z_STREAM_END);
	size_t compressed_len = (size_t) (compressor.next_out - compressed);
	// RFC 1950 2.2: "Any data which may appear after ADLER32 are not part of the zlib stream." zlib.h,
	// inflateInit2: "inflate() will return Z_STREAM_END at the end of the gzip member."
	size_t after = upto(PTRDIFF_MAX - compressed_len);
	unsigned char *input = alloc_any_bytes(compressed_len + after);
	if (input == NULL)
		return 0;
	for (size_t i = 0; i < compressed_len; i++)
		input[i] = compressed[i];
	z_stream decompressor;
	new_stream(&decompressor);
	// zlib.h, deflateInit2: "a request for 8 will result in 9"; "use 9 with inflateInit2()"
	if (window_bits == 8)
		window_bits = 9;
	code = inflateInit2(&decompressor, window_bits);
	if (code == Z_MEM_ERROR)
		return 0;
	gp_assert(code == Z_OK);
	if (with_head)
		gp_assert(inflateGetHeader(&decompressor, &got) == Z_OK);
	// zlib.h, inflateSetDictionary: "For raw inflate, this function can be called at any time to set the
	// dictionary."; "This function must be called immediately after a call of inflate, if that call returned
	// Z_NEED_DICT."
	if (with_dict && window_bits < 0) {
		code = inflateSetDictionary(&decompressor, dict_copy, (uInt) dict_len);
		if (code == Z_MEM_ERROR)
			return 0;
		gp_assert(code == Z_OK);
	}
	int asked = 0;
	decompressor.next_in = input;
	decompressor.next_out = out;
	do {
		decompressor.avail_in = clip(upto(compressed_len + after - (size_t) (decompressor.next_in - input)));
		decompressor.avail_out = clip(upto(data_len - (size_t) (decompressor.next_out - out)));
		position_of(&decompressor, &at);

		code = inflate(&decompressor, (int) nondet_u32());

		if (code == Z_MEM_ERROR)
			return 0;
		gp_assert(code == Z_OK || code == Z_BUF_ERROR || code == Z_STREAM_END || code == Z_NEED_DICT);
		gp_assert(accounted(&decompressor, &at));
		// zlib.h, inflate() "returns Z_OK if some progress has been made (more input processed or more output
		// produced)"
		if (at.avail_in == 0 && at.avail_out == 0)
			gp_assert(code != Z_OK && unmoved(&decompressor, &at));
		if (code == Z_NEED_DICT) {
			gp_assert(with_dict && window_bits > 0 && !asked);
			asked = 1;
			code = inflateSetDictionary(&decompressor, dict_copy, (uInt) dict_len);
			if (code == Z_MEM_ERROR)
				return 0;
			gp_assert(code == Z_OK);
		}
	} while (code != Z_STREAM_END);
	gp_assert(asked == (with_dict && window_bits > 0));
	gp_assert(decompressor.next_in == input + compressed_len);
	gp_assert(decompressor.next_out == out + data_len && bytes_eq(out, expected, data_len));
	if (!with_head)
		return 0;
	// zlib.h, inflateGetHeader: "head->done is set to one" once the header is complete; "If any of extra, name, or
	// comment are not present in the header, then that field's pointer is set to Z_NULL"
	gp_assert(got.done == 1 && got.text == (text != 0) && got.hcrc == (hcrc != 0));
	gp_assert(got.os == (os & 255) && got.time == time);
	gp_assert(same_field(choice & 2, got.extra, extra_copy, extra_len));
	gp_assert(!(choice & 2) || got.extra_len == extra_len);
	gp_assert(same_field(choice & 4, got.name, name_copy, name_len + 1));
	gp_assert(same_field(choice & 8, got.comment, comment_copy, comment_len + 1));
	return 0;
}
harness/laws_common.h, 40 lines
C
// laws_common.h: trivial helpers shared by the zlib laws (each law includes it once). No models, no algorithms.
#include <limits.h>
#include <stdlib.h>
#include "quickproof.h"
#include "zlib.h"
static size_t upto(size_t max) {
	size_t value = nondet_size();
	return value < max ? value : max;
}
static uInt clip(size_t n) { return n < UINT_MAX ? (uInt) n : UINT_MAX; }
static unsigned char *alloc_any_bytes(size_t n) {
	unsigned char *bytes = malloc(n);
	if (bytes != NULL)
		nondet_bytes(bytes, n);
	return bytes;
}
static unsigned char *copy_of(const unsigned char *source, size_t n) {
	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) {
	for (size_t i = 0; i < n; i++)
		if (a[i] != b[i])
			return 0;
	return 1;
}
static void set_buffer(z_stream *strm, unsigned char *in, size_t in_len, unsigned char *out, size_t out_len) {
	strm->next_in = in;
	strm->avail_in = (uInt) in_len;
	strm->next_out = out;
	strm->avail_out = (uInt) out_len;
}
static void new_stream(z_stream *strm) {
	strm->zalloc = Z_NULL;
	strm->zfree = Z_NULL;
	strm->opaque = Z_NULL;
	set_buffer(strm, Z_NULL, 0, Z_NULL, 0);
}
harness/laws_session.h, 52 lines
C
// laws_session.h: helpers of the laws that drive a z_stream, included after laws_common.h. No models, no algorithms.
static int deflate_params_ok(int level, int window_bits, int mem_level, int strategy) {
	// zlib.h, deflateInit2: level "Z_DEFAULT_COMPRESSION, or between 0 and 9"; memLevel 1..MAX_MEM_LEVEL (9,
	// zconf.h); strategy Z_DEFAULT_STRATEGY (0) .. Z_FIXED (4); windowBits 8..15, "-8..-15 for raw deflate", "Add 16
	// to windowBits to write a simple gzip header", but "For raw deflate or gzip encoding, a request for a 256-byte
	// window is rejected as invalid"
	int zlib_window = window_bits >= 8 && window_bits <= 15;
	int raw_window = window_bits >= -15 && window_bits <= -9;
	int gzip_window = window_bits >= 16 + 9 && window_bits <= 16 + 15;
	int valid = level >= -1 && level <= 9 && mem_level >= 1 && mem_level <= 9 && strategy >= 0 && strategy <= Z_FIXED;
	return valid && (zlib_window || raw_window || gzip_window);
}
static int inflate_window_ok(int window_bits) {
	// zlib.h, inflateInit2: windowBits "should be in the range 8..15", "can also be zero to request that inflate
	// use the window size in the zlib header", "can also be -8..-15 for raw inflate", "Add 32 to windowBits to
	// enable zlib and gzip decoding with automatic header detection, or add 16 to decode only the gzip format"
	int low = window_bits & 15;
	int raw = window_bits >= -15 && window_bits <= -8;
	int wrapped = window_bits >= 0 && window_bits < 48 && (low == 0 || low >= 8);
	return raw || wrapped;
}
struct position {
	unsigned char *next_in;
	uInt avail_in;
	unsigned char *next_out;
	uInt avail_out;
	uLong total_in;
	uLong total_out;
};
static void position_of(z_stream *strm, struct position *at) {
	at->next_in = strm->next_in;
	at->avail_in = strm->avail_in;
	at->next_out = strm->next_out;
	at->avail_out = strm->avail_out;
	at->total_in = strm->total_in;
	at->total_out = strm->total_out;
}
static int unmoved(z_stream *strm, struct position *at) {
	int in = strm->next_in == at->next_in && strm->avail_in == at->avail_in && strm->total_in == at->total_in;
	int out = strm->next_out == at->next_out && strm->avail_out == at->avail_out && strm->total_out == at->total_out;
	return in && out;
}
static int accounted(z_stream *strm, struct position *at) {
	int in = strm->avail_in <= at->avail_in && strm->next_in + strm->avail_in == at->next_in + at->avail_in;
	int out = strm->avail_out <= at->avail_out && strm->next_out + strm->avail_out == at->next_out + at->avail_out;
	return in && out;
}
static int counted(z_stream *strm, struct position *at) {
	int in = strm->total_in == at->total_in + (at->avail_in - strm->avail_in);
	int out = strm->total_out == at->total_out + (at->avail_out - strm->avail_out);
	return in && out;
}

The theorem

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

Rocq
Theorem rt_session : 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 rt_session : harness_safe Zlib.contracts.rt_session.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 Zlib.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
  • adler32.c
  • crc32.c
  • deflate.c
  • trees.c
  • inflate.c
  • inffast.c
  • inftrees.c
  • zutil.c
  • quickproof/libc/libc.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), and binaries built by a compiler (the theorem is about the code as CompCert defines C for x86_64, LP64), one thread.
  • Where zlib reports Z_MEM_ERROR, most specs end the run and claim nothing about it; the first comment of the spec says so.
  • The edits to zlib's code, listed in the repository, are tested, 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.