{ x1 := (uint64(arg1) * 0xffffffffffffffff) x2 := ((x1 & arg3) | ((^x1) & arg2)) *out1 = x2 } // fiatScalarMul multiplies two field elements in the Montgomery domain. // // Preconditions: // // 0 ≤ eval arg1 < m // 0 ≤ eval arg2 < m // // Postconditions: // // eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m // 0 ≤ eval out1 < m func fiatScalarMul(out1 *fiatScalarMontgomery, arg1 *fiatScalarMontgomery, arg2 *fiatScalarMontgomery) { x1 := arg1[1]...