Browse zlib specs (30 of 62)

Proofs / zlib / The stream interface

api_short_output

Given less room than the data needs (any amount, even none), uncompress2 says so (Z_BUF_ERROR), gives exactly the first bytes and has not read all of the compressed bytes (any bytes follow them).

spec
55 lines of C
with its headers
95 lines
status
Proved
30 of 62
On this page

The spec

The spec is the C program harness/api_short_output.c, 55 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_short_output: For any original data of one byte or more (any length the allocator provides) compressed by
// compress2 at any level -1..9 into original_len + (original_len >> 12) + (original_len >> 14) + (original_len >> 25)
// + 13 bytes (compressBound's formula in compress.c; Z_OK, a compressed length within that bound), uncompress2 of that
// output followed by any bytes (any number up to PTRDIFF_MAX minus the output's length) into an output space of any
// size below the original's length (0 included, and then also a Z_NULL buffer) returns Z_BUF_ERROR, sets the output
// length to the output space's size and the consumed source length to less than the compressed length, and the output
// holds the first decompressed_size bytes of the original data, as a copy made before compress2 holds them
// (Z_MEM_ERROR ends the run).
#include "laws_common.h"

int main(void) {
	size_t original_len = 1 + upto(PTRDIFF_MAX - 1);
	size_t decompressed_size = upto(original_len - 1);
	size_t null_if_empty = upto(1);
	int level = -1 + (int) upto(10);
	size_t compressed_bound = original_len + (original_len >> 12) + (original_len >> 14) + (original_len >> 25) + 13;
	unsigned char *original = alloc_any_bytes(original_len);
	if (original == NULL)
		return 0;
	unsigned char *original_copy = copy_of(original, original_len);
	unsigned char *compressed = malloc(compressed_bound);
	unsigned char *decompressed = Z_NULL;
	if (decompressed_size > 0 || null_if_empty == 0)
		decompressed = alloc_any_bytes(decompressed_size);
	if (original_copy == NULL || compressed == NULL || (decompressed == NULL && decompressed_size > 0))
		return 0;
	uLongf compressed_len = compressed_bound;

	int code = compress2(compressed, &compressed_len, original, original_len, level);

	if (code == Z_MEM_ERROR)
		return 0;
	gp_assert(code == Z_OK && compressed_len <= compressed_bound);
	size_t suffix_len = 0;
	if (compressed_len < PTRDIFF_MAX)
		suffix_len = upto(PTRDIFF_MAX - compressed_len);
	unsigned char *source = alloc_any_bytes(compressed_len + suffix_len);
	if (source == NULL)
		return 0;
	for (size_t i = 0; i < compressed_len; i++)
		source[i] = compressed[i];
	uLongf decompressed_len = decompressed_size;
	uLong source_consumed_len = compressed_len + suffix_len;

	code = uncompress2(decompressed, &decompressed_len, source, &source_consumed_len);

	if (code == Z_MEM_ERROR)
		return 0;
	// zlib.h, uncompress: "Z_BUF_ERROR if there was not enough room in the output buffer"; "In the case where there
	// is not enough room, uncompress() will fill the output buffer with the uncompressed data up to that point."
	gp_assert(code == Z_BUF_ERROR && decompressed_len == decompressed_size &&
		  bytes_eq(decompressed, original_copy, decompressed_size));
	gp_assert(source_consumed_len < compressed_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/api_short_output.v:

Rocq
Theorem api_short_output : 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_short_output : harness_safe Zlib.contracts.api_short_output.whole_prog.
Proof. exact (proj1 (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
  • deflate.c
  • trees.c
  • inflate.c
  • inffast.c
  • inftrees.c
  • compress.c
  • uncompr.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.