[david415]

ChaCha20 was the largest single cost left in huh's QUIC transfers (about a quarter of each process's CPU in quarterRound), plus allocation from building the keystream.

• ChaCha20.block now keeps the 16-word state in the unboxed fields of a structure instead of an Array UInt32 updated with set!. The previous definition stays as blockSpec, and block_eq_spec proves the two equal (axioms: propext, Classical.choice, Quot.sound).
• ChaChaPoly's keystream is appended in place into one preallocated ByteArray, and the XOR is ByteArray.ofFn over the two byte arrays, instead of round trips through Array UInt8 (ByteArray.data and ByteArray.mk both copy). size_chacha20 and chacha20_chacha20 are re-proved over the new XOR.
• Bench: chacha20 block and chacha20 block, spec.

	before	after
chacha20 block	3.0 µs (spec)	0.42–0.6 µs
chacha20 1 KiB	45 µs	6.9 µs
chacha20 4 KiB	152 µs	25.7 µs
chacha20 16 KiB	647 µs	104 µs
chacha20 64 KiB	2.53 ms	0.42 ms
chacha20-poly1305 encrypt 1200 B	63 µs	23 µs

Growth is linear (3.7×, 4.0×, 4.0× per 4× size). make test passes, including 316/316 Wycheproof ChaCha20-Poly1305 vectors and the ChaCha20 keystream vectors.