PolyXOR128, a new fast universal hash written in Rust with a formalized security proof

The link to the project: https://github.com/orlp/polyxor.

I hope this qualifies as more than just a "code dump" as it's breaking new ground in several ways:

It's a very fast hash, beating all the mainstream hashes available I tested in Rust besides CRC64 for medium to large data. E.g. on machines with AVX-512 its bulk throughput is almost twice as fast as foldhash.
On top of that it provides a 128-bit hash rather than the usual 64-bit. 64 bits just isn't enough for file integrity / secure authentication purposes.
The hash has a proven low collision probability (assuming the key is generated randomly and independently from the data), formalized in Lean.

Besides the readme I have written a more in-depth design document as well: https://github.com/orlp/polyxor/blob/master/design.md.

Perhaps a point of discussion for Rust itself as well: I did consider releasing this hash in C for portability rather than Rust, but two things kept me in Rust:

Cargo makes it super easy to depend on a known-good AES implementation with hardware acceleration.
Between target_feature(enable = ...) and std::arch::is_x86_feature_detected, doing dynamic dispatch in Rust is so much easier than in C. And the resulting code runs faster too, e.g. #[target_feature(enable = "avx")] lets the compiler use AVX-encoded instructions.

Finally, before the AI witchhunters come out, there is a disclaimer of AI usage in the README. I did use AI for prototypes, experiments and conjectures but almost all of the final code and all the text and documentation is written by me. The big exception is the Lean formalization which is fully AI-generated, but the claims are verified by me and it compiles cleanly.