x_inflate_codes

inflateInit2_, inflate, inflateSetDictionary, inflateEnd, and every entry point after inflateEnd, return exactly the documented codes, for any input up to 16 MiB and any calls of inflate and inflateSetDictionary; the first comment gives each code's conditions.

spec: 172 lines of C
with its headers: 327 lines
status: Proved; 48 of 62

On this page

The spec

The spec is the C program harness/x_inflate_codes.c, 172 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_codes: the return codes of the inflate API are exactly the documented ones (zlib.h), for ANY input and
// ANY sequence of calls.  inflateInit2_ with ANY windowBits, the right or ANY other version string and stream size,
// or a Z_NULL stream; then ANY number of calls of inflate() (ANY flush value, ANY split of the input, ANY output
// space; next_in or next_out may be Z_NULL) and of inflateSetDictionary (ANY bytes, ANY length, at any time); then
// inflateEnd, and every entry point again on the ended stream.  The input is ANY n <= 2^24 bytes; input and output
// space as in inflate_buffers (each call: objects of exactly avail_in and avail_out bytes).  Properties:
//  - inflateInit2_: Z_VERSION_ERROR exactly when the version string does not start with '1' or the stream size is not
//    sizeof(z_stream); else Z_STREAM_ERROR exactly for a Z_NULL stream or a windowBits zlib.h rejects; else Z_OK or
//    Z_MEM_ERROR;
//  - inflate() returns one of Z_OK, Z_STREAM_END, Z_NEED_DICT, Z_DATA_ERROR, Z_STREAM_ERROR, Z_MEM_ERROR,
//    Z_BUF_ERROR, and:
//    - Z_STREAM_ERROR exactly when next_out is Z_NULL or next_in is Z_NULL with avail_in > 0 (the stream is valid);
//    - Z_OK only when the call made progress (consumed or produced a byte) and flush is not Z_FINISH;
//    - Z_BUF_ERROR only when the call made no progress or flush is Z_FINISH;
//    - Z_DATA_ERROR with strm->msg set;
//    - Z_NEED_DICT only for a zlib-wrapped stream (windowBits 0..15 or 32..47) whose header has FDICT set, after
//      exactly its 6 first bytes were consumed (header and dictionary id), with strm->adler = the dictionary id (the
//      big-endian bytes 2..5); it is repeated, without progress, until a dictionary is set;
//    - Z_STREAM_END, Z_DATA_ERROR and Z_MEM_ERROR are final: every later call with valid pointers returns the same code
//      and consumes and produces nothing;
//  - inflateSetDictionary: on a raw stream Z_OK or Z_MEM_ERROR (at any time, also after Z_MEM_ERROR); on a wrapped
//    stream Z_STREAM_ERROR unless inflate just asked for a dictionary, and then Z_DATA_ERROR exactly when the Adler-32
//    of the dictionary is not the id;
//  - inflateEnd returns Z_OK and clears strm->state; afterwards inflate, inflateEnd, inflateReset, inflateReset2,
//    inflateSetDictionary, inflateGetDictionary, inflateSync, inflatePrime and inflateValidate return
//    Z_STREAM_ERROR, inflateMark -65536 and inflateCodesUsed (unsigned long)-1; inflate and inflateEnd on a
//    Z_NULL stream return Z_STREAM_ERROR.
// 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();
	const int ssize = (int) nondet_u32();
	const unsigned char vsel = nondet_u8();
	const unsigned char ssel = nondet_u8();
	const unsigned char nullstrm = nondet_u8();
	const unsigned char vbyte = nondet_u8();
	gp_assume(n <= GP_IN_MAX);
	unsigned char *src = malloc(n);
	if (src == NULL)
		return 0;
	nondet_bytes(src, n);
	char other[2];
	other[0] = (char) vbyte;
	other[1] = 0;
	const char *version = vsel != 0 ? ZLIB_VERSION : other;
	const int stream_size = ssel != 0 ? (int) sizeof(z_stream) : ssize;
	z_stream s;
	stream_defaults(&s);
	int r = inflateInit2_(nullstrm == 0 ? Z_NULL : &s, wbits, version, stream_size);
	const int verr = version[0] != '1' || stream_size != (int) sizeof(z_stream);
	gp_assert((r == Z_VERSION_ERROR) == verr);
	if (!verr) {
		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.
		if (r != Z_MEM_ERROR)
			gp_assert((r == Z_STREAM_ERROR) == (nullstrm == 0 || !inflate_wbits_ok(wbits)));
	}
	if (r != Z_OK) {
		free(src);
		return 0;
	}
	const int zlib_ok = wbits >= 0 && (wbits < 16 || wbits >= 32);      // a zlib wrapper is accepted
	unsigned pos = 0;
	int final = Z_OK;           // the final code once returned, else Z_OK
	int in_dict = 0;            // inflate() just returned Z_NEED_DICT
	for (;;) {
		const unsigned nlim = nondet_u32();
		const unsigned aout = nondet_u32();
		const int flush = (int) 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);
		const unsigned ain = nlim - 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;
		if (op < 24) {
			// a dictionary: the aout bytes of ob
			r = inflateSetDictionary(&s, ob, aout);
			if (wbits < 0) {
				gp_assert(r == Z_OK || r == Z_MEM_ERROR);
			} else if (!in_dict) {
				gp_assert(r == Z_STREAM_ERROR);
			} else {
				gp_assert((r == Z_DATA_ERROR) == (ref_adler32(1, ob, aout) != s.adler));
				gp_assert(r == Z_OK || r == Z_DATA_ERROR || r == Z_MEM_ERROR);
			}
			if (r == Z_MEM_ERROR) {
				final = Z_MEM_ERROR;
				in_dict = 0;
			}
		} else {
			s.next_in = in_null == 0 ? Z_NULL : ib;
			s.avail_in = ain;
			s.next_out = out_null == 0 ? Z_NULL : ob;
			s.avail_out = aout;
			r = inflate(&s, flush);
			gp_assert(inflate_code_ok(r));
			gp_assert(s.avail_in <= ain && s.avail_out <= aout);
			const unsigned used = ain - s.avail_in;
			const unsigned made = aout - s.avail_out;
			const int badptr = out_null == 0 || (in_null == 0 && ain != 0);
			gp_assert((r == Z_STREAM_ERROR) == badptr);
			if (r == Z_OK)
				gp_assert((used != 0 || made != 0) && flush != Z_FINISH);
			if (r == Z_BUF_ERROR)
				gp_assert((used == 0 && made == 0) || flush == Z_FINISH);
			if (r == Z_DATA_ERROR)
				gp_assert(s.msg != Z_NULL);
			if (!badptr && final != Z_OK) {
				gp_assert(r == final);
				gp_assert(used == 0 && made == 0);
			}
			if (r == Z_NEED_DICT) {
				gp_assert(zlib_ok);
				gp_assert(pos + used == 6);
				gp_assert((src[1] & 0x20) != 0);
				gp_assert(s.adler == be32(src + 2));
				if (in_dict)
					gp_assert(used == 0 && made == 0);
			}
			if (!badptr) {
				if (r == Z_STREAM_END || r == Z_DATA_ERROR || r == Z_MEM_ERROR)
					final = r;
				in_dict = r == Z_NEED_DICT;
			}
			pos += used;
		}
		free(ib);
		free(ob);
		free(osnap);
		if (stop == 0)
			break;
	}
	r = inflateEnd(&s);
	gp_assert(r == Z_OK);
	gp_assert(s.state == Z_NULL);
	unsigned char b[1];
	uInt dl;
	b[0] = 0;
	s.next_in = b;
	s.avail_in = 1;
	s.next_out = b;
	s.avail_out = 1;
	gp_assert(inflate(&s, Z_NO_FLUSH) == Z_STREAM_ERROR);
	gp_assert(inflateEnd(&s) == Z_STREAM_ERROR);
	gp_assert(inflateReset(&s) == Z_STREAM_ERROR);
	gp_assert(inflateReset2(&s, 15) == Z_STREAM_ERROR);
	gp_assert(inflateSetDictionary(&s, b, 1) == Z_STREAM_ERROR);
	gp_assert(inflateGetDictionary(&s, b, &dl) == Z_STREAM_ERROR);
	gp_assert(inflateSync(&s) == Z_STREAM_ERROR);
	gp_assert(inflatePrime(&s, 1, 1) == Z_STREAM_ERROR);
	gp_assert(inflateValidate(&s, 1) == Z_STREAM_ERROR);
	gp_assert(inflateMark(&s) == -65536L);
	gp_assert(inflateCodesUsed(&s) == (unsigned long) -1);
	gp_assert(inflate(Z_NULL, Z_NO_FLUSH) == Z_STREAM_ERROR);
	gp_assert(inflateEnd(Z_NULL) == Z_STREAM_ERROR);
	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_codes.v:

Rocq

Theorem x_inflate_codes : 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_codes : harness_safe Zlib.contracts.x_inflate_codes.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (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