fiatScalarMul function
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
Implementation
void fiatScalarMul(List<BigInt> out1, List<BigInt> arg1, List<BigInt> arg2) {
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, arg2[3]);
final (BigInt x8, BigInt x7) = Bits.mul64(x4, arg2[2]);
final (BigInt x10, BigInt x9) = Bits.mul64(x4, arg2[1]);
final (BigInt x12, BigInt x11) = Bits.mul64(x4, arg2[0]);
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 = (x18.toBigInt + x6);
final (_, BigInt x20) = Bits.mul64(x11, '15183074304973897243'.toBigInt());
final (BigInt x23, BigInt x22) =
Bits.mul64(x20, '1152921504606846976'.toBigInt());
final (BigInt x25, BigInt x24) =
Bits.mul64(x20, '1503914060200516822'.toBigInt());
final (BigInt x27, BigInt x26) =
Bits.mul64(x20, '6346243789798364141'.toBigInt());
final (BigInt x28, int x29) = Bits.add64(x27, x24, 0);
final BigInt x30 = (x29.toBigInt + x25);
final (_, int x32) = Bits.add64(x11, x26, 0);
final (BigInt x33, int x34) = Bits.add64(x13, x28, x32);
final (BigInt x35, int x36) = Bits.add64(x15, x30, x34);
final (BigInt x37, int x38) = Bits.add64(x17, x22, x36);
final (BigInt x39, int x40) = Bits.add64(x19, x23, x38);
final (BigInt x42, BigInt x41) = Bits.mul64(x1, arg2[3]);
final (BigInt x44, BigInt x43) = Bits.mul64(x1, arg2[2]);
final (BigInt x46, BigInt x45) = Bits.mul64(x1, arg2[1]);
final (BigInt x48, BigInt x47) = Bits.mul64(x1, arg2[0]);
final (BigInt x49, int x50) = Bits.add64(x48, x45, 0);
final (BigInt x51, int x52) = Bits.add64(x46, x43, x50);
final (BigInt x53, int x54) = Bits.add64(x44, x41, x52);
final x55 = (x54.toBigInt + x42);
final (BigInt x56, int x57) = Bits.add64(x33, x47, 0);
final (BigInt x58, int x59) = Bits.add64(x35, x49, x57);
final (BigInt x60, int x61) = Bits.add64(x37, x51, x59);
final (BigInt x62, int x63) = Bits.add64(x39, x53, x61);
final (BigInt x64, int x65) = Bits.add64(x40.toBigInt, x55, x63);
final (_, BigInt x66) = Bits.mul64(x56, '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 x76 = (x75.toBigInt + x71);
final (_, int x78) = Bits.add64(x56, x72, 0);
final (BigInt x79, int x80) = Bits.add64(x58, x74, x78);
final (BigInt x81, int x82) = Bits.add64(x60, x76, x80);
final (BigInt x83, int x84) = Bits.add64(x62, x68, x82);
final (BigInt x85, int x86) = Bits.add64(x64, x69, x84);
final x87 = (x86.toBigInt + x65.toBigInt);
final (BigInt x89, BigInt x88) = Bits.mul64(x2, arg2[3]);
final (BigInt x91, BigInt x90) = Bits.mul64(x2, arg2[2]);
final (BigInt x93, BigInt x92) = Bits.mul64(x2, arg2[1]);
final (BigInt x95, BigInt x94) = Bits.mul64(x2, arg2[0]);
final (BigInt x96, int x97) = Bits.add64(x95, x92, 0);
final (BigInt x98, int x99) = Bits.add64(x93, x90, x97);
final (BigInt x100, int x101) = Bits.add64(x91, x88, x99);
final x102 = (x101.toBigInt + x89);
final (BigInt x103, int x104) = Bits.add64(x79, x94, 0);
final (BigInt x105, int x106) = Bits.add64(x81, x96, x104);
final (BigInt x107, int x108) = Bits.add64(x83, x98, x106);
final (BigInt x109, int x110) = Bits.add64(x85, x100, x108);
final (BigInt x111, int x112) = Bits.add64(x87, x102, x110);
final (_, BigInt x113) = Bits.mul64(x103, '15183074304973897243'.toBigInt());
final (BigInt x116, BigInt x115) =
Bits.mul64(x113, '1152921504606846976'.toBigInt());
final (BigInt x118, BigInt x117) =
Bits.mul64(x113, '1503914060200516822'.toBigInt());
final (BigInt x120, BigInt x119) =
Bits.mul64(x113, '6346243789798364141'.toBigInt());
final (BigInt x121, int x122) = Bits.add64(x120, x117, 0);
final x123 = (x122.toBigInt + x118);
final (_, int x125) = Bits.add64(x103, x119, 0);
final (BigInt x126, int x127) = Bits.add64(x105, x121, x125);
final (BigInt x128, int x129) = Bits.add64(x107, x123, x127);
final (BigInt x130, int x131) = Bits.add64(x109, x115, x129);
final (BigInt x132, int x133) = Bits.add64(x111, x116, x131);
final x134 = (x133 + x112);
final (BigInt x136, BigInt x135) = Bits.mul64(x3, arg2[3]);
final (BigInt x138, BigInt x137) = Bits.mul64(x3, arg2[2]);
final (BigInt x140, BigInt x139) = Bits.mul64(x3, arg2[1]);
final (BigInt x142, BigInt x141) = Bits.mul64(x3, arg2[0]);
final (BigInt x143, int x144) = Bits.add64(x142, x139, 0);
final (BigInt x145, int x146) = Bits.add64(x140, x137, x144);
final (BigInt x147, int x148) = Bits.add64(x138, x135, x146);
final x149 = (x148.toBigInt + x136);
final (BigInt x150, int x151) = Bits.add64(x126, x141, 0);
final (BigInt x152, int x153) = Bits.add64(x128, x143, x151);
final (BigInt x154, int x155) = Bits.add64(x130, x145, x153);
final (BigInt x156, int x157) = Bits.add64(x132, x147, x155);
final (BigInt x158, int x159) = Bits.add64(x134.toBigInt, x149, x157);
final (_, BigInt x160) = Bits.mul64(x150, '15183074304973897243'.toBigInt());
final (BigInt x163, BigInt x162) =
Bits.mul64(x160, '1152921504606846976'.toBigInt());
final (BigInt x165, BigInt x164) =
Bits.mul64(x160, '1503914060200516822'.toBigInt());
final (BigInt x167, BigInt x166) =
Bits.mul64(x160, '6346243789798364141'.toBigInt());
final (BigInt x168, int x169) = Bits.add64(x167, x164, 0);
final x170 = (x169.toBigInt + x165);
final (_, int x172) = Bits.add64(x150, x166, 0);
final (BigInt x173, int x174) = Bits.add64(x152, x168, x172);
final (BigInt x175, int x176) = Bits.add64(x154, x170, x174);
final (BigInt x177, int x178) = Bits.add64(x156, x162, x176);
final (BigInt x179, int x180) = Bits.add64(x158, x163, x178);
final x181 = (x180 + x159);
final (BigInt x182, int x183) =
Bits.sub64(x173, '6346243789798364141'.toBigInt(), 0);
final (BigInt x184, int x185) =
Bits.sub64(x175, '1503914060200516822'.toBigInt(), x183);
final (BigInt x186, int x187) = Bits.sub64(x177, BigInt.zero, x185);
final (BigInt x188, int x189) =
Bits.sub64(x179, '1152921504606846976'.toBigInt(), x187);
final (_, int x191) = Bits.sub64(x181.toBigInt, BigInt.zero, x189);
final BigInt x192 = fiatScalarCmovznzU64(x191.toBigInt, x182, x173);
final BigInt x193 = fiatScalarCmovznzU64(x191.toBigInt, x184, x175);
final BigInt x194 = fiatScalarCmovznzU64(x191.toBigInt, x186, x177);
final BigInt x195 = fiatScalarCmovznzU64(x191.toBigInt, x188, x179);
out1[0] = x192;
out1[1] = x193;
out1[2] = x194;
out1[3] = x195;
}