Function fiat_crypto::p384_scalar_32::fiat_p384_scalar_msat
source · pub fn fiat_p384_scalar_msat(out1: &mut [u32; 13])
Expand description
The function fiat_p384_scalar_msat returns the saturated representation of the prime modulus.
Postconditions: twos_complement_eval out1 = m 0 ≤ eval out1 < m
Output Bounds: out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]