UINT8_C
x1 = ((uint64_t)(arg1[9]) * ((arg2[9]) * UINT8_C(0x26)));
x2 = ((uint64_t)(arg1[9]) * ((arg2[8]) * UINT8_C(0x13)));
x3 = ((uint64_t)(arg1[9]) * ((arg2[7]) * UINT8_C(0x26)));
x4 = ((uint64_t)(arg1[9]) * ((arg2[6]) * UINT8_C(0x13)));
x5 = ((uint64_t)(arg1[9]) * ((arg2[5]) * UINT8_C(0x26)));
x6 = ((uint64_t)(arg1[9]) * ((arg2[4]) * UINT8_C(0x13)));
x7 = ((uint64_t)(arg1[9]) * ((arg2[3]) * UINT8_C(0x26)));
x8 = ((uint64_t)(arg1[9]) * ((arg2[2]) * UINT8_C(0x13)));
x9 = ((uint64_t)(arg1[9]) * ((arg2[1]) * UINT8_C(0x26)));
x10 = ((uint64_t)(arg1[8]) * ((arg2[9]) * UINT8_C(0x13)));
x11 = ((uint64_t)(arg1[8]) * ((arg2[8]) * UINT8_C(0x13)));
x12 = ((uint64_t)(arg1[8]) * ((arg2[7]) * UINT8_C(0x13)));
x13 = ((uint64_t)(arg1[8]) * ((arg2[6]) * UINT8_C(0x13)));
x14 = ((uint64_t)(arg1[8]) * ((arg2[5]) * UINT8_C(0x13)));
x15 = ((uint64_t)(arg1[8]) * ((arg2[4]) * UINT8_C(0x13)));
x16 = ((uint64_t)(arg1[8]) * ((arg2[3]) * UINT8_C(0x13)));
x17 = ((uint64_t)(arg1[8]) * ((arg2[2]) * UINT8_C(0x13)));
x18 = ((uint64_t)(arg1[7]) * ((arg2[9]) * UINT8_C(0x26)));
x19 = ((uint64_t)(arg1[7]) * ((arg2[8]) * UINT8_C(0x13)));
x20 = ((uint64_t)(arg1[7]) * ((arg2[7]) * UINT8_C(0x26)));
x21 = ((uint64_t)(arg1[7]) * ((arg2[6]) * UINT8_C(0x13)));
x22 = ((uint64_t)(arg1[7]) * ((arg2[5]) * UINT8_C(0x26)));
x23 = ((uint64_t)(arg1[7]) * ((arg2[4]) * UINT8_C(0x13)));
x24 = ((uint64_t)(arg1[7]) * ((arg2[3]) * UINT8_C(0x26)));
x25 = ((uint64_t)(arg1[6]) * ((arg2[9]) * UINT8_C(0x13)));
x26 = ((uint64_t)(arg1[6]) * ((arg2[8]) * UINT8_C(0x13)));
x27 = ((uint64_t)(arg1[6]) * ((arg2[7]) * UINT8_C(0x13)));
x28 = ((uint64_t)(arg1[6]) * ((arg2[6]) * UINT8_C(0x13)));
x29 = ((uint64_t)(arg1[6]) * ((arg2[5]) * UINT8_C(0x13)));
x30 = ((uint64_t)(arg1[6]) * ((arg2[4]) * UINT8_C(0x13)));
x31 = ((uint64_t)(arg1[5]) * ((arg2[9]) * UINT8_C(0x26)));
x32 = ((uint64_t)(arg1[5]) * ((arg2[8]) * UINT8_C(0x13)));
x33 = ((uint64_t)(arg1[5]) * ((arg2[7]) * UINT8_C(0x26)));
x34 = ((uint64_t)(arg1[5]) * ((arg2[6]) * UINT8_C(0x13)));
x35 = ((uint64_t)(arg1[5]) * ((arg2[5]) * UINT8_C(0x26)));
x36 = ((uint64_t)(arg1[4]) * ((arg2[9]) * UINT8_C(0x13)));
x37 = ((uint64_t)(arg1[4]) * ((arg2[8]) * UINT8_C(0x13)));
x38 = ((uint64_t)(arg1[4]) * ((arg2[7]) * UINT8_C(0x13)));
x39 = ((uint64_t)(arg1[4]) * ((arg2[6]) * UINT8_C(0x13)));
x40 = ((uint64_t)(arg1[3]) * ((arg2[9]) * UINT8_C(0x26)));
x41 = ((uint64_t)(arg1[3]) * ((arg2[8]) * UINT8_C(0x13)));
x42 = ((uint64_t)(arg1[3]) * ((arg2[7]) * UINT8_C(0x26)));
x43 = ((uint64_t)(arg1[2]) * ((arg2[9]) * UINT8_C(0x13)));
x44 = ((uint64_t)(arg1[2]) * ((arg2[8]) * UINT8_C(0x13)));
x45 = ((uint64_t)(arg1[1]) * ((arg2[9]) * UINT8_C(0x26)));
x140 = (x138 * UINT8_C(0x13));
x1 = ((arg1[9]) * UINT8_C(0x13));
x4 = ((arg1[8]) * UINT8_C(0x13));
x7 = ((arg1[7]) * UINT8_C(0x13));
x10 = ((arg1[6]) * UINT8_C(0x13));
x13 = ((arg1[5]) * UINT8_C(0x13));
x113 = (x111 * UINT8_C(0x13));
x11 = ((x1 & UINT32_C(0x3ffffff)) + ((x10 >> 25) * UINT8_C(0x13)));
x1 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[4]) * UINT8_C(0x13)));
x2 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[3]) * UINT8_C(0x13)));
x3 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[2]) * UINT8_C(0x13)));
x4 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[1]) * UINT8_C(0x13)));
x5 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[4]) * UINT8_C(0x13)));
x6 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[3]) * UINT8_C(0x13)));
x50 = (uint8_t)(x22 & UINT8_C(0xff));
x7 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[2]) * UINT8_C(0x13)));
x52 = (uint8_t)(x51 & UINT8_C(0xff));
x54 = (uint8_t)(x53 & UINT8_C(0xff));
x57 = (uint8_t)(x56 & UINT8_C(0xff));
x59 = (uint8_t)(x58 & UINT8_C(0xff));
x8 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[4]) * UINT8_C(0x13)));
x61 = (uint8_t)(x60 & UINT8_C(0xff));
x64 = (uint8_t)(x63 & UINT8_C(0xff));
x66 = (uint8_t)(x65 & UINT8_C(0xff));
x68 = (uint8_t)(x67 & UINT8_C(0xff));
x9 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[3]) * UINT8_C(0x13)));
x71 = (uint8_t)(x70 & UINT8_C(0xff));
x73 = (uint8_t)(x72 & UINT8_C(0xff));
x75 = (uint8_t)(x74 & UINT8_C(0xff));
x78 = (uint8_t)(x77 & UINT8_C(0xff));
x80 = (uint8_t)(x79 & UINT8_C(0xff));
x10 = ((fiat_25519_uint128)(arg1[1]) * ((arg2[4]) * UINT8_C(0x13)));
x82 = (uint8_t)(x81 & UINT8_C(0xff));
x84 = (uint8_t)(x32 & UINT8_C(0xff));
x86 = (uint8_t)(x85 & UINT8_C(0xff));
x88 = (uint8_t)(x87 & UINT8_C(0xff));
x91 = (uint8_t)(x90 & UINT8_C(0xff));
x93 = (uint8_t)(x92 & UINT8_C(0xff));
x95 = (uint8_t)(x94 & UINT8_C(0xff));
x98 = (uint8_t)(x97 & UINT8_C(0xff));
x100 = (uint8_t)(x99 & UINT8_C(0xff));
x102 = (uint8_t)(x101 & UINT8_C(0xff));
x105 = (uint8_t)(x104 & UINT8_C(0xff));
x107 = (uint8_t)(x106 & UINT8_C(0xff));
x109 = (uint8_t)(x108 & UINT8_C(0xff));
x112 = (uint8_t)(x111 & UINT8_C(0xff));
x114 = (uint8_t)(x113 & UINT8_C(0xff));
x116 = (uint8_t)(x115 & UINT8_C(0xff));
x45 = (x43 * UINT8_C(0x13));
x1 = ((arg1[4]) * UINT8_C(0x13));
x4 = ((arg1[3]) * UINT8_C(0x13));
x43 = (x41 * UINT8_C(0x13));
x6 = ((x1 & UINT64_C(0x7ffffffffffff)) + ((x5 >> 51) * UINT8_C(0x13)));
x26 = (uint8_t)(x12 & UINT8_C(0xff));
x28 = (uint8_t)(x27 & UINT8_C(0xff));
x30 = (uint8_t)(x29 & UINT8_C(0xff));
x32 = (uint8_t)(x31 & UINT8_C(0xff));
x34 = (uint8_t)(x33 & UINT8_C(0xff));
x36 = (uint8_t)(x35 & UINT8_C(0xff));
x39 = (uint8_t)(x38 & UINT8_C(0xff));
x41 = (uint8_t)(x40 & UINT8_C(0xff));
x43 = (uint8_t)(x42 & UINT8_C(0xff));
x45 = (uint8_t)(x44 & UINT8_C(0xff));
x47 = (uint8_t)(x46 & UINT8_C(0xff));
x49 = (uint8_t)(x48 & UINT8_C(0xff));
x52 = (uint8_t)(x51 & UINT8_C(0xff));
x54 = (uint8_t)(x53 & UINT8_C(0xff));
x56 = (uint8_t)(x55 & UINT8_C(0xff));
x58 = (uint8_t)(x57 & UINT8_C(0xff));
x60 = (uint8_t)(x59 & UINT8_C(0xff));
x62 = (uint8_t)(x61 & UINT8_C(0xff));
x64 = (uint8_t)(x63 & UINT8_C(0xff));
x67 = (uint8_t)(x66 & UINT8_C(0xff));
x69 = (uint8_t)(x68 & UINT8_C(0xff));
x71 = (uint8_t)(x70 & UINT8_C(0xff));
x73 = (uint8_t)(x72 & UINT8_C(0xff));
x75 = (uint8_t)(x74 & UINT8_C(0xff));
x77 = (uint8_t)(x76 & UINT8_C(0xff));
x80 = (uint8_t)(x79 & UINT8_C(0xff));
x82 = (uint8_t)(x81 & UINT8_C(0xff));
x84 = (uint8_t)(x83 & UINT8_C(0xff));
x86 = (uint8_t)(x85 & UINT8_C(0xff));
x88 = (uint8_t)(x87 & UINT8_C(0xff));
x90 = (uint8_t)(x89 & UINT8_C(0xff));
#define HWORD(A) (UINT8_C(A))