Browse zlib specs (46 of 62)

Proofs / zlib / Earlier, longer properties

x_inflate_decode

inflate decodes every stream that a reference encoder written from RFC 1951 builds from stored, fixed and dynamic Huffman blocks (data up to 256 KiB, stream up to 512 KiB; raw, zlib or gzip wrapper; up to 16 bytes after it): only Z_OK, Z_BUF_ERROR or Z_STREAM_END, the output is always the start of the data, and at the end exactly the stream was consumed.

spec
289 lines of C
with its headers
614 lines
status
Proved
46 of 62
On this page

The spec

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

C
// Law inflate_decode: inflate decodes correctly.  The input is a stream built here by the reference encoder of
// harness/deflate_ref.h (written from RFC 1951 alone) from ANY sequence of blocks:
//  - stored blocks (3.2.4) of ANY length <= 65535 holding ANY bytes;
//  - fixed-Huffman blocks (3.2.6) and dynamic-Huffman blocks (3.2.7) of ANY sequence of literals (ANY byte) and
//    back-references of ANY length 3..258 at ANY distance 1..min(bytes so far, 2^wb) (3.2.5), ended by the
//    end-of-block code; a dynamic block with ANY nlen 257..286 and ndist 1..30 code lengths <= 15 that inflate
//    accepts (deflate_ref.h code_ok: complete codes, the single-code and empty-distance-code exceptions, a code for
//    256) and ANY complete code length code, its code lengths sent with ANY choice, per position, between the
//    literal length and a valid run (16: 3..6 copies of the previous length, 17: 3..10 zeros, 18: 11..138 zeros, of
//    ANY run length; runs may cross from the literal/length to the distance lengths);
//    (a drawn symbol that cannot be sent -- a length or distance out of range, a symbol without a code in a dynamic
//    block, an invalid run -- is not sent;)
//  - the last block marked final;
// in a raw, zlib (RFC 1950: ANY window size 2^wb, wb 8..15, ANY FLEVEL, the Adler-32 trailer) or gzip (RFC 1952: a
// minimal header, the CRC-32 and length trailer) wrapper; followed by ANY 0..16 bytes of garbage.  inflateInit2 with a
// windowBits that accepts it (raw: -wb; zlib: wb, 0, or 32 + wb; gzip: 16 + wb or 32 + wb); then inflate() calls with
// ANY flush value, offered ANY further amount of the input (an amount beyond the end offers the rest) and ANY output
// space <= 2^20 bytes (each call: objects of exactly avail_in and avail_out bytes), until Z_STREAM_END.  Properties:
//  - every call returns Z_OK, Z_BUF_ERROR or Z_STREAM_END (never an error on a valid stream);
//  - the bytes produced by each call are the next bytes of the encoded data (the output is always a prefix of it);
//  - at Z_STREAM_END all the data has been produced (total_out = its length) and exactly the stream was consumed
//    (none of the garbage after it);
//  - data_type (zlib.h): whenever inflate reports a block boundary (bit 128: just after an end-of-block code or the
//    header), the output so far is exactly the data of the blocks completed; bit 64 (decoding the last block) is set
//    exactly when the output may have reached the last block: with it, the output covers all blocks before the last,
//    without it, at most those.
// (Z_MEM_ERROR ends the run.)  Bounds: data <= 2^18 bytes, stream <= 2^19 bytes, any number of blocks and symbols.
#include "deflate_ref.h"

#define GP_DATA_MAX (1u << 18)
#define GP_STREAM_MAX (1u << 19)
#define GP_OUT_MAX (1u << 20)

static const unsigned char cl_order[19] = {16, 17, 18, 0, 8, 7, 9, 6, 10, 5, 11, 4, 12, 3, 13, 2, 14, 1, 15};

// the header of a dynamic block after BTYPE: the drawn code lengths (returns 0 when they are not acceptable: the run
// is then dropped by gp_assume), the code lengths sent with the drawn runs; the codes in lcodes/dcodes
static void dyn_header(struct bw *w, unsigned nlen, unsigned ndist, unsigned char *ll, unsigned short *lcodes,
		       unsigned short *dcodes)
{
	const unsigned m = nlen + ndist;
	unsigned char cl[19], choice[316], runs[316];
	unsigned short clcodes[19];
	nondet_bytes(ll, m);
	nondet_bytes(cl, 19);
	nondet_bytes(choice, m);
	nondet_bytes(runs, m);
	for (unsigned i = 0; i < m; ++i)
		gp_assume(ll[i] <= 15);
	for (unsigned i = 0; i < 19; ++i)
		gp_assume(cl[i] <= 7);
	gp_assume(ll[256] != 0);
	gp_assume(code_ok(ll, nlen, 1) && code_ok(ll + nlen, ndist, 2) && code_ok(cl, 19, 0));
	canonical(ll, nlen, lcodes);
	canonical(ll + nlen, ndist, dcodes);
	canonical(cl, 19, clcodes);
	bw_bits(w, nlen - 257, 5);
	bw_bits(w, ndist - 1, 5);
	bw_bits(w, 19 - 4, 4);
	for (unsigned i = 0; i < 19; ++i)
		bw_bits(w, cl[cl_order[i]], 3);
	unsigned i = 0;
	while (i < m) {
		const unsigned r = runs[i];
		unsigned same = 0;              // how many of ll[i..] equal ll[i]
		while (i + same < m && ll[i + same] == ll[i] && same < 138)
			same++;
		if (choice[i] >= 192 && ll[i] == 0 && r >= 11 && r <= 138 && r <= same && cl[18] != 0) {
			bw_code(w, clcodes[18], cl[18]);
			bw_bits(w, r - 11, 7);
			i += r;
		} else if (choice[i] >= 192 && ll[i] == 0 && r >= 3 && r <= 10 && r <= same && cl[17] != 0) {
			bw_code(w, clcodes[17], cl[17]);
			bw_bits(w, r - 3, 3);
			i += r;
		} else if (choice[i] >= 192 && i > 0 && ll[i - 1] == ll[i] && r >= 3 && r <= 6 && r <= same &&
			   cl[16] != 0) {
			bw_code(w, clcodes[16], cl[16]);
			bw_bits(w, r - 3, 2);
			i += r;
		} else {
			gp_assume(cl[ll[i]] != 0);      // the literal length must have a code
			bw_code(w, clcodes[ll[i]], cl[ll[i]]);
			i++;
		}
	}
}

int main(void)
{
	const unsigned char wrap = nondet_u8();         // 0 raw, 1 zlib, 2 gzip (others: raw)
	const unsigned wb = nondet_u32();
	const unsigned char flevel = nondet_u8();
	const unsigned char isel = nondet_u8();
	gp_assume(wb >= 8 && wb <= 15);
	unsigned char *data = malloc(GP_DATA_MAX);
	unsigned char *src = malloc(GP_STREAM_MAX);
	unsigned char *isb = malloc(GP_DATA_MAX + 1);   // isb[k]: k bytes of data end a block (or k = 0)
	if (data == NULL || src == NULL || isb == NULL)
		return 0;
	for (unsigned i = 0; i <= GP_DATA_MAX; ++i)
		isb[i] = 0;
	isb[0] = 1;
	struct bw w;
	w.buf = src;
	w.len = 0;
	w.nb = 0;
	const unsigned maxd = 1u << wb;
	if (wrap == 1) {
		const unsigned cmf = ((wb - 8) << 4) | 8;
		const unsigned flg0 = (unsigned) (flevel & 3) << 6;
		const unsigned flg = flg0 + (31 - ((cmf << 8) + flg0) % 31) % 31;
		bw_byte(&w, (unsigned char) cmf);
		bw_byte(&w, (unsigned char) flg);
	} else if (wrap == 2) {
		static const unsigned char gz[10] = {0x1f, 0x8b, 8, 0, 0, 0, 0, 0, 0, 3};
		for (unsigned i = 0; i < 10; ++i)
			bw_byte(&w, gz[i]);
	}
	unsigned char ll[316];                          // a dynamic block's code lengths, and its codes
	unsigned short lcodes[286], dcodes[30];
	unsigned n = 0;                                 // the data so far
	unsigned last_start = 0;                        // the data before the last block
	for (;;) {
		const unsigned char more = nondet_u8();
		const unsigned char btype = nondet_u8();
		const unsigned last = more == 0;
		if (last)
			last_start = n;
		const unsigned bt = btype & 3;          // 0 stored, 1 fixed, 2 dynamic, 3 fixed
		gp_assume(w.len + 8 <= GP_STREAM_MAX);
		bw_bits(&w, last, 1);
		if (bt == 0) {                          // stored
			const unsigned len = nondet_u32();
			gp_assume(len <= 65535);
			gp_assume(n + len <= GP_DATA_MAX);
			bw_bits(&w, 0, 2);
			bw_align(&w);
			gp_assume(w.len + 4 + len <= GP_STREAM_MAX);
			bw_byte(&w, (unsigned char) len);
			bw_byte(&w, (unsigned char) (len >> 8));
			bw_byte(&w, (unsigned char) ~len);
			bw_byte(&w, (unsigned char) (~len >> 8));
			nondet_bytes(data + n, len);
			bytes_copy(src + w.len, data + n, len);
			w.len += len;
			n += len;
		} else {                                // Huffman codes
			const int dyn = bt == 2;
			unsigned nlen = 0, ndist = 0;
			if (dyn) {
				nlen = nondet_u32();
				ndist = nondet_u32();
				gp_assume(nlen >= 257 && nlen <= 286 && ndist >= 1 && ndist <= 30);
				gp_assume(w.len + 16 + 2 * (nlen + ndist) <= GP_STREAM_MAX);
				bw_bits(&w, 2, 2);
				dyn_header(&w, nlen, ndist, ll, lcodes, dcodes);
			} else {
				bw_bits(&w, 1, 2);
			}
			for (;;) {
				const unsigned char kind = nondet_u8();
				gp_assume(w.len + 8 <= GP_STREAM_MAX);
				if (kind == 0)
					break;
				if (kind < 128) {
					const unsigned char lit = nondet_u8();
					if (dyn && ll[lit] == 0)
						continue;       // no code for it
					gp_assume(n < GP_DATA_MAX);
					data[n] = lit;
					n++;
					if (dyn)
						bw_code(&w, lcodes[lit], ll[lit]);
					else
						bw_fixed(&w, lit);
				} else {
					const unsigned len = nondet_u32();
					const unsigned dist = nondet_u32();
					if (len < 3 || len > 258 || dist < 1 || dist > n || dist > maxd)
						continue;
					const unsigned lc = len_code(len), dc = dist_code(dist);
					if (dyn && (257 + lc >= nlen || ll[257 + lc] == 0 || dc >= ndist ||
						    ll[nlen + dc] == 0))
						continue;       // no code for it
					gp_assume(n + len <= GP_DATA_MAX);
					for (unsigned i = 0; i < len; ++i)
						data[n + i] = data[n + i - dist];
					n += len;
					if (dyn) {
						bw_code(&w, lcodes[257 + lc], ll[257 + lc]);
						bw_bits(&w, len - ref_lbase[lc], ref_lext[lc]);
						bw_code(&w, dcodes[dc], ll[nlen + dc]);
						bw_bits(&w, dist - ref_dbase[dc], ref_dext[dc]);
					} else {
						bw_fixed_match(&w, len, dist);
					}
				}
			}
			if (dyn)
				bw_code(&w, lcodes[256], ll[256]);
			else
				bw_fixed(&w, 256);
		}
		isb[n] = 1;
		if (last)
			break;
	}
	bw_align(&w);
	gp_assume(w.len + 8 + 16 <= GP_STREAM_MAX);
	if (wrap == 1) {
		const unsigned long a = ref_adler32(1, data, n);
		bw_byte(&w, (unsigned char) (a >> 24));
		bw_byte(&w, (unsigned char) (a >> 16));
		bw_byte(&w, (unsigned char) (a >> 8));
		bw_byte(&w, (unsigned char) a);
	} else if (wrap == 2) {
		const unsigned long c = ref_crc32(0, data, n);
		bw_byte(&w, (unsigned char) c);
		bw_byte(&w, (unsigned char) (c >> 8));
		bw_byte(&w, (unsigned char) (c >> 16));
		bw_byte(&w, (unsigned char) (c >> 24));
		bw_byte(&w, (unsigned char) n);
		bw_byte(&w, (unsigned char) (n >> 8));
		bw_byte(&w, (unsigned char) (n >> 16));
		bw_byte(&w, (unsigned char) (n >> 24));
	}
	const unsigned slen = w.len;                    // the stream
	const unsigned glen = nondet_u32();
	gp_assume(glen <= 16);
	nondet_bytes(src + slen, glen);                 // garbage after it
	const unsigned total = slen + glen;

	int iw;
	if (wrap == 1)
		iw = isel < 85 ? (int) wb : isel < 170 ? 0 : 32 + (int) wb;
	else if (wrap == 2)
		iw = isel < 128 ? 16 + (int) wb : 32 + (int) wb;
	else
		iw = -(int) wb;
	z_stream s;
	stream_defaults(&s);
	int r = inflateInit2(&s, iw);
	if (r != Z_OK)
		return 0;
	unsigned pos = 0, lim = 0, opos = 0;
	for (;;) {
		const unsigned step = nondet_u32();
		const unsigned aout = nondet_u32();
		const int flush = (int) nondet_u32();
		gp_assume(aout <= GP_OUT_MAX);
		lim = step < total - lim ? lim + step : total;
		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;
		s.next_in = ib;
		s.avail_in = ain;
		s.next_out = ob;
		s.avail_out = aout;
		r = inflate(&s, flush);
		if (r == Z_MEM_ERROR)
			return 0;
		gp_assert(r == Z_OK || r == Z_BUF_ERROR || r == Z_STREAM_END);
		const unsigned made = aout - s.avail_out;
		gp_assert(made <= n - opos);
		gp_assert(bytes_same(ob, data + opos, made));
		opos += made;
		if (s.data_type & 128)
			gp_assert(isb[opos] != 0);
		if (s.data_type & 64)
			gp_assert(opos >= last_start);
		else
			gp_assert(opos <= last_start);
		pos += ain - s.avail_in;
		free(ib);
		free(ob);
		free(osnap);
		if (r == Z_STREAM_END)
			break;
	}
	gp_assert(opos == n);
	gp_assert(s.total_out == n);
	gp_assert(pos == slen);
	inflateEnd(&s);
	return 0;
}
harness/deflate_ref.h, 170 lines
C
// A reference DEFLATE encoder (RFC 1951), written from the RFC alone, for the inflate laws that check decoded output
// (inflate_decode): a bit writer, stored blocks (3.2.4), fixed-Huffman blocks (3.2.6) and dynamic-Huffman blocks
// (3.2.7) with ANY valid code lengths, literals, and back-references (3.2.5).
//
//  - Bits are packed starting with the least significant bit of each byte; data elements (lengths, extra bits) are
//    written least significant bit first, Huffman codes most significant bit first (3.1.1);
//  - canonical codes (3.2.2): bl_count[len] = the number of codes of each length, next_code[1] = 0,
//    next_code[len] = (next_code[len - 1] + bl_count[len - 1]) << 1, then the symbols in increasing order get
//    consecutive codes of their length;
//  - a dynamic block: BFINAL, BTYPE = 10, HLIT = nlen - 257, HDIST = ndist - 1, HCLEN = 19 - 4 (all 19 code length
//    code lengths, 3 bits each, in the order 16 17 18 0 8 7 9 6 10 5 11 4 12 3 13 2 14 1 15), then the nlen + ndist
//    code lengths (one sequence) in the code length code: 0..15 literally, 16 = copy the previous length 3..6 times
//    (2 extra bits), 17 = 3..10 zeros (3 extra bits), 18 = 11..138 zeros (7 extra bits), then the symbols.
// inflate accepts a dynamic block's codes when (inflate.c, inftrees.c): nlen <= 286, ndist <= 30; the code length
// code is complete; the literal/length code has a code for 256 and is complete or a single code of length 1; the
// distance code is complete, a single code of length 1, or empty.  kraft() and code_ok() state these.
#ifndef ZLIB_HARNESS_DEFLATE_REF_H
#define ZLIB_HARNESS_DEFLATE_REF_H
#include "zlib_common.h"

struct bw {                     // a bit writer, least significant bit first (RFC 1951 3.1.1)
	unsigned char *buf;
	unsigned len;           // complete bytes
	unsigned nb;            // bits in buf[len]
};

static void bw_bit(struct bw *w, unsigned b)
{
	if (w->nb == 0)
		w->buf[w->len] = 0;
	w->buf[w->len] = (unsigned char) (w->buf[w->len] | ((b & 1) << w->nb));
	w->nb++;
	if (w->nb == 8) {
		w->nb = 0;
		w->len++;
	}
}

static void bw_bits(struct bw *w, unsigned v, unsigned n)       // a value, its least significant bit first
{
	for (unsigned i = 0; i < n; ++i)
		bw_bit(w, v >> i);
}

static void bw_code(struct bw *w, unsigned c, unsigned n)       // a Huffman code, its most significant bit first
{
	for (unsigned i = n; i > 0; --i)
		bw_bit(w, c >> (i - 1));
}

static void bw_byte(struct bw *w, unsigned char b)              // at a byte boundary
{
	w->buf[w->len] = b;
	w->len++;
}

static void bw_align(struct bw *w)
{
	if (w->nb != 0) {
		w->nb = 0;
		w->len++;
	}
}

// the fixed literal/length code (RFC 1951 3.2.6)
static void bw_fixed(struct bw *w, unsigned v)
{
	if (v < 144)
		bw_code(w, 0x30 + v, 8);
	else if (v < 256)
		bw_code(w, 0x190 + (v - 144), 9);
	else if (v < 280)
		bw_code(w, v - 256, 7);
	else
		bw_code(w, 0xc0 + (v - 280), 8);
}

// RFC 1951 3.2.5: length codes 257..285 and distance codes 0..29
static const unsigned short ref_lbase[29] = {3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 15, 17, 19, 23, 27, 31, 35, 43, 51, 59,
					     67, 83, 99, 115, 131, 163, 195, 227, 258};
static const unsigned char ref_lext[29] = {0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4, 5,
					   5, 5, 5, 0};
static const unsigned short ref_dbase[30] = {1, 2, 3, 4, 5, 7, 9, 13, 17, 25, 33, 49, 65, 97, 129, 193, 257, 385, 513,
					     769, 1025, 1537, 2049, 3073, 4097, 6145, 8193, 12289, 16385, 24577};
static const unsigned char ref_dext[30] = {0, 0, 0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 10,
					   11, 11, 12, 12, 13, 13};

static unsigned len_code(unsigned len)          // the length code (0..28 for symbols 257..285) of a length 3..258
{
	unsigned i = 28;
	if (len < 258) {
		i = 0;
		while (i + 1 < 28 && ref_lbase[i + 1] <= len)
			i++;
	}
	return i;
}

static unsigned dist_code(unsigned dist)        // the distance code of a distance 1..32768
{
	unsigned j = 0;
	while (j + 1 < 30 && ref_dbase[j + 1] <= dist)
		j++;
	return j;
}

static void bw_fixed_match(struct bw *w, unsigned len, unsigned dist)
{
	const unsigned i = len_code(len), j = dist_code(dist);
	bw_fixed(w, 257 + i);
	bw_bits(w, len - ref_lbase[i], ref_lext[i]);
	bw_code(w, j, 5);
	bw_bits(w, dist - ref_dbase[j], ref_dext[j]);
}

// canonical codes (RFC 1951 3.2.2) of lens[0..n-1] (lengths <= 15) into codes[0..n-1]
static void canonical(const unsigned char *lens, unsigned n, unsigned short *codes)
{
	unsigned count[16], next[16];
	for (unsigned l = 0; l < 16; ++l)
		count[l] = 0;
	for (unsigned i = 0; i < n; ++i)
		count[lens[i]]++;
	count[0] = 0;
	unsigned c = 0;
	next[0] = 0;
	for (unsigned l = 1; l < 16; ++l) {
		c = (c + count[l - 1]) << 1;
		next[l] = c;
	}
	for (unsigned i = 0; i < n; ++i) {
		if (lens[i] != 0) {
			codes[i] = (unsigned short) next[lens[i]];
			next[lens[i]]++;
		} else {
			codes[i] = 0;
		}
	}
}

// the Kraft sum of lens[0..n-1] in units of 2^-15 (a complete code: 2^15), and the number of codes
static unsigned long kraft(const unsigned char *lens, unsigned n, unsigned *used)
{
	unsigned long k = 0;
	unsigned u = 0;
	for (unsigned i = 0; i < n; ++i) {
		if (lens[i] != 0) {
			k += 1ul << (15 - lens[i]);
			u++;
		}
	}
	*used = u;
	return k;
}

// does inflate accept these lengths (see the header comment)?  type 0: code length code, 1: literal/length, 2: distance
static int code_ok(const unsigned char *lens, unsigned n, int type)
{
	unsigned used;
	const unsigned long k = kraft(lens, n, &used);
	if (k == 32768)
		return 1;
	if (type == 0)
		return 0;
	if (used == 1 && k == 16384)
		return 1;                       // a single code of length 1
	return type == 2 && used == 0;          // no distance code at all
}

#endif
harness/zlib_common.h, 155 lines
C
// 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_decode.v:

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