BLAKE2s

The spec#

The property is stated by the C program harness/x_prim_blake2s.c, 75 lines. This is its main (lines 20–75):

int main(void)
{
	struct blake2s_ctx ctx;
	size_t keylen, outlen, n, pos, i;
	u8 key[32], key_copy[32];
	u8 *msg, *copy, *out, *ref, *out2;

	outlen = 1 + nondet_u8() % 32;
	keylen = nondet_u8() % 33;
	nondet_bytes(key, 32);
	bytes_copy(key_copy, key, 32);
	n = draw_size();
	if (n > PTRDIFF_MAX)   /* no C object is larger than PTRDIFF_MAX: see the header comment */
		return 0;
	msg = malloc(n);
	copy = malloc(n);
	out = malloc(outlen);
	ref = malloc(outlen);
	out2 = malloc(outlen);
	if ((msg == NULL || copy == NULL) || out == NULL || ref == NULL || out2 == NULL) {
		free(msg); free(copy); free(out); free(ref); free(out2);
		return 0;
	}
	nondet_bytes(msg, n);
	bytes_copy(copy, msg, n);

	if (keylen > 0)
		blake2s_init_key(&ctx, outlen, key, keylen);
	else
		blake2s_init(&ctx, outlen);
	pos = 0;
	while (pos < n) {
		size_t c = nondet_size();
		if (c > n - pos)
			c = n - pos;
		blake2s_update(&ctx, msg + pos, c);
		pos += c;
	}
	if (nondet_u8() & 1)
		blake2s_update(&ctx, msg, 0);
	blake2s_final(&ctx, out);

	ref_blake2s(ref, outlen, key, keylen, msg, n);
	CHECK(bytes_eq(out, ref, outlen));
	for (i = 0; i < 8; i++)
		CHECK(ctx.h[i] == 0);
	CHECK(ctx.t[0] == 0 && ctx.t[1] == 0 && ctx.f[0] == 0 && ctx.f[1] == 0);
	CHECK(bytes_zero(ctx.buf, 64) && ctx.buflen == 0 && ctx.outlen == 0);

	blake2s(keylen > 0 ? key : NULL, keylen, msg, n, out2, outlen);
	CHECK(bytes_eq(out2, ref, outlen));
	CHECK(bytes_eq(msg, copy, n) && bytes_eq(key, key_copy, 32));

	free(msg); free(copy); free(out); free(ref); free(out2);
	return 0;
}

The full spec at commit 3c1fc13 ↗

Law `prim_blake2s`: the kernel's BLAKE2s (lib/crypto/blake2s.c, generic compression, include/crypto/blake2s.h)
is BLAKE2s (RFC 7693, the reference ref_blake2s of common.h).

For ANY output length 1..32, ANY key of 0..32 bytes (0: blake2s_init, else blake2s_init_key; the documented
ranges), ANY message of any length (exact-size buffer), fed to blake2s_update in ANY split into chunks
(including empty chunks):
 - blake2s_final writes exactly the reference digest into an output buffer of exactly outlen bytes;
 - the context is all zero afterwards (documented: "After finishing, this zeroizes @ctx");
 - the one-shot inline blake2s(key or NULL, keylen, msg, len, out, outlen) gives the same digest;
 - the message and the key are not modified.
Buffer lengths above PTRDIFF_MAX (2^63 - 1) end the run: no real C implementation creates an object larger than
PTRDIFF_MAX (pointer differences inside it must fit ptrdiff_t; glibc's malloc returns NULL beyond it), but
CompCert's memory model and VST's malloc_spec' allow objects of up to 2^64 - 1 bytes, which would make the law
cover buffers that cannot exist (e.g. blake2s_update's DIV_ROUND_UP(inlen, 64) wraps for inlen >= 2^64 - 63).
This is an assumption about the environment, recorded as DEVIATIONS.md L13; it may later move into the
framework's malloc specification.

The code it is about#

blake2s_update in lib/crypto/blake2s.c, lines 114–136:

void blake2s_update(struct blake2s_ctx *ctx, const u8 *in, size_t inlen)
{
	const size_t fill = BLAKE2S_BLOCK_SIZE - ctx->buflen;

	if (unlikely(!inlen))
		return;
	if (inlen > fill) {
		memcpy(ctx->buf + ctx->buflen, in, fill);
		blake2s_compress(ctx, ctx->buf, 1, BLAKE2S_BLOCK_SIZE);
		ctx->buflen = 0;
		in += fill;
		inlen -= fill;
	}
	if (inlen > BLAKE2S_BLOCK_SIZE) {
		const size_t nblocks = DIV_ROUND_UP(inlen, BLAKE2S_BLOCK_SIZE);

		blake2s_compress(ctx, in, nblocks - 1, BLAKE2S_BLOCK_SIZE);
		in += BLAKE2S_BLOCK_SIZE * (nblocks - 1);
		inlen -= BLAKE2S_BLOCK_SIZE * (nblocks - 1);
	}
	memcpy(ctx->buf + ctx->buflen, in, inlen);
	ctx->buflen += inlen;
}

This is the code under test as the proof sees it: Linux at 551c722f with the two lib/crypto patches, and with the idiom rewrites that VST needs, each marked QUICKPROOF in the code and listed in DEVIATIONS.md.

The theorem#

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

Theorem x_prim_blake2s : harness_safe whole_prog.

whole_prog is the spec linked with the code under test. The 19 x_ specs are proved together, as the theorem suite_x, from one specification of every function of the code. src/contracts/laws.v states each spec on its own program and takes it from suite_x:

Theorem x_prim_blake2s : harness_safe WgNoise.contracts.x_prim_blake2s.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 WgNoise.contracts.suite.suite_x))))))))))))). Qed.

qp verify checks that this statement is the one generated from the spec at the contract commit, and that its proof uses no axiom beyond the 13 that every spec here uses: standard logical axioms and VST's abstract malloc library.

What it leaves out#

• Like every spec of this proof: runs of more than one thread (locks and RCU are those of a single thread), 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 64-bit x86).
• The kernel around the code is a shim of plain C for one thread, and the code carries rewrites of idioms that VST cannot handle. Both are tested against the kernel's code, not proved.

Recorded for this property in DEVIATIONS.md (section L, what the properties exclude or assume):

• L13. The specs x_prim_blake2s, x_prim_poly1305 and x_prim_aead end the run when a drawn buffer length (message, associated data, the bytes given to decrypt) exceeds PTRDIFF_MAX (2^63 - 1), and so do x_transport_order (payload length above PTRDIFF_MAX - 32) and x_transport_len (packet length above PTRDIFF_MAX - 32). The lengths are otherwise unbounded. The ae_ specs draw their lengths up to PTRDIFF_MAX (PTRDIFF_MAX - 16 for a message that gets a 16-byte tag) Why: no C implementation creates an object larger than PTRDIFF_MAX (pointer differences inside it must fit ptrdiff_t; glibc's malloc returns NULL beyond it), but CompCert's memory model and VST's malloc_spec' allow objects of up to 2^64 - 1 bytes, which would make the specs cover buffers that cannot exist: blake2s_update's DIV_ROUND_UP(inlen, 64) wraps for inlen of 2^64 - 63 or more. This is an assumption about the environment, not about the code

The summary page lists what the proof as a whole does not cover.

How it was proved#

src/proof/harness/prim_blake2s/ holds 2,648 lines of Rocq (formerly Coq) that are specific to this spec. It builds on the specifications and proofs of the functions of noise.c, cookie.c and lib/crypto, the protocol model, and the Diffie-Hellman agreement of X25519. The whole proof of the 38 specs is about 300,000 lines. AI agents wrote it, Rocq checks all of it, and nobody has to read it. What people have to read is the spec above, with harness/common.h, and the kernel shim that DEVIATIONS.md describes.

Other specs about lib/crypto: see the list on the left, or the summary.