Function decaf377::fields::fr::u32::fiat::fr_msat

source ·
pub fn fr_msat(out1: &mut [u32; 9])
Expand description

The function fr_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]]