Implementing Poly1305 using fiat-crypto

[brycx]

As part of an investigation into implementing support for ECC in Orion, the fiat-crypto (https://github.com/mit-plv/fiat-crypto) has been used as a source for formally verified arithmetic operations. This greatly increases confidence in the correctness of the implementation, while also reducing the amount of work needed to maintain and audit implementations utilizing fiat-crypto.

The draft PR #197 showcases these benefits well IMO. fiat-crypto also offers Rust generated code for Poly1305: https://github.com/mit-plv/fiat-crypto/blob/master/fiat-rust/src/poly1305_64.rs

I think it would be worth to explore replacing the current Poly1305 implementation with one that leverages the formally verified code generated by fiat-crypto, for the exact same reasons mentioned above.