poly1305 rust and natmod

[franziskuskiefer]

• With add --deps option hax#174 this extracts except for all the natmod code, which is not supported by hax yet.
• The arithmetic is implemented in the trait with the struct defining the operations.

The generic only generates the following

#[derive(Clone, Copy, PartialEq, Eq)]
pub struct FieldElement {
    value: [u8; 17usize],
}
#[allow(non_snake_case)]
mod FIELDELEMENT_mod {
    use super::*;
    const FIELDELEMENT_MODULUS: [u8; 17usize] = [
        3u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8,
        255u8, 255u8, 255u8, 251u8,
    ];
    static FIELDELEMENT_MODULUS_STR: &str = "03fffffffffffffffffffffffffffffffb";
    impl NatMod<17usize> for FieldElement {
        const MODULUS: [u8; 17usize] = [
            3u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8, 255u8,
            255u8, 255u8, 255u8, 255u8, 251u8,
        ];
        const MODULUS_STR: &'static str = "03fffffffffffffffffffffffffffffffb";
        const ZERO: [u8; 17usize] = [0u8; 17usize];
        fn new(value: [u8; 17usize]) -> Self {
            Self { value }
        }
        fn value(&self) -> &[u8] {
            &self.value
        }
    }
    impl core::convert::AsRef<[u8]> for FieldElement {
        fn as_ref(&self) -> &[u8] {
            &self.value
        }
    }
    impl core::fmt::Display for FieldElement {
        fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
            write!(f, "{}", self.to_hex())
        }
    }
    impl Into<[u8; 17usize]> for FieldElement {
        fn into(self) -> [u8; 17usize] {
            self.value
        }
    }
    impl core::ops::Add for FieldElement {
        type Output = Self;
        fn add(self, rhs: Self) -> Self::Output {
            self.fadd(rhs)
        }
    }
    impl core::ops::Mul for FieldElement {
        type Output = Self;
        fn mul(self, rhs: Self) -> Self::Output {
            self.fmul(rhs)
        }
    }
}

cc @W95Psp @karthikbhargavan

Part of #13