x_bound

The spec#

The spec is the C program harness/x_bound.c, 16 lines, shown whole as it is in the repository at 2e46017. Its first comment states the property in full, with every bound.

// Law bound (PROMISES.md: C6): the compression bound of zstd.h.
//
// Claim (QuickProof.Contract.harness_safe of this program): every gp_assert holds: for ANY sizes A, B >= 128 KB with
// A + B < ZSTD_MAX_INPUT_SIZE, "bound(A) + bound(B) <= bound(A+B)" (ZSTD_COMPRESSBOUND: "this formula ensures that
// bound(A) + bound(B) <= bound(A+B) as long as A and B >= 128 KB").  (ZSTD_compressBound, the function, is the
// compressor's, which this project does not verify.)
#include "quickproof.h"
#include "zstd.h"

int main(void)
{
	size_t a = nondet_size(), b = nondet_size();
	if (a >= (128 << 10) && b >= (128 << 10) && a < ZSTD_MAX_INPUT_SIZE && b < ZSTD_MAX_INPUT_SIZE - a)
		gp_assert(ZSTD_COMPRESSBOUND(a) + ZSTD_COMPRESSBOUND(b) <= ZSTD_COMPRESSBOUND(a + b));
	return 0;
}

The theorem#

QuickProof generated this statement from the spec, in src/contracts/x_bound.v:

Theorem x_bound : 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:

Theorem x_bound : harness_safe Zstd.contracts.x_bound.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 Zstd.contracts.suite.suite_x))))))))). 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.

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), one thread, and binaries built by a compiler (the theorem is about the code as CompCert defines C for x86_64, LP64).
• Other configurations of zstd (flags, legacy formats, assembly) and the compressor.
• The edits to zstd's code, listed in the repository, are checked against the original by testing, 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.