fiatScalarToMontgomery function
fiatScalarToMontgomery translates a field element into the Montgomery domain.
Preconditions: 0 ≤ eval arg1 < m Postconditions: eval (from_montgomery out1) mod m = eval arg1 mod m 0 ≤ eval out1 < m
Implementation
void fiatScalarToMontgomery(List<BigInt> out1, List<BigInt> arg1) {
final BigInt x1 = arg1[1];
final BigInt x2 = arg1[2];
final BigInt x3 = arg1[3];
final BigInt x4 = arg1[0];
final (BigInt x6, BigInt x5) =
Bits.mul64(x4, '259310039853996605'.toBigInt());
final (BigInt x8, BigInt x7) =
Bits.mul64(x4, '14910419812499177061'.toBigInt());
final (BigInt x10, BigInt x9) =
Bits.mul64(x4, '14991950615390032711'.toBigInt());
final (BigInt x12, BigInt x11) =
Bits.mul64(x4, '11819153939886771969'.toBigInt());
final (BigInt x13, int x14) = Bits.add64(x12, x9, 0);
final (BigInt x15, int x16) = Bits.add64(x10, x7, x14);
final (BigInt x17, int x18) = Bits.add64(x8, x5, x16);
final (_, BigInt x19) = Bits.mul64(x11, '15183074304973897243'.toBigInt());
final (BigInt x22, BigInt x21) =
Bits.mul64(x19, '1152921504606846976'.toBigInt());
final (BigInt x24, BigInt x23) =
Bits.mul64(x19, '1503914060200516822'.toBigInt());
final (BigInt x26, BigInt x25) =
Bits.mul64(x19, '6346243789798364141'.toBigInt());
final (BigInt x27, int x28) = Bits.add64(x26, x23, 0);
final (_, int x30) = Bits.add64(x11, x25, 0);
final (BigInt x31, int x32) = Bits.add64(x13, x27, x30);
final (BigInt x33, int x34) = Bits.add64(x15, (x28.toBigInt + x24), x32);
final (BigInt x35, int x36) = Bits.add64(x17, x21, x34);
final (BigInt x38, BigInt x37) =
Bits.mul64(x1, '259310039853996605'.toBigInt());
final (BigInt x40, BigInt x39) =
Bits.mul64(x1, '14910419812499177061'.toBigInt());
final (BigInt x42, BigInt x41) =
Bits.mul64(x1, '14991950615390032711'.toBigInt());
final (BigInt x44, BigInt x43) =
Bits.mul64(x1, '11819153939886771969'.toBigInt());
final (BigInt x45, int x46) = Bits.add64(x44, x41, 0);
final (BigInt x47, int x48) = Bits.add64(x42, x39, x46);
final (BigInt x49, int x50) = Bits.add64(x40, x37, x48);
final (BigInt x51, int x52) = Bits.add64(x31, x43, 0);
final (BigInt x53, int x54) = Bits.add64(x33, x45, x52);
final (BigInt x55, int x56) = Bits.add64(x35, x47, x54);
final (BigInt x57, int x58) =
Bits.add64(((x36.toBigInt + (x18.toBigInt + x6)) + x22), x49, x56);
final (_, BigInt x59) = Bits.mul64(x51, '15183074304973897243'.toBigInt());
final (BigInt x62, BigInt x61) =
Bits.mul64(x59, '1152921504606846976'.toBigInt());
final (BigInt x64, BigInt x63) =
Bits.mul64(x59, '1503914060200516822'.toBigInt());
final (BigInt x66, BigInt x65) =
Bits.mul64(x59, '6346243789798364141'.toBigInt());
final (BigInt x67, int x68) = Bits.add64(x66, x63, 0);
final (_, int x70) = Bits.add64(x51, x65, 0);
final (BigInt x71, int x72) = Bits.add64(x53, x67, x70);
final (BigInt x73, int x74) = Bits.add64(x55, (x68.toBigInt + x64), x72);
final (BigInt x75, int x76) = Bits.add64(x57, x61, x74);
final (BigInt x78, BigInt x77) =
Bits.mul64(x2, '259310039853996605'.toBigInt());
final (BigInt x80, BigInt x79) =
Bits.mul64(x2, '14910419812499177061'.toBigInt());
final (BigInt x82, BigInt x81) =
Bits.mul64(x2, '14991950615390032711'.toBigInt());
final (BigInt x84, BigInt x83) =
Bits.mul64(x2, '11819153939886771969'.toBigInt());
final (BigInt x85, int x86) = Bits.add64(x84, x81, 0);
final (BigInt x87, int x88) = Bits.add64(x82, x79, x86);
final (BigInt x89, int x90) = Bits.add64(x80, x77, x88);
final (BigInt x91, int x92) = Bits.add64(x71, x83, 0);
final (BigInt x93, int x94) = Bits.add64(x73, x85, x92);
final (BigInt x95, int x96) = Bits.add64(x75, x87, x94);
final (BigInt x97, int x98) = Bits.add64(
((x76.toBigInt + (x58.toBigInt + (x50.toBigInt + x38))) + x62), x89, x96);
final (_, BigInt x99) = Bits.mul64(x91, '15183074304973897243'.toBigInt());
final (BigInt x102, BigInt x101) =
Bits.mul64(x99, '1152921504606846976'.toBigInt());
final (BigInt x104, BigInt x103) =
Bits.mul64(x99, '1503914060200516822'.toBigInt());
final (BigInt x106, BigInt x105) =
Bits.mul64(x99, '6346243789798364141'.toBigInt());
final (BigInt x107, int x108) = Bits.add64(x106, x103, 0);
final (_, int x110) = Bits.add64(x91, x105, 0);
final (BigInt x111, int x112) = Bits.add64(x93, x107, x110);
final (BigInt x113, int x114) = Bits.add64(x95, (x108.toBigInt + x104), x112);
final (BigInt x115, int x116) = Bits.add64(x97, x101, x114);
final (BigInt x118, BigInt x117) =
Bits.mul64(x3, '259310039853996605'.toBigInt());
final (BigInt x120, BigInt x119) =
Bits.mul64(x3, '14910419812499177061'.toBigInt());
final (BigInt x122, BigInt x121) =
Bits.mul64(x3, '14991950615390032711'.toBigInt());
final (BigInt x124, BigInt x123) =
Bits.mul64(x3, '11819153939886771969'.toBigInt());
final (BigInt x125, int x126) = Bits.add64(x124, x121, 0);
final (BigInt x127, int x128) = Bits.add64(x122, x119, x126);
final (BigInt x129, int x130) = Bits.add64(x120, x117, x128);
final (BigInt x131, int x132) = Bits.add64(x111, x123, 0);
final (BigInt x133, int x134) = Bits.add64(x113, x125, x132);
final (BigInt x135, int x136) = Bits.add64(x115, x127, x134);
final (BigInt x137, int x138) = Bits.add64(
((x116.toBigInt + (x98.toBigInt + (x90.toBigInt + x78))) + x102),
x129,
x136);
final (_, BigInt x139) = Bits.mul64(x131, '15183074304973897243'.toBigInt());
final (BigInt x142, BigInt x141) =
Bits.mul64(x139, '1152921504606846976'.toBigInt());
final (BigInt x144, BigInt x143) =
Bits.mul64(x139, '1503914060200516822'.toBigInt());
final (BigInt x146, BigInt x145) =
Bits.mul64(x139, '6346243789798364141'.toBigInt());
final (BigInt x147, int x148) = Bits.add64(x146, x143, 0);
final (_, int x150) = Bits.add64(x131, x145, 0);
final (BigInt x151, int x152) = Bits.add64(x133, x147, x150);
final (BigInt x153, int x154) =
Bits.add64(x135, (x148.toBigInt + x144), x152);
final (BigInt x155, int x156) = Bits.add64(x137, x141, x154);
final x157 =
((x156.toBigInt + (x138.toBigInt + (x130.toBigInt + x118))) + x142);
final (BigInt x158, int x159) =
Bits.sub64(x151, '6346243789798364141'.toBigInt(), 0);
final (BigInt x160, int x161) =
Bits.sub64(x153, '1503914060200516822'.toBigInt(), x159);
final (BigInt x162, int x163) = Bits.sub64(x155, BigInt.zero, x161);
final (BigInt x164, int x165) =
Bits.sub64(x157, '1152921504606846976'.toBigInt(), x163);
final (_, int x167) = Bits.sub64(BigInt.zero, BigInt.zero, x165);
final BigInt x168 = fiatScalarCmovznzU64(x167.toBigInt, x158, x151);
final BigInt x169 = fiatScalarCmovznzU64(x167.toBigInt, x160, x153);
final BigInt x170 = fiatScalarCmovznzU64(x167.toBigInt, x162, x155);
final BigInt x171 = fiatScalarCmovznzU64(x167.toBigInt, x164, x157);
out1[0] = x168;
out1[1] = x169;
out1[2] = x170;
out1[3] = x171;
}