Function fiat_crypto::p434_64::fiat_p434_msat

pub fn fiat_p434_msat(out1: &mut [u64; 8])

The function fiat_p434_msat returns the saturated representation of the prime modulus.

Postconditions: twos_complement_eval out1 = m 0 ≤ eval out1 < m

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