Browse zlib specs (26 of 62)

Proofs / zlib / The stream interface

api_split_invariant

For any input under 4 GiB, one call or any pieces give the same bytes and the same end result (32 KiB window).

spec
76 lines of C
with its headers
116 lines
status
Proved
26 of 62
On this page

The spec

The spec is the C program harness/api_split_invariant.c, 76 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_split_invariant: For any input (under 2^32 bytes), even garbage, and any wrapper with the 32 KiB window
// (inflateInit2 windowBits -15, 15, 31 or 47; inflateInit2 returns Z_OK), one inflate() call offered all of it, any
// output space and any flush but Z_BLOCK and Z_TREES gives the same result as a second stream fed the same input (a
// copy made before the first call) and output space in any pieces with any flush per call (until it returns
// Z_STREAM_END, Z_NEED_DICT or Z_DATA_ERROR, or a call offered all the rest with a flush other than Z_BLOCK and Z_TREES
// changes nothing): the same bytes written, and the same final code if the one call returned one of those three, else
// none of them (Z_MEM_ERROR ends the run).
#include "laws_common.h"

static int final(int code) {
	return code == Z_STREAM_END || code == Z_NEED_DICT || code == Z_DATA_ERROR;
}

int main(void) {
	int window_bits[4] = {-15, 15, 31, 47};
	int window = window_bits[upto(3)];
	size_t input_len = nondet_u32();
	size_t room = nondet_u32();
	unsigned char *input = alloc_any_bytes(input_len);
	if (input == NULL)
		return 0;
	unsigned char *input_split = copy_of(input, input_len);
	unsigned char *out_one = malloc(room);
	unsigned char *out_split = malloc(room);
	int flush = (int) nondet_u32();
	gp_assume(flush != Z_BLOCK && flush != Z_TREES);
	if (input_split == NULL || out_one == NULL || out_split == NULL)
		return 0;
	// zlib.h, inflate: "In this implementation, inflate() always flushes as much output as possible to the output
	// buffer"
	z_stream one;
	new_stream(&one);
	int code_one = inflateInit2(&one, window);
	if (code_one == Z_MEM_ERROR)
		return 0;
	gp_assert(code_one == Z_OK);
	set_buffer(&one, input, input_len, out_one, room);

	code_one = inflate(&one, flush);

	if (code_one == Z_MEM_ERROR)
		return 0;
	z_stream split;
	new_stream(&split);
	int code_split = inflateInit2(&split, window);
	if (code_split == Z_MEM_ERROR)
		return 0;
	gp_assert(code_split == Z_OK);
	split.next_in = input_split;
	split.next_out = out_split;
	for (;;) {
		size_t rest_in = input_len - (size_t) (split.next_in - input_split);
		size_t rest_out = room - (size_t) (split.next_out - out_split);
		uInt take = (uInt) upto(rest_in);
		uInt give = (uInt) upto(rest_out);
		int piece_flush = (int) nondet_u32();
		split.avail_in = take;
		split.avail_out = give;

		code_split = inflate(&split, piece_flush);

		if (code_split == Z_MEM_ERROR)
			return 0;
		int all_offered = take == rest_in && give == rest_out;
		int no_progress = split.avail_in == take && split.avail_out == give;
		int may_stop = piece_flush != Z_BLOCK && piece_flush != Z_TREES;
		if (final(code_split) || (all_offered && no_progress && may_stop))
			break;
	}
	if (final(code_one))
		gp_assert(code_split == code_one);
	else
		gp_assert(!final(code_split));
	gp_assert(split.total_out == one.total_out && bytes_eq(out_one, out_split, one.total_out));
	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_split_invariant.v:

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