Compiler Explorer

Source code

/* from header */
# if !defined(SECP256K1_GNUC_PREREQ)
#  if defined(__GNUC__)&&defined(__GNUC_MINOR__)
#   define SECP256K1_GNUC_PREREQ(_maj,_min) \
 ((__GNUC__<<16)+__GNUC_MINOR__>=((_maj)<<16)+(_min))
#  else
#   define SECP256K1_GNUC_PREREQ(_maj,_min) 0
#  endif
# endif

/* from util.h */

#ifndef SECP256K1_UTIL_H
#define SECP256K1_UTIL_H

#include <stdlib.h>
#include <stdint.h>
#include <stdio.h>
#include <limits.h>

#define STR_(x) #x
#define STR(x) STR_(x)
#define DEBUG_CONFIG_MSG(x) "DEBUG_CONFIG: " x
#define DEBUG_CONFIG_DEF(x) DEBUG_CONFIG_MSG(#x "=" STR(x))

/* Debug helper for printing arrays of unsigned char. */
#define PRINT_BUF(buf, len) do { \
    printf("%s[%lu] = ", #buf, (unsigned long)len); \
    print_buf_plain(buf, len); \
} while(0)

static void print_buf_plain(const unsigned char *buf, size_t len) {
    size_t i;
    printf("{");
    for (i = 0; i < len; i++) {
        if (i % 8 == 0) {
            printf("\n    ");
        } else {
            printf(" ");
        }
        printf("0x%02X,", buf[i]);
    }
    printf("\n}\n");
}

# if (!defined(__STDC_VERSION__) || (__STDC_VERSION__ < 199901L) )
#  if SECP256K1_GNUC_PREREQ(2,7)
#   define SECP256K1_INLINE __inline__
#  elif (defined(_MSC_VER))
#   define SECP256K1_INLINE __inline
#  else
#   define SECP256K1_INLINE
#  endif
# else
#  define SECP256K1_INLINE inline
# endif

/** Assert statically that expr is an integer constant expression, and run stmt.
 *
 * Useful for example to enforce that magnitude arguments are constant.
 */
#define ASSERT_INT_CONST_AND_DO(expr, stmt) do { \
    switch(42) { \
        case /* ERROR: integer argument is not constant */ expr: \
            break; \
        default: ; \
    } \
    stmt; \
} while(0)

typedef struct {
    void (*fn)(const char *text, void* data);
    const void* data;
} secp256k1_callback;

static SECP256K1_INLINE void secp256k1_callback_call(const secp256k1_callback * const cb, const char * const text) {
    cb->fn(text, (void*)cb->data);
}

#ifndef USE_EXTERNAL_DEFAULT_CALLBACKS
static void secp256k1_default_illegal_callback_fn(const char* str, void* data) {
    (void)data;
    fprintf(stderr, "[libsecp256k1] illegal argument: %s\n", str);
    abort();
}
static void secp256k1_default_error_callback_fn(const char* str, void* data) {
    (void)data;
    fprintf(stderr, "[libsecp256k1] internal consistency check failed: %s\n", str);
    abort();
}
#else
void secp256k1_default_illegal_callback_fn(const char* str, void* data);
void secp256k1_default_error_callback_fn(const char* str, void* data);
#endif

static const secp256k1_callback default_illegal_callback = {
    secp256k1_default_illegal_callback_fn,
    NULL
};

static const secp256k1_callback default_error_callback = {
    secp256k1_default_error_callback_fn,
    NULL
};

#ifdef DETERMINISTIC
#define TEST_FAILURE(msg) do { \
    fprintf(stderr, "%s\n", msg); \
    abort(); \
} while(0);
#else
#define TEST_FAILURE(msg) do { \
    fprintf(stderr, "%s:%d: %s\n", __FILE__, __LINE__, msg); \
    abort(); \
} while(0)
#endif

#if SECP256K1_GNUC_PREREQ(3, 0)
#define EXPECT(x,c) __builtin_expect((x),(c))
#else
#define EXPECT(x,c) (x)
#endif

#ifdef DETERMINISTIC
#define CHECK(cond) do { \
    if (EXPECT(!(cond), 0)) { \
        TEST_FAILURE("test condition failed"); \
    } \
} while(0)
#else
#define CHECK(cond) do { \
    if (EXPECT(!(cond), 0)) { \
        TEST_FAILURE("test condition failed: " #cond); \
    } \
} while(0)
#endif

/* Like assert(), but when VERIFY is defined, and side-effect safe. */
#if defined(COVERAGE)
#define VERIFY_CHECK(check)
#define VERIFY_SETUP(stmt)
#elif defined(VERIFY)
#define VERIFY_CHECK CHECK
#define VERIFY_SETUP(stmt) do { stmt; } while(0)
#else
#define VERIFY_CHECK(cond) do { (void)(cond); } while(0)
#define VERIFY_SETUP(stmt)
#endif

static SECP256K1_INLINE void *checked_malloc(const secp256k1_callback* cb, size_t size) {
    void *ret = malloc(size);
    if (ret == NULL) {
        secp256k1_callback_call(cb, "Out of memory");
    }
    return ret;
}

#if defined(__BIGGEST_ALIGNMENT__)
#define ALIGNMENT __BIGGEST_ALIGNMENT__
#else
/* Using 16 bytes alignment because common architectures never have alignment
 * requirements above 8 for any of the types we care about. In addition we
 * leave some room because currently we don't care about a few bytes. */
#define ALIGNMENT 16
#endif

#define ROUND_TO_ALIGN(size) ((((size) + ALIGNMENT - 1) / ALIGNMENT) * ALIGNMENT)

/* Macro for restrict, when available and not in a VERIFY build. */
#if defined(SECP256K1_BUILD) && defined(VERIFY)
# define SECP256K1_RESTRICT
#else
# if (!defined(__STDC_VERSION__) || (__STDC_VERSION__ < 199901L) )
#  if SECP256K1_GNUC_PREREQ(3,0)
#   define SECP256K1_RESTRICT __restrict__
#  elif (defined(_MSC_VER) && _MSC_VER >= 1400)
#   define SECP256K1_RESTRICT __restrict
#  else
#   define SECP256K1_RESTRICT
#  endif
# else
#  define SECP256K1_RESTRICT restrict
# endif
#endif

#if defined(_WIN32)
# define I64FORMAT "I64d"
# define I64uFORMAT "I64u"
#else
# define I64FORMAT "lld"
# define I64uFORMAT "llu"
#endif

#if defined(__GNUC__)
# define SECP256K1_GNUC_EXT __extension__
#else
# define SECP256K1_GNUC_EXT
#endif

/* Zero memory if flag == 1. Flag must be 0 or 1. Constant time. */
static SECP256K1_INLINE void secp256k1_memczero(void *s, size_t len, int flag) {
    unsigned char *p = (unsigned char *)s;
    /* Access flag with a volatile-qualified lvalue.
       This prevents clang from figuring out (after inlining) that flag can
       take only be 0 or 1, which leads to variable time code. */
    volatile int vflag = flag;
    unsigned char mask = -(unsigned char) vflag;
    while (len) {
        *p &= ~mask;
        p++;
        len--;
    }
}

/** Semantics like memcmp. Variable-time.
 *
 * We use this to avoid possible compiler bugs with memcmp, e.g.
 * https://gcc.gnu.org/bugzilla/show_bug.cgi?id=95189
 */
static SECP256K1_INLINE int secp256k1_memcmp_var(const void *s1, const void *s2, size_t n) {
    const unsigned char *p1 = s1, *p2 = s2;
    size_t i;

for (i = 0; i < n; i++) {
        int diff = p1[i] - p2[i];
        if (diff != 0) {
            return diff;
        }
    }
    return 0;
}

/** If flag is true, set *r equal to *a; otherwise leave it. Constant-time.  Both *r and *a must be initialized and non-negative.*/
static SECP256K1_INLINE void secp256k1_int_cmov(int *r, const int *a, int flag) {
    unsigned int mask0, mask1, r_masked, a_masked;
    /* Access flag with a volatile-qualified lvalue.
       This prevents clang from figuring out (after inlining) that flag can
       take only be 0 or 1, which leads to variable time code. */
    volatile int vflag = flag;

/* Casting a negative int to unsigned and back to int is implementation defined behavior */
    VERIFY_CHECK(*r >= 0 && *a >= 0);

mask0 = (unsigned int)vflag + ~0u;
    mask1 = ~mask0;
    r_masked = ((unsigned int)*r & mask0);
    a_masked = ((unsigned int)*a & mask1);

*r = (int)(r_masked | a_masked);
}

#if defined(USE_FORCE_WIDEMUL_INT128_STRUCT)
/* If USE_FORCE_WIDEMUL_INT128_STRUCT is set, use int128_struct. */
# define SECP256K1_WIDEMUL_INT128 1
# define SECP256K1_INT128_STRUCT 1
#elif defined(USE_FORCE_WIDEMUL_INT128)
/* If USE_FORCE_WIDEMUL_INT128 is set, use int128. */
# define SECP256K1_WIDEMUL_INT128 1
# define SECP256K1_INT128_NATIVE 1
#elif defined(USE_FORCE_WIDEMUL_INT64)
/* If USE_FORCE_WIDEMUL_INT64 is set, use int64. */
# define SECP256K1_WIDEMUL_INT64 1
#elif defined(UINT128_MAX) || defined(__SIZEOF_INT128__)
/* If a native 128-bit integer type exists, use int128. */
# define SECP256K1_WIDEMUL_INT128 1
# define SECP256K1_INT128_NATIVE 1
#elif defined(_MSC_VER) && (defined(_M_X64) || defined(_M_ARM64))
/* On 64-bit MSVC targets (x86_64 and arm64), use int128_struct
 * (which has special logic to implement using intrinsics on those systems). */
# define SECP256K1_WIDEMUL_INT128 1
# define SECP256K1_INT128_STRUCT 1
#elif SIZE_MAX > 0xffffffff
/* Systems with 64-bit pointers (and thus registers) very likely benefit from
 * using 64-bit based arithmetic (even if we need to fall back to 32x32->64 based
 * multiplication logic). */
# define SECP256K1_WIDEMUL_INT128 1
# define SECP256K1_INT128_STRUCT 1
#else
/* Lastly, fall back to int64 based arithmetic. */
# define SECP256K1_WIDEMUL_INT64 1
#endif

#ifndef __has_builtin
#define __has_builtin(x) 0
#endif

/* Determine the number of trailing zero bits in a (non-zero) 32-bit x.
 * This function is only intended to be used as fallback for
 * secp256k1_ctz32_var, but permits it to be tested separately. */
static SECP256K1_INLINE int secp256k1_ctz32_var_debruijn(uint32_t x) {
    static const uint8_t debruijn[32] = {
        0x00, 0x01, 0x02, 0x18, 0x03, 0x13, 0x06, 0x19, 0x16, 0x04, 0x14, 0x0A,
        0x10, 0x07, 0x0C, 0x1A, 0x1F, 0x17, 0x12, 0x05, 0x15, 0x09, 0x0F, 0x0B,
        0x1E, 0x11, 0x08, 0x0E, 0x1D, 0x0D, 0x1C, 0x1B
    };
    return debruijn[(uint32_t)((x & -x) * 0x04D7651FU) >> 27];
}

/* Determine the number of trailing zero bits in a (non-zero) 64-bit x.
 * This function is only intended to be used as fallback for
 * secp256k1_ctz64_var, but permits it to be tested separately. */
static SECP256K1_INLINE int secp256k1_ctz64_var_debruijn(uint64_t x) {
    static const uint8_t debruijn[64] = {
        0, 1, 2, 53, 3, 7, 54, 27, 4, 38, 41, 8, 34, 55, 48, 28,
        62, 5, 39, 46, 44, 42, 22, 9, 24, 35, 59, 56, 49, 18, 29, 11,
        63, 52, 6, 26, 37, 40, 33, 47, 61, 45, 43, 21, 23, 58, 17, 10,
        51, 25, 36, 32, 60, 20, 57, 16, 50, 31, 19, 15, 30, 14, 13, 12
    };
    return debruijn[(uint64_t)((x & -x) * 0x022FDD63CC95386DU) >> 58];
}

/* Determine the number of trailing zero bits in a (non-zero) 32-bit x. */
static SECP256K1_INLINE int secp256k1_ctz32_var(uint32_t x) {
    VERIFY_CHECK(x != 0);
#if (__has_builtin(__builtin_ctz) || SECP256K1_GNUC_PREREQ(3,4))
    /* If the unsigned type is sufficient to represent the largest uint32_t, consider __builtin_ctz. */
    if (((unsigned)UINT32_MAX) == UINT32_MAX) {
        return __builtin_ctz(x);
    }
#endif
#if (__has_builtin(__builtin_ctzl) || SECP256K1_GNUC_PREREQ(3,4))
    /* Otherwise consider __builtin_ctzl (the unsigned long type is always at least 32 bits). */
    return __builtin_ctzl(x);
#else
    /* If no suitable CTZ builtin is available, use a (variable time) software emulation. */
    return secp256k1_ctz32_var_debruijn(x);
#endif
}

/* Determine the number of trailing zero bits in a (non-zero) 64-bit x. */
static SECP256K1_INLINE int secp256k1_ctz64_var(uint64_t x) {
    VERIFY_CHECK(x != 0);
#if (__has_builtin(__builtin_ctzl) || SECP256K1_GNUC_PREREQ(3,4))
    /* If the unsigned long type is sufficient to represent the largest uint64_t, consider __builtin_ctzl. */
    if (((unsigned long)UINT64_MAX) == UINT64_MAX) {
        return __builtin_ctzl(x);
    }
#endif
#if (__has_builtin(__builtin_ctzll) || SECP256K1_GNUC_PREREQ(3,4))
    /* Otherwise consider __builtin_ctzll (the unsigned long long type is always at least 64 bits). */
    return __builtin_ctzll(x);
#else
    /* If no suitable CTZ builtin is available, use a (variable time) software emulation. */
    return secp256k1_ctz64_var_debruijn(x);
#endif
}

/* Read a uint32_t in big endian */
SECP256K1_INLINE static uint32_t secp256k1_read_be32(const unsigned char* p) {
    return (uint32_t)p[0] << 24 |
           (uint32_t)p[1] << 16 |
           (uint32_t)p[2] << 8  |
           (uint32_t)p[3];
}

/* Write a uint32_t in big endian */
SECP256K1_INLINE static void secp256k1_write_be32(unsigned char* p, uint32_t x) {
    p[3] = x;
    p[2] = x >>  8;
    p[1] = x >> 16;
    p[0] = x >> 24;
}

/* Read a uint64_t in big endian */
SECP256K1_INLINE static uint64_t secp256k1_read_be64(const unsigned char* p) {
    return (uint64_t)p[0] << 56 |
           (uint64_t)p[1] << 48 |
           (uint64_t)p[2] << 40 |
           (uint64_t)p[3] << 32 |
           (uint64_t)p[4] << 24 |
           (uint64_t)p[5] << 16 |
           (uint64_t)p[6] << 8  |
           (uint64_t)p[7];
}

/* Write a uint64_t in big endian */
SECP256K1_INLINE static void secp256k1_write_be64(unsigned char* p, uint64_t x) {
    p[7] = x;
    p[6] = x >>  8;
    p[5] = x >> 16;
    p[4] = x >> 24;
    p[3] = x >> 32;
    p[2] = x >> 40;
    p[1] = x >> 48;
    p[0] = x >> 56;
}

#endif /* SECP256K1_UTIL_H */

/* from uint128_native.h */
#ifndef SECP256K1_INT128_NATIVE_H
#define SECP256K1_INT128_NATIVE_H

#include <stdint.h>

#if !defined(UINT128_MAX) && defined(__SIZEOF_INT128__)
SECP256K1_GNUC_EXT typedef unsigned __int128 uint128_t;
SECP256K1_GNUC_EXT typedef __int128 int128_t;
# define UINT128_MAX ((uint128_t)(-1))
# define INT128_MAX ((int128_t)(UINT128_MAX >> 1))
# define INT128_MIN (-INT128_MAX - 1)
/* No (U)INT128_C macros because compilers providing __int128 do not support 128-bit literals.  */
#endif

typedef uint128_t secp256k1_uint128;
typedef int128_t secp256k1_int128;

#endif

/* from uint128_native_impl.h */
#ifndef SECP256K1_INT128_NATIVE_IMPL_H
#define SECP256K1_INT128_NATIVE_IMPL_H

static SECP256K1_INLINE void secp256k1_u128_load(secp256k1_uint128 *r, uint64_t hi, uint64_t lo) {
    *r = (((uint128_t)hi) << 64) + lo;
}

static SECP256K1_INLINE void secp256k1_u128_mul(secp256k1_uint128 *r, uint64_t a, uint64_t b) {
   *r = (uint128_t)a * b;
}

static SECP256K1_INLINE void secp256k1_u128_accum_mul(secp256k1_uint128 *r, uint64_t a, uint64_t b) {
   *r += (uint128_t)a * b;
}

static SECP256K1_INLINE void secp256k1_u128_accum_u64(secp256k1_uint128 *r, uint64_t a) {
   *r += a;
}

static SECP256K1_INLINE void secp256k1_u128_accum(secp256k1_uint128 *r, secp256k1_uint128 *a){
   *r += *a;
}

static SECP256K1_INLINE void secp256k1_u128_rshift(secp256k1_uint128 *r, unsigned int n) {
   VERIFY_CHECK(n < 128);
   *r >>= n;
}

static SECP256K1_INLINE uint64_t secp256k1_u128_to_u64(const secp256k1_uint128 *a) {
   return (uint64_t)(*a);
}

static SECP256K1_INLINE uint64_t secp256k1_u128_hi_u64(const secp256k1_uint128 *a) {
   return (uint64_t)(*a >> 64);
}

static SECP256K1_INLINE void secp256k1_u128_from_u64(secp256k1_uint128 *r, uint64_t a) {
   *r = a;
}

static SECP256K1_INLINE int secp256k1_u128_check_bits(const secp256k1_uint128 *r, unsigned int n) {
   VERIFY_CHECK(n < 128);
   return (*r >> n == 0);
}

static SECP256K1_INLINE void secp256k1_i128_load(secp256k1_int128 *r, int64_t hi, uint64_t lo) {
    *r = (((uint128_t)(uint64_t)hi) << 64) + lo;
}

static SECP256K1_INLINE void secp256k1_i128_mul(secp256k1_int128 *r, int64_t a, int64_t b) {
   *r = (int128_t)a * b;
}

static SECP256K1_INLINE void secp256k1_i128_accum_mul(secp256k1_int128 *r, int64_t a, int64_t b) {
   int128_t ab = (int128_t)a * b;
   VERIFY_CHECK(0 <= ab ? *r <= INT128_MAX - ab : INT128_MIN - ab <= *r);
   *r += ab;
}

static SECP256K1_INLINE void secp256k1_i128_det(secp256k1_int128 *r, int64_t a, int64_t b, int64_t c, int64_t d) {
   int128_t ad = (int128_t)a * d;
   int128_t bc = (int128_t)b * c;
   VERIFY_CHECK(0 <= bc ? INT128_MIN + bc <= ad : ad <= INT128_MAX + bc);
   *r = ad - bc;
}

static SECP256K1_INLINE void secp256k1_i128_rshift(secp256k1_int128 *r, unsigned int n) {
   VERIFY_CHECK(n < 128);
   *r >>= n;
}

static SECP256K1_INLINE uint64_t secp256k1_i128_to_u64(const secp256k1_int128 *a) {
   return (uint64_t)*a;
}

static SECP256K1_INLINE int64_t secp256k1_i128_to_i64(const secp256k1_int128 *a) {
   VERIFY_CHECK(INT64_MIN <= *a && *a <= INT64_MAX);
   return *a;
}

static SECP256K1_INLINE void secp256k1_i128_from_i64(secp256k1_int128 *r, int64_t a) {
   *r = a;
}

static SECP256K1_INLINE int secp256k1_i128_eq_var(const secp256k1_int128 *a, const secp256k1_int128 *b) {
   return *a == *b;
}

static SECP256K1_INLINE int secp256k1_i128_check_pow2(const secp256k1_int128 *r, unsigned int n, int sign) {
   VERIFY_CHECK(n < 127);
   VERIFY_CHECK(sign == 1 || sign == -1);
   return (*r == (int128_t)((uint128_t)sign << n));
}

#endif

/* rest */

#ifndef SECP256K1_FIELD_INNER5X52_IMPL_H
#define SECP256K1_FIELD_INNER5X52_IMPL_H

#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

static FIAT_SECP256K1_DETTMAN_FIAT_INLINE secp256k1_uint128 u128_mul_u64_u64(uint64_t a, uint64_t b) {
  secp256k1_uint128 r;
  secp256k1_u128_mul(&r, a, b);
  return r;
}

static FIAT_SECP256K1_DETTMAN_FIAT_INLINE uint64_t u64_shr_u128(secp256k1_uint128 a, unsigned int n) {
  secp256k1_uint128 r = a;
  secp256k1_u128_rshift(&r, n);
  return secp256k1_u128_to_u64(&r);
}

static FIAT_SECP256K1_DETTMAN_FIAT_INLINE uint64_t u64_and_u128_u64(secp256k1_uint128 a, uint64_t b) {
  return secp256k1_u128_to_u64(&a) & b;
}

static FIAT_SECP256K1_DETTMAN_FIAT_INLINE secp256k1_uint128 u128_add_u128_u128(secp256k1_uint128 a, secp256k1_uint128 b) {
  secp256k1_uint128 r = a;

secp256k1_u128_accum(&r, &b);

return r;
}
static FIAT_SECP256K1_DETTMAN_FIAT_INLINE secp256k1_uint128 u128_add_u64_u128(uint64_t a, secp256k1_uint128 b) {
  secp256k1_uint128 r = b;
  secp256k1_u128_accum_u64(&r, a);
  return r;
}

/* Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --inline --static -use-value-barrier secp256k1_dettman 64 5 48 2 '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")
 * last_reduction = 2 (from "2")
 * s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273")
 * inbounds_multiplier: None (from "")
 */

typedef secp256k1_uint128 fiat_secp256k1_dettman_uint128;

#define secp256k1_fe_sqr_inner fiat_secp256k1_dettman_square
#define secp256k1_fe_mul_inner fiat_secp256k1_dettman_mul

#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 ~> 0x17fffffffffff]]
 */
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;
  fiat_secp256k1_dettman_uint128 x10;
  uint64_t x11;
  uint64_t 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 = u128_mul_u64_u64((arg1[4]), (arg2[4]));
  x2 = u64_shr_u128(x1, 64);
  x3 = u64_and_u128_u64(x1, UINT64_C(0xffffffffffffffff));
  x4 = u128_add_u128_u128(u128_add_u128_u128(u128_mul_u64_u64((arg1[0]), (arg2[3])), u128_add_u128_u128(u128_mul_u64_u64((arg1[1]), (arg2[2])), u128_add_u128_u128(u128_mul_u64_u64((arg1[2]), (arg2[1])), u128_mul_u64_u64((arg1[3]), (arg2[0]))))), u128_mul_u64_u64(x3, UINT64_C(0x1000003d10)));
  x5 = u64_shr_u128(x4, 52);
  x6 = u64_and_u128_u64(x4, UINT64_C(0xfffffffffffff));
  x7 = u128_add_u128_u128(u128_add_u64_u128(x5, u128_add_u128_u128(u128_mul_u64_u64((arg1[0]), (arg2[4])), u128_add_u128_u128(u128_mul_u64_u64((arg1[1]), (arg2[3])), u128_add_u128_u128(u128_mul_u64_u64((arg1[2]), (arg2[2])), u128_add_u128_u128(u128_mul_u64_u64((arg1[3]), (arg2[1])), u128_mul_u64_u64((arg1[4]), (arg2[0]))))))), u128_mul_u64_u64(x2, UINT64_C(0x1000003d10000)));
  x8 = u64_shr_u128(x7, 52);
  x9 = u64_and_u128_u64(x7, UINT64_C(0xfffffffffffff));
  x10 = u128_add_u64_u128(x8, u128_add_u128_u128(u128_mul_u64_u64((arg1[1]), (arg2[4])), u128_add_u128_u128(u128_mul_u64_u64((arg1[2]), (arg2[3])), u128_add_u128_u128(u128_mul_u64_u64((arg1[3]), (arg2[2])), u128_mul_u64_u64((arg1[4]), (arg2[1]))))));
  x11 = u64_shr_u128(x10, 52);
  x12 = u64_and_u128_u64(x10, UINT64_C(0xfffffffffffff));
  x13 = (x9 >> 48);
  x14 = (x9 & UINT64_C(0xffffffffffff));
  x15 = u128_add_u128_u128(u128_mul_u64_u64((arg1[0]), (arg2[0])), u128_mul_u64_u64((x13 + (x12 << 4)), UINT64_C(0x1000003d1)));
  x16 = u64_shr_u128(x15, 52);
  x17 = u64_and_u128_u64(x15, UINT64_C(0xfffffffffffff));
  x18 = u128_add_u64_u128(x11, u128_add_u128_u128(u128_mul_u64_u64((arg1[2]), (arg2[4])), u128_add_u128_u128(u128_mul_u64_u64((arg1[3]), (arg2[3])), u128_mul_u64_u64((arg1[4]), (arg2[2])))));
  x19 = u64_shr_u128(x18, 52);
  /* x19 = x18 >> 52; */
  x20 = u64_and_u128_u64(x18, UINT64_C(0xfffffffffffff));
  x21 = u128_add_u128_u128(u128_add_u64_u128(x16, u128_add_u128_u128(u128_mul_u64_u64((arg1[0]), (arg2[1])), u128_mul_u64_u64((arg1[1]), (arg2[0])))), u128_mul_u64_u64(x20, UINT64_C(0x1000003d10)));
  x22 = u64_shr_u128(x21, 52);
  x23 = u64_and_u128_u64(x21, UINT64_C(0xfffffffffffff));
  x24 = u128_add_u64_u128(x19, u128_add_u128_u128(u128_mul_u64_u64((arg1[3]), (arg2[4])), u128_mul_u64_u64((arg1[4]), (arg2[3]))));
  x25 = u64_shr_u128(x24, 64);
  x26 = u64_and_u128_u64(x24, UINT64_C(0xffffffffffffffff));
  x27 = u128_add_u128_u128(u128_add_u64_u128(x22, u128_add_u128_u128(u128_mul_u64_u64((arg1[0]), (arg2[2])), u128_add_u128_u128(u128_mul_u64_u64((arg1[1]), (arg2[1])), u128_mul_u64_u64((arg1[2]), (arg2[0]))))), u128_mul_u64_u64(x26, UINT64_C(0x1000003d10)));
  x28 = u64_shr_u128(x27, 52);
  x29 = u64_and_u128_u64(x27, UINT64_C(0xfffffffffffff));
  x30 = u128_add_u64_u128((x28 + x6), u128_mul_u64_u64(x25, UINT64_C(0x1000003d10000)));
  x31 = u64_shr_u128(x30, 52);
  x32 = u64_and_u128_u64(x30, UINT64_C(0xfffffffffffff));
  x33 = (x31 + x14);
  out1[0] = x17;
  out1[1] = x23;
  out1[2] = x29;
  out1[3] = x32;
  out1[4] = x33;
}

/*
 * 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 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;
  fiat_secp256k1_dettman_uint128 x5;
  uint64_t x6;
  uint64_t x7;
  fiat_secp256k1_dettman_uint128 x8;
  uint64_t x9;
  uint64_t x10;
  fiat_secp256k1_dettman_uint128 x11;
  uint64_t x12;
  uint64_t x13;
  fiat_secp256k1_dettman_uint128 x14;
  uint64_t x15;
  uint64_t x16;
  uint64_t x17;
  uint64_t x18;
  fiat_secp256k1_dettman_uint128 x19;
  uint64_t x20;
  uint64_t x21;
  fiat_secp256k1_dettman_uint128 x22;
  uint64_t x23;
  uint64_t x24;
  fiat_secp256k1_dettman_uint128 x25;
  uint64_t x26;
  uint64_t x27;
  fiat_secp256k1_dettman_uint128 x28;
  uint64_t x29;
  uint64_t x30;
  fiat_secp256k1_dettman_uint128 x31;
  uint64_t x32;
  uint64_t x33;
  fiat_secp256k1_dettman_uint128 x34;
  uint64_t x35;
  uint64_t x36;
  uint64_t x37;
  x1 = ((arg1[3]) * 0x2);
  x2 = ((arg1[2]) * 0x2);
  x3 = ((arg1[1]) * 0x2);
  x4 = ((arg1[0]) * 0x2);
  x5 = u128_mul_u64_u64((arg1[4]), (arg1[4]));
  x6 = u64_shr_u128(x5, 64);
  x7 = u64_and_u128_u64(x5, UINT64_C(0xffffffffffffffff));
  x8 = u128_add_u128_u128(u128_add_u128_u128(u128_mul_u64_u64(x4, (arg1[3])), u128_mul_u64_u64(x3, (arg1[2]))), u128_mul_u64_u64(x7, UINT64_C(0x1000003d10)));
  x9 = u64_shr_u128(x8, 52);
  x10 = u64_and_u128_u64(x8, UINT64_C(0xfffffffffffff));
  x11 = u128_add_u128_u128(u128_add_u64_u128(x9, u128_add_u128_u128(u128_mul_u64_u64(x4, (arg1[4])), u128_add_u128_u128(u128_mul_u64_u64(x3, (arg1[3])), u128_mul_u64_u64((arg1[2]), (arg1[2]))))), u128_mul_u64_u64(x6, UINT64_C(0x1000003d10000)));
  x12 = u64_shr_u128(x11, 52);
  x13 = u64_and_u128_u64(x11, UINT64_C(0xfffffffffffff));
  x14 = u128_add_u64_u128(x12, u128_add_u128_u128(u128_mul_u64_u64(x3, (arg1[4])), u128_mul_u64_u64(x2, (arg1[3]))));
  x15 = u64_shr_u128(x14, 52);
  x16 = u64_and_u128_u64(x14, UINT64_C(0xfffffffffffff));
  x17 = (x13 >> 48);
  x18 = (x13 & UINT64_C(0xffffffffffff));
  x19 = u128_add_u128_u128(u128_mul_u64_u64((arg1[0]), (arg1[0])), u128_mul_u64_u64((x17 + (x16 << 4)), UINT64_C(0x1000003d1)));
  x20 = u64_shr_u128(x19, 52);
  x21 = u64_and_u128_u64(x19, UINT64_C(0xfffffffffffff));
  x22 = u128_add_u64_u128(x15, u128_add_u128_u128(u128_mul_u64_u64(x2, (arg1[4])), u128_mul_u64_u64((arg1[3]), (arg1[3]))));
  x23 = u64_shr_u128(x22, 52);
  x24 = u64_and_u128_u64(x22, UINT64_C(0xfffffffffffff));
  x25 = u128_add_u128_u128(u128_add_u64_u128(x20, u128_mul_u64_u64(x4, (arg1[1]))), u128_mul_u64_u64(x24, UINT64_C(0x1000003d10)));
  x26 = u64_shr_u128(x25, 52);
  x27 = u64_and_u128_u64(x25, UINT64_C(0xfffffffffffff));
  x28 = u128_add_u64_u128(x23, u128_mul_u64_u64(x1, (arg1[4])));
  x29 = u64_shr_u128(x28, 64);
  x30 = u64_and_u128_u64(x28, UINT64_C(0xffffffffffffffff));
  x31 = u128_add_u128_u128(u128_add_u64_u128(x26, u128_add_u128_u128(u128_mul_u64_u64(x4, (arg1[2])), u128_mul_u64_u64((arg1[1]), (arg1[1])))), u128_mul_u64_u64(x30, UINT64_C(0x1000003d10)));
  x32 = u64_shr_u128(x31, 52);
  x33 = u64_and_u128_u64(x31, UINT64_C(0xfffffffffffff));
  x34 = u128_add_u64_u128((x32 + x10), u128_mul_u64_u64(x29, UINT64_C(0x1000003d10000)));
  x35 = u64_shr_u128(x34, 52);
  x36 = u64_and_u128_u64(x34, UINT64_C(0xfffffffffffff));
  x37 = (x35 + x18);
  out1[0] = x21;
  out1[1] = x27;
  out1[2] = x33;
  out1[3] = x36;
  out1[4] = x37;
}

#endif /* SECP256K1_FIELD_INNER5X52_IMPL_H */

/***********************************************************************
 * Copyright (c) 2013, 2014 Pieter Wuille                              *
 * Distributed under the MIT software license, see the accompanying    *
 * file COPYING or https://www.opensource.org/licenses/mit-license.php.*
 ***********************************************************************/

#include <stdint.h>

#ifdef VERIFY
#define VERIFY_BITS(x, n) VERIFY_CHECK(((x) >> (n)) == 0)
#define VERIFY_BITS_128(x, n) VERIFY_CHECK(secp256k1_u128_check_bits((x), (n)))
#else
#define VERIFY_BITS(x, n) do { } while(0)
#define VERIFY_BITS_128(x, n) do { } while(0)
#endif

void secp256k1_fe_mul_inner_orig(uint64_t *r, const uint64_t *a, const uint64_t * SECP256K1_RESTRICT b) {
    secp256k1_uint128 c, d;
    uint64_t t3, t4, tx, u0;
    uint64_t a0 = a[0], a1 = a[1], a2 = a[2], a3 = a[3], a4 = a[4];
    const uint64_t M = 0xFFFFFFFFFFFFFULL, R = 0x1000003D10ULL;

VERIFY_BITS(a[0], 56);
    VERIFY_BITS(a[1], 56);
    VERIFY_BITS(a[2], 56);
    VERIFY_BITS(a[3], 56);
    VERIFY_BITS(a[4], 52);
    VERIFY_BITS(b[0], 56);
    VERIFY_BITS(b[1], 56);
    VERIFY_BITS(b[2], 56);
    VERIFY_BITS(b[3], 56);
    VERIFY_BITS(b[4], 52);
    VERIFY_CHECK(r != b);
    VERIFY_CHECK(a != b);

/*  [... a b c] is a shorthand for ... + a<<104 + b<<52 + c<<0 mod n.
     *  for 0 <= x <= 4, px is a shorthand for sum(a[i]*b[x-i], i=0..x).
     *  for 4 <= x <= 8, px is a shorthand for sum(a[i]*b[x-i], i=(x-4)..4)
     *  Note that [x 0 0 0 0 0] = [x*R].
     */

secp256k1_u128_mul(&d, a0, b[3]);
    secp256k1_u128_accum_mul(&d, a1, b[2]);
    secp256k1_u128_accum_mul(&d, a2, b[1]);
    secp256k1_u128_accum_mul(&d, a3, b[0]);
    VERIFY_BITS_128(&d, 114);
    /* [d 0 0 0] = [p3 0 0 0] */
    secp256k1_u128_mul(&c, a4, b[4]);
    VERIFY_BITS_128(&c, 112);
    /* [c 0 0 0 0 d 0 0 0] = [p8 0 0 0 0 p3 0 0 0] */
    secp256k1_u128_accum_mul(&d, R, secp256k1_u128_to_u64(&c)); secp256k1_u128_rshift(&c, 64);
    VERIFY_BITS_128(&d, 115);
    VERIFY_BITS_128(&c, 48);
    /* [(c<<12) 0 0 0 0 0 d 0 0 0] = [p8 0 0 0 0 p3 0 0 0] */
    t3 = secp256k1_u128_to_u64(&d) & M; secp256k1_u128_rshift(&d, 52);
    VERIFY_BITS(t3, 52);
    VERIFY_BITS_128(&d, 63);
    /* [(c<<12) 0 0 0 0 d t3 0 0 0] = [p8 0 0 0 0 p3 0 0 0] */

secp256k1_u128_accum_mul(&d, a0, b[4]);
    secp256k1_u128_accum_mul(&d, a1, b[3]);
    secp256k1_u128_accum_mul(&d, a2, b[2]);
    secp256k1_u128_accum_mul(&d, a3, b[1]);
    secp256k1_u128_accum_mul(&d, a4, b[0]);
    VERIFY_BITS_128(&d, 115);
    /* [(c<<12) 0 0 0 0 d t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0] */
    secp256k1_u128_accum_mul(&d, R << 12, secp256k1_u128_to_u64(&c));
    VERIFY_BITS_128(&d, 116);
    /* [d t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0] */
    t4 = secp256k1_u128_to_u64(&d) & M; secp256k1_u128_rshift(&d, 52);
    VERIFY_BITS(t4, 52);
    VERIFY_BITS_128(&d, 64);
    /* [d t4 t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0] */
    tx = (t4 >> 48); t4 &= (M >> 4);
    VERIFY_BITS(tx, 4);
    VERIFY_BITS(t4, 48);
    /* [d t4+(tx<<48) t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0] */

secp256k1_u128_mul(&c, a0, b[0]);
    VERIFY_BITS_128(&c, 112);
    /* [d t4+(tx<<48) t3 0 0 c] = [p8 0 0 0 p4 p3 0 0 p0] */
    secp256k1_u128_accum_mul(&d, a1, b[4]);
    secp256k1_u128_accum_mul(&d, a2, b[3]);
    secp256k1_u128_accum_mul(&d, a3, b[2]);
    secp256k1_u128_accum_mul(&d, a4, b[1]);
    VERIFY_BITS_128(&d, 115);
    /* [d t4+(tx<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    u0 = secp256k1_u128_to_u64(&d) & M; secp256k1_u128_rshift(&d, 52);
    VERIFY_BITS(u0, 52);
    VERIFY_BITS_128(&d, 63);
    /* [d u0 t4+(tx<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    /* [d 0 t4+(tx<<48)+(u0<<52) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    u0 = (u0 << 4) | tx;
    VERIFY_BITS(u0, 56);
    /* [d 0 t4+(u0<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    secp256k1_u128_accum_mul(&c, u0, R >> 4);
    VERIFY_BITS_128(&c, 115);
    /* [d 0 t4 t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    r[0] = secp256k1_u128_to_u64(&c) & M; secp256k1_u128_rshift(&c, 52);
    VERIFY_BITS(r[0], 52);
    VERIFY_BITS_128(&c, 61);
    /* [d 0 t4 t3 0 c r0] = [p8 0 0 p5 p4 p3 0 0 p0] */

secp256k1_u128_accum_mul(&c, a0, b[1]);
    secp256k1_u128_accum_mul(&c, a1, b[0]);
    VERIFY_BITS_128(&c, 114);
    /* [d 0 t4 t3 0 c r0] = [p8 0 0 p5 p4 p3 0 p1 p0] */
    secp256k1_u128_accum_mul(&d, a2, b[4]);
    secp256k1_u128_accum_mul(&d, a3, b[3]);
    secp256k1_u128_accum_mul(&d, a4, b[2]);
    VERIFY_BITS_128(&d, 114);
    /* [d 0 t4 t3 0 c r0] = [p8 0 p6 p5 p4 p3 0 p1 p0] */
    secp256k1_u128_accum_mul(&c, secp256k1_u128_to_u64(&d) & M, R); secp256k1_u128_rshift(&d, 52);
    VERIFY_BITS_128(&c, 115);
    VERIFY_BITS_128(&d, 62);
    /* [d 0 0 t4 t3 0 c r0] = [p8 0 p6 p5 p4 p3 0 p1 p0] */
    r[1] = secp256k1_u128_to_u64(&c) & M; secp256k1_u128_rshift(&c, 52);
    VERIFY_BITS(r[1], 52);
    VERIFY_BITS_128(&c, 63);
    /* [d 0 0 t4 t3 c r1 r0] = [p8 0 p6 p5 p4 p3 0 p1 p0] */

secp256k1_u128_accum_mul(&c, a0, b[2]);
    secp256k1_u128_accum_mul(&c, a1, b[1]);
    secp256k1_u128_accum_mul(&c, a2, b[0]);
    VERIFY_BITS_128(&c, 114);
    /* [d 0 0 t4 t3 c r1 r0] = [p8 0 p6 p5 p4 p3 p2 p1 p0] */
    secp256k1_u128_accum_mul(&d, a3, b[4]);
    secp256k1_u128_accum_mul(&d, a4, b[3]);
    VERIFY_BITS_128(&d, 114);
    /* [d 0 0 t4 t3 c t1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
    secp256k1_u128_accum_mul(&c, R, secp256k1_u128_to_u64(&d)); secp256k1_u128_rshift(&d, 64);
    VERIFY_BITS_128(&c, 115);
    VERIFY_BITS_128(&d, 50);
    /* [(d<<12) 0 0 0 t4 t3 c r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */

r[2] = secp256k1_u128_to_u64(&c) & M; secp256k1_u128_rshift(&c, 52);
    VERIFY_BITS(r[2], 52);
    VERIFY_BITS_128(&c, 63);
    /* [(d<<12) 0 0 0 t4 t3+c r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
    secp256k1_u128_accum_mul(&c, R << 12, secp256k1_u128_to_u64(&d));
    secp256k1_u128_accum_u64(&c, t3);
    VERIFY_BITS_128(&c, 100);
    /* [t4 c r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
    r[3] = secp256k1_u128_to_u64(&c) & M; secp256k1_u128_rshift(&c, 52);
    VERIFY_BITS(r[3], 52);
    VERIFY_BITS_128(&c, 48);
    /* [t4+c r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
    r[4] = secp256k1_u128_to_u64(&c) + t4;
    VERIFY_BITS(r[4], 49);
    /* [r4 r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
}

static void secp256k1_fe_sqr_inner_orig(uint64_t *r, const uint64_t *a) {
    secp256k1_uint128 c, d;
    uint64_t a0 = a[0], a1 = a[1], a2 = a[2], a3 = a[3], a4 = a[4];
    int64_t t3, t4, tx, u0;
    const uint64_t M = 0xFFFFFFFFFFFFFULL, R = 0x1000003D10ULL;

VERIFY_BITS(a[0], 56);
    VERIFY_BITS(a[1], 56);
    VERIFY_BITS(a[2], 56);
    VERIFY_BITS(a[3], 56);
    VERIFY_BITS(a[4], 52);

/**  [... a b c] is a shorthand for ... + a<<104 + b<<52 + c<<0 mod n.
     *  px is a shorthand for sum(a[i]*a[x-i], i=0..x).
     *  Note that [x 0 0 0 0 0] = [x*R].
     */

secp256k1_u128_mul(&d, a0*2, a3);
    secp256k1_u128_accum_mul(&d, a1*2, a2);
    VERIFY_BITS_128(&d, 114);
    /* [d 0 0 0] = [p3 0 0 0] */
    secp256k1_u128_mul(&c, a4, a4);
    VERIFY_BITS_128(&c, 112);
    /* [c 0 0 0 0 d 0 0 0] = [p8 0 0 0 0 p3 0 0 0] */
    secp256k1_u128_accum_mul(&d, R, secp256k1_u128_to_u64(&c)); secp256k1_u128_rshift(&c, 64);
    VERIFY_BITS_128(&d, 115);
    VERIFY_BITS_128(&c, 48);
    /* [(c<<12) 0 0 0 0 0 d 0 0 0] = [p8 0 0 0 0 p3 0 0 0] */
    t3 = secp256k1_u128_to_u64(&d) & M; secp256k1_u128_rshift(&d, 52);
    VERIFY_BITS(t3, 52);
    VERIFY_BITS_128(&d, 63);
    /* [(c<<12) 0 0 0 0 d t3 0 0 0] = [p8 0 0 0 0 p3 0 0 0] */

a4 *= 2;
    secp256k1_u128_accum_mul(&d, a0, a4);
    secp256k1_u128_accum_mul(&d, a1*2, a3);
    secp256k1_u128_accum_mul(&d, a2, a2);
    VERIFY_BITS_128(&d, 115);
    /* [(c<<12) 0 0 0 0 d t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0] */
    secp256k1_u128_accum_mul(&d, R << 12, secp256k1_u128_to_u64(&c));
    VERIFY_BITS_128(&d, 116);
    /* [d t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0] */
    t4 = secp256k1_u128_to_u64(&d) & M; secp256k1_u128_rshift(&d, 52);
    VERIFY_BITS(t4, 52);
    VERIFY_BITS_128(&d, 64);
    /* [d t4 t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0] */
    tx = (t4 >> 48); t4 &= (M >> 4);
    VERIFY_BITS(tx, 4);
    VERIFY_BITS(t4, 48);
    /* [d t4+(tx<<48) t3 0 0 0] = [p8 0 0 0 p4 p3 0 0 0] */

secp256k1_u128_mul(&c, a0, a0);
    VERIFY_BITS_128(&c, 112);
    /* [d t4+(tx<<48) t3 0 0 c] = [p8 0 0 0 p4 p3 0 0 p0] */
    secp256k1_u128_accum_mul(&d, a1, a4);
    secp256k1_u128_accum_mul(&d, a2*2, a3);
    VERIFY_BITS_128(&d, 114);
    /* [d t4+(tx<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    u0 = secp256k1_u128_to_u64(&d) & M; secp256k1_u128_rshift(&d, 52);
    VERIFY_BITS(u0, 52);
    VERIFY_BITS_128(&d, 62);
    /* [d u0 t4+(tx<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    /* [d 0 t4+(tx<<48)+(u0<<52) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    u0 = (u0 << 4) | tx;
    VERIFY_BITS(u0, 56);
    /* [d 0 t4+(u0<<48) t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    secp256k1_u128_accum_mul(&c, u0, R >> 4);
    VERIFY_BITS_128(&c, 113);
    /* [d 0 t4 t3 0 0 c] = [p8 0 0 p5 p4 p3 0 0 p0] */
    r[0] = secp256k1_u128_to_u64(&c) & M; secp256k1_u128_rshift(&c, 52);
    VERIFY_BITS(r[0], 52);
    VERIFY_BITS_128(&c, 61);
    /* [d 0 t4 t3 0 c r0] = [p8 0 0 p5 p4 p3 0 0 p0] */

a0 *= 2;
    secp256k1_u128_accum_mul(&c, a0, a1);
    VERIFY_BITS_128(&c, 114);
    /* [d 0 t4 t3 0 c r0] = [p8 0 0 p5 p4 p3 0 p1 p0] */
    secp256k1_u128_accum_mul(&d, a2, a4);
    secp256k1_u128_accum_mul(&d, a3, a3);
    VERIFY_BITS_128(&d, 114);
    /* [d 0 t4 t3 0 c r0] = [p8 0 p6 p5 p4 p3 0 p1 p0] */
    secp256k1_u128_accum_mul(&c, secp256k1_u128_to_u64(&d) & M, R); secp256k1_u128_rshift(&d, 52);
    VERIFY_BITS_128(&c, 115);
    VERIFY_BITS_128(&d, 62);
    /* [d 0 0 t4 t3 0 c r0] = [p8 0 p6 p5 p4 p3 0 p1 p0] */
    r[1] = secp256k1_u128_to_u64(&c) & M; secp256k1_u128_rshift(&c, 52);
    VERIFY_BITS(r[1], 52);
    VERIFY_BITS_128(&c, 63);
    /* [d 0 0 t4 t3 c r1 r0] = [p8 0 p6 p5 p4 p3 0 p1 p0] */

secp256k1_u128_accum_mul(&c, a0, a2);
    secp256k1_u128_accum_mul(&c, a1, a1);
    VERIFY_BITS_128(&c, 114);
    /* [d 0 0 t4 t3 c r1 r0] = [p8 0 p6 p5 p4 p3 p2 p1 p0] */
    secp256k1_u128_accum_mul(&d, a3, a4);
    VERIFY_BITS_128(&d, 114);
    /* [d 0 0 t4 t3 c r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
    secp256k1_u128_accum_mul(&c, R, secp256k1_u128_to_u64(&d)); secp256k1_u128_rshift(&d, 64);
    VERIFY_BITS_128(&c, 115);
    VERIFY_BITS_128(&d, 50);
    /* [(d<<12) 0 0 0 t4 t3 c r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
    r[2] = secp256k1_u128_to_u64(&c) & M; secp256k1_u128_rshift(&c, 52);
    VERIFY_BITS(r[2], 52);
    VERIFY_BITS_128(&c, 63);
    /* [(d<<12) 0 0 0 t4 t3+c r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */

secp256k1_u128_accum_mul(&c, R << 12, secp256k1_u128_to_u64(&d));
    secp256k1_u128_accum_u64(&c, t3);
    VERIFY_BITS_128(&c, 100);
    /* [t4 c r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
    r[3] = secp256k1_u128_to_u64(&c) & M; secp256k1_u128_rshift(&c, 52);
    VERIFY_BITS(r[3], 52);
    VERIFY_BITS_128(&c, 48);
    /* [t4+c r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
    r[4] = secp256k1_u128_to_u64(&c) + t4;
    VERIFY_BITS(r[4], 49);
    /* [r4 r3 r2 r1 r0] = [p8 p7 p6 p5 p4 p3 p2 p1 p0] */
}