Browse zlib specs (6 of 62)

Proofs / zlib / Round trips

rt_gzip_header

Every field of a gzip header (text flag, OS, time, extra field, name, comment; each present or not) comes back as it was given.

spec
110 lines of C
with its headers
150 lines
status
Proved
6 of 62
On this page

The spec

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

C
// Law rt_gzip_header: For any gzip header given to deflateSetHeader (text, os, hcrc: any ints; time below 2^32; an
// extra field of up to 65535 bytes, a name and a comment of any length up to 2^32 - 2 nonzero bytes, as much as
// inflateGetHeader's buffers take with the zero, each present or not), after deflateInit2 with any windowBits
// 16 + 9..15 and any level, memLevel and strategy it accepts and deflate(Z_FINISH) into deflateBound_z bytes, in pieces
// of at most 2^32 - 1 bytes (the run ends unless these succeed), inflate(Z_FINISH) with inflateGetHeader (buffers of
// exactly the fields' sizes) fed the compressed bytes in pieces of at most 2^32 - 1 bytes reports the header complete
// with the same fields as copies made before compression hold, and Z_NULL for an absent one (Z_MEM_ERROR ends the
// run).
#include "laws_common.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) {
	// RFC 1952 2.3: MTIME is 4 bytes, OS 1, XLEN 2; the name and the comment are "zero-terminated"
	size_t extra_len = upto(65535);
	size_t name_len = upto(UINT_MAX - 1);
	size_t comment_len = upto(UINT_MAX - 1);
	unsigned char present = nondet_u8();
	int text = (int) nondet_u32();
	uLong time = nondet_u32();
	int os = (int) nondet_u32();
	int hcrc = (int) nondet_u32();
	unsigned char *extra = alloc_any_bytes(extra_len);
	unsigned char *name = any_string(name_len);
	unsigned char *comment = any_string(comment_len);
	if (!extra || !name || !comment)
		return 0;
	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);
	gz_header head;
	head.text = text;
	head.time = time;
	head.os = os;
	head.hcrc = hcrc;
	head.extra = (present & 1) ? extra : Z_NULL;
	head.extra_len = (uInt) extra_len;
	head.name = (present & 2) ? name : Z_NULL;
	head.comment = (present & 4) ? comment : Z_NULL;
	int level = (int) nondet_u32();
	int window_bits = 16 + 9 + (int) upto(6);
	int mem_level = (int) nondet_u32();
	int strategy = (int) nondet_u32();
	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 (!extra_copy || !name_copy || !comment_copy || !got.extra || !got.name || !got.comment)
		return 0;
	z_stream compressor;
	new_stream(&compressor);
	if (deflateInit2(&compressor, level, Z_DEFLATED, window_bits, mem_level, strategy) != Z_OK)
		return 0;
	if (deflateSetHeader(&compressor, &head) != Z_OK)
		return 0;
	size_t out_size = deflateBound_z(&compressor, 0);
	unsigned char *compressed = malloc(out_size);
	if (compressed == NULL)
		return 0;
	compressor.next_out = compressed;
	int code;
	do {
		compressor.avail_out = clip(out_size - (size_t) (compressor.next_out - compressed));

		code = deflate(&compressor, Z_FINISH);
	} while (code == Z_OK);
	if (code != Z_STREAM_END)
		return 0;
	size_t compressed_len = (size_t) (compressor.next_out - compressed);
	z_stream decompressor;
	new_stream(&decompressor);
	if (inflateInit2(&decompressor, window_bits) != Z_OK || inflateGetHeader(&decompressor, &got) != Z_OK)
		return 0;
	unsigned char room[1];
	set_buffer(&decompressor, compressed, 0, room, 1);
	do {
		decompressor.avail_in = clip(compressed_len - (size_t) (decompressor.next_in - compressed));

		code = inflate(&decompressor, Z_FINISH);

		if (code == Z_MEM_ERROR)
			return 0;
	} while (code == Z_BUF_ERROR && decompressor.next_in != compressed + compressed_len);
	// 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(present & 1, got.extra, extra_copy, extra_len));
	gp_assert(!(present & 1) || got.extra_len == extra_len);
	gp_assert(same_field(present & 2, got.name, name_copy, name_len + 1));
	gp_assert(same_field(present & 4, 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);
}

The theorem

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

Rocq
Theorem rt_gzip_header : 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_gzip_header : harness_safe Zlib.contracts.rt_gzip_header.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 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.