Session keys and their lifetime

Law `keypairs`: keypair rotation and lifetime against a shadow model, over ANY sequence of operations.

One peer P of a device (any identity), with ANY other mutable state (common.h peer_randomize_rest);
ANY number of other peers of the device with ANY state (handshake, cookie, ...), their handshake entries in the
index table or not, and ANY number of keypairs of theirs (whole objects of ANY content, common.h kents_add) in the
table, possibly in their slots.  A sequence of ANY length of operations, each one of:
  - wg_noise_handshake_begin_session after setting P's handshake to ANY mutable state (common.h hs_randomize: any
    of the five states - CREATED_RESPONSE: responder, CONSUMED_RESPONSE: initiator -, any chaining key, remote
    index, ephemeral keys, hash, latest timestamp, last consumption), its index entry hashed or not, P dead or
    not; the allocation may fail;
  - wg_noise_received_with_keypair with ANY live keypair (current, previous, next or one only a reference
    holder keeps), a keypair of another peer, or NULL: receive.c
    always passes the keypair it looked up, but the function's behaviour on NULL is defined and claimed too (with
    no next keypair, NULL is the next keypair and the slots rotate);
  - wg_noise_expire_current_peer_keypairs;  - wg_noise_keypairs_clear;
  - wg_noise_keypair_get of NULL or any live keypair (the harness keeps the reference);
  - wg_noise_keypair_put of ANY kept reference (any keypair the harness holds one of), with unreference_now true
    or false, or of NULL;
  - the data path's use of ANY live keypair: its sending counter and its receiving counter set to
    ANY values (what send.c / receive.c do; out of scope themselves);
with the boot clock moving forward by any amount.  No bound on the number of operations, of sessions or of
references (as the kernel does it: the reference count is the kernel's refcount_t, which the
shim models exactly - quickproof_kref.h, S04 - and the 64-bit keypair counter wraps like the kernel's atomic).
Shadow model (in this file): the three slots (previous, current, next), every live keypair with its reference
count, index-table membership and index, keys, validity, birthdate, role, remote index and internal id; the
rotation rules of the WireGuard paper (initiator: the new keypair becomes current, the old current previous or,
if a next keypair was waiting, that one previous and the old current is dropped; responder: the new keypair
waits as next and previous is dropped; confirmation (received_with_keypair of next): next becomes current,
current previous, previous dropped); "dropped" = unhashed now and one reference less; the reference count as
include/linux/refcount.h documents refcount_t: +1 per get and -1 per put while it is below INT_MAX = 2^31 - 1,
a keypair is freed exactly when its last reference goes; a get that finds INT_MAX references SATURATES the
count (REFCOUNT_SATURATED = 0xc0000000, the kernel's warning "saturated; leaking memory"); a saturated count
never changes again (every later put is the kernel's warning "underflow; use-after-free" on the saturated
count, and does nothing else), and a saturated keypair is never freed: it is leaked, as the kernel leaks it.
Claims after EVERY operation: return values, slot pointers, every live keypair's fields, reference counts
(exactly the model's, the saturated value included) and table membership (the table holds exactly the hashed
live keypairs, P's handshake entry if hashed and the other peers' entries, with unique indices), P's handshake
(zeroed by begin_session and expire, else unchanged), expire invalidates the sending keys of current and next
and resets last_sent_handshake to now - 6 s; allocations minus frees = live keypairs; the kernel's refcount_t
warnings are exactly the model's: NEVER an increment from 0 ("addition on 0; use-after-free"), never an
underflow of a count that is not saturated, never kref_get's overflow or a decrement to 0 without release - the
only warnings are a get at INT_MAX (saturation) and the puts of an already saturated count.  A saturated keypair
stays readable and unchanged (the model compares its every field after every operation: it is never freed, so
never used after free).  At the end, clear and putting every kept reference free every keypair that never
saturated; the saturated ones (and only they) are leaked.
Also, after EVERY operation: a new keypair starts with fresh counters (sending counter 0, replay
window counter 0 with an empty bitmap); no operation ever changes the counters of a live keypair (rotation and
teardown never reset or rewind a nonce counter); P's handshake is checked after EVERY operation (whole, against
the model's copy); the rest of P (cookie state, dead flag, last sent handshake but by expire, internal id,
public-key table link) and its reference count, every other peer as a whole and its keypairs (every byte), and the
device (identity, cookie checker, public-key table), never change.