[david415]

Stacked on #56. Its base becomes `main` once #56 merges.

Poly1305 ran on `Nat` arithmetic: about 150 ns per byte, twice ChaCha20's cost, and every block allocated bignums. This moves it to a new `Cipher/Poly1305.lean` with two versions:

• `spec`: the RFC 8439 §2.5 algorithm over `Nat`, moved unchanged from `ChaChaPoly`.
• `mac`: the accumulator in five 26-bit limbs held in `UInt64`s, reduced each block with `2^130 ≡ 5 (mod p)`, and reduced modulo `p` once at the end. Blocks are read as two little-endian words.

`mac_eq_spec : mac otk msg = spec otk msg` proves them equal, using only `propext`, `Classical.choice` and `Quot.sound` (no `sorry`, no `native_decide`, no `bv_decide`). The proof has four parts:

• `block_chunk`: a block's limbs are the RFC's chunk plus its `2^(8·len)`.
• `step_val`: no limb product or column sum overflows `UInt64`, every limb stays below `2^27`, and a step's value equals `(h + m)·r` less a multiple of `p`. The identity itself is `step_arith`, by `linear_combination`.
• `ofNat_val`: `r` in limbs is exact.
• `fold_val`: induction over the blocks.

`tagOf` uses `mac`.

	before	after
poly1305 1232 B	112 µs (`spec`)	16 µs
poly1305 64 KiB	7.8 ms	0.99 ms
chacha20-poly1305 encrypt 1200 B	247 µs (after #56; 383 µs before it)	63 µs

The benchmark gains `poly1305 1232B` and `poly1305 1232B, Nat spec` rows, as for GHASH and POLYVAL.

`make test` passes, including 316/316 Wycheproof ChaCha20-Poly1305 vectors.

ChaCha20 itself, about 45 µs per KiB, is now the larger cost.