fiat_25519_uint128
fiat_25519_uint128 x1;
fiat_25519_uint128 x2;
fiat_25519_uint128 x3;
fiat_25519_uint128 x4;
fiat_25519_uint128 x5;
fiat_25519_uint128 x6;
fiat_25519_uint128 x7;
fiat_25519_uint128 x8;
fiat_25519_uint128 x9;
fiat_25519_uint128 x10;
fiat_25519_uint128 x11;
fiat_25519_uint128 x12;
fiat_25519_uint128 x13;
fiat_25519_uint128 x14;
fiat_25519_uint128 x15;
fiat_25519_uint128 x16;
fiat_25519_uint128 x17;
fiat_25519_uint128 x18;
fiat_25519_uint128 x19;
fiat_25519_uint128 x20;
fiat_25519_uint128 x21;
fiat_25519_uint128 x22;
fiat_25519_uint128 x23;
fiat_25519_uint128 x24;
fiat_25519_uint128 x25;
fiat_25519_uint128 x26;
fiat_25519_uint128 x29;
fiat_25519_uint128 x30;
fiat_25519_uint128 x31;
fiat_25519_uint128 x32;
fiat_25519_uint128 x33;
fiat_25519_uint128 x36;
fiat_25519_uint128 x39;
fiat_25519_uint128 x42;
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)));
x7 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[2]) * UINT8_C(0x13)));
x8 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[4]) * UINT8_C(0x13)));
x9 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[3]) * UINT8_C(0x13)));
x10 = ((fiat_25519_uint128)(arg1[1]) * ((arg2[4]) * UINT8_C(0x13)));
x11 = ((fiat_25519_uint128)(arg1[4]) * (arg2[0]));
x12 = ((fiat_25519_uint128)(arg1[3]) * (arg2[1]));
x13 = ((fiat_25519_uint128)(arg1[3]) * (arg2[0]));
x14 = ((fiat_25519_uint128)(arg1[2]) * (arg2[2]));
x15 = ((fiat_25519_uint128)(arg1[2]) * (arg2[1]));
x16 = ((fiat_25519_uint128)(arg1[2]) * (arg2[0]));
x17 = ((fiat_25519_uint128)(arg1[1]) * (arg2[3]));
x18 = ((fiat_25519_uint128)(arg1[1]) * (arg2[2]));
x19 = ((fiat_25519_uint128)(arg1[1]) * (arg2[1]));
x20 = ((fiat_25519_uint128)(arg1[1]) * (arg2[0]));
x21 = ((fiat_25519_uint128)(arg1[0]) * (arg2[4]));
x22 = ((fiat_25519_uint128)(arg1[0]) * (arg2[3]));
x23 = ((fiat_25519_uint128)(arg1[0]) * (arg2[2]));
x24 = ((fiat_25519_uint128)(arg1[0]) * (arg2[1]));
x25 = ((fiat_25519_uint128)(arg1[0]) * (arg2[0]));
fiat_25519_uint128 x9;
fiat_25519_uint128 x10;
fiat_25519_uint128 x11;
fiat_25519_uint128 x12;
fiat_25519_uint128 x13;
fiat_25519_uint128 x14;
fiat_25519_uint128 x15;
fiat_25519_uint128 x16;
fiat_25519_uint128 x17;
fiat_25519_uint128 x18;
fiat_25519_uint128 x19;
fiat_25519_uint128 x20;
fiat_25519_uint128 x21;
fiat_25519_uint128 x22;
fiat_25519_uint128 x23;
fiat_25519_uint128 x24;
fiat_25519_uint128 x27;
fiat_25519_uint128 x28;
fiat_25519_uint128 x29;
fiat_25519_uint128 x30;
fiat_25519_uint128 x31;
fiat_25519_uint128 x34;
fiat_25519_uint128 x37;
fiat_25519_uint128 x40;
x9 = ((fiat_25519_uint128)(arg1[4]) * x1);
x10 = ((fiat_25519_uint128)(arg1[3]) * x2);
x11 = ((fiat_25519_uint128)(arg1[3]) * x4);
x12 = ((fiat_25519_uint128)(arg1[2]) * x2);
x13 = ((fiat_25519_uint128)(arg1[2]) * x5);
x14 = ((fiat_25519_uint128)(arg1[2]) * (arg1[2]));
x15 = ((fiat_25519_uint128)(arg1[1]) * x2);
x16 = ((fiat_25519_uint128)(arg1[1]) * x6);
x17 = ((fiat_25519_uint128)(arg1[1]) * x7);
x18 = ((fiat_25519_uint128)(arg1[1]) * (arg1[1]));
x19 = ((fiat_25519_uint128)(arg1[0]) * x3);
x20 = ((fiat_25519_uint128)(arg1[0]) * x6);
x21 = ((fiat_25519_uint128)(arg1[0]) * x7);
x22 = ((fiat_25519_uint128)(arg1[0]) * x8);
x23 = ((fiat_25519_uint128)(arg1[0]) * (arg1[0]));