Function fiat_crypto::p434_64::fiat_p434_from_montgomery

pub fn fiat_p434_from_montgomery(out1: &mut [u64; 7], arg1: &[u64; 7])

The function fiat_p434_from_montgomery translates a field element out of the Montgomery domain. Preconditions: 0 ≤ eval arg1 < m Postconditions: eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^7) mod m 0 ≤ eval out1 < m

Input Bounds: arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] Output Bounds: out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]