Browse zlib specs (33 of 62)

Proofs / zlib / The stream interface

api_reset

After any use and inflateReset, a stream behaves exactly like a new one.

spec
67 lines of C
with its headers
107 lines
status
Proved
33 of 62
On this page

The spec

The spec is the C program harness/api_reset.c, 67 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 api_reset: For any windowBits that inflateInit2 accepts, after any use of a stream (any input in any pieces, any
// output space, any flush, any number of calls), inflateReset (Z_OK) makes it behave exactly like a new one from
// inflateInit2 with the same windowBits: given any input (any length the allocator provides) in the same pieces (below
// 2^32 bytes), with the same output space and flush, each inflate() call returns the same code on both, reads and
// writes as many bytes, writes the same bytes, and leaves the same total_in, total_out, msg, data_type and (except for
// raw streams, where zlib does not set it) adler (Z_MEM_ERROR ends the run).
#include "laws_common.h"

int main(void) {
	int window_bits = (int) nondet_u32();
	z_stream used;
	z_stream fresh;
	new_stream(&used);
	new_stream(&fresh);
	if (inflateInit2(&used, window_bits) != Z_OK)
		return 0;
	for (int phase = 0; phase < 2; phase++) {
		size_t input_len = upto(PTRDIFF_MAX);
		unsigned char *input = alloc_any_bytes(input_len);
		if (input == NULL)
			return 0;
		size_t read = 0;
		do {
			size_t take = upto(clip(input_len - read));
			size_t room = nondet_u32();
			int flush = (int) nondet_u32();
			unsigned char *in_used = copy_of(input + read, take);
			unsigned char *in_fresh = copy_of(input + read, take);
			unsigned char *out_used = malloc(room);
			unsigned char *out_fresh = malloc(room);
			if (in_used == NULL || in_fresh == NULL || out_used == NULL || out_fresh == NULL)
				return 0;
			set_buffer(&used, in_used, take, out_used, room);
			set_buffer(&fresh, in_fresh, take, out_fresh, room);

			int code_used = inflate(&used, flush);
			int code_fresh = code_used;
			if (phase == 1)
				code_fresh = inflate(&fresh, flush);

			if (code_used == Z_MEM_ERROR || code_fresh == Z_MEM_ERROR)
				return 0;
			if (phase == 1) {
				gp_assert(code_used == code_fresh);
				gp_assert(used.avail_in == fresh.avail_in && used.avail_out == fresh.avail_out);
				gp_assert(bytes_eq(out_used, out_fresh, room - used.avail_out));
				gp_assert(used.total_in == fresh.total_in && used.total_out == fresh.total_out);
				gp_assert(used.msg == fresh.msg && used.data_type == fresh.data_type);
				gp_assert(window_bits < 0 || used.adler == fresh.adler);
			}
			read += take - used.avail_in;
			free(in_used);
			free(in_fresh);
			free(out_used);
			free(out_fresh);
		} while (nondet_u8() != 0);
		// zlib.h, inflateReset: "This function is equivalent to inflateEnd followed by inflateInit, but does
		// not free and reallocate the internal decompression state. The stream will keep attributes that may
		// have been set by inflateInit2."
		if (phase == 0) {
			gp_assert(inflateReset(&used) == Z_OK);
			if (inflateInit2(&fresh, window_bits) != Z_OK)
				return 0;
		}
	}
	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/api_reset.v:

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