Skip to content

Conversation

@franziskuskiefer
Copy link
Member

@franziskuskiefer franziskuskiefer commented Jun 29, 2023

  • With add --deps option cryspen/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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants