fiatScalarNonzero function

BigInt fiatScalarNonzero(
  1. List<BigInt> arg1
)

fiatScalarNonzero 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] Output Bounds: out1: 0x0 ~> 0xffffffffffffffff

Implementation

BigInt fiatScalarNonzero(List<BigInt> arg1) {
  return (arg1[0] | (arg1[1] | (arg1[2] | arg1[3])));
}