x_inflate_buffers

Any sequence of calls of the inflate API (inflate with any flush, inflateSync, inflateGetDictionary, inflateSetDictionary, inflatePrime, inflateReset, inflateReset2, inflateValidate, inflateMark, inflateCodesUsed, inflateSyncPoint), any windowBits, input up to 16 MiB and output space up to 1 MiB per call: every call reads and writes only its buffers, pointers and counters move by exactly what was consumed and produced, and inflate leaves the output space it did not write unchanged.

spec: 167 lines of C
with its headers: 322 lines
status: Proved; 47 of 62

On this page

The spec

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

// Law inflate_buffers: inflate's buffer discipline and counters, for ANY input and ANY sequence of calls of the inflate
// API.  inflateInit2 with ANY windowBits (any int: zlib, gzip, raw, auto-detect, and every invalid value), then ANY
// number of calls, each of them, at the caller's choice: inflate() with ANY flush value (any int), inflateSync,
// inflateGetDictionary, inflateSetDictionary (any bytes, any length), inflatePrime (any bits, any value),
// inflateReset, inflateReset2 (any windowBits), inflateValidate, inflateMark, inflateCodesUsed, inflateSyncPoint; then
// inflateEnd.  The input is ANY n <= 2^24 bytes; each call is offered the next ANY number of not yet consumed bytes
// (next_in = the start of a new object of exactly that many bytes; for inflate() also Z_NULL with any avail_in) and
// ANY output space of at most 2^20 bytes (next_out = a new object of exactly avail_out bytes with any contents; for
// inflate() also Z_NULL).  Misuse not covered: a Z_NULL next_in with avail_in > 0 for inflateSync (which does not
// check it, unlike inflate()).
// Properties:
//  - no undefined behaviour: in particular every call reads only [next_in, next_in + avail_in) and writes only
//    [next_out, next_out + avail_out) (each its own object), and inflateGetDictionary writes only the dictionary
//    length it reports;
//  - inflateInit2 returns Z_OK, Z_MEM_ERROR, or Z_STREAM_ERROR, the last exactly for the windowBits zlib.h rejects
//    (unless the state allocation failed first: Z_MEM_ERROR); after Z_OK
//    total_in and total_out are 0;
//  - after every call: 0 <= avail_in <= what was offered, next_in advanced by exactly the bytes consumed
//    (avail_in decrease), the same for next_out/avail_out and the bytes produced; next_in stays Z_NULL when it was;
//  - inflate() writes only the bytes it reports as produced: the rest of the output space is unchanged, and the
//    input is unchanged;
//  - total_in and total_out count exactly the bytes consumed and produced since the last init or reset (inflateSync:
//    total_in counts the bytes it skipped), except in the inflate() call that returns Z_MEM_ERROR (the stream is then
//    unusable; on the unmodified code also after Z_NEED_DICT, fixed by patch F1);
//  - inflateGetDictionary reports at most 2^15 bytes and writes exactly that many;
//  - inflateEnd returns Z_OK.
// Bounds: n <= 2^24 input bytes, at most 2^20 bytes of output space per call, any number of calls.
#include "zlib_common.h"

#define GP_IN_MAX (1u << 24)
#define GP_OUT_MAX (1u << 20)

int main(void)
{
	const int wbits = (int) nondet_u32();
	const unsigned n = nondet_u32();
	gp_assume(n <= GP_IN_MAX);
	unsigned char *src = malloc(n);
	if (src == NULL)
		return 0;
	nondet_bytes(src, n);
	z_stream s;
	stream_defaults(&s);
	int r = inflateInit2(&s, wbits);
	gp_assert(r == Z_OK || r == Z_STREAM_ERROR || r == Z_MEM_ERROR);
	// inflateInit2_ allocates its state before it checks windowBits, so a failed allocation gives
	// Z_MEM_ERROR whatever windowBits is: the exact Z_STREAM_ERROR condition is stated for the other results
	// (as in inflate_codes.c).
	if (r != Z_MEM_ERROR)
		gp_assert((r == Z_STREAM_ERROR) == !inflate_wbits_ok(wbits));
	if (r != Z_OK) {
		free(src);
		return 0;
	}
	gp_assert(s.total_in == 0 && s.total_out == 0);
	unsigned pos = 0;           // input consumed so far: the next call is offered src[pos..lim)
	unsigned lim = 0;
	for (;;) {
		const unsigned nlim = nondet_u32();
		const unsigned aout = nondet_u32();
		const int flush = (int) nondet_u32();
		const unsigned arg = nondet_u32();
		const unsigned char op = nondet_u8();
		const unsigned char in_null = nondet_u8();
		const unsigned char out_null = nondet_u8();
		const unsigned char stop = nondet_u8();
		gp_assume(pos <= nlim && nlim <= n);
		gp_assume(aout <= GP_OUT_MAX);
		lim = nlim;
		const unsigned ain = lim - pos;
		unsigned char *ib = exact_copy(src + pos, ain);
		unsigned char *osnap;
		unsigned char *ob = exact_space(aout, &osnap);
		if (ib == NULL || ob == NULL)
			return 0;
		// Z_NULL pointers are passed to inflate() only (the other functions do not check them)
		const int nin = op < 200 && in_null == 0, nout = op < 200 && out_null == 0;
		s.next_in = nin ? Z_NULL : ib;
		s.avail_in = ain;
		s.next_out = nout ? Z_NULL : ob;
		s.avail_out = aout;
		const unsigned long tin = s.total_in, tout = s.total_out;
		int reset = 0;
		if (op < 200) {
			r = inflate(&s, flush);
		} else if (op < 210) {
			r = inflateSync(&s);
			gp_assert(r == Z_OK || r == Z_BUF_ERROR || r == Z_DATA_ERROR || r == Z_STREAM_ERROR);
		} else if (op < 220) {
			uInt dl = 0;
			r = inflateGetDictionary(&s, Z_NULL, &dl);
			gp_assert(r == Z_OK);
			gp_assert(dl <= 32768);
			if (dl <= aout) {
				r = inflateGetDictionary(&s, ob, Z_NULL);
				gp_assert(r == Z_OK);
				gp_assert(bytes_same(ob + dl, osnap + dl, aout - dl));
				bytes_copy(osnap, ob, dl);      // the dictionary is not output: the checks below see no change
			}
		} else if (op < 230) {
			r = inflateSetDictionary(&s, ob, aout);
			gp_assert(r == Z_OK || r == Z_STREAM_ERROR || r == Z_DATA_ERROR || r == Z_MEM_ERROR);
		} else if (op < 235) {
			r = inflatePrime(&s, (int) arg, flush);
			gp_assert(r == Z_OK || r == Z_STREAM_ERROR);
		} else if (op < 240) {
			r = inflateReset(&s);
			gp_assert(r == Z_OK);
			reset = 1;
		} else if (op < 245) {
			r = inflateReset2(&s, (int) arg);
			gp_assert((r == Z_OK) == inflate_wbits_ok((int) arg));
			gp_assert(r == Z_OK || r == Z_STREAM_ERROR);
			reset = r == Z_OK;
		} else if (op < 250) {
			r = inflateValidate(&s, (int) arg);
			gp_assert(r == Z_OK);
		} else if (op < 252) {
			(void) inflateMark(&s);
			r = Z_OK;
		} else if (op < 254) {
			(void) inflateCodesUsed(&s);
			r = Z_OK;
		} else {
			r = inflateSyncPoint(&s);
			gp_assert(r == 0 || r == 1);
		}
		gp_assert(s.avail_in <= ain);
		gp_assert(s.avail_out <= aout);
		const unsigned used = ain - s.avail_in;
		const unsigned made = aout - s.avail_out;
		if (nin) {
			gp_assert(s.next_in == Z_NULL);
			gp_assert(used == 0);
		} else {
			gp_assert(s.next_in == ib + used);
		}
		if (nout) {
			gp_assert(s.next_out == Z_NULL);
			gp_assert(made == 0);
		} else {
			gp_assert(s.next_out == ob + made);
		}
		gp_assert(bytes_same(ib, src + pos, ain));
		gp_assert(bytes_same(ob + made, osnap + made, aout - made));
		if (reset) {
			gp_assert(s.total_in == 0 && s.total_out == 0);
		} else if (!(op < 200 && r == Z_MEM_ERROR)) {
			gp_assert(s.total_in == tin + used);
			gp_assert(s.total_out == tout + made);
		}
		pos += used;
		if (reset) {
			// a new stream: the rest of the input is offered from where it stands
			lim = pos;
		}
		free(ib);
		free(ob);
		free(osnap);
		if (stop == 0)
			break;
	}
	r = inflateEnd(&s);
	gp_assert(r == Z_OK);
	free(src);
	return 0;
}

harness/zlib_common.h, 155 lines

// Shared by the zlib harnesses (zlib 1.3.2 core: adler32.c, crc32.c, deflate.c, trees.c, inflate.c, inffast.c,
// inftrees.c, compress.c, uncompr.c, zutil.c).
//
// A harness draws every input from quickproof.h (nondet_*, pick), restricts it with gp_assume, and states each property
// with gp_assert (undefined behaviour when the property fails).  Buffers have exactly the size the claim allows.  Every
// call of inflate() or deflate() gets its input and its output space as objects of their own, allocated with exactly
// avail_in and avail_out bytes (exact_copy, exact_space): an access before next_in, after next_in + avail_in, before
// next_out or after next_out + avail_out is then outside an object, i.e. undefined behaviour in the semantics of the
// theorem, so "inflate reads only the input it is offered and writes only the space it is offered" is part of every
// law's "no undefined behaviour".
//
// The reference facts, written from the definitions, not from zlib:
//  - Adler-32 (RFC 1950 8.2): s1 = 1 + the sum of the bytes, s2 = the sum of the successive values of s1, both mod
//    65521; the checksum is s2 * 65536 + s1.  ref_adler32 updates a checksum byte by byte;
//  - CRC-32 (RFC 1952 8, ISO 3309): the reflected polynomial 0xedb88320, register preset to all ones and inverted at
//    the end.  ref_crc32 updates a checksum bit by bit;
//  - the zlib wrapper (RFC 1950): 2 header bytes, an optional 4-byte dictionary id (big-endian Adler-32 of the
//    dictionary), the deflate data, then the big-endian Adler-32 of the uncompressed data;
//  - the gzip wrapper (RFC 1952): a header of at least 10 bytes (1f 8b 08 FLG MTIME(4) XFL OS, then the optional
//    fields), the deflate data, then the little-endian CRC-32 and the little-endian length mod 2^32 of the data;
//  - the inflate windowBits of zlib.h: 8..15 (zlib wrapper, 2^windowBits window), 0 (zlib wrapper, the window size of
//    the header), -8..-15 (raw deflate), + 16 (gzip wrapper only; 16 itself: the window size of the header), + 32
//    (zlib or gzip, detected); everything else is rejected with Z_STREAM_ERROR.
#ifndef ZLIB_HARNESS_COMMON_H
#define ZLIB_HARNESS_COMMON_H
#include <stddef.h>
#include <stdint.h>
#include <stdlib.h>
#include "quickproof.h"
#include "zlib.h"

#define GP_BASE 65521ul             // the Adler-32 modulus (RFC 1950)
#define GP_POLY 0xedb88320ul        // the CRC-32 polynomial, reflected (RFC 1952)

// Adler-32 of buf[0..n-1] continued from the checksum a (both halves < 65521 for a checksum).
static unsigned long ref_adler32(unsigned long a, const unsigned char *buf, unsigned long n)
{
	unsigned long s1 = a & 0xffff;
	unsigned long s2 = (a >> 16) & 0xffff;
	for (unsigned long i = 0; i < n; ++i) {
		s1 = (s1 + buf[i]) % GP_BASE;
		s2 = (s2 + s1) % GP_BASE;
	}
	return (s2 << 16) | s1;
}

// The CRC-32 register update by one byte, without pre- or post-conditioning (the register is the 32 low bits).
static unsigned long ref_crc_byte(unsigned long c, unsigned char b)
{
	c ^= b;
	for (int k = 0; k < 8; ++k) {
		if (c & 1)
			c = (c >> 1) ^ GP_POLY;
		else
			c = c >> 1;
	}
	return c;
}

// CRC-32 of buf[0..n-1] continued from the checksum c (its 32 low bits).
static unsigned long ref_crc32(unsigned long c, const unsigned char *buf, unsigned long n)
{
	c = (~c) & 0xffffffff;
	for (unsigned long i = 0; i < n; ++i)
		c = ref_crc_byte(c, buf[i]);
	return (~c) & 0xffffffff;
}

static unsigned long be32(const unsigned char *p)
{
	return ((unsigned long) p[0] << 24) | ((unsigned long) p[1] << 16) | ((unsigned long) p[2] << 8) | p[3];
}

static unsigned long le32(const unsigned char *p)
{
	return ((unsigned long) p[3] << 24) | ((unsigned long) p[2] << 16) | ((unsigned long) p[1] << 8) | p[0];
}

static int bytes_same(const unsigned char *a, const unsigned char *b, unsigned long n)
{
	for (unsigned long i = 0; i < n; ++i)
		if (a[i] != b[i])
			return 0;
	return 1;
}

static void bytes_copy(unsigned char *d, const unsigned char *s, unsigned long n)
{
	for (unsigned long i = 0; i < n; ++i)
		d[i] = s[i];
}

// A new object of exactly n bytes holding src[0..n-1] (NULL when the allocation fails).
static unsigned char *exact_copy(const unsigned char *src, unsigned n)
{
	unsigned char *p = malloc(n);
	if (p != NULL)
		bytes_copy(p, src, n);
	return p;
}

// A new object of exactly n bytes with any contents, and a snapshot of them in *snap (NULL when an allocation fails).
static unsigned char *exact_space(unsigned n, unsigned char **snap)
{
	unsigned char *p = malloc(n);
	unsigned char *q = malloc(n);
	if (p == NULL || q == NULL) {
		free(p);
		free(q);
		*snap = NULL;
		return NULL;
	}
	nondet_bytes(p, n);
	bytes_copy(q, p, n);
	*snap = q;
	return p;
}

// inflateInit2's windowBits check (zlib.h): accepted values.
static int inflate_wbits_ok(int w)
{
	if (w < 0)
		return w >= -15 && w <= -8;
	if (w >= 48)
		return 0;
	w &= 15;
	return w == 0 || (w >= 8 && w <= 15);
}

// Is a value one of inflate()'s documented return codes (zlib.h)?
static int inflate_code_ok(int r)
{
	return r == Z_OK || r == Z_STREAM_END || r == Z_NEED_DICT || r == Z_DATA_ERROR || r == Z_STREAM_ERROR ||
	       r == Z_MEM_ERROR || r == Z_BUF_ERROR;
}

// A z_stream with the default allocator (zalloc, zfree, opaque all Z_NULL: zlib uses zcalloc/zcfree, i.e. malloc and
// free) and any values in the fields the caller does not have to set.
static void stream_defaults(z_stream *s)
{
	s->zalloc = Z_NULL;
	s->zfree = Z_NULL;
	s->opaque = Z_NULL;
	s->next_in = Z_NULL;
	s->avail_in = 0;
	s->next_out = Z_NULL;
	s->avail_out = 0;
	pick(s->total_in);
	pick(s->total_out);
	pick(s->adler);
	pick(s->data_type);
	pick(s->reserved);
}

#endif

The theorem

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

Rocq

Theorem x_inflate_buffers : 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 x_inflate_buffers : harness_safe Zlib.contracts.x_inflate_buffers.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 Zlib.contracts.suite.suite_x)))))))))). 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
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.

The spec#

The theorem#

What it leaves out#

How it was proved#

The spec

The theorem

What it leaves out

How it was proved