fiat_crypto::p521_32
pub fn fiat_p521_carry_mul( out1: &mut [u32; 17], arg1: &[u64; 17], arg2: &[u64; 17])