The function mul 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
pub fn mul(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) voidpub fn mul(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .debug);
const x1 = (arg1[1]);
const x2 = (arg1[2]);
const x3 = (arg1[3]);
const x4 = (arg1[4]);
const x5 = (arg1[5]);
const x6 = (arg1[0]);
var x7: u64 = undefined;
var x8: u64 = undefined;
mulxU64(&x7, &x8, x6, (arg2[5]));
var x9: u64 = undefined;
var x10: u64 = undefined;
mulxU64(&x9, &x10, x6, (arg2[4]));
var x11: u64 = undefined;
var x12: u64 = undefined;
mulxU64(&x11, &x12, x6, (arg2[3]));
var x13: u64 = undefined;
var x14: u64 = undefined;
mulxU64(&x13, &x14, x6, (arg2[2]));
var x15: u64 = undefined;
var x16: u64 = undefined;
mulxU64(&x15, &x16, x6, (arg2[1]));
var x17: u64 = undefined;
var x18: u64 = undefined;
mulxU64(&x17, &x18, x6, (arg2[0]));
var x19: u64 = undefined;
var x20: u1 = undefined;
addcarryxU64(&x19, &x20, 0x0, x18, x15);
var x21: u64 = undefined;
var x22: u1 = undefined;
addcarryxU64(&x21, &x22, x20, x16, x13);
var x23: u64 = undefined;
var x24: u1 = undefined;
addcarryxU64(&x23, &x24, x22, x14, x11);
var x25: u64 = undefined;
var x26: u1 = undefined;
addcarryxU64(&x25, &x26, x24, x12, x9);
var x27: u64 = undefined;
var x28: u1 = undefined;
addcarryxU64(&x27, &x28, x26, x10, x7);
const x29 = (@as(u64, x28) + x8);
var x30: u64 = undefined;
var x31: u64 = undefined;
mulxU64(&x30, &x31, x17, 0x6ed46089e88fdc45);
var x32: u64 = undefined;
var x33: u64 = undefined;
mulxU64(&x32, &x33, x30, 0xffffffffffffffff);
var x34: u64 = undefined;
var x35: u64 = undefined;
mulxU64(&x34, &x35, x30, 0xffffffffffffffff);
var x36: u64 = undefined;
var x37: u64 = undefined;
mulxU64(&x36, &x37, x30, 0xffffffffffffffff);
var x38: u64 = undefined;
var x39: u64 = undefined;
mulxU64(&x38, &x39, x30, 0xc7634d81f4372ddf);
var x40: u64 = undefined;
var x41: u64 = undefined;
mulxU64(&x40, &x41, x30, 0x581a0db248b0a77a);
var x42: u64 = undefined;
var x43: u64 = undefined;
mulxU64(&x42, &x43, x30, 0xecec196accc52973);
var x44: u64 = undefined;
var x45: u1 = undefined;
addcarryxU64(&x44, &x45, 0x0, x43, x40);
var x46: u64 = undefined;
var x47: u1 = undefined;
addcarryxU64(&x46, &x47, x45, x41, x38);
var x48: u64 = undefined;
var x49: u1 = undefined;
addcarryxU64(&x48, &x49, x47, x39, x36);
var x50: u64 = undefined;
var x51: u1 = undefined;
addcarryxU64(&x50, &x51, x49, x37, x34);
var x52: u64 = undefined;
var x53: u1 = undefined;
addcarryxU64(&x52, &x53, x51, x35, x32);
const x54 = (@as(u64, x53) + x33);
var x55: u64 = undefined;
var x56: u1 = undefined;
addcarryxU64(&x55, &x56, 0x0, x17, x42);
var x57: u64 = undefined;
var x58: u1 = undefined;
addcarryxU64(&x57, &x58, x56, x19, x44);
var x59: u64 = undefined;
var x60: u1 = undefined;
addcarryxU64(&x59, &x60, x58, x21, x46);
var x61: u64 = undefined;
var x62: u1 = undefined;
addcarryxU64(&x61, &x62, x60, x23, x48);
var x63: u64 = undefined;
var x64: u1 = undefined;
addcarryxU64(&x63, &x64, x62, x25, x50);
var x65: u64 = undefined;
var x66: u1 = undefined;
addcarryxU64(&x65, &x66, x64, x27, x52);
var x67: u64 = undefined;
var x68: u1 = undefined;
addcarryxU64(&x67, &x68, x66, x29, x54);
var x69: u64 = undefined;
var x70: u64 = undefined;
mulxU64(&x69, &x70, x1, (arg2[5]));
var x71: u64 = undefined;
var x72: u64 = undefined;
mulxU64(&x71, &x72, x1, (arg2[4]));
var x73: u64 = undefined;
var x74: u64 = undefined;
mulxU64(&x73, &x74, x1, (arg2[3]));
var x75: u64 = undefined;
var x76: u64 = undefined;
mulxU64(&x75, &x76, x1, (arg2[2]));
var x77: u64 = undefined;
var x78: u64 = undefined;
mulxU64(&x77, &x78, x1, (arg2[1]));
var x79: u64 = undefined;
var x80: u64 = undefined;
mulxU64(&x79, &x80, x1, (arg2[0]));
var x81: u64 = undefined;
var x82: u1 = undefined;
addcarryxU64(&x81, &x82, 0x0, x80, x77);
var x83: u64 = undefined;
var x84: u1 = undefined;
addcarryxU64(&x83, &x84, x82, x78, x75);
var x85: u64 = undefined;
var x86: u1 = undefined;
addcarryxU64(&x85, &x86, x84, x76, x73);
var x87: u64 = undefined;
var x88: u1 = undefined;
addcarryxU64(&x87, &x88, x86, x74, x71);
var x89: u64 = undefined;
var x90: u1 = undefined;
addcarryxU64(&x89, &x90, x88, x72, x69);
const x91 = (@as(u64, x90) + x70);
var x92: u64 = undefined;
var x93: u1 = undefined;
addcarryxU64(&x92, &x93, 0x0, x57, x79);
var x94: u64 = undefined;
var x95: u1 = undefined;
addcarryxU64(&x94, &x95, x93, x59, x81);
var x96: u64 = undefined;
var x97: u1 = undefined;
addcarryxU64(&x96, &x97, x95, x61, x83);
var x98: u64 = undefined;
var x99: u1 = undefined;
addcarryxU64(&x98, &x99, x97, x63, x85);
var x100: u64 = undefined;
var x101: u1 = undefined;
addcarryxU64(&x100, &x101, x99, x65, x87);
var x102: u64 = undefined;
var x103: u1 = undefined;
addcarryxU64(&x102, &x103, x101, x67, x89);
var x104: u64 = undefined;
var x105: u1 = undefined;
addcarryxU64(&x104, &x105, x103, @as(u64, x68), x91);
var x106: u64 = undefined;
var x107: u64 = undefined;
mulxU64(&x106, &x107, x92, 0x6ed46089e88fdc45);
var x108: u64 = undefined;
var x109: u64 = undefined;
mulxU64(&x108, &x109, x106, 0xffffffffffffffff);
var x110: u64 = undefined;
var x111: u64 = undefined;
mulxU64(&x110, &x111, x106, 0xffffffffffffffff);
var x112: u64 = undefined;
var x113: u64 = undefined;
mulxU64(&x112, &x113, x106, 0xffffffffffffffff);
var x114: u64 = undefined;
var x115: u64 = undefined;
mulxU64(&x114, &x115, x106, 0xc7634d81f4372ddf);
var x116: u64 = undefined;
var x117: u64 = undefined;
mulxU64(&x116, &x117, x106, 0x581a0db248b0a77a);
var x118: u64 = undefined;
var x119: u64 = undefined;
mulxU64(&x118, &x119, x106, 0xecec196accc52973);
var x120: u64 = undefined;
var x121: u1 = undefined;
addcarryxU64(&x120, &x121, 0x0, x119, x116);
var x122: u64 = undefined;
var x123: u1 = undefined;
addcarryxU64(&x122, &x123, x121, x117, x114);
var x124: u64 = undefined;
var x125: u1 = undefined;
addcarryxU64(&x124, &x125, x123, x115, x112);
var x126: u64 = undefined;
var x127: u1 = undefined;
addcarryxU64(&x126, &x127, x125, x113, x110);
var x128: u64 = undefined;
var x129: u1 = undefined;
addcarryxU64(&x128, &x129, x127, x111, x108);
const x130 = (@as(u64, x129) + x109);
var x131: u64 = undefined;
var x132: u1 = undefined;
addcarryxU64(&x131, &x132, 0x0, x92, x118);
var x133: u64 = undefined;
var x134: u1 = undefined;
addcarryxU64(&x133, &x134, x132, x94, x120);
var x135: u64 = undefined;
var x136: u1 = undefined;
addcarryxU64(&x135, &x136, x134, x96, x122);
var x137: u64 = undefined;
var x138: u1 = undefined;
addcarryxU64(&x137, &x138, x136, x98, x124);
var x139: u64 = undefined;
var x140: u1 = undefined;
addcarryxU64(&x139, &x140, x138, x100, x126);
var x141: u64 = undefined;
var x142: u1 = undefined;
addcarryxU64(&x141, &x142, x140, x102, x128);
var x143: u64 = undefined;
var x144: u1 = undefined;
addcarryxU64(&x143, &x144, x142, x104, x130);
const x145 = (@as(u64, x144) + @as(u64, x105));
var x146: u64 = undefined;
var x147: u64 = undefined;
mulxU64(&x146, &x147, x2, (arg2[5]));
var x148: u64 = undefined;
var x149: u64 = undefined;
mulxU64(&x148, &x149, x2, (arg2[4]));
var x150: u64 = undefined;
var x151: u64 = undefined;
mulxU64(&x150, &x151, x2, (arg2[3]));
var x152: u64 = undefined;
var x153: u64 = undefined;
mulxU64(&x152, &x153, x2, (arg2[2]));
var x154: u64 = undefined;
var x155: u64 = undefined;
mulxU64(&x154, &x155, x2, (arg2[1]));
var x156: u64 = undefined;
var x157: u64 = undefined;
mulxU64(&x156, &x157, x2, (arg2[0]));
var x158: u64 = undefined;
var x159: u1 = undefined;
addcarryxU64(&x158, &x159, 0x0, x157, x154);
var x160: u64 = undefined;
var x161: u1 = undefined;
addcarryxU64(&x160, &x161, x159, x155, x152);
var x162: u64 = undefined;
var x163: u1 = undefined;
addcarryxU64(&x162, &x163, x161, x153, x150);
var x164: u64 = undefined;
var x165: u1 = undefined;
addcarryxU64(&x164, &x165, x163, x151, x148);
var x166: u64 = undefined;
var x167: u1 = undefined;
addcarryxU64(&x166, &x167, x165, x149, x146);
const x168 = (@as(u64, x167) + x147);
var x169: u64 = undefined;
var x170: u1 = undefined;
addcarryxU64(&x169, &x170, 0x0, x133, x156);
var x171: u64 = undefined;
var x172: u1 = undefined;
addcarryxU64(&x171, &x172, x170, x135, x158);
var x173: u64 = undefined;
var x174: u1 = undefined;
addcarryxU64(&x173, &x174, x172, x137, x160);
var x175: u64 = undefined;
var x176: u1 = undefined;
addcarryxU64(&x175, &x176, x174, x139, x162);
var x177: u64 = undefined;
var x178: u1 = undefined;
addcarryxU64(&x177, &x178, x176, x141, x164);
var x179: u64 = undefined;
var x180: u1 = undefined;
addcarryxU64(&x179, &x180, x178, x143, x166);
var x181: u64 = undefined;
var x182: u1 = undefined;
addcarryxU64(&x181, &x182, x180, x145, x168);
var x183: u64 = undefined;
var x184: u64 = undefined;
mulxU64(&x183, &x184, x169, 0x6ed46089e88fdc45);
var x185: u64 = undefined;
var x186: u64 = undefined;
mulxU64(&x185, &x186, x183, 0xffffffffffffffff);
var x187: u64 = undefined;
var x188: u64 = undefined;
mulxU64(&x187, &x188, x183, 0xffffffffffffffff);
var x189: u64 = undefined;
var x190: u64 = undefined;
mulxU64(&x189, &x190, x183, 0xffffffffffffffff);
var x191: u64 = undefined;
var x192: u64 = undefined;
mulxU64(&x191, &x192, x183, 0xc7634d81f4372ddf);
var x193: u64 = undefined;
var x194: u64 = undefined;
mulxU64(&x193, &x194, x183, 0x581a0db248b0a77a);
var x195: u64 = undefined;
var x196: u64 = undefined;
mulxU64(&x195, &x196, x183, 0xecec196accc52973);
var x197: u64 = undefined;
var x198: u1 = undefined;
addcarryxU64(&x197, &x198, 0x0, x196, x193);
var x199: u64 = undefined;
var x200: u1 = undefined;
addcarryxU64(&x199, &x200, x198, x194, x191);
var x201: u64 = undefined;
var x202: u1 = undefined;
addcarryxU64(&x201, &x202, x200, x192, x189);
var x203: u64 = undefined;
var x204: u1 = undefined;
addcarryxU64(&x203, &x204, x202, x190, x187);
var x205: u64 = undefined;
var x206: u1 = undefined;
addcarryxU64(&x205, &x206, x204, x188, x185);
const x207 = (@as(u64, x206) + x186);
var x208: u64 = undefined;
var x209: u1 = undefined;
addcarryxU64(&x208, &x209, 0x0, x169, x195);
var x210: u64 = undefined;
var x211: u1 = undefined;
addcarryxU64(&x210, &x211, x209, x171, x197);
var x212: u64 = undefined;
var x213: u1 = undefined;
addcarryxU64(&x212, &x213, x211, x173, x199);
var x214: u64 = undefined;
var x215: u1 = undefined;
addcarryxU64(&x214, &x215, x213, x175, x201);
var x216: u64 = undefined;
var x217: u1 = undefined;
addcarryxU64(&x216, &x217, x215, x177, x203);
var x218: u64 = undefined;
var x219: u1 = undefined;
addcarryxU64(&x218, &x219, x217, x179, x205);
var x220: u64 = undefined;
var x221: u1 = undefined;
addcarryxU64(&x220, &x221, x219, x181, x207);
const x222 = (@as(u64, x221) + @as(u64, x182));
var x223: u64 = undefined;
var x224: u64 = undefined;
mulxU64(&x223, &x224, x3, (arg2[5]));
var x225: u64 = undefined;
var x226: u64 = undefined;
mulxU64(&x225, &x226, x3, (arg2[4]));
var x227: u64 = undefined;
var x228: u64 = undefined;
mulxU64(&x227, &x228, x3, (arg2[3]));
var x229: u64 = undefined;
var x230: u64 = undefined;
mulxU64(&x229, &x230, x3, (arg2[2]));
var x231: u64 = undefined;
var x232: u64 = undefined;
mulxU64(&x231, &x232, x3, (arg2[1]));
var x233: u64 = undefined;
var x234: u64 = undefined;
mulxU64(&x233, &x234, x3, (arg2[0]));
var x235: u64 = undefined;
var x236: u1 = undefined;
addcarryxU64(&x235, &x236, 0x0, x234, x231);
var x237: u64 = undefined;
var x238: u1 = undefined;
addcarryxU64(&x237, &x238, x236, x232, x229);
var x239: u64 = undefined;
var x240: u1 = undefined;
addcarryxU64(&x239, &x240, x238, x230, x227);
var x241: u64 = undefined;
var x242: u1 = undefined;
addcarryxU64(&x241, &x242, x240, x228, x225);
var x243: u64 = undefined;
var x244: u1 = undefined;
addcarryxU64(&x243, &x244, x242, x226, x223);
const x245 = (@as(u64, x244) + x224);
var x246: u64 = undefined;
var x247: u1 = undefined;
addcarryxU64(&x246, &x247, 0x0, x210, x233);
var x248: u64 = undefined;
var x249: u1 = undefined;
addcarryxU64(&x248, &x249, x247, x212, x235);
var x250: u64 = undefined;
var x251: u1 = undefined;
addcarryxU64(&x250, &x251, x249, x214, x237);
var x252: u64 = undefined;
var x253: u1 = undefined;
addcarryxU64(&x252, &x253, x251, x216, x239);
var x254: u64 = undefined;
var x255: u1 = undefined;
addcarryxU64(&x254, &x255, x253, x218, x241);
var x256: u64 = undefined;
var x257: u1 = undefined;
addcarryxU64(&x256, &x257, x255, x220, x243);
var x258: u64 = undefined;
var x259: u1 = undefined;
addcarryxU64(&x258, &x259, x257, x222, x245);
var x260: u64 = undefined;
var x261: u64 = undefined;
mulxU64(&x260, &x261, x246, 0x6ed46089e88fdc45);
var x262: u64 = undefined;
var x263: u64 = undefined;
mulxU64(&x262, &x263, x260, 0xffffffffffffffff);
var x264: u64 = undefined;
var x265: u64 = undefined;
mulxU64(&x264, &x265, x260, 0xffffffffffffffff);
var x266: u64 = undefined;
var x267: u64 = undefined;
mulxU64(&x266, &x267, x260, 0xffffffffffffffff);
var x268: u64 = undefined;
var x269: u64 = undefined;
mulxU64(&x268, &x269, x260, 0xc7634d81f4372ddf);
var x270: u64 = undefined;
var x271: u64 = undefined;
mulxU64(&x270, &x271, x260, 0x581a0db248b0a77a);
var x272: u64 = undefined;
var x273: u64 = undefined;
mulxU64(&x272, &x273, x260, 0xecec196accc52973);
var x274: u64 = undefined;
var x275: u1 = undefined;
addcarryxU64(&x274, &x275, 0x0, x273, x270);
var x276: u64 = undefined;
var x277: u1 = undefined;
addcarryxU64(&x276, &x277, x275, x271, x268);
var x278: u64 = undefined;
var x279: u1 = undefined;
addcarryxU64(&x278, &x279, x277, x269, x266);
var x280: u64 = undefined;
var x281: u1 = undefined;
addcarryxU64(&x280, &x281, x279, x267, x264);
var x282: u64 = undefined;
var x283: u1 = undefined;
addcarryxU64(&x282, &x283, x281, x265, x262);
const x284 = (@as(u64, x283) + x263);
var x285: u64 = undefined;
var x286: u1 = undefined;
addcarryxU64(&x285, &x286, 0x0, x246, x272);
var x287: u64 = undefined;
var x288: u1 = undefined;
addcarryxU64(&x287, &x288, x286, x248, x274);
var x289: u64 = undefined;
var x290: u1 = undefined;
addcarryxU64(&x289, &x290, x288, x250, x276);
var x291: u64 = undefined;
var x292: u1 = undefined;
addcarryxU64(&x291, &x292, x290, x252, x278);
var x293: u64 = undefined;
var x294: u1 = undefined;
addcarryxU64(&x293, &x294, x292, x254, x280);
var x295: u64 = undefined;
var x296: u1 = undefined;
addcarryxU64(&x295, &x296, x294, x256, x282);
var x297: u64 = undefined;
var x298: u1 = undefined;
addcarryxU64(&x297, &x298, x296, x258, x284);
const x299 = (@as(u64, x298) + @as(u64, x259));
var x300: u64 = undefined;
var x301: u64 = undefined;
mulxU64(&x300, &x301, x4, (arg2[5]));
var x302: u64 = undefined;
var x303: u64 = undefined;
mulxU64(&x302, &x303, x4, (arg2[4]));
var x304: u64 = undefined;
var x305: u64 = undefined;
mulxU64(&x304, &x305, x4, (arg2[3]));
var x306: u64 = undefined;
var x307: u64 = undefined;
mulxU64(&x306, &x307, x4, (arg2[2]));
var x308: u64 = undefined;
var x309: u64 = undefined;
mulxU64(&x308, &x309, x4, (arg2[1]));
var x310: u64 = undefined;
var x311: u64 = undefined;
mulxU64(&x310, &x311, x4, (arg2[0]));
var x312: u64 = undefined;
var x313: u1 = undefined;
addcarryxU64(&x312, &x313, 0x0, x311, x308);
var x314: u64 = undefined;
var x315: u1 = undefined;
addcarryxU64(&x314, &x315, x313, x309, x306);
var x316: u64 = undefined;
var x317: u1 = undefined;
addcarryxU64(&x316, &x317, x315, x307, x304);
var x318: u64 = undefined;
var x319: u1 = undefined;
addcarryxU64(&x318, &x319, x317, x305, x302);
var x320: u64 = undefined;
var x321: u1 = undefined;
addcarryxU64(&x320, &x321, x319, x303, x300);
const x322 = (@as(u64, x321) + x301);
var x323: u64 = undefined;
var x324: u1 = undefined;
addcarryxU64(&x323, &x324, 0x0, x287, x310);
var x325: u64 = undefined;
var x326: u1 = undefined;
addcarryxU64(&x325, &x326, x324, x289, x312);
var x327: u64 = undefined;
var x328: u1 = undefined;
addcarryxU64(&x327, &x328, x326, x291, x314);
var x329: u64 = undefined;
var x330: u1 = undefined;
addcarryxU64(&x329, &x330, x328, x293, x316);
var x331: u64 = undefined;
var x332: u1 = undefined;
addcarryxU64(&x331, &x332, x330, x295, x318);
var x333: u64 = undefined;
var x334: u1 = undefined;
addcarryxU64(&x333, &x334, x332, x297, x320);
var x335: u64 = undefined;
var x336: u1 = undefined;
addcarryxU64(&x335, &x336, x334, x299, x322);
var x337: u64 = undefined;
var x338: u64 = undefined;
mulxU64(&x337, &x338, x323, 0x6ed46089e88fdc45);
var x339: u64 = undefined;
var x340: u64 = undefined;
mulxU64(&x339, &x340, x337, 0xffffffffffffffff);
var x341: u64 = undefined;
var x342: u64 = undefined;
mulxU64(&x341, &x342, x337, 0xffffffffffffffff);
var x343: u64 = undefined;
var x344: u64 = undefined;
mulxU64(&x343, &x344, x337, 0xffffffffffffffff);
var x345: u64 = undefined;
var x346: u64 = undefined;
mulxU64(&x345, &x346, x337, 0xc7634d81f4372ddf);
var x347: u64 = undefined;
var x348: u64 = undefined;
mulxU64(&x347, &x348, x337, 0x581a0db248b0a77a);
var x349: u64 = undefined;
var x350: u64 = undefined;
mulxU64(&x349, &x350, x337, 0xecec196accc52973);
var x351: u64 = undefined;
var x352: u1 = undefined;
addcarryxU64(&x351, &x352, 0x0, x350, x347);
var x353: u64 = undefined;
var x354: u1 = undefined;
addcarryxU64(&x353, &x354, x352, x348, x345);
var x355: u64 = undefined;
var x356: u1 = undefined;
addcarryxU64(&x355, &x356, x354, x346, x343);
var x357: u64 = undefined;
var x358: u1 = undefined;
addcarryxU64(&x357, &x358, x356, x344, x341);
var x359: u64 = undefined;
var x360: u1 = undefined;
addcarryxU64(&x359, &x360, x358, x342, x339);
const x361 = (@as(u64, x360) + x340);
var x362: u64 = undefined;
var x363: u1 = undefined;
addcarryxU64(&x362, &x363, 0x0, x323, x349);
var x364: u64 = undefined;
var x365: u1 = undefined;
addcarryxU64(&x364, &x365, x363, x325, x351);
var x366: u64 = undefined;
var x367: u1 = undefined;
addcarryxU64(&x366, &x367, x365, x327, x353);
var x368: u64 = undefined;
var x369: u1 = undefined;
addcarryxU64(&x368, &x369, x367, x329, x355);
var x370: u64 = undefined;
var x371: u1 = undefined;
addcarryxU64(&x370, &x371, x369, x331, x357);
var x372: u64 = undefined;
var x373: u1 = undefined;
addcarryxU64(&x372, &x373, x371, x333, x359);
var x374: u64 = undefined;
var x375: u1 = undefined;
addcarryxU64(&x374, &x375, x373, x335, x361);
const x376 = (@as(u64, x375) + @as(u64, x336));
var x377: u64 = undefined;
var x378: u64 = undefined;
mulxU64(&x377, &x378, x5, (arg2[5]));
var x379: u64 = undefined;
var x380: u64 = undefined;
mulxU64(&x379, &x380, x5, (arg2[4]));
var x381: u64 = undefined;
var x382: u64 = undefined;
mulxU64(&x381, &x382, x5, (arg2[3]));
var x383: u64 = undefined;
var x384: u64 = undefined;
mulxU64(&x383, &x384, x5, (arg2[2]));
var x385: u64 = undefined;
var x386: u64 = undefined;
mulxU64(&x385, &x386, x5, (arg2[1]));
var x387: u64 = undefined;
var x388: u64 = undefined;
mulxU64(&x387, &x388, x5, (arg2[0]));
var x389: u64 = undefined;
var x390: u1 = undefined;
addcarryxU64(&x389, &x390, 0x0, x388, x385);
var x391: u64 = undefined;
var x392: u1 = undefined;
addcarryxU64(&x391, &x392, x390, x386, x383);
var x393: u64 = undefined;
var x394: u1 = undefined;
addcarryxU64(&x393, &x394, x392, x384, x381);
var x395: u64 = undefined;
var x396: u1 = undefined;
addcarryxU64(&x395, &x396, x394, x382, x379);
var x397: u64 = undefined;
var x398: u1 = undefined;
addcarryxU64(&x397, &x398, x396, x380, x377);
const x399 = (@as(u64, x398) + x378);
var x400: u64 = undefined;
var x401: u1 = undefined;
addcarryxU64(&x400, &x401, 0x0, x364, x387);
var x402: u64 = undefined;
var x403: u1 = undefined;
addcarryxU64(&x402, &x403, x401, x366, x389);
var x404: u64 = undefined;
var x405: u1 = undefined;
addcarryxU64(&x404, &x405, x403, x368, x391);
var x406: u64 = undefined;
var x407: u1 = undefined;
addcarryxU64(&x406, &x407, x405, x370, x393);
var x408: u64 = undefined;
var x409: u1 = undefined;
addcarryxU64(&x408, &x409, x407, x372, x395);
var x410: u64 = undefined;
var x411: u1 = undefined;
addcarryxU64(&x410, &x411, x409, x374, x397);
var x412: u64 = undefined;
var x413: u1 = undefined;
addcarryxU64(&x412, &x413, x411, x376, x399);
var x414: u64 = undefined;
var x415: u64 = undefined;
mulxU64(&x414, &x415, x400, 0x6ed46089e88fdc45);
var x416: u64 = undefined;
var x417: u64 = undefined;
mulxU64(&x416, &x417, x414, 0xffffffffffffffff);
var x418: u64 = undefined;
var x419: u64 = undefined;
mulxU64(&x418, &x419, x414, 0xffffffffffffffff);
var x420: u64 = undefined;
var x421: u64 = undefined;
mulxU64(&x420, &x421, x414, 0xffffffffffffffff);
var x422: u64 = undefined;
var x423: u64 = undefined;
mulxU64(&x422, &x423, x414, 0xc7634d81f4372ddf);
var x424: u64 = undefined;
var x425: u64 = undefined;
mulxU64(&x424, &x425, x414, 0x581a0db248b0a77a);
var x426: u64 = undefined;
var x427: u64 = undefined;
mulxU64(&x426, &x427, x414, 0xecec196accc52973);
var x428: u64 = undefined;
var x429: u1 = undefined;
addcarryxU64(&x428, &x429, 0x0, x427, x424);
var x430: u64 = undefined;
var x431: u1 = undefined;
addcarryxU64(&x430, &x431, x429, x425, x422);
var x432: u64 = undefined;
var x433: u1 = undefined;
addcarryxU64(&x432, &x433, x431, x423, x420);
var x434: u64 = undefined;
var x435: u1 = undefined;
addcarryxU64(&x434, &x435, x433, x421, x418);
var x436: u64 = undefined;
var x437: u1 = undefined;
addcarryxU64(&x436, &x437, x435, x419, x416);
const x438 = (@as(u64, x437) + x417);
var x439: u64 = undefined;
var x440: u1 = undefined;
addcarryxU64(&x439, &x440, 0x0, x400, x426);
var x441: u64 = undefined;
var x442: u1 = undefined;
addcarryxU64(&x441, &x442, x440, x402, x428);
var x443: u64 = undefined;
var x444: u1 = undefined;
addcarryxU64(&x443, &x444, x442, x404, x430);
var x445: u64 = undefined;
var x446: u1 = undefined;
addcarryxU64(&x445, &x446, x444, x406, x432);
var x447: u64 = undefined;
var x448: u1 = undefined;
addcarryxU64(&x447, &x448, x446, x408, x434);
var x449: u64 = undefined;
var x450: u1 = undefined;
addcarryxU64(&x449, &x450, x448, x410, x436);
var x451: u64 = undefined;
var x452: u1 = undefined;
addcarryxU64(&x451, &x452, x450, x412, x438);
const x453 = (@as(u64, x452) + @as(u64, x413));
var x454: u64 = undefined;
var x455: u1 = undefined;
subborrowxU64(&x454, &x455, 0x0, x441, 0xecec196accc52973);
var x456: u64 = undefined;
var x457: u1 = undefined;
subborrowxU64(&x456, &x457, x455, x443, 0x581a0db248b0a77a);
var x458: u64 = undefined;
var x459: u1 = undefined;
subborrowxU64(&x458, &x459, x457, x445, 0xc7634d81f4372ddf);
var x460: u64 = undefined;
var x461: u1 = undefined;
subborrowxU64(&x460, &x461, x459, x447, 0xffffffffffffffff);
var x462: u64 = undefined;
var x463: u1 = undefined;
subborrowxU64(&x462, &x463, x461, x449, 0xffffffffffffffff);
var x464: u64 = undefined;
var x465: u1 = undefined;
subborrowxU64(&x464, &x465, x463, x451, 0xffffffffffffffff);
var x466: u64 = undefined;
var x467: u1 = undefined;
subborrowxU64(&x466, &x467, x465, x453, 0x0);
var x468: u64 = undefined;
cmovznzU64(&x468, x467, x454, x441);
var x469: u64 = undefined;
cmovznzU64(&x469, x467, x456, x443);
var x470: u64 = undefined;
cmovznzU64(&x470, x467, x458, x445);
var x471: u64 = undefined;
cmovznzU64(&x471, x467, x460, x447);
var x472: u64 = undefined;
cmovznzU64(&x472, x467, x462, x449);
var x473: u64 = undefined;
cmovznzU64(&x473, x467, x464, x451);
out1[0] = x468;
out1[1] = x469;
out1[2] = x470;
out1[3] = x471;
out1[4] = x472;
out1[5] = x473;
}