Function decaf377::fields::fr::u32::fiat::fr_nonzero

source ·
pub fn fr_nonzero(out1: &mut u32, arg1: &[u32; 8])
Expand description

The function fr_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.

Preconditions: 0 ≤ eval arg1 < m Postconditions: out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0

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