fiatScalarFromMontgomery function

void fiatScalarFromMontgomery(List<BigInt> out1, List<BigInt> arg1)

fiatScalarFromMontgomery translates a field element out of the Montgomery domain.

Preconditions: 0 ≤ eval arg1 < m Postconditions: eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m 0 ≤ eval out1 < m

Implementation

void fiatScalarFromMontgomery(List<BigInt> out1, List<BigInt> arg1) {
  final BigInt x1 = arg1[0];

  final (_, BigInt x2) = Bits.mul64(x1, '15183074304973897243'.toBigInt());

  final (BigInt x5, BigInt x4) =
      Bits.mul64(x2, '1152921504606846976'.toBigInt());

  final (BigInt x7, BigInt x6) =
      Bits.mul64(x2, '1503914060200516822'.toBigInt());

  final (BigInt x9, BigInt x8) =
      Bits.mul64(x2, '6346243789798364141'.toBigInt());

  final (BigInt x10, int x11) = Bits.add64(x9, x6, 0);

  final (_, int x13) = Bits.add64(x1, x8, 0);

  final (BigInt x14, int x15) = Bits.add64(BigInt.zero, x10, x13);

  final (BigInt x16, int x17) = Bits.add64(x14, arg1[1], 0);

  final (_, BigInt x18) = Bits.mul64(x16, '15183074304973897243'.toBigInt());

  final (BigInt x21, BigInt x20) =
      Bits.mul64(x18, '1152921504606846976'.toBigInt());

  final (BigInt x23, BigInt x22) =
      Bits.mul64(x18, '1503914060200516822'.toBigInt());

  final (BigInt x25, BigInt x24) =
      Bits.mul64(x18, '6346243789798364141'.toBigInt());

  final (BigInt x26, int x27) = Bits.add64(x25, x22, 0);

  final (_, int x29) = Bits.add64(x16, x24, 0);

  final (BigInt x30, int x31) = Bits.add64(
      (x17.toBigInt + (x15.toBigInt + (x11.toBigInt + x7))), x26, x29);

  final (BigInt x32, int x33) = Bits.add64(x4, (x27.toBigInt + x23), x31);

  final (BigInt x34, int x35) = Bits.add64(x5, x20, x33);

  final (BigInt x36, int x37) = Bits.add64(x30, arg1[2], 0);

  final (BigInt x38, int x39) = Bits.add64(x32, BigInt.zero, x37);

  final (BigInt x40, int x41) = Bits.add64(x34, BigInt.zero, x39);

  final (_, BigInt x42) = Bits.mul64(x36, '15183074304973897243'.toBigInt());

  final (BigInt x45, BigInt x44) =
      Bits.mul64(x42, '1152921504606846976'.toBigInt());

  final (BigInt x47, BigInt x46) =
      Bits.mul64(x42, '1503914060200516822'.toBigInt());

  final (BigInt x49, BigInt x48) =
      Bits.mul64(x42, '6346243789798364141'.toBigInt());

  final (BigInt x50, int x51) = Bits.add64(x49, x46, 0);

  final (_, int x53) = Bits.add64(x36, x48, 0);

  final (BigInt x54, int x55) = Bits.add64(x38, x50, x53);

  final (BigInt x56, int x57) = Bits.add64(x40, (x51.toBigInt + x47), x55);

  final (BigInt x58, int x59) =
      Bits.add64((x41.toBigInt + (x35.toBigInt + x21)), x44, x57);

  final (BigInt x60, int x61) = Bits.add64(x54, arg1[3], 0);

  final (BigInt x62, int x63) = Bits.add64(x56, BigInt.zero, x61);

  final (BigInt x64, int x65) = Bits.add64(x58, BigInt.zero, x63);

  final (_, BigInt x66) = Bits.mul64(x60, '15183074304973897243'.toBigInt());

  final (BigInt x69, BigInt x68) =
      Bits.mul64(x66, '1152921504606846976'.toBigInt());

  final (BigInt x71, BigInt x70) =
      Bits.mul64(x66, '1503914060200516822'.toBigInt());

  final (BigInt x73, BigInt x72) =
      Bits.mul64(x66, '6346243789798364141'.toBigInt());

  final (BigInt x74, int x75) = Bits.add64(x73, x70, 0);

  final (_, int x77) = Bits.add64(x60, x72, 0);

  final (BigInt x78, int x79) = Bits.add64(x62, x74, x77);

  final (BigInt x80, int x81) = Bits.add64(x64, (x75.toBigInt + x71), x79);

  final (BigInt x82, int x83) =
      Bits.add64((x65.toBigInt + (x59.toBigInt + x45)), x68, x81);
  final x84 = (x83.toBigInt + x69);

  final (BigInt x85, int x86) =
      Bits.sub64(x78, '6346243789798364141'.toBigInt(), 0);

  final (BigInt x87, int x88) =
      Bits.sub64(x80, '1503914060200516822'.toBigInt(), x86);

  final (BigInt x89, int x90) = Bits.sub64(x82, BigInt.zero, x88);

  final (BigInt x91, int x92) =
      Bits.sub64(x84, '1152921504606846976'.toBigInt(), x90);

  final (_, int x94) = Bits.sub64(BigInt.zero, BigInt.zero, x92);

  final BigInt x95 = fiatScalarCmovznzU64(x94.toBigInt, x85, x78);

  final BigInt x96 = fiatScalarCmovznzU64(x94.toBigInt, x87, x80);

  final BigInt x97 = fiatScalarCmovznzU64(x94.toBigInt, x89, x82);

  final BigInt x98 = fiatScalarCmovznzU64(x94.toBigInt, x91, x84);

  out1[0] = x95;
  out1[1] = x96;
  out1[2] = x97;
  out1[3] = x98;
}