Browse zstd specs (25 of 44)
ck_xxh64
ZSTD_XXH64 equals XXH64 as the xxHash specification defines it, written out in the spec, for any bytes and seed.
- spec
- 60 lines of C
- with its headers
- 93 lines
- status
- Proved
- 25 of 44
On this page
The spec
The spec is the C program harness/ck_xxh64.c, 60 lines, shown whole as it is in the repository at 2e46017. It includes harness/laws_common.h (33 lines). Its first comment states the property in full, with every bound.
// Law ck_xxh64: For any bytes (any length the allocator provides) and any seed, zstd's XXH64 (ZSTD_XXH64, the hash of
// the frame's Content_Checksum) equals XXH64 as the xxHash specification defines it, written out below.
#include "laws_common.h"
// xxHash specification (doc/xxhash_spec.md), "XXH64 Algorithm Description": "All operations are performed modulo 2^64".
#define PRIME64_1 0x9E3779B185EBCA87ULL
#define PRIME64_2 0xC2B2AE3D27D4EB4FULL
#define PRIME64_3 0x165667B19E3779F9ULL
#define PRIME64_4 0x85EBCA77C2B2AE63ULL
#define PRIME64_5 0x27D4EB2F165667C5ULL
static uint64_t rotl(uint64_t x, int r) { return x << r | x >> (64 - r); } // "<<<", 0 < r < 64
static uint64_t le(const unsigned char *p, int size) { // "read_64bit_little_endian", "read_32bit_little_endian"
uint64_t value = 0;
for (int i = size - 1; i >= 0; i--)
value = value << 8 | p[i];
return value;
}
static uint64_t round64(uint64_t acc, uint64_t lane) { return rotl(acc + lane * PRIME64_2, 31) * PRIME64_1; }
static uint64_t merge(uint64_t acc, uint64_t accn) { return (acc ^ round64(0, accn)) * PRIME64_1 + PRIME64_4; }
static uint64_t xxh64(const unsigned char *p, size_t len, uint64_t seed) {
uint64_t acc = seed + PRIME64_5; // Step 1, "input is less than 32 bytes"
size_t left = len;
if (len >= 32) { // Steps 1 to 3
uint64_t acc1 = seed + PRIME64_1 + PRIME64_2, acc2 = seed + PRIME64_2;
uint64_t acc3 = seed, acc4 = seed - PRIME64_1;
for (; left >= 32; left -= 32, p += 32) {
acc1 = round64(acc1, le(p, 8));
acc2 = round64(acc2, le(p + 8, 8));
acc3 = round64(acc3, le(p + 16, 8));
acc4 = round64(acc4, le(p + 24, 8));
}
acc = rotl(acc1, 1) + rotl(acc2, 7) + rotl(acc3, 12) + rotl(acc4, 18);
acc = merge(merge(merge(merge(acc, acc1), acc2), acc3), acc4);
}
acc += len; // Step 4
for (; left >= 8; left -= 8, p += 8) // Step 5
acc = rotl(acc ^ round64(0, le(p, 8)), 27) * PRIME64_1 + PRIME64_4;
if (left >= 4) {
acc = rotl(acc ^ le(p, 4) * PRIME64_1, 23) * PRIME64_2 + PRIME64_3;
left -= 4;
p += 4;
}
for (; left >= 1; left--, p++)
acc = rotl(acc ^ *p * PRIME64_5, 11) * PRIME64_1;
acc = (acc ^ acc >> 33) * PRIME64_2; // Step 6
acc = (acc ^ acc >> 29) * PRIME64_3;
return acc ^ acc >> 32;
}
int main(void) {
size_t len = upto(PTRDIFF_MAX);
unsigned char *data = any_bytes(len);
uint64_t seed;
pick(seed);
if (data == NULL)
return 0;
gp_assert(ZSTD_XXH64(data, len, seed) == xxh64(data, len, seed));
return 0;
}harness/laws_common.h, 33 lines
// laws_common.h: trivial helpers shared by the zstd laws (each law includes it once). No models, no algorithms.
#define ZSTD_STATIC_LINKING_ONLY // zstd.h's experimental part (ZSTD_WINDOWLOG_MAX, ...)
#include <stdint.h>
#include <stdlib.h>
#include "quickproof.h"
#include "zstd.h"
#include "zstd_errors.h"
uint64_t ZSTD_XXH64(const void *input, size_t length, uint64_t seed); // zstd's XXH64 (law ck_xxh64 checks it)
static size_t upto(size_t max) { // any value from 0 to max
size_t value = nondet_size();
return value < max ? value : max;
}
static unsigned char *any_bytes(size_t n) { // a new object of n arbitrary bytes (NULL if malloc fails)
unsigned char *bytes = malloc(n);
if (bytes != NULL && n != 0)
nondet_bytes(bytes, n);
return bytes;
}
static unsigned char *copy_of(const unsigned char *source, size_t n) { // a new object holding source[0..n-1]
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) { // a[0..n-1] == b[0..n-1]
for (size_t i = 0; i < n; i++)
if (a[i] != b[i])
return 0;
return 1;
}
static int out_of_memory(size_t result) { // zstd could not allocate (this ends a run: no claim)
return ZSTD_getErrorCode(result) == ZSTD_error_memory_allocation;
}The theorem
QuickProof generated this statement from the spec, in src/contracts/ck_xxh64.v:
Theorem ck_xxh64 : 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 ck_xxh64 : harness_safe Zstd.contracts.ck_xxh64.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 Zstd.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
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.