Sending nonces

The spec#

The property is stated by the C program harness/x_transport_send_nonce.c, 77 lines. This is its main (lines 34–77):

int main(void)
{
	struct noise_keypair kp;             // only sending.is_valid and sending_counter are used
	u64 shadow, start;
	size_t steps, i;

	// Start values: any counter of a valid key, [0, R].  ASSUMPTION (DEVIATIONS.md L16, of the class of L02): the
	// run ends before the counter would step from 2^63 - 1 to 2^63 (a key never sends 2^63 messages:
	// it expires after REJECT_AFTER_TIME, 180 s); nonces >= 2^63 are still drawn, from starts in [2^63, R].  (The shim's increment
	// wraps like the kernel's atomic64 (quickproof_kref.h), so this guard is not needed for definedness; it is part
	// of the law as stated.)
	switch (nondet_u8() % 5) {
	case 0: start = 0; break;                                                // a fresh key
	case 1: start = M_R - (u64)(nondet_u32() % 8); break;                   // just below / at the limit
	case 2: start = (1ULL << 63) + draw_u64() % (M_R - (1ULL << 63) + 1); break;  // upper half, up to the limit
	case 3: start = S64_TOP - (u64)(nondet_u32() % 8); break;               // just below the s64 boundary
	default: start = draw_u64() % (M_R + 1); break;                         // anywhere a valid key can be
	}
	kp.sending.is_valid = true;
	atomic64_set(&kp.sending_counter, (s64)start);
	shadow = start;

	steps = draw_steps();
	for (i = 0; i < steps; i++) {
		u64 v, nonce, nonce_model;

		if (!READ_ONCE(kp.sending.is_valid))              // send.c:363: no nonce on an invalid key
			break;
		if (shadow == S64_TOP)                            // L16: the shim's s64 `++` would overflow
			break;
		v = (u64)atomic64_inc_return(&kp.sending_counter);  // send.c:379-380, the draw
		nonce = v - 1;
		nonce_model = shadow;
		shadow += 1;

		CHECK(nonce == nonce_model);                     // monotonic, +1 each draw, never repeats
		CHECK((nonce >= REJECT_AFTER_MESSAGES) == (nonce >= M_R));  // refused exactly at the limit
		if (nonce >= REJECT_AFTER_MESSAGES)              // send.c:381-382, 391-392
			WRITE_ONCE(kp.sending.is_valid, false);
	}
	CHECK((u64)kp.sending_counter.counter == shadow);
	CHECK(shadow <= M_R + 1);                                // at most one refused draw: the nonce never wraps
	return 0;
}

The full spec at commit 3c1fc13 ↗

Law `transport_send_nonce`: the per-keypair sending nonce is monotonic and never repeats, sending is
refused at REJECT_AFTER_MESSAGES, and a key's nonce never wraps.

!!! MODEL ONLY -- NOT backed by extracted upstream code (DEVIATIONS.md L16). !!!
drivers/net/wireguard/send.c is NOT part of the code under test (receive.c is; the handshake laws never needed
send.c), so wg_packet_send_staged_packets' nonce draw cannot be called.  This
harness writes that draw out as send.c has it at the pin (send.c:363-364, 379-382, 391-392):
    if (!READ_ONCE(keypair->sending.is_valid)) goto out_nokey;          -- no nonce on an invalid key
    nonce = atomic64_inc_return(&keypair->sending_counter) - 1;
    if (nonce >= REJECT_AFTER_MESSAGES) goto out_invalid;               -- out_invalid: is_valid = false
with the shim's atomic64_inc_return (quickproof_kref.h, which wraps like the kernel's atomic64) and the kernel's
REJECT_AFTER_MESSAGES as compiled (messages.h; DEVIATIONS.md C04), so the law is READY to be pointed at the real
draw once send.c is added (the send path also pulls in skb allocation, padding to MESSAGE_PADDING_MULTIPLE, and
the per-peer tx queue).

A sending keypair in ANY state a valid key can be in -- counter = any value in [0, REJECT_AFTER_MESSAGES], as
after that many messages (0, near REJECT_AFTER_MESSAGES, around 2^63, anywhere) -- then a sequence of ANY length
of draws as above.
Shadow model: shadow (u64) tracks the counter; nonce_model = shadow (the pre-increment value), shadow += 1;
R = REJECT_AFTER_MESSAGES = 2^64 - 1 - 8128 - 1, computed here (as counter.c does).
CHECKs after every draw:
  - the drawn nonce == nonce_model  => strictly monotonic, increments by exactly 1, never repeats;
  - the kernel's refusal test (nonce >= REJECT_AFTER_MESSAGES as compiled) == (nonce >= R)  => sending refused
    exactly at the limit;
and at the end: the counter == shadow <= R + 1 (at most one refused draw per key: the counter never wraps, so a
nonce is never issued twice over the key's life).  (The kernel never draws on an invalid key, and the law models
that rule: for the bare counter, "once refused, every later draw is refused" would be false for an unbounded
number of draws, since the u64 nonce wraps to 0 after 8130 refused draws from R.)

The code it is about#

The spec itself carries the code this property is about; see the notes above.

The theorem#

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

Theorem x_transport_send_nonce : 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_transport_send_nonce : harness_safe WgNoise.contracts.x_transport_send_nonce.whole_prog.
Proof. exact (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (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):

• L16. x_transport_send_nonce is a model only: send.c is not in the code under test, so the spec runs the send path's nonce draw as the spec writes it out from send.c at the pin (wg_packet_send_staged_packets: no draw on an invalid key; nonce = atomic64_inc_return(&keypair->sending_counter) - 1; nonce >= REJECT_AFTER_MESSAGES invalidates the key), with the shim's atomic64_inc_return (S04) and the kernel's REJECT_AFTER_MESSAGES as compiled (C04). The run also ends before the counter would step from 2^63 - 1 to 2^63 (a key never sends 2^63 messages: it expires after REJECT_AFTER_TIME, 180 s); nonces of 2^63 and more are still covered, from start counters in [2^63, REJECT_AFTER_MESSAGES] Why: send.c needs skb allocation, padding to MESSAGE_PADDING_MULTIPLE and the per-peer transmit queue

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

How it was proved#

src/proof/harness/transport_send_nonce/ holds 481 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 receive.c: see the list on the left, or the summary.