mac1 and mac2

Law `cookie_mac`: mac1/mac2 creation (wg_cookie_add_mac_to_packet) and validation (wg_cookie_validate_packet)
against the model, on ANY message and ANY cookie state.

Responder device B with ANY static key (its cookie checker keys precomputed; its cookie secret and the secret's
birthdate ANY); a peer P of another device whose public key is B's (honest) or ANY; P's cookie state ANY
(valid or not, any birthdate, any cookie, any last mac1) or, in one mode, the cookie B would make for the
packet's source; a message of ANY length >= 32 (its last 32 bytes are mac1 || mac2; exact-size buffer) with ANY
content; ANY boot clock; the packet's protocol IPv4, IPv6 or other, ANY source address and port; the rate
limiter's answer ANY; check_cookie ANY.
Claims:
 - the checker's keys are HASH("mac1----" || S_pub) and HASH("cookie--" || S_pub) (zero without identity);
   the peer's are the same for its public key; wg_cookie_checker_init gives the checker a fresh
   random secret (the shim's draw) born now;
 - add_mac writes mac1 = MAC(mac1 key, m[0..len-32)), and mac2 = MAC(cookie, m[0..len-16)) if the cookie is
   valid and younger than 115 s (COOKIE_SECRET_MAX_AGE - COOKIE_SECRET_LATENCY: birthdate + 115 s > now,
   signed), else 16 zero bytes; nothing else of the message; the peer remembers mac1 (last_mac1_sent,
   have_sent_mac1) and nothing else of its cookie state changes;
 - validate returns exactly the model's verdict: INVALID_MAC if mac1 is not MAC(checker mac1 key, ...);
   VALID_MAC_BUT_NO_COOKIE if !check_cookie or mac2 does not match the cookie of the packet's source;
   VALID_MAC_WITH_COOKIE_BUT_RATELIMITED if the rate limiter refuses; else VALID_MAC_WITH_COOKIE.  The cookie
   is MAC32(secret, source address (4 bytes for IPv4, 16 for IPv6, none otherwise) || source port), and the
   secret is replaced by fresh random bytes (birthdate now) when it is 120 s old, exactly as cookie.c decides it
   (wg_birthdate_has_expired: (s64)(birthdate + 120 s) <= (s64)now): at EXACTLY 120 s the secret is new, so a
   mac2 made with the old one fails (wireguard-go rotates only after 120 s); the harness draws the clock at
   120 s +- 2 ns and 115 s +- 2 ns on purpose;
 - validate modifies neither the message nor the packet; the checker only by that rotation;
 - (whole-state frame; P has ANY handshake state, dead flag, last sent handshake, reference count
   below INT_MAX, its handshake entry in A's index table or not, and ANY keypairs - whole objects of any content -
   in that table and possibly in its slots) add_mac changes nothing of the peer but those two cookie fields
   (handshake, reference count, keypair slots and every byte of the keypairs, ... unchanged), neither device and
   not A's index table; validate changes nothing of either device but that rotation (identity, both checker keys,
   the checker's device, tables) nor the peer (its keypairs and A's index table included), and leaves every field
   of the packet as it was (data, length, protocol, source address and port); neither allocates nor makes a
   reference count warn;
 - round trips: a message with macs added by a peer that has B's public key has a valid mac1 at B; if the peer
   also holds B's current cookie for the packet's source (fresh), mac2 is valid too.