Browse zlib specs (9 of 62)

Proofs / zlib / Rejecting bad input

rj_uncompress_any

The same for uncompress2: any bytes, any output size: only documented codes, and the output space after what it reports written is left as it was.

spec
38 lines of C
with its headers
78 lines
status
Proved
9 of 62
On this page

The spec

The spec is the C program harness/rj_uncompress_any.c, 38 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 rj_uncompress_any: For any source (any bytes, any length the allocator provides, 0 included, and then also a
// Z_NULL buffer) and an output space of any size (0 included, and then also a Z_NULL buffer), uncompress2 returns one of
// the codes zlib.h documents for it: Z_OK, Z_MEM_ERROR, Z_BUF_ERROR or Z_DATA_ERROR; it sets the output length to at
// most the output space's size and the consumed source length to at most the source's length, and leaves the rest of
// the output space (after the bytes it reports written) as it was.
#include "laws_common.h"

int main(void) {
	size_t source_len = upto(PTRDIFF_MAX);
	size_t decompressed_size = upto(PTRDIFF_MAX);
	size_t null_if_empty = upto(1);
	unsigned char *source = Z_NULL;
	if (source_len > 0 || null_if_empty == 0)
		source = alloc_any_bytes(source_len);
	unsigned char *decompressed = Z_NULL;
	if (decompressed_size > 0 || null_if_empty == 0)
		decompressed = alloc_any_bytes(decompressed_size);
	if ((source == NULL && source_len > 0) || (decompressed == NULL && decompressed_size > 0))
		return 0;
	unsigned char *decompressed_copy = copy_of(decompressed, decompressed_size);
	if (decompressed_copy == NULL && decompressed_size > 0)
		return 0;
	uLongf decompressed_len = decompressed_size;
	uLong source_consumed_len = source_len;

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

	// zlib.h, uncompress: "uncompress returns Z_OK if success, Z_MEM_ERROR if there was not enough memory,
	// Z_BUF_ERROR if there was not enough room in the output buffer, or Z_DATA_ERROR if the input data was corrupted
	// or incomplete"; "On exit, *destLen is the actual size of the uncompressed data."; uncompress2: "On return,
	// *sourceLen is the number of source bytes consumed."
	gp_assert(code == Z_OK || code == Z_MEM_ERROR || code == Z_BUF_ERROR || code == Z_DATA_ERROR);
	gp_assert(decompressed_len <= decompressed_size && source_consumed_len <= source_len);
	if (decompressed_size > 0)
		gp_assert(bytes_eq(decompressed + decompressed_len, decompressed_copy + decompressed_len,
				   decompressed_size - decompressed_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/rj_uncompress_any.v:

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