/* Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --inline --static --use-value-barrier secp256k1_dettman 64 5 52 '2^256 - 4294968273' 1 mul */
/* curve description: secp256k1_dettman */
/* machine_wordsize = 64 (from "64") */
/* requested operations: mul */
/* n = 5 (from "5") */
/* limbwidth = 52 (from "52") */
/* s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273") */
/* input magnitude: 1 (from "1") */
/*  */
/* Computed values: */
/*  */
/*  */

#include <stdint.h>
#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

FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION typedef signed __int128 fiat_secp256k1_dettman_int128;
FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION typedef unsigned __int128 fiat_secp256k1_dettman_uint128;

#if (-1 & 3) != 3
#error "This code only works on a two's complement system"
#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 ~> 0x1fffffffffffe]]
 */
void fiat_secp256k1_dettman_mul(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
  fiat_secp256k1_dettman_uint128 x1;
  uint64_t x2;
  uint64_t x3;
  fiat_secp256k1_dettman_uint128 x4;
  uint64_t x5;
  uint64_t x6;
  fiat_secp256k1_dettman_uint128 x7;
  uint64_t x8;
  uint64_t x9;
  uint64_t x10;
  uint64_t x11;
  fiat_secp256k1_dettman_uint128 x12;
  uint64_t x13;
  uint64_t x14;
  fiat_secp256k1_dettman_uint128 x15;
  uint64_t x16;
  uint64_t x17;
  fiat_secp256k1_dettman_uint128 x18;
  uint64_t x19;
  uint64_t x20;
  fiat_secp256k1_dettman_uint128 x21;
  uint64_t x22;
  uint64_t x23;
  fiat_secp256k1_dettman_uint128 x24;
  uint64_t x25;
  uint64_t x26;
  fiat_secp256k1_dettman_uint128 x27;
  uint64_t x28;
  uint64_t x29;
  fiat_secp256k1_dettman_uint128 x30;
  uint64_t x31;
  uint64_t x32;
  uint64_t x33;
  x1 = ((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[4]));
  x2 = (uint64_t)(x1 >> 52);
  x3 = (uint64_t)(x1 & UINT64_C(0xfffffffffffff));
  x4 = (((fiat_secp256k1_dettman_uint128)x3 * UINT64_C(0x1000003d10)) + (((((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[0])) + ((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[1]))) + ((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[2]))) + ((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[3]))));
  x5 = (uint64_t)(x4 >> 52);
  x6 = (uint64_t)(x4 & UINT64_C(0xfffffffffffff));
  x7 = (((fiat_secp256k1_dettman_uint128)x2 * UINT64_C(0x1000003d10)) + (x5 + ((((((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[0])) + ((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[1]))) + ((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[2]))) + ((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[3]))) + ((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[4])))));
  x8 = (uint64_t)(x7 >> 52);
  x9 = (uint64_t)(x7 & UINT64_C(0xfffffffffffff));
  x10 = (x9 >> 48);
  x11 = (x9 & UINT64_C(0xffffffffffff));
  x12 = (x8 + (((((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[1])) + ((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[2]))) + ((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[3]))) + ((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[4]))));
  x13 = (uint64_t)(x12 >> 52);
  x14 = (uint64_t)(x12 & UINT64_C(0xfffffffffffff));
  x15 = (((fiat_secp256k1_dettman_uint128)(x10 + (x14 << 4)) * UINT64_C(0x1000003d1)) + ((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[0])));
  x16 = (uint64_t)(x15 >> 52);
  x17 = (uint64_t)(x15 & UINT64_C(0xfffffffffffff));
  x18 = (x13 + ((((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[2])) + ((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[3]))) + ((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[4]))));
  x19 = (uint64_t)(x18 >> 52);
  x20 = (uint64_t)(x18 & UINT64_C(0xfffffffffffff));
  x21 = (((fiat_secp256k1_dettman_uint128)x20 * UINT64_C(0x1000003d10)) + (x16 + (((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[0])) + ((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[1])))));
  x22 = (uint64_t)(x21 >> 52);
  x23 = (uint64_t)(x21 & UINT64_C(0xfffffffffffff));
  x24 = (x19 + (((fiat_secp256k1_dettman_uint128)(arg1[4]) * (arg2[3])) + ((fiat_secp256k1_dettman_uint128)(arg1[3]) * (arg2[4]))));
  x25 = (uint64_t)(x24 >> 52);
  x26 = (uint64_t)(x24 & UINT64_C(0xfffffffffffff));
  x27 = (((fiat_secp256k1_dettman_uint128)x26 * UINT64_C(0x1000003d10)) + (x22 + ((((fiat_secp256k1_dettman_uint128)(arg1[2]) * (arg2[0])) + ((fiat_secp256k1_dettman_uint128)(arg1[1]) * (arg2[1]))) + ((fiat_secp256k1_dettman_uint128)(arg1[0]) * (arg2[2])))));
  x28 = (uint64_t)(x27 >> 52);
  x29 = (uint64_t)(x27 & UINT64_C(0xfffffffffffff));
  x30 = (((fiat_secp256k1_dettman_uint128)x25 * UINT64_C(0x1000003d10)) + (x28 + x6));
  x31 = (uint64_t)(x30 >> 52);
  x32 = (uint64_t)(x30 & UINT64_C(0xfffffffffffff));
  x33 = (x31 + x11);
  out1[0] = x17;
  out1[1] = x23;
  out1[2] = x29;
  out1[3] = x32;
  out1[4] = x33;
}

