Function fiat_crypto::p224_32::fiat_p224_msat

pub fn fiat_p224_msat(out1: &mut [u32; 8])

The function fiat_p224_msat returns the saturated represtation of the prime modulus. Postconditions: twos_complement_eval out1 = m 0 ≤ eval out1 < m

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