mashup.h

/* Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --inline --static
 * --use-value-barrier --no-wide-int secp256k1_dettman 64 5 48 '2^256 -
 * 4294968273' mul square */
/* curve description: secp256k1_dettman */
/* machine_wordsize = 64 (from "64") */
/* requested operations: mul, square */
/* n = 5 (from "5") */
/* last_limb_width = 48 (from "48") */
/* s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273") */
/* inbounds_multiplier: None (from "") */
/*  */
/* Computed values: */
/*  */
/*  */

#include <stdint.h>
typedef unsigned char fiat_secp256k1_dettman_uint1;
typedef signed char fiat_secp256k1_dettman_int1;
#if defined(__GNUC__) || defined(__clang__)
#define FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION __extension__
#define FIAT_SECP256K1_DETTMAN_FIAT_INLINE __inline__
#else
#define FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION
#define FIAT_SECP256K1_DETTMAN_FIAT_INLINE
#endif

#if (-1 & 3) != 3
#error "This code only works on a two's complement system"
#endif

#if defined(__has_builtin)
#define HAS_BUILTIN(x) __has_builtin(x)
#else
#define HAS_BUILTIN(x) 0
#endif

/*
 * The function fiat_secp256k1_dettman_addcarryx_u64 is an addition with carry.
 *
 * Postconditions:
 *   out1 = (arg1 + arg2 + arg3) mod 2^64
 *   out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
 *
 * Input Bounds:
 *   arg1: [0x0 ~> 0x1]
 *   arg2: [0x0 ~> 0xffffffffffffffff]
 *   arg3: [0x0 ~> 0xffffffffffffffff]
 * Output Bounds:
 *   out1: [0x0 ~> 0xffffffffffffffff]
 *   out2: [0x0 ~> 0x1]
 */
static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void
fiat_secp256k1_dettman_addcarryx_u64(uint64_t *out,
                                     fiat_secp256k1_dettman_uint1 *outc,
                                     fiat_secp256k1_dettman_uint1 c, uint64_t a,
                                     uint64_t b) {

#if HAS_BUILTIN(__builtin_ia32_addcarryx_u64)
  unsigned long long t;
  *outc = __builtin_ia32_addcarryx_u64(c, a, b, &t);
  *out = t;
#elif HAS_BUILTIN(__builtin_addcll)
  unsigned long long t;
  *out = __builtin_addcll(a, b, c, &t);
  *outc = t;
#elif defined(_M_X64)
  *outc = _addcarryx_u64(c, a, b, out);
#elif defined(__SIZEOF_INT128__)
  unsigned __int128 big = a + (unsigned __int128)b + c;
  *out = big;
  *outc = big >> 64;
#else
  // #error "need adc"
  a += c;
  c = a < c;
  uint64_t ret = a + b;
  c += ret < a;
  *out = ret;
  *outc = c;
#endif
}

/*
 * The function fiat_secp256k1_dettman_mulx_u64 is a multiplication, returning
 * the full double-width result.
 *
 * Postconditions:
 *   out1 = (arg1 * arg2) mod 2^64
 *   out2 = ⌊arg1 * arg2 / 2^64⌋
 *
 * Input Bounds:
 *   arg1: [0x0 ~> 0xffffffffffffffff]
 *   arg2: [0x0 ~> 0xffffffffffffffff]
 * Output Bounds:
 *   out1: [0x0 ~> 0xffffffffffffffff]
 *   out2: [0x0 ~> 0xffffffffffffffff]
 */
static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void
fiat_secp256k1_dettman_mulx_u64(uint64_t *lo, uint64_t *hi, uint64_t a,
                                uint64_t b) {
#if defined(__SIZEOF_INT128__)
  unsigned __int128 big = a * (unsigned __int128)b;
  *lo = big;
  *hi = big >> 64;
#elif defined(_MSC_VER)
  *lo = _umul128(a, b, hi);
#else
#error "need mul128"
  uint64_t W = (uint64_t)4 * sizeof(uint64_t); // half-word width
  uint64_t M = ((uint64_t)1 << W) - 1;
  uint64_t lh = (a & M) * (b >> W);
  uint64_t hl = (a >> W) * (b & M);
  uint64_t sW = lh + hl;
  uint64_t r2W = (a >> W) * (b >> W);
  uint64_t c3W = sW < lh;
  r2W += c3W << W;
  r2W += sW >> W;
  uint64_t r0 = (a & M) * (b & M);
  uint64_t s0 = r0 + (sW << W);
  uint64_t c2W = s0 < r0;
  r2W += c2W;
  *lo = s0;
  *hi = r2W;
#endif
}

/*
 * The function fiat_secp256k1_dettman_mul multiplies two field elements.
 *
 * Postconditions:
 *   eval out1 mod
 * 115792089237316195423570985008687907853269984665640564039457584007908834671663
 * = (eval arg1 * eval arg2) mod
 * 115792089237316195423570985008687907853269984665640564039457584007908834671663
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~>
 * 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x1fffffffffffe]] arg2:
 * [[0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~>
 * 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x1fffffffffffe]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~>
 * 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x17fffffffffff]]
 */
static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void
fiat_secp256k1_dettman_mul(uint64_t out1[5], const uint64_t arg1[5],
                           const uint64_t arg2[5]) {
  uint64_t x1;
  uint64_t x2;
  uint64_t x3;
  uint64_t x4;
  uint64_t x5;
  uint64_t x6;
  uint64_t x7;
  uint64_t x8;
  uint64_t x9;
  fiat_secp256k1_dettman_uint1 x10;
  uint64_t x11;
  fiat_secp256k1_dettman_uint1 x12;
  uint64_t x13;
  uint64_t x14;
  uint64_t x15;
  fiat_secp256k1_dettman_uint1 x16;
  uint64_t x17;
  fiat_secp256k1_dettman_uint1 x18;
  uint64_t x19;
  uint64_t x20;
  uint64_t x21;
  fiat_secp256k1_dettman_uint1 x22;
  uint64_t x23;
  fiat_secp256k1_dettman_uint1 x24;
  uint64_t x25;
  fiat_secp256k1_dettman_uint1 x26;
  uint64_t x27;
  fiat_secp256k1_dettman_uint1 x28;
  uint64_t x29;
  uint64_t x30;
  uint64_t x31;
  uint64_t x32;
  uint64_t x33;
  uint64_t x34;
  uint64_t x35;
  uint64_t x36;
  uint64_t x37;
  fiat_secp256k1_dettman_uint1 x38;
  uint64_t x39;
  fiat_secp256k1_dettman_uint1 x40;
  uint64_t x41;
  uint64_t x42;
  uint64_t x43;
  fiat_secp256k1_dettman_uint1 x44;
  uint64_t x45;
  fiat_secp256k1_dettman_uint1 x46;
  uint64_t x47;
  uint64_t x48;
  uint64_t x49;
  fiat_secp256k1_dettman_uint1 x50;
  uint64_t x51;
  fiat_secp256k1_dettman_uint1 x52;
  uint64_t x53;
  uint64_t x54;
  uint64_t x55;
  fiat_secp256k1_dettman_uint1 x56;
  uint64_t x57;
  fiat_secp256k1_dettman_uint1 x58;
  uint64_t x59;
  fiat_secp256k1_dettman_uint1 x60;
  uint64_t x61;
  uint64_t x62;
  fiat_secp256k1_dettman_uint1 x63;
  uint64_t x64;
  fiat_secp256k1_dettman_uint1 x65;
  uint64_t x66;
  uint64_t x67;
  uint64_t x68;
  uint64_t x69;
  uint64_t x70;
  uint64_t x71;
  uint64_t x72;
  uint64_t x73;
  uint64_t x74;
  fiat_secp256k1_dettman_uint1 x75;
  uint64_t x76;
  fiat_secp256k1_dettman_uint1 x77;
  uint64_t x78;
  uint64_t x79;
  uint64_t x80;
  fiat_secp256k1_dettman_uint1 x81;
  uint64_t x82;
  fiat_secp256k1_dettman_uint1 x83;
  uint64_t x84;
  uint64_t x85;
  uint64_t x86;
  fiat_secp256k1_dettman_uint1 x87;
  uint64_t x88;
  fiat_secp256k1_dettman_uint1 x89;
  uint64_t x90;
  fiat_secp256k1_dettman_uint1 x91;
  uint64_t x92;
  uint64_t x93;
  uint64_t x94;
  uint64_t x95;
  uint64_t x96;
  uint64_t x97;
  uint64_t x98;
  uint64_t x99;
  fiat_secp256k1_dettman_uint1 x100;
  uint64_t x101;
  fiat_secp256k1_dettman_uint1 x102;
  uint64_t x103;
  uint64_t x104;
  uint64_t x105;
  uint64_t x106;
  uint64_t x107;
  uint64_t x108;
  uint64_t x109;
  fiat_secp256k1_dettman_uint1 x110;
  uint64_t x111;
  fiat_secp256k1_dettman_uint1 x112;
  uint64_t x113;
  uint64_t x114;
  uint64_t x115;
  fiat_secp256k1_dettman_uint1 x116;
  uint64_t x117;
  fiat_secp256k1_dettman_uint1 x118;
  uint64_t x119;
  fiat_secp256k1_dettman_uint1 x120;
  uint64_t x121;
  uint64_t x122;
  uint64_t x123;
  uint64_t x124;
  uint64_t x125;
  uint64_t x126;
  uint64_t x127;
  uint64_t x128;
  uint64_t x129;
  uint64_t x130;
  fiat_secp256k1_dettman_uint1 x131;
  uint64_t x132;
  fiat_secp256k1_dettman_uint1 x133;
  uint64_t x134;
  fiat_secp256k1_dettman_uint1 x135;
  uint64_t x136;
  uint64_t x137;
  fiat_secp256k1_dettman_uint1 x138;
  uint64_t x139;
  fiat_secp256k1_dettman_uint1 x140;
  uint64_t x141;
  uint64_t x142;
  uint64_t x143;
  uint64_t x144;
  uint64_t x145;
  uint64_t x146;
  uint64_t x147;
  fiat_secp256k1_dettman_uint1 x148;
  uint64_t x149;
  fiat_secp256k1_dettman_uint1 x150;
  uint64_t x151;
  fiat_secp256k1_dettman_uint1 x152;
  uint64_t x153;
  uint64_t x154;
  uint64_t x155;
  uint64_t x156;
  uint64_t x157;
  uint64_t x158;
  uint64_t x159;
  uint64_t x160;
  fiat_secp256k1_dettman_uint1 x161;
  uint64_t x162;
  fiat_secp256k1_dettman_uint1 x163;
  uint64_t x164;
  uint64_t x165;
  uint64_t x166;
  fiat_secp256k1_dettman_uint1 x167;
  uint64_t x168;
  fiat_secp256k1_dettman_uint1 x169;
  uint64_t x170;
  fiat_secp256k1_dettman_uint1 x171;
  uint64_t x172;
  uint64_t x173;
  fiat_secp256k1_dettman_uint1 x174;
  uint64_t x175;
  fiat_secp256k1_dettman_uint1 x176;
  uint64_t x177;
  uint64_t x178;
  uint64_t x179;
  uint64_t x180;
  uint64_t x181;
  fiat_secp256k1_dettman_uint1 x182;
  uint64_t x183;
  uint64_t x184;
  uint64_t x185;
  uint64_t x186;
  fiat_secp256k1_dettman_mulx_u64(&x1, &x2, (arg1[4]), (arg2[4]));
  fiat_secp256k1_dettman_mulx_u64(&x3, &x4, x1, UINT64_C(0x1000003d10));
  fiat_secp256k1_dettman_mulx_u64(&x5, &x6, (arg1[3]), (arg2[0]));
  fiat_secp256k1_dettman_mulx_u64(&x7, &x8, (arg1[2]), (arg2[1]));
  fiat_secp256k1_dettman_addcarryx_u64(&x9, &x10, 0x0, x7, x5);
  fiat_secp256k1_dettman_addcarryx_u64(&x11, &x12, x10, x8, x6);
  fiat_secp256k1_dettman_mulx_u64(&x13, &x14, (arg1[1]), (arg2[2]));
  fiat_secp256k1_dettman_addcarryx_u64(&x15, &x16, 0x0, x13, x9);
  fiat_secp256k1_dettman_addcarryx_u64(&x17, &x18, x16, x14, x11);
  fiat_secp256k1_dettman_mulx_u64(&x19, &x20, (arg1[0]), (arg2[3]));
  fiat_secp256k1_dettman_addcarryx_u64(&x21, &x22, 0x0, x19, x15);
  fiat_secp256k1_dettman_addcarryx_u64(&x23, &x24, x22, x20, x17);
  fiat_secp256k1_dettman_addcarryx_u64(&x25, &x26, 0x0, x21, x3);
  fiat_secp256k1_dettman_addcarryx_u64(&x27, &x28, x26, x23, x4);
  x29 = ((x25 >> 52) | ((x27 << 12) & UINT64_C(0xffffffffffffffff)));
  x30 = (x25 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x31, &x32, x2, UINT64_C(0x1000003d10000));
  fiat_secp256k1_dettman_mulx_u64(&x33, &x34, (arg1[4]), (arg2[0]));
  fiat_secp256k1_dettman_mulx_u64(&x35, &x36, (arg1[3]), (arg2[1]));
  fiat_secp256k1_dettman_addcarryx_u64(&x37, &x38, 0x0, x35, x33);
  fiat_secp256k1_dettman_addcarryx_u64(&x39, &x40, x38, x36, x34);
  fiat_secp256k1_dettman_mulx_u64(&x41, &x42, (arg1[2]), (arg2[2]));
  fiat_secp256k1_dettman_addcarryx_u64(&x43, &x44, 0x0, x41, x37);
  fiat_secp256k1_dettman_addcarryx_u64(&x45, &x46, x44, x42, x39);
  fiat_secp256k1_dettman_mulx_u64(&x47, &x48, (arg1[1]), (arg2[3]));
  fiat_secp256k1_dettman_addcarryx_u64(&x49, &x50, 0x0, x47, x43);
  fiat_secp256k1_dettman_addcarryx_u64(&x51, &x52, x50, x48, x45);
  fiat_secp256k1_dettman_mulx_u64(&x53, &x54, (arg1[0]), (arg2[4]));
  fiat_secp256k1_dettman_addcarryx_u64(&x55, &x56, 0x0, x53, x49);
  fiat_secp256k1_dettman_addcarryx_u64(&x57, &x58, x56, x54, x51);
  fiat_secp256k1_dettman_addcarryx_u64(&x59, &x60, 0x0, x55, x29);
  x61 = (x60 + x57);
  fiat_secp256k1_dettman_addcarryx_u64(&x62, &x63, 0x0, x59, x31);
  fiat_secp256k1_dettman_addcarryx_u64(&x64, &x65, x63, x61, x32);
  x66 = ((x62 >> 52) | ((x64 << 12) & UINT64_C(0xffffffffffffffff)));
  x67 = (x62 & UINT64_C(0xfffffffffffff));
  x68 = (x67 >> 48);
  x69 = (x67 & UINT64_C(0xffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x70, &x71, (arg1[4]), (arg2[1]));
  fiat_secp256k1_dettman_mulx_u64(&x72, &x73, (arg1[3]), (arg2[2]));
  fiat_secp256k1_dettman_addcarryx_u64(&x74, &x75, 0x0, x72, x70);
  fiat_secp256k1_dettman_addcarryx_u64(&x76, &x77, x75, x73, x71);
  fiat_secp256k1_dettman_mulx_u64(&x78, &x79, (arg1[2]), (arg2[3]));
  fiat_secp256k1_dettman_addcarryx_u64(&x80, &x81, 0x0, x78, x74);
  fiat_secp256k1_dettman_addcarryx_u64(&x82, &x83, x81, x79, x76);
  fiat_secp256k1_dettman_mulx_u64(&x84, &x85, (arg1[1]), (arg2[4]));
  fiat_secp256k1_dettman_addcarryx_u64(&x86, &x87, 0x0, x84, x80);
  fiat_secp256k1_dettman_addcarryx_u64(&x88, &x89, x87, x85, x82);
  fiat_secp256k1_dettman_addcarryx_u64(&x90, &x91, 0x0, x86, x66);
  x92 = (x91 + x88);
  x93 = ((x90 >> 52) | ((x92 << 12) & UINT64_C(0xffffffffffffffff)));
  x94 = (x90 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x95, &x96, ((x94 << 4) + x68),
                                  UINT64_C(0x1000003d1));
  fiat_secp256k1_dettman_mulx_u64(&x97, &x98, (arg1[0]), (arg2[0]));
  fiat_secp256k1_dettman_addcarryx_u64(&x99, &x100, 0x0, x97, x95);
  fiat_secp256k1_dettman_addcarryx_u64(&x101, &x102, x100, x98, x96);
  x103 = ((x99 >> 52) | ((x101 << 12) & UINT64_C(0xffffffffffffffff)));
  x104 = (x99 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x105, &x106, (arg1[4]), (arg2[2]));
  fiat_secp256k1_dettman_mulx_u64(&x107, &x108, (arg1[3]), (arg2[3]));
  fiat_secp256k1_dettman_addcarryx_u64(&x109, &x110, 0x0, x107, x105);
  fiat_secp256k1_dettman_addcarryx_u64(&x111, &x112, x110, x108, x106);
  fiat_secp256k1_dettman_mulx_u64(&x113, &x114, (arg1[2]), (arg2[4]));
  fiat_secp256k1_dettman_addcarryx_u64(&x115, &x116, 0x0, x113, x109);
  fiat_secp256k1_dettman_addcarryx_u64(&x117, &x118, x116, x114, x111);
  fiat_secp256k1_dettman_addcarryx_u64(&x119, &x120, 0x0, x115, x93);
  x121 = (x120 + x117);
  x122 = ((x119 >> 52) | ((x121 << 12) & UINT64_C(0xffffffffffffffff)));
  x123 = (x119 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x124, &x125, x123, UINT64_C(0x1000003d10));
  fiat_secp256k1_dettman_mulx_u64(&x126, &x127, (arg1[1]), (arg2[0]));
  fiat_secp256k1_dettman_mulx_u64(&x128, &x129, (arg1[0]), (arg2[1]));
  fiat_secp256k1_dettman_addcarryx_u64(&x130, &x131, 0x0, x128, x126);
  fiat_secp256k1_dettman_addcarryx_u64(&x132, &x133, x131, x129, x127);
  fiat_secp256k1_dettman_addcarryx_u64(&x134, &x135, 0x0, x130, x103);
  x136 = (x135 + x132);
  fiat_secp256k1_dettman_addcarryx_u64(&x137, &x138, 0x0, x134, x124);
  fiat_secp256k1_dettman_addcarryx_u64(&x139, &x140, x138, x136, x125);
  x141 = ((x137 >> 52) | ((x139 << 12) & UINT64_C(0xffffffffffffffff)));
  x142 = (x137 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x143, &x144, (arg1[4]), (arg2[3]));
  fiat_secp256k1_dettman_mulx_u64(&x145, &x146, (arg1[3]), (arg2[4]));
  fiat_secp256k1_dettman_addcarryx_u64(&x147, &x148, 0x0, x145, x143);
  fiat_secp256k1_dettman_addcarryx_u64(&x149, &x150, x148, x146, x144);
  fiat_secp256k1_dettman_addcarryx_u64(&x151, &x152, 0x0, x147, x122);
  x153 = (x152 + x149);
  fiat_secp256k1_dettman_mulx_u64(&x154, &x155, x151, UINT64_C(0x1000003d10));
  fiat_secp256k1_dettman_mulx_u64(&x156, &x157, (arg1[2]), (arg2[0]));
  fiat_secp256k1_dettman_mulx_u64(&x158, &x159, (arg1[1]), (arg2[1]));
  fiat_secp256k1_dettman_addcarryx_u64(&x160, &x161, 0x0, x158, x156);
  fiat_secp256k1_dettman_addcarryx_u64(&x162, &x163, x161, x159, x157);
  fiat_secp256k1_dettman_mulx_u64(&x164, &x165, (arg1[0]), (arg2[2]));
  fiat_secp256k1_dettman_addcarryx_u64(&x166, &x167, 0x0, x164, x160);
  fiat_secp256k1_dettman_addcarryx_u64(&x168, &x169, x167, x165, x162);
  fiat_secp256k1_dettman_addcarryx_u64(&x170, &x171, 0x0, x166, x141);
  x172 = (x171 + x168);
  fiat_secp256k1_dettman_addcarryx_u64(&x173, &x174, 0x0, x170, x154);
  fiat_secp256k1_dettman_addcarryx_u64(&x175, &x176, x174, x172, x155);
  x177 = ((x173 >> 52) | ((x175 << 12) & UINT64_C(0xffffffffffffffff)));
  x178 = (x173 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x179, &x180, x153,
                                  UINT64_C(0x1000003d10000));
  fiat_secp256k1_dettman_addcarryx_u64(&x181, &x182, 0x0, (x30 + x177), x179);
  x183 = (x182 + x180);
  x184 = ((x181 >> 52) | ((x183 << 12) & UINT64_C(0xffffffffffffffff)));
  x185 = (x181 & UINT64_C(0xfffffffffffff));
  x186 = (x69 + x184);
  out1[0] = x104;
  out1[1] = x142;
  out1[2] = x178;
  out1[3] = x185;
  out1[4] = x186;
}

/*
 * The function fiat_secp256k1_dettman_square squares a field element.
 *
 * Postconditions:
 *   eval out1 mod
 * 115792089237316195423570985008687907853269984665640564039457584007908834671663
 * = (eval arg1 * eval arg1) mod
 * 115792089237316195423570985008687907853269984665640564039457584007908834671663
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~>
 * 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x1fffffffffffe]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~>
 * 0x1ffffffffffffe], [0x0 ~> 0x1ffffffffffffe], [0x0 ~> 0x17fffffffffff]]
 */
static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void
fiat_secp256k1_dettman_square(uint64_t out1[5], const uint64_t arg1[5]) {
  uint64_t x1;
  uint64_t x2;
  uint64_t x3;
  uint64_t x4;
  uint64_t x5;
  uint64_t x6;
  uint64_t x7;
  uint64_t x8;
  uint64_t x9;
  uint64_t x10;
  uint64_t x11;
  uint64_t x12;
  uint64_t x13;
  fiat_secp256k1_dettman_uint1 x14;
  uint64_t x15;
  fiat_secp256k1_dettman_uint1 x16;
  uint64_t x17;
  fiat_secp256k1_dettman_uint1 x18;
  uint64_t x19;
  fiat_secp256k1_dettman_uint1 x20;
  uint64_t x21;
  uint64_t x22;
  uint64_t x23;
  uint64_t x24;
  uint64_t x25;
  uint64_t x26;
  uint64_t x27;
  uint64_t x28;
  uint64_t x29;
  fiat_secp256k1_dettman_uint1 x30;
  uint64_t x31;
  fiat_secp256k1_dettman_uint1 x32;
  uint64_t x33;
  uint64_t x34;
  uint64_t x35;
  fiat_secp256k1_dettman_uint1 x36;
  uint64_t x37;
  fiat_secp256k1_dettman_uint1 x38;
  uint64_t x39;
  fiat_secp256k1_dettman_uint1 x40;
  uint64_t x41;
  uint64_t x42;
  fiat_secp256k1_dettman_uint1 x43;
  uint64_t x44;
  fiat_secp256k1_dettman_uint1 x45;
  uint64_t x46;
  uint64_t x47;
  uint64_t x48;
  uint64_t x49;
  uint64_t x50;
  uint64_t x51;
  uint64_t x52;
  uint64_t x53;
  uint64_t x54;
  fiat_secp256k1_dettman_uint1 x55;
  uint64_t x56;
  fiat_secp256k1_dettman_uint1 x57;
  uint64_t x58;
  fiat_secp256k1_dettman_uint1 x59;
  uint64_t x60;
  uint64_t x61;
  uint64_t x62;
  uint64_t x63;
  uint64_t x64;
  uint64_t x65;
  uint64_t x66;
  uint64_t x67;
  fiat_secp256k1_dettman_uint1 x68;
  uint64_t x69;
  fiat_secp256k1_dettman_uint1 x70;
  uint64_t x71;
  uint64_t x72;
  uint64_t x73;
  uint64_t x74;
  uint64_t x75;
  uint64_t x76;
  uint64_t x77;
  fiat_secp256k1_dettman_uint1 x78;
  uint64_t x79;
  fiat_secp256k1_dettman_uint1 x80;
  uint64_t x81;
  fiat_secp256k1_dettman_uint1 x82;
  uint64_t x83;
  uint64_t x84;
  uint64_t x85;
  uint64_t x86;
  uint64_t x87;
  uint64_t x88;
  uint64_t x89;
  uint64_t x90;
  fiat_secp256k1_dettman_uint1 x91;
  uint64_t x92;
  uint64_t x93;
  fiat_secp256k1_dettman_uint1 x94;
  uint64_t x95;
  fiat_secp256k1_dettman_uint1 x96;
  uint64_t x97;
  uint64_t x98;
  uint64_t x99;
  uint64_t x100;
  uint64_t x101;
  fiat_secp256k1_dettman_uint1 x102;
  uint64_t x103;
  uint64_t x104;
  uint64_t x105;
  uint64_t x106;
  uint64_t x107;
  uint64_t x108;
  uint64_t x109;
  uint64_t x110;
  fiat_secp256k1_dettman_uint1 x111;
  uint64_t x112;
  fiat_secp256k1_dettman_uint1 x113;
  uint64_t x114;
  fiat_secp256k1_dettman_uint1 x115;
  uint64_t x116;
  uint64_t x117;
  fiat_secp256k1_dettman_uint1 x118;
  uint64_t x119;
  fiat_secp256k1_dettman_uint1 x120;
  uint64_t x121;
  uint64_t x122;
  uint64_t x123;
  uint64_t x124;
  uint64_t x125;
  fiat_secp256k1_dettman_uint1 x126;
  uint64_t x127;
  uint64_t x128;
  uint64_t x129;
  uint64_t x130;
  x1 = ((arg1[3]) * 0x2);
  x2 = ((arg1[2]) * 0x2);
  x3 = ((arg1[1]) * 0x2);
  x4 = ((arg1[0]) * 0x2);
  fiat_secp256k1_dettman_mulx_u64(&x5, &x6, (arg1[4]), (arg1[4]));
  fiat_secp256k1_dettman_mulx_u64(&x7, &x8, x5, UINT64_C(0x1000003d10));
  fiat_secp256k1_dettman_mulx_u64(&x9, &x10, x3, (arg1[2]));
  fiat_secp256k1_dettman_mulx_u64(&x11, &x12, x4, (arg1[3]));
  fiat_secp256k1_dettman_addcarryx_u64(&x13, &x14, 0x0, x11, x9);
  fiat_secp256k1_dettman_addcarryx_u64(&x15, &x16, x14, x12, x10);
  fiat_secp256k1_dettman_addcarryx_u64(&x17, &x18, 0x0, x13, x7);
  fiat_secp256k1_dettman_addcarryx_u64(&x19, &x20, x18, x15, x8);
  x21 = ((x17 >> 52) | ((x19 << 12) & UINT64_C(0xffffffffffffffff)));
  x22 = (x17 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x23, &x24, x6, UINT64_C(0x1000003d10000));
  fiat_secp256k1_dettman_mulx_u64(&x25, &x26, (arg1[2]), (arg1[2]));
  fiat_secp256k1_dettman_mulx_u64(&x27, &x28, x3, (arg1[3]));
  fiat_secp256k1_dettman_addcarryx_u64(&x29, &x30, 0x0, x27, x25);
  fiat_secp256k1_dettman_addcarryx_u64(&x31, &x32, x30, x28, x26);
  fiat_secp256k1_dettman_mulx_u64(&x33, &x34, x4, (arg1[4]));
  fiat_secp256k1_dettman_addcarryx_u64(&x35, &x36, 0x0, x33, x29);
  fiat_secp256k1_dettman_addcarryx_u64(&x37, &x38, x36, x34, x31);
  fiat_secp256k1_dettman_addcarryx_u64(&x39, &x40, 0x0, x35, x21);
  x41 = (x40 + x37);
  fiat_secp256k1_dettman_addcarryx_u64(&x42, &x43, 0x0, x39, x23);
  fiat_secp256k1_dettman_addcarryx_u64(&x44, &x45, x43, x41, x24);
  x46 = ((x42 >> 52) | ((x44 << 12) & UINT64_C(0xffffffffffffffff)));
  x47 = (x42 & UINT64_C(0xfffffffffffff));
  x48 = (x47 >> 48);
  x49 = (x47 & UINT64_C(0xffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x50, &x51, x2, (arg1[3]));
  fiat_secp256k1_dettman_mulx_u64(&x52, &x53, x3, (arg1[4]));
  fiat_secp256k1_dettman_addcarryx_u64(&x54, &x55, 0x0, x52, x50);
  fiat_secp256k1_dettman_addcarryx_u64(&x56, &x57, x55, x53, x51);
  fiat_secp256k1_dettman_addcarryx_u64(&x58, &x59, 0x0, x54, x46);
  x60 = (x59 + x56);
  x61 = ((x58 >> 52) | ((x60 << 12) & UINT64_C(0xffffffffffffffff)));
  x62 = (x58 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x63, &x64, ((x62 << 4) + x48),
                                  UINT64_C(0x1000003d1));
  fiat_secp256k1_dettman_mulx_u64(&x65, &x66, (arg1[0]), (arg1[0]));
  fiat_secp256k1_dettman_addcarryx_u64(&x67, &x68, 0x0, x65, x63);
  fiat_secp256k1_dettman_addcarryx_u64(&x69, &x70, x68, x66, x64);
  x71 = ((x67 >> 52) | ((x69 << 12) & UINT64_C(0xffffffffffffffff)));
  x72 = (x67 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x73, &x74, (arg1[3]), (arg1[3]));
  fiat_secp256k1_dettman_mulx_u64(&x75, &x76, x2, (arg1[4]));
  fiat_secp256k1_dettman_addcarryx_u64(&x77, &x78, 0x0, x75, x73);
  fiat_secp256k1_dettman_addcarryx_u64(&x79, &x80, x78, x76, x74);
  fiat_secp256k1_dettman_addcarryx_u64(&x81, &x82, 0x0, x77, x61);
  x83 = (x82 + x79);
  x84 = ((x81 >> 52) | ((x83 << 12) & UINT64_C(0xffffffffffffffff)));
  x85 = (x81 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x86, &x87, x85, UINT64_C(0x1000003d10));
  fiat_secp256k1_dettman_mulx_u64(&x88, &x89, x4, (arg1[1]));
  fiat_secp256k1_dettman_addcarryx_u64(&x90, &x91, 0x0, x88, x71);
  x92 = (x91 + x89);
  fiat_secp256k1_dettman_addcarryx_u64(&x93, &x94, 0x0, x90, x86);
  fiat_secp256k1_dettman_addcarryx_u64(&x95, &x96, x94, x92, x87);
  x97 = ((x93 >> 52) | ((x95 << 12) & UINT64_C(0xffffffffffffffff)));
  x98 = (x93 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x99, &x100, x1, (arg1[4]));
  fiat_secp256k1_dettman_addcarryx_u64(&x101, &x102, 0x0, x99, x84);
  x103 = (x102 + x100);
  fiat_secp256k1_dettman_mulx_u64(&x104, &x105, x101, UINT64_C(0x1000003d10));
  fiat_secp256k1_dettman_mulx_u64(&x106, &x107, (arg1[1]), (arg1[1]));
  fiat_secp256k1_dettman_mulx_u64(&x108, &x109, x4, (arg1[2]));
  fiat_secp256k1_dettman_addcarryx_u64(&x110, &x111, 0x0, x108, x106);
  fiat_secp256k1_dettman_addcarryx_u64(&x112, &x113, x111, x109, x107);
  fiat_secp256k1_dettman_addcarryx_u64(&x114, &x115, 0x0, x110, x97);
  x116 = (x115 + x112);
  fiat_secp256k1_dettman_addcarryx_u64(&x117, &x118, 0x0, x114, x104);
  fiat_secp256k1_dettman_addcarryx_u64(&x119, &x120, x118, x116, x105);
  x121 = ((x117 >> 52) | ((x119 << 12) & UINT64_C(0xffffffffffffffff)));
  x122 = (x117 & UINT64_C(0xfffffffffffff));
  fiat_secp256k1_dettman_mulx_u64(&x123, &x124, x103,
                                  UINT64_C(0x1000003d10000));
  fiat_secp256k1_dettman_addcarryx_u64(&x125, &x126, 0x0, (x22 + x121), x123);
  x127 = (x126 + x124);
  x128 = ((x125 >> 52) | ((x127 << 12) & UINT64_C(0xffffffffffffffff)));
  x129 = (x125 & UINT64_C(0xfffffffffffff));
  x130 = (x49 + x128);
  out1[0] = x72;
  out1[1] = x98;
  out1[2] = x122;
  out1[3] = x129;
  out1[4] = x130;
}