Function fiat_crypto::p434_64::fiat_p434_nonzero
source · pub fn fiat_p434_nonzero(out1: &mut u64, arg1: &[u64; 7])
Expand description
The function fiat_p434_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 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] Output Bounds: out1: [0x0 ~> 0xffffffffffffffff]