fiat_crypto::p521_64
pub fn fiat_p521_carry_mul( out1: &mut [u64; 9], arg1: &[u64; 9], arg2: &[u64; 9])