Browse zlib specs (20 of 62)

Proofs / zlib / The standard on valid input

rfc_stored

A stream of stored blocks built by hand from the RFCs (any data, any block sizes, any wrapper, any bytes after it) decompresses to exactly the data.

spec
103 lines of C
with its headers
143 lines
status
Proved
20 of 62
On this page

The spec

The spec is the C program harness/rfc_stored.c, 103 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_stored: Build, by RFC 1950/1951/1952, a stream of any data cut into any number of stored blocks of any sizes
// up to 65535 (any padding bits after each block header), raw, zlib (any CINFO the window allows, any FLEVEL) or gzip
// (any FTEXT, MTIME, XFL, OS), followed by any bytes (data, blocks and bytes after each up to 2^60, more than any
// allocator provides). inflate() (any window 8..15) fed it and room for the data, in pieces of at most 2^32 - 1 bytes,
// with any flush, returns Z_OK or Z_BUF_ERROR until Z_STREAM_END and has then written exactly the data, as a copy made
// before any zlib call holds it (Z_MEM_ERROR ends the run).
#include "laws_common.h"

int main(void) {
	size_t data_len = upto(1ul << 60);
	size_t blocks = 1 + upto((1ul << 60) - 1);
	size_t after = upto(1ul << 60);
	int wrapper = (int) upto(2);
	int window = 8 + (int) upto(7);
	size_t head_len = 0;
	size_t trailer_len = 0;
	if (wrapper == 1) {
		head_len = 2;
		trailer_len = 4;
	}
	if (wrapper == 2) {
		head_len = 10;
		trailer_len = 8;
	}
	size_t stream_len = head_len + 5 * blocks + data_len + trailer_len + after;
	unsigned char *stream = alloc_any_bytes(stream_len);
	unsigned char *data = alloc_any_bytes(data_len);
	if (stream == NULL || data == NULL)
		return 0;
	unsigned char *expected = copy_of(data, data_len);
	unsigned char *out = malloc(data_len);
	if (expected == NULL || out == NULL)
		return 0;
	// RFC 1950 2.2: CMF = CINFO << 4 | CM 8; FLG = FLEVEL (any), FDICT 0, FCHECK. RFC 1952 2.3: ID1 ID2 CM FLG
	// (FTEXT only) MTIME XFL OS (any)
	if (wrapper == 1) {
		stream[0] = (unsigned char) (upto(window - 8) << 4 | 8);
		stream[1] = (unsigned char) (stream[1] & 0xc0);
		stream[1] = (unsigned char) (stream[1] + (31 - (stream[0] * 256 + stream[1]) % 31) % 31);
	}
	if (wrapper == 2) {
		stream[0] = 0x1f;
		stream[1] = 0x8b;
		stream[2] = 8;
		stream[3] = stream[3] & 1;
	}
	// RFC 1951 3.2.3: "BFINAL is set if and only if this is the last block of the data set"; BTYPE "00 - no
	// compression". 3.2.4: "Any bits of input up to the next byte boundary are ignored. The rest of the block
	// consists of the following information: LEN NLEN ... LEN bytes of literal data"; "NLEN is the one's complement
	// of LEN"
	size_t at = head_len;
	size_t done = 0;
	for (size_t i = 0; i < blocks; i++) {
		size_t len = data_len - done;
		if (i + 1 < blocks && len > 65535)
			len = upto(65535);
		else if (i + 1 < blocks)
			len = upto(len);
		gp_assume(len <= 65535);
		int last = i + 1 == blocks;
		stream[at] = (unsigned char) ((stream[at] & 0xf8) | last);
		stream[at + 1] = (unsigned char) (len & 255);
		stream[at + 2] = (unsigned char) (len >> 8);
		stream[at + 3] = (unsigned char) (~len & 255);
		stream[at + 4] = (unsigned char) ((~len >> 8) & 255);
		for (size_t j = 0; j < len; j++)
			stream[at + 5 + j] = data[done + j];
		at += 5 + len;
		done += len;
	}
	// RFC 1950 2.2: ADLER32, 4 bytes, most significant first (2.1); RFC 1952 2.3: CRC32, ISIZE, 4 bytes each, least
	// significant first (2.1)
	uLong adler = adler32_z(1, data, data_len);
	uLong crc = crc32_z(0, data, data_len);
	for (int i = 0; i < 4; i++) {
		if (wrapper == 1)
			stream[at + i] = (unsigned char) (adler >> (24 - 8 * i));
		if (wrapper == 2) {
			stream[at + i] = (unsigned char) (crc >> (8 * i));
			stream[at + 4 + i] = (unsigned char) (data_len >> (8 * i));
		}
	}
	z_stream strm;
	new_stream(&strm);
	int window_bits[3] = {-window, window, 16 + window};
	if (inflateInit2(&strm, window_bits[wrapper]) != Z_OK)
		return 0;
	strm.next_in = stream;
	strm.next_out = out;
	int code;
	do {
		strm.avail_in = clip(stream_len - (size_t) (strm.next_in - stream));
		strm.avail_out = clip(data_len - (size_t) (strm.next_out - out));

		code = inflate(&strm, (int) nondet_u32());

		if (code == Z_MEM_ERROR)
			return 0;
		gp_assert(code == Z_OK || code == Z_BUF_ERROR || code == Z_STREAM_END);
	} while (code != Z_STREAM_END);
	gp_assert(strm.next_out == out + data_len && bytes_eq(out, expected, data_len));
	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_stored.v:

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