Browse zlib specs (22 of 62)

Proofs / zlib / The standard on valid input

rfc_level0_size

At level 0 the output size is exactly the data plus 5 bytes per block plus the wrapper (the data given in pieces of whole 65535-byte blocks, one call or many).

spec
59 lines of C
with its headers
99 lines
status
Proved
22 of 62
On this page

The spec

The spec is the C program harness/rfc_level0_size.c, 59 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 rfc_level0_size: For any data (any length the allocator provides) in b = max(1, ceil(data length / 65535))
// stored blocks, after deflateInit2 with level 0 and any windowBits, memLevel and strategy it accepts (others end the
// run), deflate() offered the data in pieces of any 1 to 65531 whole blocks of 65535 bytes (the rest last, with
// Z_FINISH) and any output space of at least that size (at most 2^32 - 1 bytes per call) returns Z_STREAM_END having
// written exactly the data plus 5 bytes per block plus the wrapper (raw: none; zlib: 2 header and 4 trailer bytes;
// gzip: 10 and 8).
#include "laws_common.h"

int main(void) {
	size_t data_len = upto(PTRDIFF_MAX);
	int window_bits = (int) nondet_u32();
	int mem_level = (int) nondet_u32();
	int strategy = (int) nondet_u32();
	size_t blocks = 1;
	if (data_len > 0)
		blocks = (data_len + 65534) / 65535;
	// RFC 1950 2.2: CMF, FLG ... ADLER32 (2 + 4 bytes); RFC 1952 2.3: a 10-byte header ... CRC32, ISIZE (8 bytes)
	size_t head_len = 0;
	size_t trailer_len = 0;
	if (window_bits >= 0 && window_bits <= 15) {
		head_len = 2;
		trailer_len = 4;
	}
	if (window_bits > 15) {
		head_len = 10;
		trailer_len = 8;
	}
	size_t size = head_len + 5 * blocks + data_len + trailer_len;
	size_t room = size + upto(SIZE_MAX - size);
	unsigned char *data = alloc_any_bytes(data_len);
	unsigned char *compressed = malloc(room);
	if (data == NULL || compressed == NULL)
		return 0;
	// zlib.h, deflateInit: "0 gives no compression at all (the input data is simply copied a block at a time)"
	z_stream strm;
	new_stream(&strm);
	if (deflateInit2(&strm, 0, Z_DEFLATED, window_bits, mem_level, strategy) != Z_OK)
		return 0;
	strm.next_in = data;
	strm.next_out = compressed;
	int code;
	do {
		size_t rest = data_len - (size_t) (strm.next_in - data);
		size_t piece = 65535 * (1 + upto(65530));
		int flush = Z_NO_FLUSH;
		if (piece >= rest) {
			piece = rest;
			flush = Z_FINISH;
		}
		strm.avail_in = (uInt) piece;
		strm.avail_out = clip(room - (size_t) (strm.next_out - compressed));

		code = deflate(&strm, flush);
	} while (code == Z_OK);
	// RFC 1951 3.2.4: each stored block is its header bits padded to a byte, LEN and NLEN (2 bytes each), then "LEN
	// bytes of literal data", at most 65535
	gp_assert(code == Z_STREAM_END && strm.total_out == size);
	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/rfc_level0_size.v:

Rocq
Theorem rfc_level0_size : 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 rfc_level0_size : harness_safe Zlib.contracts.rfc_level0_size.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 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
  • 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.