Browse zstd specs (43 of 44)
Proofs / zstd / Earlier, longer properties
x_detect
A compliant series with one frame's checksum changed or reserved bit set is refused, one-shot and streamed.
- spec
- 78 lines of C
- with its headers
- 1,372 lines
- status
- Proved
- 43 of 44
On this page
The spec
The spec is the C program harness/x_detect.c, 78 lines, shown whole as it is in the repository at 2e46017. It includes harness/writer.h (1,231 lines) and harness/zlimits.h (63 lines). Its first comment states the property in full, with every bound.
// Law detect (PROMISES.md: V10, V11): ANY series of compliant frames in which one Zstandard frame is made invalid in
// a way zstd must detect: its Content_Checksum changed (zstd validates checksums by default: ZSTD_d_forceIgnoreChecksum
// "Default is 0"), or its Reserved_bit set ("A decoder compliant with this specification version must ensure it is not
// set").
//
// Claim (QuickProof.Contract.harness_safe of this program): no execution has undefined behaviour, and every gp_assert
// holds: one-shot decoding (ZSTD_decompress, any capacity) returns an error; streaming decoding (any chunks) never
// reports that frame complete (no 0 return at or after its end) before an error.
#include <stdlib.h>
#include "quickproof.h"
#include "writer.h"
#include "zlimits.h"
#define CALLS_MAX 4096
static wseries_t sr;
int main(void)
{
unsigned k, kind = choose(2), j;
size_t cap, r, end;
unsigned char *src, *dst;
w_series(&sr, 0);
k = choose(sr.nframes);
gp_assume(!sr.f[k].skippable);
if (kind == 0) {
unsigned x = 1 + choose(0xFFFFFFFFU);
gp_assume(sr.f[k].checksum);
for (j = 0; j < 4; j++)
sr.bytes[sr.f[k].start + sr.f[k].size - 4 + j] ^= (unsigned char) ((x >> (8 * j)) & 255);
} else {
sr.bytes[sr.f[k].start + 4] |= 8; /* Reserved_bit: bit 3 of Frame_Header_Descriptor */
}
end = sr.f[k].start + sr.f[k].size;
src = exact_copy(sr.bytes, sr.n);
if (src == NULL)
return 0; /* harness out of memory: end the run */
if (choose(2)) {
cap = choose_in(0, sr.content_n + 16);
dst = malloc(cap > 0 ? cap : 1);
if (dst != NULL) {
r = ZSTD_decompress(dst, cap, src, sr.n);
gp_assert(ZSTD_isError(r));
free(dst);
}
} else {
ZSTD_DStream *ds = ZSTD_createDStream();
size_t ipos = 0, calls;
for (calls = 0; ds != NULL && calls < CALLS_MAX; calls++) {
size_t ilen = choose_in(0, sr.n - ipos), olen = choose_in(1, sr.content_n + 1);
unsigned char *ib = exact_copy(src + ipos, ilen), *ob = malloc(olen);
ZSTD_inBuffer in;
ZSTD_outBuffer out;
if (ib == NULL || ob == NULL) {
free(ib);
free(ob);
break;
}
in.src = ib;
in.size = ilen;
in.pos = 0;
out.dst = ob;
out.size = olen;
out.pos = 0;
r = ZSTD_decompressStream(ds, &out, &in);
ipos += in.pos;
free(ib);
free(ob);
if (ZSTD_isError(r))
break;
if (r == 0)
gp_assert(ipos < end);
}
ZSTD_freeDStream(ds);
}
free(src);
return 0;
}harness/writer.h (1,231 lines) is too long to show here; it is in the repository.
harness/zlimits.h, 63 lines
// The limits under which zstd may refuse a compliant frame, as its documents state them (PROMISES.md V4): "a decoder
// is allowed to reject a compressed frame which requests a memory size beyond decoder's authorized range"
// (format), zstd's range being ZSTD_WINDOWLOG_MAX (31 on 64-bit: zstd.h) for any decoding and, for streaming,
// "By default, a decompression context accepts window sizes <= (1 << ZSTD_WINDOWLOG_LIMIT_DEFAULT)" (zstd.h);
// the memory allocation of its contexts; and, for streaming, zstd's deliberate busy-loop guard (stall_error).
#ifndef ZSTD_HARNESS_ZLIMITS_H
#define ZSTD_HARNESS_ZLIMITS_H
#include "writer.h"
#ifndef ZSTD_STATIC_LINKING_ONLY
#define ZSTD_STATIC_LINKING_ONLY /* ZSTD_WINDOWLOG_MAX, ZSTD_WINDOWLOG_LIMIT_DEFAULT */
#endif
#include "zstd.h"
#include "zstd_errors.h"
/* every Zstandard frame of the series is within zstd's window range (single-segment: Window_Size = content size) */
static int within_oneshot(const wseries_t *sr)
{
unsigned k;
for (k = 0; k < sr->nframes; k++)
if (!sr->f[k].skippable && !sr->f[k].single && sr->f[k].window_log > ZSTD_WINDOWLOG_MAX)
return 0;
return 1;
}
/* ... and within the streaming default */
static int within_stream(const wseries_t *sr)
{
unsigned k;
for (k = 0; k < sr->nframes; k++)
if (!sr->f[k].skippable && sr->f[k].window > (1ULL << ZSTD_WINDOWLOG_LIMIT_DEFAULT))
return 0;
return within_oneshot(sr);
}
/* zstd's busy-loop guard, deliberate (commit 31769ce70 "error on no forward progress": a caller "may be caught in an
infinite loop, calling the streaming decompression function again and again, without making any progress";
db18a62f8 gave it its error codes): ZSTD_decompressStream fails on the ZSTD_NO_FORWARD_PROGRESS_MAX-th (16 by
default) call in a row that reads no input and writes no output, with noForwardProgress_destFull if the output is
full, else noForwardProgress_inputEmpty (the input is then empty). zstd.h does not document it. True iff error
code e is that error, legitimately: this call (fresh input, output position opos0 before it) read and wrote
nothing, and so did the `stalled` calls in a row before it. */
#define NO_PROGRESS_MAX 16
static int stall_error(ZSTD_ErrorCode e, size_t stalled, const ZSTD_inBuffer *in, const ZSTD_outBuffer *out,
size_t opos0)
{
if (stalled + 1 < NO_PROGRESS_MAX || in->pos != 0 || out->pos != opos0)
return 0;
if (e == ZSTD_error_noForwardProgress_destFull)
return out->pos == out->size;
return e == ZSTD_error_noForwardProgress_inputEmpty && out->pos < out->size && in->pos == in->size;
}
/* a copy of b[0..n) in a buffer of exactly n bytes (NULL: out of memory) */
static unsigned char *exact_copy(const unsigned char *b, size_t n)
{
unsigned char *p = malloc(n > 0 ? n : 1);
size_t i;
if (p != NULL)
for (i = 0; i < n; i++)
p[i] = b[i];
return p;
}
#endifThe theorem
QuickProof generated this statement from the spec, in src/contracts/x_detect.v:
Theorem x_detect : 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_detect : harness_safe Zstd.contracts.x_detect.whole_prog.
Proof. exact (proj1 (proj2 (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.
The C files (units) its program links
patch/decoder.cquickproof/libc/libc.cquickproof/libc/malloc_unit.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), 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.