<|start_filename|>pasta_fp.c<|end_filename|>
/* Autogenerated: ./src/ExtractionOCaml/word_by_word_montgomery pasta_fp 64 '2^254 + 45560315531419706090280762371685220353' */
/* curve description: pasta_fp */
/* machine_wordsize = 64 (from "64") */
/* requested operations: (all) */
/* m = 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001 (from "2^254 + 45560315531419706090280762371685220353") */
/*                                                                    */
/* NOTE: In addition to the bounds specified above each function, all */
/*   functions synthesized for this Montgomery arithmetic require the */
/*   input to be strictly less than the prime modulus (m), and also   */
/*   require the input to be in the unique saturated representation.  */
/*   All functions also ensure that these two properties are true of  */
/*   return values.                                                   */
/*  */
/* Computed values: */
/* eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) */
/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */

#include <stdint.h>
#include <inttypes.h>
#include <stdbool.h>
#include <stddef.h>

typedef unsigned char fiat_pasta_fp_uint1;
typedef signed char fiat_pasta_fp_int1;

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

// x^{(p - 1) / 2}
const bool P_MINUS_1_OVER_2[] = {1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 0, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
const size_t P_MINUS_1_OVER_2_LEN = 254;

/*
 * The function fiat_pasta_fp_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]
 */
void fiat_pasta_fp_addcarryx_u64(uint64_t* out1, fiat_pasta_fp_uint1* out2, fiat_pasta_fp_uint1 arg1, uint64_t arg2, uint64_t arg3) {
  uint64_t tmp = arg3 + arg1;
  *out1 = arg2 + tmp;
  *out2 = (arg2 > *out1) | (arg3 > tmp);
}

/*
 * The function fiat_pasta_fp_subborrowx_u64 is a subtraction with borrow.
 * 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]
 */
void fiat_pasta_fp_subborrowx_u64(uint64_t* out1, fiat_pasta_fp_uint1* out2, fiat_pasta_fp_uint1 arg1, uint64_t arg2, uint64_t arg3) {
  uint64_t tmp = arg3 + arg1;
  *out1 = arg2 - tmp;
  *out2 = (arg2 < *out1) | (arg3 > tmp);
}

/*
 * The function fiat_pasta_fp_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]
 */
void fiat_pasta_fp_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t a, uint64_t b) {
  uint64_t    a_lo = (uint32_t)a;
  uint64_t    a_hi = a >> 32;
  uint64_t    b_lo = (uint32_t)b;
  uint64_t    b_hi = b >> 32;

  uint64_t    a_x_b_hi =  a_hi * b_hi;
  uint64_t    a_x_b_mid = a_hi * b_lo;
  uint64_t    b_x_a_mid = b_hi * a_lo;
  uint64_t    a_x_b_lo =  a_lo * b_lo;

  uint64_t    carry_bit = ((uint64_t)(uint32_t)a_x_b_mid +
                          (uint64_t)(uint32_t)b_x_a_mid +
                          (a_x_b_lo >> 32) ) >> 32;

  uint64_t    multhi = a_x_b_hi +
                      (a_x_b_mid >> 32) + (b_x_a_mid >> 32) +
                      carry_bit;

  *out2 = multhi;
  // TODO: This multiplication could be avoided.
  *out1 = a * b;
}

/*
 * The function fiat_pasta_fp_cmovznz_u64 is a single-word conditional move.
 * Postconditions:
 *   out1 = (if arg1 = 0 then arg2 else arg3)
 *
 * Input Bounds:
 *   arg1: [0x0 ~> 0x1]
 *   arg2: [0x0 ~> 0xffffffffffffffff]
 *   arg3: [0x0 ~> 0xffffffffffffffff]
 * Output Bounds:
 *   out1: [0x0 ~> 0xffffffffffffffff]
 */
void fiat_pasta_fp_cmovznz_u64(uint64_t* out1, fiat_pasta_fp_uint1 arg1, uint64_t arg2, uint64_t arg3) {
  fiat_pasta_fp_uint1 x1;
  uint64_t x2;
  uint64_t x3;
  x1 = (!(!arg1));
  x2 = ((fiat_pasta_fp_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff));
  x3 = ((x2 & arg3) | ((~x2) & arg2));
  *out1 = x3;
}

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

/*
 * The function fiat_pasta_fp_square squares a field element in the Montgomery domain.
 * Preconditions:
 *   0 ≤ eval arg1 < m
 * Postconditions:
 *   eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_square(uint64_t out1[4], const uint64_t arg1[4]) {
  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_pasta_fp_uint1 x14;
  uint64_t x15;
  fiat_pasta_fp_uint1 x16;
  uint64_t x17;
  fiat_pasta_fp_uint1 x18;
  uint64_t x19;
  uint64_t 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;
  fiat_pasta_fp_uint1 x29;
  uint64_t x30;
  uint64_t x31;
  fiat_pasta_fp_uint1 x32;
  uint64_t x33;
  fiat_pasta_fp_uint1 x34;
  uint64_t x35;
  fiat_pasta_fp_uint1 x36;
  uint64_t x37;
  fiat_pasta_fp_uint1 x38;
  uint64_t x39;
  fiat_pasta_fp_uint1 x40;
  uint64_t x41;
  uint64_t x42;
  uint64_t x43;
  uint64_t x44;
  uint64_t x45;
  uint64_t x46;
  uint64_t x47;
  uint64_t x48;
  uint64_t x49;
  fiat_pasta_fp_uint1 x50;
  uint64_t x51;
  fiat_pasta_fp_uint1 x52;
  uint64_t x53;
  fiat_pasta_fp_uint1 x54;
  uint64_t x55;
  uint64_t x56;
  fiat_pasta_fp_uint1 x57;
  uint64_t x58;
  fiat_pasta_fp_uint1 x59;
  uint64_t x60;
  fiat_pasta_fp_uint1 x61;
  uint64_t x62;
  fiat_pasta_fp_uint1 x63;
  uint64_t x64;
  fiat_pasta_fp_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_pasta_fp_uint1 x75;
  uint64_t x76;
  uint64_t x77;
  fiat_pasta_fp_uint1 x78;
  uint64_t x79;
  fiat_pasta_fp_uint1 x80;
  uint64_t x81;
  fiat_pasta_fp_uint1 x82;
  uint64_t x83;
  fiat_pasta_fp_uint1 x84;
  uint64_t x85;
  fiat_pasta_fp_uint1 x86;
  uint64_t x87;
  uint64_t x88;
  uint64_t x89;
  uint64_t x90;
  uint64_t x91;
  uint64_t x92;
  uint64_t x93;
  uint64_t x94;
  uint64_t x95;
  uint64_t x96;
  fiat_pasta_fp_uint1 x97;
  uint64_t x98;
  fiat_pasta_fp_uint1 x99;
  uint64_t x100;
  fiat_pasta_fp_uint1 x101;
  uint64_t x102;
  uint64_t x103;
  fiat_pasta_fp_uint1 x104;
  uint64_t x105;
  fiat_pasta_fp_uint1 x106;
  uint64_t x107;
  fiat_pasta_fp_uint1 x108;
  uint64_t x109;
  fiat_pasta_fp_uint1 x110;
  uint64_t x111;
  fiat_pasta_fp_uint1 x112;
  uint64_t x113;
  uint64_t x114;
  uint64_t x115;
  uint64_t x116;
  uint64_t x117;
  uint64_t x118;
  uint64_t x119;
  uint64_t x120;
  uint64_t x121;
  fiat_pasta_fp_uint1 x122;
  uint64_t x123;
  uint64_t x124;
  fiat_pasta_fp_uint1 x125;
  uint64_t x126;
  fiat_pasta_fp_uint1 x127;
  uint64_t x128;
  fiat_pasta_fp_uint1 x129;
  uint64_t x130;
  fiat_pasta_fp_uint1 x131;
  uint64_t x132;
  fiat_pasta_fp_uint1 x133;
  uint64_t x134;
  uint64_t x135;
  uint64_t x136;
  uint64_t x137;
  uint64_t x138;
  uint64_t x139;
  uint64_t x140;
  uint64_t x141;
  uint64_t x142;
  uint64_t x143;
  fiat_pasta_fp_uint1 x144;
  uint64_t x145;
  fiat_pasta_fp_uint1 x146;
  uint64_t x147;
  fiat_pasta_fp_uint1 x148;
  uint64_t x149;
  uint64_t x150;
  fiat_pasta_fp_uint1 x151;
  uint64_t x152;
  fiat_pasta_fp_uint1 x153;
  uint64_t x154;
  fiat_pasta_fp_uint1 x155;
  uint64_t x156;
  fiat_pasta_fp_uint1 x157;
  uint64_t x158;
  fiat_pasta_fp_uint1 x159;
  uint64_t x160;
  uint64_t x161;
  uint64_t x162;
  uint64_t x163;
  uint64_t x164;
  uint64_t x165;
  uint64_t x166;
  uint64_t x167;
  uint64_t x168;
  fiat_pasta_fp_uint1 x169;
  uint64_t x170;
  uint64_t x171;
  fiat_pasta_fp_uint1 x172;
  uint64_t x173;
  fiat_pasta_fp_uint1 x174;
  uint64_t x175;
  fiat_pasta_fp_uint1 x176;
  uint64_t x177;
  fiat_pasta_fp_uint1 x178;
  uint64_t x179;
  fiat_pasta_fp_uint1 x180;
  uint64_t x181;
  uint64_t x182;
  fiat_pasta_fp_uint1 x183;
  uint64_t x184;
  fiat_pasta_fp_uint1 x185;
  uint64_t x186;
  fiat_pasta_fp_uint1 x187;
  uint64_t x188;
  fiat_pasta_fp_uint1 x189;
  uint64_t x190;
  fiat_pasta_fp_uint1 x191;
  uint64_t x192;
  uint64_t x193;
  uint64_t x194;
  uint64_t x195;
  x1 = (arg1[1]);
  x2 = (arg1[2]);
  x3 = (arg1[3]);
  x4 = (arg1[0]);
  fiat_pasta_fp_mulx_u64(&x5, &x6, x4, (arg1[3]));
  fiat_pasta_fp_mulx_u64(&x7, &x8, x4, (arg1[2]));
  fiat_pasta_fp_mulx_u64(&x9, &x10, x4, (arg1[1]));
  fiat_pasta_fp_mulx_u64(&x11, &x12, x4, (arg1[0]));
  fiat_pasta_fp_addcarryx_u64(&x13, &x14, 0x0, x12, x9);
  fiat_pasta_fp_addcarryx_u64(&x15, &x16, x14, x10, x7);
  fiat_pasta_fp_addcarryx_u64(&x17, &x18, x16, x8, x5);
  x19 = (x18 + x6);
  fiat_pasta_fp_mulx_u64(&x20, &x21, x11, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x22, &x23, x20, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x24, &x25, x20, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x26, &x27, x20, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x28, &x29, 0x0, x27, x24);
  x30 = (x29 + x25);
  fiat_pasta_fp_addcarryx_u64(&x31, &x32, 0x0, x11, x26);
  fiat_pasta_fp_addcarryx_u64(&x33, &x34, x32, x13, x28);
  fiat_pasta_fp_addcarryx_u64(&x35, &x36, x34, x15, x30);
  fiat_pasta_fp_addcarryx_u64(&x37, &x38, x36, x17, x22);
  fiat_pasta_fp_addcarryx_u64(&x39, &x40, x38, x19, x23);
  fiat_pasta_fp_mulx_u64(&x41, &x42, x1, (arg1[3]));
  fiat_pasta_fp_mulx_u64(&x43, &x44, x1, (arg1[2]));
  fiat_pasta_fp_mulx_u64(&x45, &x46, x1, (arg1[1]));
  fiat_pasta_fp_mulx_u64(&x47, &x48, x1, (arg1[0]));
  fiat_pasta_fp_addcarryx_u64(&x49, &x50, 0x0, x48, x45);
  fiat_pasta_fp_addcarryx_u64(&x51, &x52, x50, x46, x43);
  fiat_pasta_fp_addcarryx_u64(&x53, &x54, x52, x44, x41);
  x55 = (x54 + x42);
  fiat_pasta_fp_addcarryx_u64(&x56, &x57, 0x0, x33, x47);
  fiat_pasta_fp_addcarryx_u64(&x58, &x59, x57, x35, x49);
  fiat_pasta_fp_addcarryx_u64(&x60, &x61, x59, x37, x51);
  fiat_pasta_fp_addcarryx_u64(&x62, &x63, x61, x39, x53);
  fiat_pasta_fp_addcarryx_u64(&x64, &x65, x63, x40, x55);
  fiat_pasta_fp_mulx_u64(&x66, &x67, x56, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x68, &x69, x66, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x70, &x71, x66, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x72, &x73, x66, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x74, &x75, 0x0, x73, x70);
  x76 = (x75 + x71);
  fiat_pasta_fp_addcarryx_u64(&x77, &x78, 0x0, x56, x72);
  fiat_pasta_fp_addcarryx_u64(&x79, &x80, x78, x58, x74);
  fiat_pasta_fp_addcarryx_u64(&x81, &x82, x80, x60, x76);
  fiat_pasta_fp_addcarryx_u64(&x83, &x84, x82, x62, x68);
  fiat_pasta_fp_addcarryx_u64(&x85, &x86, x84, x64, x69);
  x87 = ((uint64_t)x86 + x65);
  fiat_pasta_fp_mulx_u64(&x88, &x89, x2, (arg1[3]));
  fiat_pasta_fp_mulx_u64(&x90, &x91, x2, (arg1[2]));
  fiat_pasta_fp_mulx_u64(&x92, &x93, x2, (arg1[1]));
  fiat_pasta_fp_mulx_u64(&x94, &x95, x2, (arg1[0]));
  fiat_pasta_fp_addcarryx_u64(&x96, &x97, 0x0, x95, x92);
  fiat_pasta_fp_addcarryx_u64(&x98, &x99, x97, x93, x90);
  fiat_pasta_fp_addcarryx_u64(&x100, &x101, x99, x91, x88);
  x102 = (x101 + x89);
  fiat_pasta_fp_addcarryx_u64(&x103, &x104, 0x0, x79, x94);
  fiat_pasta_fp_addcarryx_u64(&x105, &x106, x104, x81, x96);
  fiat_pasta_fp_addcarryx_u64(&x107, &x108, x106, x83, x98);
  fiat_pasta_fp_addcarryx_u64(&x109, &x110, x108, x85, x100);
  fiat_pasta_fp_addcarryx_u64(&x111, &x112, x110, x87, x102);
  fiat_pasta_fp_mulx_u64(&x113, &x114, x103, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x115, &x116, x113, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x117, &x118, x113, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x119, &x120, x113, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x121, &x122, 0x0, x120, x117);
  x123 = (x122 + x118);
  fiat_pasta_fp_addcarryx_u64(&x124, &x125, 0x0, x103, x119);
  fiat_pasta_fp_addcarryx_u64(&x126, &x127, x125, x105, x121);
  fiat_pasta_fp_addcarryx_u64(&x128, &x129, x127, x107, x123);
  fiat_pasta_fp_addcarryx_u64(&x130, &x131, x129, x109, x115);
  fiat_pasta_fp_addcarryx_u64(&x132, &x133, x131, x111, x116);
  x134 = ((uint64_t)x133 + x112);
  fiat_pasta_fp_mulx_u64(&x135, &x136, x3, (arg1[3]));
  fiat_pasta_fp_mulx_u64(&x137, &x138, x3, (arg1[2]));
  fiat_pasta_fp_mulx_u64(&x139, &x140, x3, (arg1[1]));
  fiat_pasta_fp_mulx_u64(&x141, &x142, x3, (arg1[0]));
  fiat_pasta_fp_addcarryx_u64(&x143, &x144, 0x0, x142, x139);
  fiat_pasta_fp_addcarryx_u64(&x145, &x146, x144, x140, x137);
  fiat_pasta_fp_addcarryx_u64(&x147, &x148, x146, x138, x135);
  x149 = (x148 + x136);
  fiat_pasta_fp_addcarryx_u64(&x150, &x151, 0x0, x126, x141);
  fiat_pasta_fp_addcarryx_u64(&x152, &x153, x151, x128, x143);
  fiat_pasta_fp_addcarryx_u64(&x154, &x155, x153, x130, x145);
  fiat_pasta_fp_addcarryx_u64(&x156, &x157, x155, x132, x147);
  fiat_pasta_fp_addcarryx_u64(&x158, &x159, x157, x134, x149);
  fiat_pasta_fp_mulx_u64(&x160, &x161, x150, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x162, &x163, x160, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x164, &x165, x160, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x166, &x167, x160, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x168, &x169, 0x0, x167, x164);
  x170 = (x169 + x165);
  fiat_pasta_fp_addcarryx_u64(&x171, &x172, 0x0, x150, x166);
  fiat_pasta_fp_addcarryx_u64(&x173, &x174, x172, x152, x168);
  fiat_pasta_fp_addcarryx_u64(&x175, &x176, x174, x154, x170);
  fiat_pasta_fp_addcarryx_u64(&x177, &x178, x176, x156, x162);
  fiat_pasta_fp_addcarryx_u64(&x179, &x180, x178, x158, x163);
  x181 = ((uint64_t)x180 + x159);
  fiat_pasta_fp_subborrowx_u64(&x182, &x183, 0x0, x173, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_subborrowx_u64(&x184, &x185, x183, x175, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_subborrowx_u64(&x186, &x187, x185, x177, 0x0);
  fiat_pasta_fp_subborrowx_u64(&x188, &x189, x187, x179, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_subborrowx_u64(&x190, &x191, x189, x181, 0x0);
  fiat_pasta_fp_cmovznz_u64(&x192, x191, x182, x173);
  fiat_pasta_fp_cmovznz_u64(&x193, x191, x184, x175);
  fiat_pasta_fp_cmovznz_u64(&x194, x191, x186, x177);
  fiat_pasta_fp_cmovznz_u64(&x195, x191, x188, x179);
  out1[0] = x192;
  out1[1] = x193;
  out1[2] = x194;
  out1[3] = x195;
}

/*
 * The function fiat_pasta_fp_add adds two field elements in the Montgomery domain.
 * Preconditions:
 *   0 ≤ eval arg1 < m
 *   0 ≤ eval arg2 < m
 * Postconditions:
 *   eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_add(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]) {
  uint64_t x1;
  fiat_pasta_fp_uint1 x2;
  uint64_t x3;
  fiat_pasta_fp_uint1 x4;
  uint64_t x5;
  fiat_pasta_fp_uint1 x6;
  uint64_t x7;
  fiat_pasta_fp_uint1 x8;
  uint64_t x9;
  fiat_pasta_fp_uint1 x10;
  uint64_t x11;
  fiat_pasta_fp_uint1 x12;
  uint64_t x13;
  fiat_pasta_fp_uint1 x14;
  uint64_t x15;
  fiat_pasta_fp_uint1 x16;
  uint64_t x17;
  fiat_pasta_fp_uint1 x18;
  uint64_t x19;
  uint64_t x20;
  uint64_t x21;
  uint64_t x22;
  fiat_pasta_fp_addcarryx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
  fiat_pasta_fp_addcarryx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
  fiat_pasta_fp_addcarryx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
  fiat_pasta_fp_addcarryx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
  fiat_pasta_fp_subborrowx_u64(&x9, &x10, 0x0, x1, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_subborrowx_u64(&x11, &x12, x10, x3, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_subborrowx_u64(&x13, &x14, x12, x5, 0x0);
  fiat_pasta_fp_subborrowx_u64(&x15, &x16, x14, x7, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_subborrowx_u64(&x17, &x18, x16, x8, 0x0);
  fiat_pasta_fp_cmovznz_u64(&x19, x18, x9, x1);
  fiat_pasta_fp_cmovznz_u64(&x20, x18, x11, x3);
  fiat_pasta_fp_cmovznz_u64(&x21, x18, x13, x5);
  fiat_pasta_fp_cmovznz_u64(&x22, x18, x15, x7);
  out1[0] = x19;
  out1[1] = x20;
  out1[2] = x21;
  out1[3] = x22;
}

/*
 * The function fiat_pasta_fp_sub subtracts two field elements in the Montgomery domain.
 * Preconditions:
 *   0 ≤ eval arg1 < m
 *   0 ≤ eval arg2 < m
 * Postconditions:
 *   eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]) {
  uint64_t x1;
  fiat_pasta_fp_uint1 x2;
  uint64_t x3;
  fiat_pasta_fp_uint1 x4;
  uint64_t x5;
  fiat_pasta_fp_uint1 x6;
  uint64_t x7;
  fiat_pasta_fp_uint1 x8;
  uint64_t x9;
  uint64_t x10;
  fiat_pasta_fp_uint1 x11;
  uint64_t x12;
  fiat_pasta_fp_uint1 x13;
  uint64_t x14;
  fiat_pasta_fp_uint1 x15;
  uint64_t x16;
  fiat_pasta_fp_uint1 x17;
  fiat_pasta_fp_subborrowx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
  fiat_pasta_fp_subborrowx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
  fiat_pasta_fp_subborrowx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
  fiat_pasta_fp_subborrowx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
  fiat_pasta_fp_cmovznz_u64(&x9, x8, 0x0, UINT64_C(0xffffffffffffffff));
  fiat_pasta_fp_addcarryx_u64(&x10, &x11, 0x0, x1, (x9 & UINT64_C(0x992d30ed00000001)));
  fiat_pasta_fp_addcarryx_u64(&x12, &x13, x11, x3, (x9 & UINT64_C(0x224698fc094cf91b)));
  fiat_pasta_fp_addcarryx_u64(&x14, &x15, x13, x5, 0x0);
  fiat_pasta_fp_addcarryx_u64(&x16, &x17, x15, x7, (x9 & UINT64_C(0x4000000000000000)));
  out1[0] = x10;
  out1[1] = x12;
  out1[2] = x14;
  out1[3] = x16;
}

/*
 * The function fiat_pasta_fp_opp negates a field element in the Montgomery domain.
 * Preconditions:
 *   0 ≤ eval arg1 < m
 * Postconditions:
 *   eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_opp(uint64_t out1[4], const uint64_t arg1[4]) {
  uint64_t x1;
  fiat_pasta_fp_uint1 x2;
  uint64_t x3;
  fiat_pasta_fp_uint1 x4;
  uint64_t x5;
  fiat_pasta_fp_uint1 x6;
  uint64_t x7;
  fiat_pasta_fp_uint1 x8;
  uint64_t x9;
  uint64_t x10;
  fiat_pasta_fp_uint1 x11;
  uint64_t x12;
  fiat_pasta_fp_uint1 x13;
  uint64_t x14;
  fiat_pasta_fp_uint1 x15;
  uint64_t x16;
  fiat_pasta_fp_uint1 x17;
  fiat_pasta_fp_subborrowx_u64(&x1, &x2, 0x0, 0x0, (arg1[0]));
  fiat_pasta_fp_subborrowx_u64(&x3, &x4, x2, 0x0, (arg1[1]));
  fiat_pasta_fp_subborrowx_u64(&x5, &x6, x4, 0x0, (arg1[2]));
  fiat_pasta_fp_subborrowx_u64(&x7, &x8, x6, 0x0, (arg1[3]));
  fiat_pasta_fp_cmovznz_u64(&x9, x8, 0x0, UINT64_C(0xffffffffffffffff));
  fiat_pasta_fp_addcarryx_u64(&x10, &x11, 0x0, x1, (x9 & UINT64_C(0x992d30ed00000001)));
  fiat_pasta_fp_addcarryx_u64(&x12, &x13, x11, x3, (x9 & UINT64_C(0x224698fc094cf91b)));
  fiat_pasta_fp_addcarryx_u64(&x14, &x15, x13, x5, 0x0);
  fiat_pasta_fp_addcarryx_u64(&x16, &x17, x15, x7, (x9 & UINT64_C(0x4000000000000000)));
  out1[0] = x10;
  out1[1] = x12;
  out1[2] = x14;
  out1[3] = x16;
}

/*
 * The function fiat_pasta_fp_from_montgomery translates a field element out of the Montgomery domain.
 * Preconditions:
 *   0 ≤ eval arg1 < m
 * Postconditions:
 *   eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]) {
  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;
  fiat_pasta_fp_uint1 x11;
  uint64_t x12;
  fiat_pasta_fp_uint1 x13;
  uint64_t x14;
  fiat_pasta_fp_uint1 x15;
  uint64_t x16;
  fiat_pasta_fp_uint1 x17;
  uint64_t x18;
  uint64_t x19;
  uint64_t x20;
  uint64_t x21;
  uint64_t x22;
  uint64_t x23;
  uint64_t x24;
  uint64_t x25;
  uint64_t x26;
  fiat_pasta_fp_uint1 x27;
  uint64_t x28;
  fiat_pasta_fp_uint1 x29;
  uint64_t x30;
  fiat_pasta_fp_uint1 x31;
  uint64_t x32;
  fiat_pasta_fp_uint1 x33;
  uint64_t x34;
  fiat_pasta_fp_uint1 x35;
  uint64_t x36;
  fiat_pasta_fp_uint1 x37;
  uint64_t x38;
  fiat_pasta_fp_uint1 x39;
  uint64_t x40;
  fiat_pasta_fp_uint1 x41;
  uint64_t x42;
  uint64_t x43;
  uint64_t x44;
  uint64_t x45;
  uint64_t x46;
  uint64_t x47;
  uint64_t x48;
  uint64_t x49;
  uint64_t x50;
  fiat_pasta_fp_uint1 x51;
  uint64_t x52;
  fiat_pasta_fp_uint1 x53;
  uint64_t x54;
  fiat_pasta_fp_uint1 x55;
  uint64_t x56;
  fiat_pasta_fp_uint1 x57;
  uint64_t x58;
  fiat_pasta_fp_uint1 x59;
  uint64_t x60;
  fiat_pasta_fp_uint1 x61;
  uint64_t x62;
  fiat_pasta_fp_uint1 x63;
  uint64_t x64;
  fiat_pasta_fp_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_pasta_fp_uint1 x75;
  uint64_t x76;
  fiat_pasta_fp_uint1 x77;
  uint64_t x78;
  fiat_pasta_fp_uint1 x79;
  uint64_t x80;
  fiat_pasta_fp_uint1 x81;
  uint64_t x82;
  fiat_pasta_fp_uint1 x83;
  uint64_t x84;
  uint64_t x85;
  fiat_pasta_fp_uint1 x86;
  uint64_t x87;
  fiat_pasta_fp_uint1 x88;
  uint64_t x89;
  fiat_pasta_fp_uint1 x90;
  uint64_t x91;
  fiat_pasta_fp_uint1 x92;
  uint64_t x93;
  fiat_pasta_fp_uint1 x94;
  uint64_t x95;
  uint64_t x96;
  uint64_t x97;
  uint64_t x98;
  x1 = (arg1[0]);
  fiat_pasta_fp_mulx_u64(&x2, &x3, x1, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x4, &x5, x2, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x6, &x7, x2, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x8, &x9, x2, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x10, &x11, 0x0, x9, x6);
  fiat_pasta_fp_addcarryx_u64(&x12, &x13, 0x0, x1, x8);
  fiat_pasta_fp_addcarryx_u64(&x14, &x15, x13, 0x0, x10);
  fiat_pasta_fp_addcarryx_u64(&x16, &x17, 0x0, x14, (arg1[1]));
  fiat_pasta_fp_mulx_u64(&x18, &x19, x16, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x20, &x21, x18, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x22, &x23, x18, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x24, &x25, x18, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x26, &x27, 0x0, x25, x22);
  fiat_pasta_fp_addcarryx_u64(&x28, &x29, 0x0, x16, x24);
  fiat_pasta_fp_addcarryx_u64(&x30, &x31, x29, (x17 + (x15 + (x11 + x7))), x26);
  fiat_pasta_fp_addcarryx_u64(&x32, &x33, x31, x4, (x27 + x23));
  fiat_pasta_fp_addcarryx_u64(&x34, &x35, x33, x5, x20);
  fiat_pasta_fp_addcarryx_u64(&x36, &x37, 0x0, x30, (arg1[2]));
  fiat_pasta_fp_addcarryx_u64(&x38, &x39, x37, x32, 0x0);
  fiat_pasta_fp_addcarryx_u64(&x40, &x41, x39, x34, 0x0);
  fiat_pasta_fp_mulx_u64(&x42, &x43, x36, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x44, &x45, x42, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x46, &x47, x42, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x48, &x49, x42, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x50, &x51, 0x0, x49, x46);
  fiat_pasta_fp_addcarryx_u64(&x52, &x53, 0x0, x36, x48);
  fiat_pasta_fp_addcarryx_u64(&x54, &x55, x53, x38, x50);
  fiat_pasta_fp_addcarryx_u64(&x56, &x57, x55, x40, (x51 + x47));
  fiat_pasta_fp_addcarryx_u64(&x58, &x59, x57, (x41 + (x35 + x21)), x44);
  fiat_pasta_fp_addcarryx_u64(&x60, &x61, 0x0, x54, (arg1[3]));
  fiat_pasta_fp_addcarryx_u64(&x62, &x63, x61, x56, 0x0);
  fiat_pasta_fp_addcarryx_u64(&x64, &x65, x63, x58, 0x0);
  fiat_pasta_fp_mulx_u64(&x66, &x67, x60, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x68, &x69, x66, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x70, &x71, x66, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x72, &x73, x66, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x74, &x75, 0x0, x73, x70);
  fiat_pasta_fp_addcarryx_u64(&x76, &x77, 0x0, x60, x72);
  fiat_pasta_fp_addcarryx_u64(&x78, &x79, x77, x62, x74);
  fiat_pasta_fp_addcarryx_u64(&x80, &x81, x79, x64, (x75 + x71));
  fiat_pasta_fp_addcarryx_u64(&x82, &x83, x81, (x65 + (x59 + x45)), x68);
  x84 = (x83 + x69);
  fiat_pasta_fp_subborrowx_u64(&x85, &x86, 0x0, x78, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_subborrowx_u64(&x87, &x88, x86, x80, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_subborrowx_u64(&x89, &x90, x88, x82, 0x0);
  fiat_pasta_fp_subborrowx_u64(&x91, &x92, x90, x84, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_subborrowx_u64(&x93, &x94, x92, 0x0, 0x0);
  fiat_pasta_fp_cmovznz_u64(&x95, x94, x85, x78);
  fiat_pasta_fp_cmovznz_u64(&x96, x94, x87, x80);
  fiat_pasta_fp_cmovznz_u64(&x97, x94, x89, x82);
  fiat_pasta_fp_cmovznz_u64(&x98, x94, x91, x84);
  out1[0] = x95;
  out1[1] = x96;
  out1[2] = x97;
  out1[3] = x98;
}

/*
 * The function fiat_pasta_fp_to_montgomery translates a field element into the Montgomery domain.
 * Preconditions:
 *   0 ≤ eval arg1 < m
 * Postconditions:
 *   eval (from_montgomery out1) mod m = eval arg1 mod m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_to_montgomery(uint64_t out1[4], const uint64_t arg1[4]) {
  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_pasta_fp_uint1 x14;
  uint64_t x15;
  fiat_pasta_fp_uint1 x16;
  uint64_t x17;
  fiat_pasta_fp_uint1 x18;
  uint64_t x19;
  uint64_t x20;
  uint64_t x21;
  uint64_t x22;
  uint64_t x23;
  uint64_t x24;
  uint64_t x25;
  uint64_t x26;
  uint64_t x27;
  fiat_pasta_fp_uint1 x28;
  uint64_t x29;
  fiat_pasta_fp_uint1 x30;
  uint64_t x31;
  fiat_pasta_fp_uint1 x32;
  uint64_t x33;
  fiat_pasta_fp_uint1 x34;
  uint64_t x35;
  fiat_pasta_fp_uint1 x36;
  uint64_t x37;
  uint64_t x38;
  uint64_t x39;
  uint64_t x40;
  uint64_t x41;
  uint64_t x42;
  uint64_t x43;
  uint64_t x44;
  uint64_t x45;
  fiat_pasta_fp_uint1 x46;
  uint64_t x47;
  fiat_pasta_fp_uint1 x48;
  uint64_t x49;
  fiat_pasta_fp_uint1 x50;
  uint64_t x51;
  fiat_pasta_fp_uint1 x52;
  uint64_t x53;
  fiat_pasta_fp_uint1 x54;
  uint64_t x55;
  fiat_pasta_fp_uint1 x56;
  uint64_t x57;
  fiat_pasta_fp_uint1 x58;
  uint64_t 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_pasta_fp_uint1 x68;
  uint64_t x69;
  fiat_pasta_fp_uint1 x70;
  uint64_t x71;
  fiat_pasta_fp_uint1 x72;
  uint64_t x73;
  fiat_pasta_fp_uint1 x74;
  uint64_t x75;
  fiat_pasta_fp_uint1 x76;
  uint64_t x77;
  uint64_t x78;
  uint64_t x79;
  uint64_t x80;
  uint64_t x81;
  uint64_t x82;
  uint64_t x83;
  uint64_t x84;
  uint64_t x85;
  fiat_pasta_fp_uint1 x86;
  uint64_t x87;
  fiat_pasta_fp_uint1 x88;
  uint64_t x89;
  fiat_pasta_fp_uint1 x90;
  uint64_t x91;
  fiat_pasta_fp_uint1 x92;
  uint64_t x93;
  fiat_pasta_fp_uint1 x94;
  uint64_t x95;
  fiat_pasta_fp_uint1 x96;
  uint64_t x97;
  fiat_pasta_fp_uint1 x98;
  uint64_t x99;
  uint64_t x100;
  uint64_t x101;
  uint64_t x102;
  uint64_t x103;
  uint64_t x104;
  uint64_t x105;
  uint64_t x106;
  uint64_t x107;
  fiat_pasta_fp_uint1 x108;
  uint64_t x109;
  fiat_pasta_fp_uint1 x110;
  uint64_t x111;
  fiat_pasta_fp_uint1 x112;
  uint64_t x113;
  fiat_pasta_fp_uint1 x114;
  uint64_t x115;
  fiat_pasta_fp_uint1 x116;
  uint64_t x117;
  uint64_t x118;
  uint64_t x119;
  uint64_t x120;
  uint64_t x121;
  uint64_t x122;
  uint64_t x123;
  uint64_t x124;
  uint64_t x125;
  fiat_pasta_fp_uint1 x126;
  uint64_t x127;
  fiat_pasta_fp_uint1 x128;
  uint64_t x129;
  fiat_pasta_fp_uint1 x130;
  uint64_t x131;
  fiat_pasta_fp_uint1 x132;
  uint64_t x133;
  fiat_pasta_fp_uint1 x134;
  uint64_t x135;
  fiat_pasta_fp_uint1 x136;
  uint64_t x137;
  fiat_pasta_fp_uint1 x138;
  uint64_t x139;
  uint64_t x140;
  uint64_t x141;
  uint64_t x142;
  uint64_t x143;
  uint64_t x144;
  uint64_t x145;
  uint64_t x146;
  uint64_t x147;
  fiat_pasta_fp_uint1 x148;
  uint64_t x149;
  fiat_pasta_fp_uint1 x150;
  uint64_t x151;
  fiat_pasta_fp_uint1 x152;
  uint64_t x153;
  fiat_pasta_fp_uint1 x154;
  uint64_t x155;
  fiat_pasta_fp_uint1 x156;
  uint64_t x157;
  uint64_t x158;
  fiat_pasta_fp_uint1 x159;
  uint64_t x160;
  fiat_pasta_fp_uint1 x161;
  uint64_t x162;
  fiat_pasta_fp_uint1 x163;
  uint64_t x164;
  fiat_pasta_fp_uint1 x165;
  uint64_t x166;
  fiat_pasta_fp_uint1 x167;
  uint64_t x168;
  uint64_t x169;
  uint64_t x170;
  uint64_t x171;
  x1 = (arg1[1]);
  x2 = (arg1[2]);
  x3 = (arg1[3]);
  x4 = (arg1[0]);
  fiat_pasta_fp_mulx_u64(&x5, &x6, x4, UINT64_C(0x96d41af7b9cb714));
  fiat_pasta_fp_mulx_u64(&x7, &x8, x4, UINT64_C(0x7797a99bc3c95d18));
  fiat_pasta_fp_mulx_u64(&x9, &x10, x4, UINT64_C(0xd7d30dbd8b0de0e7));
  fiat_pasta_fp_mulx_u64(&x11, &x12, x4, UINT64_C(0x8c78ecb30000000f));
  fiat_pasta_fp_addcarryx_u64(&x13, &x14, 0x0, x12, x9);
  fiat_pasta_fp_addcarryx_u64(&x15, &x16, x14, x10, x7);
  fiat_pasta_fp_addcarryx_u64(&x17, &x18, x16, x8, x5);
  fiat_pasta_fp_mulx_u64(&x19, &x20, x11, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x21, &x22, x19, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x23, &x24, x19, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x25, &x26, x19, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x27, &x28, 0x0, x26, x23);
  fiat_pasta_fp_addcarryx_u64(&x29, &x30, 0x0, x11, x25);
  fiat_pasta_fp_addcarryx_u64(&x31, &x32, x30, x13, x27);
  fiat_pasta_fp_addcarryx_u64(&x33, &x34, x32, x15, (x28 + x24));
  fiat_pasta_fp_addcarryx_u64(&x35, &x36, x34, x17, x21);
  fiat_pasta_fp_mulx_u64(&x37, &x38, x1, UINT64_C(0x96d41af7b9cb714));
  fiat_pasta_fp_mulx_u64(&x39, &x40, x1, UINT64_C(0x7797a99bc3c95d18));
  fiat_pasta_fp_mulx_u64(&x41, &x42, x1, UINT64_C(0xd7d30dbd8b0de0e7));
  fiat_pasta_fp_mulx_u64(&x43, &x44, x1, UINT64_C(0x8c78ecb30000000f));
  fiat_pasta_fp_addcarryx_u64(&x45, &x46, 0x0, x44, x41);
  fiat_pasta_fp_addcarryx_u64(&x47, &x48, x46, x42, x39);
  fiat_pasta_fp_addcarryx_u64(&x49, &x50, x48, x40, x37);
  fiat_pasta_fp_addcarryx_u64(&x51, &x52, 0x0, x31, x43);
  fiat_pasta_fp_addcarryx_u64(&x53, &x54, x52, x33, x45);
  fiat_pasta_fp_addcarryx_u64(&x55, &x56, x54, x35, x47);
  fiat_pasta_fp_addcarryx_u64(&x57, &x58, x56, ((x36 + (x18 + x6)) + x22), x49);
  fiat_pasta_fp_mulx_u64(&x59, &x60, x51, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x61, &x62, x59, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x63, &x64, x59, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x65, &x66, x59, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x67, &x68, 0x0, x66, x63);
  fiat_pasta_fp_addcarryx_u64(&x69, &x70, 0x0, x51, x65);
  fiat_pasta_fp_addcarryx_u64(&x71, &x72, x70, x53, x67);
  fiat_pasta_fp_addcarryx_u64(&x73, &x74, x72, x55, (x68 + x64));
  fiat_pasta_fp_addcarryx_u64(&x75, &x76, x74, x57, x61);
  fiat_pasta_fp_mulx_u64(&x77, &x78, x2, UINT64_C(0x96d41af7b9cb714));
  fiat_pasta_fp_mulx_u64(&x79, &x80, x2, UINT64_C(0x7797a99bc3c95d18));
  fiat_pasta_fp_mulx_u64(&x81, &x82, x2, UINT64_C(0xd7d30dbd8b0de0e7));
  fiat_pasta_fp_mulx_u64(&x83, &x84, x2, UINT64_C(0x8c78ecb30000000f));
  fiat_pasta_fp_addcarryx_u64(&x85, &x86, 0x0, x84, x81);
  fiat_pasta_fp_addcarryx_u64(&x87, &x88, x86, x82, x79);
  fiat_pasta_fp_addcarryx_u64(&x89, &x90, x88, x80, x77);
  fiat_pasta_fp_addcarryx_u64(&x91, &x92, 0x0, x71, x83);
  fiat_pasta_fp_addcarryx_u64(&x93, &x94, x92, x73, x85);
  fiat_pasta_fp_addcarryx_u64(&x95, &x96, x94, x75, x87);
  fiat_pasta_fp_addcarryx_u64(&x97, &x98, x96, ((x76 + (x58 + (x50 + x38))) + x62), x89);
  fiat_pasta_fp_mulx_u64(&x99, &x100, x91, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x101, &x102, x99, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x103, &x104, x99, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x105, &x106, x99, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x107, &x108, 0x0, x106, x103);
  fiat_pasta_fp_addcarryx_u64(&x109, &x110, 0x0, x91, x105);
  fiat_pasta_fp_addcarryx_u64(&x111, &x112, x110, x93, x107);
  fiat_pasta_fp_addcarryx_u64(&x113, &x114, x112, x95, (x108 + x104));
  fiat_pasta_fp_addcarryx_u64(&x115, &x116, x114, x97, x101);
  fiat_pasta_fp_mulx_u64(&x117, &x118, x3, UINT64_C(0x96d41af7b9cb714));
  fiat_pasta_fp_mulx_u64(&x119, &x120, x3, UINT64_C(0x7797a99bc3c95d18));
  fiat_pasta_fp_mulx_u64(&x121, &x122, x3, UINT64_C(0xd7d30dbd8b0de0e7));
  fiat_pasta_fp_mulx_u64(&x123, &x124, x3, UINT64_C(0x8c78ecb30000000f));
  fiat_pasta_fp_addcarryx_u64(&x125, &x126, 0x0, x124, x121);
  fiat_pasta_fp_addcarryx_u64(&x127, &x128, x126, x122, x119);
  fiat_pasta_fp_addcarryx_u64(&x129, &x130, x128, x120, x117);
  fiat_pasta_fp_addcarryx_u64(&x131, &x132, 0x0, x111, x123);
  fiat_pasta_fp_addcarryx_u64(&x133, &x134, x132, x113, x125);
  fiat_pasta_fp_addcarryx_u64(&x135, &x136, x134, x115, x127);
  fiat_pasta_fp_addcarryx_u64(&x137, &x138, x136, ((x116 + (x98 + (x90 + x78))) + x102), x129);
  fiat_pasta_fp_mulx_u64(&x139, &x140, x131, UINT64_C(0x992d30ecffffffff));
  fiat_pasta_fp_mulx_u64(&x141, &x142, x139, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_mulx_u64(&x143, &x144, x139, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_mulx_u64(&x145, &x146, x139, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_addcarryx_u64(&x147, &x148, 0x0, x146, x143);
  fiat_pasta_fp_addcarryx_u64(&x149, &x150, 0x0, x131, x145);
  fiat_pasta_fp_addcarryx_u64(&x151, &x152, x150, x133, x147);
  fiat_pasta_fp_addcarryx_u64(&x153, &x154, x152, x135, (x148 + x144));
  fiat_pasta_fp_addcarryx_u64(&x155, &x156, x154, x137, x141);
  x157 = ((x156 + (x138 + (x130 + x118))) + x142);
  fiat_pasta_fp_subborrowx_u64(&x158, &x159, 0x0, x151, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_subborrowx_u64(&x160, &x161, x159, x153, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_subborrowx_u64(&x162, &x163, x161, x155, 0x0);
  fiat_pasta_fp_subborrowx_u64(&x164, &x165, x163, x157, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_subborrowx_u64(&x166, &x167, x165, 0x0, 0x0);
  fiat_pasta_fp_cmovznz_u64(&x168, x167, x158, x151);
  fiat_pasta_fp_cmovznz_u64(&x169, x167, x160, x153);
  fiat_pasta_fp_cmovznz_u64(&x170, x167, x162, x155);
  fiat_pasta_fp_cmovznz_u64(&x171, x167, x164, x157);
  out1[0] = x168;
  out1[1] = x169;
  out1[2] = x170;
  out1[3] = x171;
}

/*
 * The function fiat_pasta_fp_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
 * Preconditions:
 *   0 ≤ eval arg1 < m
 * Postconditions:
 *   out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [0x0 ~> 0xffffffffffffffff]
 */
void fiat_pasta_fp_nonzero(uint64_t* out1, const uint64_t arg1[4]) {
  uint64_t x1;
  x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | (arg1[3]))));
  *out1 = x1;
}

/*
 * The function fiat_pasta_fp_selectznz is a multi-limb conditional select.
 * Postconditions:
 *   eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
 *
 * Input Bounds:
 *   arg1: [0x0 ~> 0x1]
 *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_selectznz(uint64_t out1[4], fiat_pasta_fp_uint1 arg1, const uint64_t arg2[4], const uint64_t arg3[4]) {
  uint64_t x1;
  uint64_t x2;
  uint64_t x3;
  uint64_t x4;
  fiat_pasta_fp_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0]));
  fiat_pasta_fp_cmovznz_u64(&x2, arg1, (arg2[1]), (arg3[1]));
  fiat_pasta_fp_cmovznz_u64(&x3, arg1, (arg2[2]), (arg3[2]));
  fiat_pasta_fp_cmovznz_u64(&x4, arg1, (arg2[3]), (arg3[3]));
  out1[0] = x1;
  out1[1] = x2;
  out1[2] = x3;
  out1[3] = x4;
}

/*
 * The function fiat_pasta_fp_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
 * Preconditions:
 *   0 ≤ eval arg1 < m
 * Postconditions:
 *   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x7fffffffffffffff]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
 */
void fiat_pasta_fp_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) {
  uint64_t x1;
  uint64_t x2;
  uint64_t x3;
  uint64_t x4;
  uint8_t x5;
  uint64_t x6;
  uint8_t x7;
  uint64_t x8;
  uint8_t x9;
  uint64_t x10;
  uint8_t x11;
  uint64_t x12;
  uint8_t x13;
  uint64_t x14;
  uint8_t x15;
  uint64_t x16;
  uint8_t x17;
  uint8_t x18;
  uint8_t x19;
  uint64_t x20;
  uint8_t x21;
  uint64_t x22;
  uint8_t x23;
  uint64_t x24;
  uint8_t x25;
  uint64_t x26;
  uint8_t x27;
  uint64_t x28;
  uint8_t x29;
  uint64_t x30;
  uint8_t x31;
  uint8_t x32;
  uint8_t x33;
  uint64_t x34;
  uint8_t x35;
  uint64_t x36;
  uint8_t x37;
  uint64_t x38;
  uint8_t x39;
  uint64_t x40;
  uint8_t x41;
  uint64_t x42;
  uint8_t x43;
  uint64_t x44;
  uint8_t x45;
  uint8_t x46;
  uint8_t x47;
  uint64_t x48;
  uint8_t x49;
  uint64_t x50;
  uint8_t x51;
  uint64_t x52;
  uint8_t x53;
  uint64_t x54;
  uint8_t x55;
  uint64_t x56;
  uint8_t x57;
  uint64_t x58;
  uint8_t x59;
  uint8_t x60;
  x1 = (arg1[3]);
  x2 = (arg1[2]);
  x3 = (arg1[1]);
  x4 = (arg1[0]);
  x5 = (uint8_t)(x4 & UINT8_C(0xff));
  x6 = (x4 >> 8);
  x7 = (uint8_t)(x6 & UINT8_C(0xff));
  x8 = (x6 >> 8);
  x9 = (uint8_t)(x8 & UINT8_C(0xff));
  x10 = (x8 >> 8);
  x11 = (uint8_t)(x10 & UINT8_C(0xff));
  x12 = (x10 >> 8);
  x13 = (uint8_t)(x12 & UINT8_C(0xff));
  x14 = (x12 >> 8);
  x15 = (uint8_t)(x14 & UINT8_C(0xff));
  x16 = (x14 >> 8);
  x17 = (uint8_t)(x16 & UINT8_C(0xff));
  x18 = (uint8_t)(x16 >> 8);
  x19 = (uint8_t)(x3 & UINT8_C(0xff));
  x20 = (x3 >> 8);
  x21 = (uint8_t)(x20 & UINT8_C(0xff));
  x22 = (x20 >> 8);
  x23 = (uint8_t)(x22 & UINT8_C(0xff));
  x24 = (x22 >> 8);
  x25 = (uint8_t)(x24 & UINT8_C(0xff));
  x26 = (x24 >> 8);
  x27 = (uint8_t)(x26 & UINT8_C(0xff));
  x28 = (x26 >> 8);
  x29 = (uint8_t)(x28 & UINT8_C(0xff));
  x30 = (x28 >> 8);
  x31 = (uint8_t)(x30 & UINT8_C(0xff));
  x32 = (uint8_t)(x30 >> 8);
  x33 = (uint8_t)(x2 & UINT8_C(0xff));
  x34 = (x2 >> 8);
  x35 = (uint8_t)(x34 & UINT8_C(0xff));
  x36 = (x34 >> 8);
  x37 = (uint8_t)(x36 & UINT8_C(0xff));
  x38 = (x36 >> 8);
  x39 = (uint8_t)(x38 & UINT8_C(0xff));
  x40 = (x38 >> 8);
  x41 = (uint8_t)(x40 & UINT8_C(0xff));
  x42 = (x40 >> 8);
  x43 = (uint8_t)(x42 & UINT8_C(0xff));
  x44 = (x42 >> 8);
  x45 = (uint8_t)(x44 & UINT8_C(0xff));
  x46 = (uint8_t)(x44 >> 8);
  x47 = (uint8_t)(x1 & UINT8_C(0xff));
  x48 = (x1 >> 8);
  x49 = (uint8_t)(x48 & UINT8_C(0xff));
  x50 = (x48 >> 8);
  x51 = (uint8_t)(x50 & UINT8_C(0xff));
  x52 = (x50 >> 8);
  x53 = (uint8_t)(x52 & UINT8_C(0xff));
  x54 = (x52 >> 8);
  x55 = (uint8_t)(x54 & UINT8_C(0xff));
  x56 = (x54 >> 8);
  x57 = (uint8_t)(x56 & UINT8_C(0xff));
  x58 = (x56 >> 8);
  x59 = (uint8_t)(x58 & UINT8_C(0xff));
  x60 = (uint8_t)(x58 >> 8);
  out1[0] = x5;
  out1[1] = x7;
  out1[2] = x9;
  out1[3] = x11;
  out1[4] = x13;
  out1[5] = x15;
  out1[6] = x17;
  out1[7] = x18;
  out1[8] = x19;
  out1[9] = x21;
  out1[10] = x23;
  out1[11] = x25;
  out1[12] = x27;
  out1[13] = x29;
  out1[14] = x31;
  out1[15] = x32;
  out1[16] = x33;
  out1[17] = x35;
  out1[18] = x37;
  out1[19] = x39;
  out1[20] = x41;
  out1[21] = x43;
  out1[22] = x45;
  out1[23] = x46;
  out1[24] = x47;
  out1[25] = x49;
  out1[26] = x51;
  out1[27] = x53;
  out1[28] = x55;
  out1[29] = x57;
  out1[30] = x59;
  out1[31] = x60;
}

/*
 * The function fiat_pasta_fp_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
 * Preconditions:
 *   0 ≤ bytes_eval arg1 < m
 * Postconditions:
 *   eval out1 mod m = bytes_eval arg1 mod m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x7fffffffffffffff]]
 */
void fiat_pasta_fp_from_bytes(uint64_t out1[4], const uint8_t arg1[32]) {
  uint64_t x1;
  uint64_t x2;
  uint64_t x3;
  uint64_t x4;
  uint64_t x5;
  uint64_t x6;
  uint64_t x7;
  uint8_t x8;
  uint64_t x9;
  uint64_t x10;
  uint64_t x11;
  uint64_t x12;
  uint64_t x13;
  uint64_t x14;
  uint64_t x15;
  uint8_t x16;
  uint64_t x17;
  uint64_t x18;
  uint64_t x19;
  uint64_t x20;
  uint64_t x21;
  uint64_t x22;
  uint64_t x23;
  uint8_t x24;
  uint64_t x25;
  uint64_t x26;
  uint64_t x27;
  uint64_t x28;
  uint64_t x29;
  uint64_t x30;
  uint64_t x31;
  uint8_t x32;
  uint64_t x33;
  uint64_t x34;
  uint64_t x35;
  uint64_t x36;
  uint64_t x37;
  uint64_t x38;
  uint64_t x39;
  uint64_t x40;
  uint64_t x41;
  uint64_t x42;
  uint64_t x43;
  uint64_t x44;
  uint64_t 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;
  uint64_t x55;
  uint64_t x56;
  uint64_t x57;
  uint64_t x58;
  uint64_t x59;
  uint64_t x60;
  x1 = ((uint64_t)(arg1[31]) << 56);
  x2 = ((uint64_t)(arg1[30]) << 48);
  x3 = ((uint64_t)(arg1[29]) << 40);
  x4 = ((uint64_t)(arg1[28]) << 32);
  x5 = ((uint64_t)(arg1[27]) << 24);
  x6 = ((uint64_t)(arg1[26]) << 16);
  x7 = ((uint64_t)(arg1[25]) << 8);
  x8 = (arg1[24]);
  x9 = ((uint64_t)(arg1[23]) << 56);
  x10 = ((uint64_t)(arg1[22]) << 48);
  x11 = ((uint64_t)(arg1[21]) << 40);
  x12 = ((uint64_t)(arg1[20]) << 32);
  x13 = ((uint64_t)(arg1[19]) << 24);
  x14 = ((uint64_t)(arg1[18]) << 16);
  x15 = ((uint64_t)(arg1[17]) << 8);
  x16 = (arg1[16]);
  x17 = ((uint64_t)(arg1[15]) << 56);
  x18 = ((uint64_t)(arg1[14]) << 48);
  x19 = ((uint64_t)(arg1[13]) << 40);
  x20 = ((uint64_t)(arg1[12]) << 32);
  x21 = ((uint64_t)(arg1[11]) << 24);
  x22 = ((uint64_t)(arg1[10]) << 16);
  x23 = ((uint64_t)(arg1[9]) << 8);
  x24 = (arg1[8]);
  x25 = ((uint64_t)(arg1[7]) << 56);
  x26 = ((uint64_t)(arg1[6]) << 48);
  x27 = ((uint64_t)(arg1[5]) << 40);
  x28 = ((uint64_t)(arg1[4]) << 32);
  x29 = ((uint64_t)(arg1[3]) << 24);
  x30 = ((uint64_t)(arg1[2]) << 16);
  x31 = ((uint64_t)(arg1[1]) << 8);
  x32 = (arg1[0]);
  x33 = (x31 + (uint64_t)x32);
  x34 = (x30 + x33);
  x35 = (x29 + x34);
  x36 = (x28 + x35);
  x37 = (x27 + x36);
  x38 = (x26 + x37);
  x39 = (x25 + x38);
  x40 = (x23 + (uint64_t)x24);
  x41 = (x22 + x40);
  x42 = (x21 + x41);
  x43 = (x20 + x42);
  x44 = (x19 + x43);
  x45 = (x18 + x44);
  x46 = (x17 + x45);
  x47 = (x15 + (uint64_t)x16);
  x48 = (x14 + x47);
  x49 = (x13 + x48);
  x50 = (x12 + x49);
  x51 = (x11 + x50);
  x52 = (x10 + x51);
  x53 = (x9 + x52);
  x54 = (x7 + (uint64_t)x8);
  x55 = (x6 + x54);
  x56 = (x5 + x55);
  x57 = (x4 + x56);
  x58 = (x3 + x57);
  x59 = (x2 + x58);
  x60 = (x1 + x59);
  out1[0] = x39;
  out1[1] = x46;
  out1[2] = x53;
  out1[3] = x60;
}

/*
 * The function fiat_pasta_fp_set_one returns the field element one in the Montgomery domain.
 * Postconditions:
 *   eval (from_montgomery out1) mod m = 1 mod m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_set_one(uint64_t out1[4]) {
  out1[0] = UINT64_C(0x34786d38fffffffd);
  out1[1] = UINT64_C(0x992c350be41914ad);
  out1[2] = UINT64_C(0xffffffffffffffff);
  out1[3] = UINT64_C(0x3fffffffffffffff);
}

/*
 * The function fiat_pasta_fp_msat returns the saturated represtation of the prime modulus.
 * Postconditions:
 *   twos_complement_eval out1 = m
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_msat(uint64_t out1[5]) {
  out1[0] = UINT64_C(0x992d30ed00000001);
  out1[1] = UINT64_C(0x224698fc094cf91b);
  out1[2] = 0x0;
  out1[3] = UINT64_C(0x4000000000000000);
  out1[4] = 0x0;
}

/*
 * The function fiat_pasta_fp_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
 * Postconditions:
 *   eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if (log2 m) + 1 < 46 then ⌊(49 * ((log2 m) + 1) + 80) / 17⌋ else ⌊(49 * ((log2 m) + 1) + 57) / 17⌋)
 *   0 ≤ eval out1 < m
 *
 * Input Bounds:
 * Output Bounds:
 *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_divstep_precomp(uint64_t out1[4]) {
  out1[0] = UINT64_C(0xeb9f9ebd71876582);
  out1[1] = UINT64_C(0x61d4a765274d339b);
  out1[2] = UINT64_C(0x4bf06d486f0671ed);
  out1[3] = UINT64_C(0x278227fb0b195a26);
}

/*
 * The function fiat_pasta_fp_divstep computes a divstep.
 * Preconditions:
 *   0 ≤ eval arg4 < m
 *   0 ≤ eval arg5 < m
 * Postconditions:
 *   out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)
 *   twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)
 *   twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋)
 *   eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m)
 *   eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m)
 *   0 ≤ eval out5 < m
 *   0 ≤ eval out5 < m
 *   0 ≤ eval out2 < m
 *   0 ≤ eval out3 < m
 *
 * Input Bounds:
 *   arg1: [0x0 ~> 0xffffffffffffffff]
 *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out1: [0x0 ~> 0xffffffffffffffff]
 *   out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
void fiat_pasta_fp_divstep(uint64_t* out1, uint64_t out2[5], uint64_t out3[5], uint64_t out4[4], uint64_t out5[4], uint64_t arg1, const uint64_t arg2[5], const uint64_t arg3[5], const uint64_t arg4[4], const uint64_t arg5[4]) {
  uint64_t x1;
  fiat_pasta_fp_uint1 x2;
  fiat_pasta_fp_uint1 x3;
  uint64_t x4;
  fiat_pasta_fp_uint1 x5;
  uint64_t x6;
  uint64_t x7;
  uint64_t x8;
  uint64_t x9;
  uint64_t x10;
  uint64_t x11;
  uint64_t x12;
  fiat_pasta_fp_uint1 x13;
  uint64_t x14;
  fiat_pasta_fp_uint1 x15;
  uint64_t x16;
  fiat_pasta_fp_uint1 x17;
  uint64_t x18;
  fiat_pasta_fp_uint1 x19;
  uint64_t x20;
  fiat_pasta_fp_uint1 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;
  uint64_t x30;
  uint64_t x31;
  fiat_pasta_fp_uint1 x32;
  uint64_t x33;
  fiat_pasta_fp_uint1 x34;
  uint64_t x35;
  fiat_pasta_fp_uint1 x36;
  uint64_t x37;
  fiat_pasta_fp_uint1 x38;
  uint64_t x39;
  fiat_pasta_fp_uint1 x40;
  uint64_t x41;
  fiat_pasta_fp_uint1 x42;
  uint64_t x43;
  fiat_pasta_fp_uint1 x44;
  uint64_t x45;
  fiat_pasta_fp_uint1 x46;
  uint64_t x47;
  fiat_pasta_fp_uint1 x48;
  uint64_t x49;
  uint64_t x50;
  uint64_t x51;
  uint64_t x52;
  uint64_t x53;
  fiat_pasta_fp_uint1 x54;
  uint64_t x55;
  fiat_pasta_fp_uint1 x56;
  uint64_t x57;
  fiat_pasta_fp_uint1 x58;
  uint64_t x59;
  fiat_pasta_fp_uint1 x60;
  uint64_t x61;
  uint64_t x62;
  fiat_pasta_fp_uint1 x63;
  uint64_t x64;
  fiat_pasta_fp_uint1 x65;
  uint64_t x66;
  fiat_pasta_fp_uint1 x67;
  uint64_t x68;
  fiat_pasta_fp_uint1 x69;
  uint64_t x70;
  uint64_t x71;
  uint64_t x72;
  uint64_t x73;
  fiat_pasta_fp_uint1 x74;
  uint64_t x75;
  uint64_t x76;
  uint64_t x77;
  uint64_t x78;
  uint64_t x79;
  uint64_t x80;
  fiat_pasta_fp_uint1 x81;
  uint64_t x82;
  fiat_pasta_fp_uint1 x83;
  uint64_t x84;
  fiat_pasta_fp_uint1 x85;
  uint64_t x86;
  fiat_pasta_fp_uint1 x87;
  uint64_t x88;
  fiat_pasta_fp_uint1 x89;
  uint64_t x90;
  uint64_t x91;
  uint64_t x92;
  uint64_t x93;
  uint64_t x94;
  fiat_pasta_fp_uint1 x95;
  uint64_t x96;
  fiat_pasta_fp_uint1 x97;
  uint64_t x98;
  fiat_pasta_fp_uint1 x99;
  uint64_t x100;
  fiat_pasta_fp_uint1 x101;
  uint64_t x102;
  fiat_pasta_fp_uint1 x103;
  uint64_t x104;
  fiat_pasta_fp_uint1 x105;
  uint64_t x106;
  fiat_pasta_fp_uint1 x107;
  uint64_t x108;
  fiat_pasta_fp_uint1 x109;
  uint64_t x110;
  fiat_pasta_fp_uint1 x111;
  uint64_t x112;
  fiat_pasta_fp_uint1 x113;
  uint64_t x114;
  uint64_t x115;
  uint64_t x116;
  uint64_t x117;
  uint64_t x118;
  uint64_t x119;
  uint64_t x120;
  uint64_t x121;
  uint64_t x122;
  uint64_t x123;
  uint64_t x124;
  uint64_t x125;
  uint64_t x126;
  fiat_pasta_fp_addcarryx_u64(&x1, &x2, 0x0, (~arg1), 0x1);
  x3 = (fiat_pasta_fp_uint1)((fiat_pasta_fp_uint1)(x1 >> 63) & (fiat_pasta_fp_uint1)((arg3[0]) & 0x1));
  fiat_pasta_fp_addcarryx_u64(&x4, &x5, 0x0, (~arg1), 0x1);
  fiat_pasta_fp_cmovznz_u64(&x6, x3, arg1, x4);
  fiat_pasta_fp_cmovznz_u64(&x7, x3, (arg2[0]), (arg3[0]));
  fiat_pasta_fp_cmovznz_u64(&x8, x3, (arg2[1]), (arg3[1]));
  fiat_pasta_fp_cmovznz_u64(&x9, x3, (arg2[2]), (arg3[2]));
  fiat_pasta_fp_cmovznz_u64(&x10, x3, (arg2[3]), (arg3[3]));
  fiat_pasta_fp_cmovznz_u64(&x11, x3, (arg2[4]), (arg3[4]));
  fiat_pasta_fp_addcarryx_u64(&x12, &x13, 0x0, 0x1, (~(arg2[0])));
  fiat_pasta_fp_addcarryx_u64(&x14, &x15, x13, 0x0, (~(arg2[1])));
  fiat_pasta_fp_addcarryx_u64(&x16, &x17, x15, 0x0, (~(arg2[2])));
  fiat_pasta_fp_addcarryx_u64(&x18, &x19, x17, 0x0, (~(arg2[3])));
  fiat_pasta_fp_addcarryx_u64(&x20, &x21, x19, 0x0, (~(arg2[4])));
  fiat_pasta_fp_cmovznz_u64(&x22, x3, (arg3[0]), x12);
  fiat_pasta_fp_cmovznz_u64(&x23, x3, (arg3[1]), x14);
  fiat_pasta_fp_cmovznz_u64(&x24, x3, (arg3[2]), x16);
  fiat_pasta_fp_cmovznz_u64(&x25, x3, (arg3[3]), x18);
  fiat_pasta_fp_cmovznz_u64(&x26, x3, (arg3[4]), x20);
  fiat_pasta_fp_cmovznz_u64(&x27, x3, (arg4[0]), (arg5[0]));
  fiat_pasta_fp_cmovznz_u64(&x28, x3, (arg4[1]), (arg5[1]));
  fiat_pasta_fp_cmovznz_u64(&x29, x3, (arg4[2]), (arg5[2]));
  fiat_pasta_fp_cmovznz_u64(&x30, x3, (arg4[3]), (arg5[3]));
  fiat_pasta_fp_addcarryx_u64(&x31, &x32, 0x0, x27, x27);
  fiat_pasta_fp_addcarryx_u64(&x33, &x34, x32, x28, x28);
  fiat_pasta_fp_addcarryx_u64(&x35, &x36, x34, x29, x29);
  fiat_pasta_fp_addcarryx_u64(&x37, &x38, x36, x30, x30);
  fiat_pasta_fp_subborrowx_u64(&x39, &x40, 0x0, x31, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_subborrowx_u64(&x41, &x42, x40, x33, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_subborrowx_u64(&x43, &x44, x42, x35, 0x0);
  fiat_pasta_fp_subborrowx_u64(&x45, &x46, x44, x37, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_subborrowx_u64(&x47, &x48, x46, x38, 0x0);
  x49 = (arg4[3]);
  x50 = (arg4[2]);
  x51 = (arg4[1]);
  x52 = (arg4[0]);
  fiat_pasta_fp_subborrowx_u64(&x53, &x54, 0x0, 0x0, x52);
  fiat_pasta_fp_subborrowx_u64(&x55, &x56, x54, 0x0, x51);
  fiat_pasta_fp_subborrowx_u64(&x57, &x58, x56, 0x0, x50);
  fiat_pasta_fp_subborrowx_u64(&x59, &x60, x58, 0x0, x49);
  fiat_pasta_fp_cmovznz_u64(&x61, x60, 0x0, UINT64_C(0xffffffffffffffff));
  fiat_pasta_fp_addcarryx_u64(&x62, &x63, 0x0, x53, (x61 & UINT64_C(0x992d30ed00000001)));
  fiat_pasta_fp_addcarryx_u64(&x64, &x65, x63, x55, (x61 & UINT64_C(0x224698fc094cf91b)));
  fiat_pasta_fp_addcarryx_u64(&x66, &x67, x65, x57, 0x0);
  fiat_pasta_fp_addcarryx_u64(&x68, &x69, x67, x59, (x61 & UINT64_C(0x4000000000000000)));
  fiat_pasta_fp_cmovznz_u64(&x70, x3, (arg5[0]), x62);
  fiat_pasta_fp_cmovznz_u64(&x71, x3, (arg5[1]), x64);
  fiat_pasta_fp_cmovznz_u64(&x72, x3, (arg5[2]), x66);
  fiat_pasta_fp_cmovznz_u64(&x73, x3, (arg5[3]), x68);
  x74 = (fiat_pasta_fp_uint1)(x22 & 0x1);
  fiat_pasta_fp_cmovznz_u64(&x75, x74, 0x0, x7);
  fiat_pasta_fp_cmovznz_u64(&x76, x74, 0x0, x8);
  fiat_pasta_fp_cmovznz_u64(&x77, x74, 0x0, x9);
  fiat_pasta_fp_cmovznz_u64(&x78, x74, 0x0, x10);
  fiat_pasta_fp_cmovznz_u64(&x79, x74, 0x0, x11);
  fiat_pasta_fp_addcarryx_u64(&x80, &x81, 0x0, x22, x75);
  fiat_pasta_fp_addcarryx_u64(&x82, &x83, x81, x23, x76);
  fiat_pasta_fp_addcarryx_u64(&x84, &x85, x83, x24, x77);
  fiat_pasta_fp_addcarryx_u64(&x86, &x87, x85, x25, x78);
  fiat_pasta_fp_addcarryx_u64(&x88, &x89, x87, x26, x79);
  fiat_pasta_fp_cmovznz_u64(&x90, x74, 0x0, x27);
  fiat_pasta_fp_cmovznz_u64(&x91, x74, 0x0, x28);
  fiat_pasta_fp_cmovznz_u64(&x92, x74, 0x0, x29);
  fiat_pasta_fp_cmovznz_u64(&x93, x74, 0x0, x30);
  fiat_pasta_fp_addcarryx_u64(&x94, &x95, 0x0, x70, x90);
  fiat_pasta_fp_addcarryx_u64(&x96, &x97, x95, x71, x91);
  fiat_pasta_fp_addcarryx_u64(&x98, &x99, x97, x72, x92);
  fiat_pasta_fp_addcarryx_u64(&x100, &x101, x99, x73, x93);
  fiat_pasta_fp_subborrowx_u64(&x102, &x103, 0x0, x94, UINT64_C(0x992d30ed00000001));
  fiat_pasta_fp_subborrowx_u64(&x104, &x105, x103, x96, UINT64_C(0x224698fc094cf91b));
  fiat_pasta_fp_subborrowx_u64(&x106, &x107, x105, x98, 0x0);
  fiat_pasta_fp_subborrowx_u64(&x108, &x109, x107, x100, UINT64_C(0x4000000000000000));
  fiat_pasta_fp_subborrowx_u64(&x110, &x111, x109, x101, 0x0);
  fiat_pasta_fp_addcarryx_u64(&x112, &x113, 0x0, x6, 0x1);
  x114 = ((x80 >> 1) | ((x82 << 63) & UINT64_C(0xffffffffffffffff)));
  x115 = ((x82 >> 1) | ((x84 << 63) & UINT64_C(0xffffffffffffffff)));
  x116 = ((x84 >> 1) | ((x86 << 63) & UINT64_C(0xffffffffffffffff)));
  x117 = ((x86 >> 1) | ((x88 << 63) & UINT64_C(0xffffffffffffffff)));
  x118 = ((x88 & UINT64_C(0x8000000000000000)) | (x88 >> 1));
  fiat_pasta_fp_cmovznz_u64(&x119, x48, x39, x31);
  fiat_pasta_fp_cmovznz_u64(&x120, x48, x41, x33);
  fiat_pasta_fp_cmovznz_u64(&x121, x48, x43, x35);
  fiat_pasta_fp_cmovznz_u64(&x122, x48, x45, x37);
  fiat_pasta_fp_cmovznz_u64(&x123, x111, x102, x94);
  fiat_pasta_fp_cmovznz_u64(&x124, x111, x104, x96);
  fiat_pasta_fp_cmovznz_u64(&x125, x111, x106, x98);
  fiat_pasta_fp_cmovznz_u64(&x126, x111, x108, x100);
  *out1 = x112;
  out2[0] = x7;
  out2[1] = x8;
  out2[2] = x9;
  out2[3] = x10;
  out2[4] = x11;
  out3[0] = x114;
  out3[1] = x115;
  out3[2] = x116;
  out3[3] = x117;
  out3[4] = x118;
  out4[0] = x119;
  out4[1] = x120;
  out4[2] = x121;
  out4[3] = x122;
  out5[0] = x123;
  out5[1] = x124;
  out5[2] = x125;
  out5[3] = x126;
}

void fiat_pasta_fp_copy(uint64_t out[4], const uint64_t value[4]) {
    for (size_t j = 0; j < 4; ++j) { out[j] = value[j]; }
}

void fiat_pasta_fp_pow(uint64_t out1[4], const uint64_t arg1[4], const bool* msb_bits, const size_t bits_len) {
  fiat_pasta_fp_set_one(out1);

  uint64_t tmp[4];

  // square and multiply
  for (size_t i = 0; i < bits_len; ++i) {
    // out1 = out1 * out1
    fiat_pasta_fp_copy(tmp, out1);
    fiat_pasta_fp_square(out1, tmp);

    if (msb_bits[i]) {
      // out1 = out1 * arg1
      fiat_pasta_fp_copy(tmp, out1);
      fiat_pasta_fp_mul(out1, tmp, arg1);
    }
  }
}

void fiat_pasta_fp_inv(uint64_t out1[4], const uint64_t arg1[4]) {
  // invert by Fermat's little theorem:
  // x^{p - 2} * x = 1

  const bool P_MINUS_2[] = {1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 0, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 0, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1};
  fiat_pasta_fp_pow(out1, arg1, P_MINUS_2, 255);
}

bool fiat_pasta_fp_equals(const uint64_t x[4], const uint64_t y[4]) {
  uint64_t x_minus_y[4];
  fiat_pasta_fp_sub(x_minus_y, x, y);

  uint64_t x_minus_y_nonzero;
  fiat_pasta_fp_nonzero(&x_minus_y_nonzero, x_minus_y);
  if (x_minus_y_nonzero) {
    return false;
  } else {
    return true;
  }
}

bool fiat_pasta_fp_equals_zero(const uint64_t x[4]) {
  uint64_t x_nonzero;
  fiat_pasta_fp_nonzero(&x_nonzero, x);
  if (x_nonzero) {
    return false;
  } else {
    return true;
  }
}

bool fiat_pasta_fp_equals_one(const uint64_t x[4]) {
  uint64_t one[4];
  fiat_pasta_fp_set_one(one);

  uint64_t x_minus_1[4];
  fiat_pasta_fp_sub(x_minus_1, x, one);

  uint64_t x_minus_1_nonzero;
  fiat_pasta_fp_nonzero(&x_minus_1_nonzero, x_minus_1);
  if (x_minus_1_nonzero) {
    return false;
  } else {
    return true;
  }
}

int fiat_pasta_fp_legendre(const uint64_t arg1[4]) {
  uint64_t tmp[4];

  fiat_pasta_fp_pow(tmp, arg1, P_MINUS_1_OVER_2, 254);

  uint64_t input_non_zero;
  fiat_pasta_fp_nonzero(&input_non_zero, arg1);
  if (input_non_zero) {
    if (fiat_pasta_fp_equals_one(tmp)) {
      return 1;
    } else {
      return -1;
    }
  } else {
    return 0;
  }
}

#include <stdio.h>

void fiat_pasta_fp_print(const uint64_t x[4]) {
    printf("[ ");
    for (size_t j = 0; j < 4; ++j) {
      printf("0x%" PRIx64 ", ", x[j]);
    }
    printf("] \n");
}

bool fiat_pasta_fp_sqrt(uint64_t x[4], const uint64_t value[4]) {
    // A few assertions to make sure s, t, and nqr are initialized.

    if (fiat_pasta_fp_equals_zero(value)) {
      for (size_t j = 0; j < 4; ++j) { x[j] = 0; }
      return true;
    }

    uint64_t check[4];
    fiat_pasta_fp_pow(check, value, P_MINUS_1_OVER_2, P_MINUS_1_OVER_2_LEN);
    if (!fiat_pasta_fp_equals_one(check)) {
      return false;
    }

    uint64_t one[4];
    fiat_pasta_fp_set_one(one);

    size_t v = 32;

    // z = 5^( (p - 1)/2^32 )
    uint64_t z[4] = { 0xa28db849bad6dbf0, 0x9083cd03d3b539df, 0xfba6b9ca9dc8448e, 0x3ec928747b89c6da };

    const bool T_MINUS_ONE_DIV_TWO[] = {1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 0, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 0, 1, 1, 0};
    const size_t T_MINUS_ONE_DIV_TWO_LEN = 222;

    // w = value^((t - 1) / 2)
    // where
    // t = (p - 1) / 2^32
    uint64_t w[4];
    fiat_pasta_fp_pow(w, value, T_MINUS_ONE_DIV_TWO, T_MINUS_ONE_DIV_TWO_LEN);

    fiat_pasta_fp_mul(x, value, w);

    uint64_t b[4];
    fiat_pasta_fp_mul(b, x, w);

    // compute square root with Tonelli--Shanks
    // (does not terminate if not a square!)

    uint64_t b2m[4];
    uint64_t tmp[4];

    while (! fiat_pasta_fp_equals_one(b))
    {
        size_t m = 0;
        fiat_pasta_fp_copy(b2m, b);

        while (! fiat_pasta_fp_equals_one(b2m))
        {
          // looping here
          // b2m = b2m * b2m
            fiat_pasta_fp_copy(tmp, b2m);
            fiat_pasta_fp_square(b2m, tmp);

            /* invariant: b2m = b^(2^m) after entering this loop */
            m += 1;
        }

        int j = v-m-1;
        fiat_pasta_fp_copy(w, z);

        while (j > 0)
        {
            fiat_pasta_fp_copy(tmp, w);
            fiat_pasta_fp_square(w, tmp);
            --j;
        } // w = z^2^(v-m-1)

        fiat_pasta_fp_square(z, w);

        fiat_pasta_fp_copy(tmp, b);
        fiat_pasta_fp_mul(b, tmp, z);

        fiat_pasta_fp_copy(tmp, x);
        fiat_pasta_fp_mul(x, tmp, w);

        v = m;
    }

    return true;
}


<|start_filename|>pasta_fp.h<|end_filename|>
#include <stdint.h>
#include <stddef.h>
#include <stdbool.h>

bool fiat_pasta_fp_sqrt(uint64_t x[4], const uint64_t value[4]);
void fiat_pasta_fp_set_one(uint64_t out1[4]);
void fiat_pasta_fp_add(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]);
void fiat_pasta_fp_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]);
void fiat_pasta_fp_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]);
void fiat_pasta_fp_inv(uint64_t out1[4], const uint64_t arg1[4]);
void fiat_pasta_fp_opp(uint64_t out1[4], const uint64_t arg1[4]);
void fiat_pasta_fp_square(uint64_t out1[4], const uint64_t arg1[4]);
bool fiat_pasta_fp_equals_one(const uint64_t x[4]);
bool fiat_pasta_fp_equals(const uint64_t x[4], const uint64_t y[4]);
void fiat_pasta_fp_pow(uint64_t out1[4], const uint64_t arg1[4], const bool* msb_bits, const size_t bits_len);
void fiat_pasta_fp_print(const uint64_t x[4]);
void fiat_pasta_fp_to_montgomery(uint64_t out1[4], const uint64_t arg1[4]);
void fiat_pasta_fp_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]);
void fiat_pasta_fp_copy(uint64_t out[4], const uint64_t value[4]);


<|start_filename|>unit_tests.c<|end_filename|>
#include <stdio.h>
#include <assert.h>
#include <sys/resource.h>
#include <inttypes.h>

#include "pasta_fp.h"
#include "pasta_fq.h"
#include "crypto.h"
#include "poseidon.h"
#include "base10.h"
#include "utils.h"
#include "sha256.h"
#include "curve_checks.h"

#define ARRAY_LEN(x) (sizeof(x)/sizeof(x[0]))

#define DEFAULT_TOKEN_ID 1
static bool _verbose;
static bool _ledger_gen;

void privkey_to_hex(char *hex, const size_t len, const Scalar priv_key) {
  uint64_t priv_words[4];
  hex[0] = '\0';

  assert(len > 2*sizeof(priv_words));
  if (len < 2*sizeof(priv_words)) {
    return;
  }

  uint8_t *p = (uint8_t *)priv_words;
  fiat_pasta_fq_from_montgomery(priv_words, priv_key);
  // Mina privkey hex format is in big-endian
  for (size_t i = sizeof(priv_words); i > 0; i--) {
    sprintf(&hex[2*(sizeof(priv_words) - i)], "%02x", p[i - 1]);
  }
  hex[len] = '\0';
}

bool privkey_from_hex(Scalar priv_key, const char *priv_hex) {
  size_t priv_hex_len = strnlen(priv_hex, 64);
  if (priv_hex_len != 64) {
    return false;
  }
  uint8_t priv_bytes[32];
  // Mina privkey hex format is in big-endian
  for (size_t i = sizeof(priv_bytes); i > 0; i--) {
    sscanf(&priv_hex[2*(i - 1)], "%02hhx", &priv_bytes[sizeof(priv_bytes) - i]);
  }

  if (priv_bytes[3] & 0xc000000000000000) {
      return false;
  }

  fiat_pasta_fq_to_montgomery(priv_key, (uint64_t *)priv_bytes);

  char priv_key_hex[65];
  privkey_to_hex(priv_key_hex, sizeof(priv_key_hex), priv_key);

  // sanity check
  int result = memcmp(priv_key_hex, priv_hex, sizeof(priv_key_hex)) == 0;
  assert(result);
  return result;
}

bool privhex_to_address(char *address, const size_t len,
                        const char *account_number, const char *priv_hex) {
  Scalar priv_key;
  if (!privkey_from_hex(priv_key, priv_hex)) {
    return false;
  }

  Keypair kp;
  scalar_copy(kp.priv, priv_key);
  generate_pubkey(&kp.pub, priv_key);

  if (!generate_address(address, len, &kp.pub)) {
    return false;
  }

  if (_verbose) {
    printf("%s => %s\n", priv_hex, address);
  }
  else if (_ledger_gen) {
    printf("    # account %s\n", account_number);
    printf("    # private key %s\n", priv_hex);
    printf("    assert(test_get_address(%s) == \"%s\")\n\n",
           account_number, address);
  }

  return true;
}

void sig_to_hex(char *hex, const size_t len, const Signature sig) {
  hex[0] = '\0';

  assert(len == 2*sizeof(Signature) + 1);
  if (len < 2*sizeof(Signature) + 1) {
    return;
  }

  uint64_t words[4];
  fiat_pasta_fp_from_montgomery(words, sig.rx);
  for (size_t i = 4; i > 0; i--) {
    sprintf(&hex[16*(4 - i)], "%016lx", htole64(words[i - 1]));
  }
  fiat_pasta_fq_from_montgomery(words, sig.s);
  for (size_t i = 4; i > 0; i--) {
    sprintf(&hex[64 + 16*(4 - i)], "%016lx", htole64(words[i - 1]));
  }
}

bool sign_transaction(char *signature, const size_t len,
                      const char *account_number,
                      const char *sender_priv_hex,
                      const char *receiver_address,
                      Currency amount,
                      Currency fee,
                      Nonce nonce,
                      GlobalSlot valid_until,
                      const char *memo,
                      bool delegation,
                      uint8_t network_id) {
  Transaction txn;

  assert(len == 2*sizeof(Signature) + 1);
  if (len != 2*sizeof(Signature) + 1) {
    return false;
  }

  prepare_memo(txn.memo, memo);

  Scalar priv_key;
  if (!privkey_from_hex(priv_key, sender_priv_hex)) {
    return false;
  }

  Keypair kp;
  scalar_copy(kp.priv, priv_key);
  generate_pubkey(&kp.pub, priv_key);

  char source_str[MINA_ADDRESS_LEN];
  if (!generate_address(source_str, sizeof(source_str), &kp.pub)) {
    return false;
  }

  char *fee_payer_str = source_str;

  txn.fee = fee;
  txn.fee_token = DEFAULT_TOKEN_ID;
  read_public_key_compressed(&txn.fee_payer_pk, fee_payer_str);
  txn.nonce = nonce;
  txn.valid_until = valid_until;

  if (delegation) {
    txn.tag[0] = 0;
    txn.tag[1] = 0;
    txn.tag[2] = 1;
  }
  else {
    txn.tag[0] = 0;
    txn.tag[1] = 0;
    txn.tag[2] = 0;
  }

  read_public_key_compressed(&txn.source_pk, source_str);
  read_public_key_compressed(&txn.receiver_pk, receiver_address);
  txn.token_id = DEFAULT_TOKEN_ID;
  txn.amount = amount;
  txn.token_locked = false;

  Compressed pub_compressed;
  compress(&pub_compressed, &kp.pub);

  Signature sig;
  sign(&sig, &kp, &txn, network_id);

  if (!verify(&sig, &pub_compressed, &txn, network_id)) {
    return false;
  }

  sig_to_hex(signature, len, sig);

  if (_verbose) {
    fprintf(stderr, "%d %s\n", delegation, signature);
  }
  else if (_ledger_gen) {
    printf("    # account %s\n", account_number);
    printf("    # private key %s\n", sender_priv_hex);
    printf("    # sig=%s\n", signature);
    printf("    assert(test_sign_tx(mina.%s,\n"
           "                        %s,\n"
           "                        \"%s\",\n"
           "                        \"%s\",\n"
           "                        %zu,\n"
           "                        %zu,\n"
           "                        %u,\n"
           "                        %u,\n"
           "                        \"%s\",\n"
           "                        mina.%s) == \"%s\")\n\n",
           delegation ? "TX_TYPE_DELEGATION" : "TX_TYPE_PAYMENT",
           account_number,
           source_str,
           receiver_address,
           amount,
           fee,
           nonce,
           valid_until,
           memo,
           network_id == MAINNET_ID ? "MAINNET_ID" : "TESTNET_ID",
           signature);
  }

  return true;
}

bool check_get_address(const char *account_number,
                       const char *priv_hex, const char *address) {
  char target[MINA_ADDRESS_LEN];
  if (!privhex_to_address(target, sizeof(target), account_number, priv_hex)) {
    return false;
  }

  return strcmp(address, target) == 0;
}

bool check_sign_tx(const char *account_number,
                   const char *sender_priv_hex,
                   const char *receiver_address,
                   Currency amount,
                   Currency fee,
                   Nonce nonce,
                   GlobalSlot valid_until,
                   const char *memo,
                   bool delegation,
                   const char *signature,
                   uint8_t network_id) {
  char target[129];
  if (!sign_transaction(target, sizeof(target),
                        account_number,
                        sender_priv_hex,
                        receiver_address,
                        amount,
                        fee,
                        nonce,
                        valid_until,
                        memo,
                        delegation,
                        network_id)) {
    return false;
   }

   return strcmp(signature, target) == 0;
}

char *field_to_hex(char *hex, size_t len, const Field x) {
  assert(len == 65);
  hex[64] = '\0';
  Scalar y;
  fiat_pasta_fp_from_montgomery(y, x);
  uint8_t *p = (uint8_t *)y;
  for (size_t i = 0; i < sizeof(y); i++) {
    sprintf(&hex[2*i], "%02x", p[i]);
  }

  return hex;
}

char *scalar_to_hex(char *hex, size_t len, const Scalar x) {
  assert(len == 65);
  hex[64] = '\0';
  Scalar y;
  fiat_pasta_fq_from_montgomery(y, x);
  uint8_t *p = (uint8_t *)y;
  for (size_t i = 0; i < sizeof(y); i++) {
    sprintf(&hex[2*i], "%02x", p[i]);
  }

  return hex;
}

void print_scalar_as_cstruct(const Scalar x) {
  printf("        { ");
  for (size_t i = 0; i < sizeof(Scalar)/sizeof(x[0]); i++) {
    printf("0x%016lx, ", x[i]);
  }
  printf("},\n");
}

void print_affine_as_cstruct(const Affine *a) {
  printf("        {\n");
  printf("            { ");
  for (size_t i = 0; i < sizeof(Field)/sizeof(a->x[0]); i++) {
    printf("0x%016lx, ", a->x[i]);
  }
  printf(" },\n");
  printf("            { ");
  for (size_t i = 0; i < sizeof(Field)/sizeof(a->y[0]); i++) {
    printf("0x%016lx, ", a->y[i]);
  }
  printf(" },");
  printf("\n        },\n");
}

void print_scalar_as_ledger_cstruct(const Scalar x) {
  uint64_t tmp[4];
  uint8_t *p = (uint8_t *)tmp;

  fiat_pasta_fq_from_montgomery(tmp, x);
  printf("        {");
  for (size_t i = sizeof(Scalar); i > 0; i--) {
    if (i % 8 == 0) {
      printf("\n            ");
    }
    printf("0x%02x, ", p[i - 1]);
  }
  printf("\n        },\n");
}

void print_affine_as_ledger_cstruct(const Affine *a) {
  uint64_t tmp[4];
  uint8_t *p = (uint8_t *)tmp;

  fiat_pasta_fp_from_montgomery(tmp, a->x);
  printf("        {\n");
  printf("            {");
  for (size_t i = sizeof(Field); i > 0; i--) {
    if (i % 8 == 0) {
      printf("\n                ");
    }
    printf("0x%02x, ", p[i - 1]);
  }
  printf("\n            },\n");
  fiat_pasta_fp_from_montgomery(tmp, a->y);
  printf("            {");
  for (size_t i = sizeof(Field); i > 0; i--) {
    if (i % 8 == 0) {
      printf("\n                ");
    }
    printf("0x%02x, ", p[i - 1]);
  }
  printf("\n            },");
  printf("\n        },\n");
}

void generate_curve_checks(bool ledger_gen) {
  Scalar S[EPOCHS][3];
  Affine A[EPOCHS][3];

  printf("// curve_checks.h - elliptic curve unit tests\n");
  printf("//\n");
  printf("//    These constants were generated from the Mina c-reference-signer\n");
  printf("//    Do not edit this file\n");

  if (ledger_gen) {
    printf("//\n");
    printf("//    Details:  https://github.com/MinaProtocol/c-reference-signer/README.markdown\n");
    printf("//    Generate: ./unit_tests ledger_gen\n");
  }

  printf("\n");
  printf("#pragma once\n");
  printf("\n");
  printf("#include \"crypto.h\"\n");

  printf("\n");
  printf("#define EPOCHS %u\n", EPOCHS);
  printf("\n");

  // Generate test scalars
  printf("// Test scalars\n");
  printf("static const Scalar S[%u][2] = {\n", EPOCHS);

  Scalar s0; // Seed with zero scalar
  explicit_bzero(s0, sizeof(s0));
  for (size_t i = 0; i < EPOCHS; i++) {
    // Generate two more scalars
    Scalar s1, s2;
    sha256_hash(s0, sizeof(s0), s1, sizeof(s1));
    scalar_from_words(s1, s1);

    sha256_hash(s1, sizeof(s1), s2, sizeof(s2));
    scalar_from_words(s2, s2);

    memcpy(S[i][0], &s0, sizeof(S[i][0]));
    memcpy(S[i][1], &s1, sizeof(S[i][1]));
    memcpy(S[i][2], &s2, sizeof(S[i][2]));

    printf("    {\n");
    if (ledger_gen) {
      print_scalar_as_ledger_cstruct(S[i][0]);
      print_scalar_as_ledger_cstruct(S[i][1]);
      // Tests do not need S2
    }
    else {
      print_scalar_as_cstruct(S[i][0]);
      print_scalar_as_cstruct(S[i][1]);
      // Tests do not need S2
    }
    printf("    },\n");

    sha256_hash(s2, sizeof(s2), s0, sizeof(s0));
    scalar_from_words(s0, s0);
    // s0 is seed for next round!
  }
  printf("};\n");
  printf("\n");

  // Generate test curve points
  printf("// Test curve points\n");
  printf("static const Affine A[%u][3] = {\n", EPOCHS);

  for (size_t i = 0; i < EPOCHS; i++) {
    // Generate three curve points
    generate_pubkey(&A[i][0], S[i][0]);
    generate_pubkey(&A[i][1], S[i][1]);
    generate_pubkey(&A[i][2], S[i][2]);

    // Check on curve
    assert(affine_is_on_curve(&A[i][0]));
    assert(affine_is_on_curve(&A[i][1]));
    assert(affine_is_on_curve(&A[i][2]));

    printf("    {\n");
    if (ledger_gen) {
      print_affine_as_ledger_cstruct(&A[i][0]);
      print_affine_as_ledger_cstruct(&A[i][1]);
      print_affine_as_ledger_cstruct(&A[i][2]);
    }
    else {
      print_affine_as_cstruct(&A[i][0]);
      print_affine_as_cstruct(&A[i][1]);
      print_affine_as_cstruct(&A[i][2]);
    }
    printf("    },\n");
  }
  printf("};\n");
  printf("\n");

  // Generate target outputs
  printf("// Target outputs\n");
  printf("static const Affine T[%u][5] = {\n", EPOCHS);
  for (size_t i = 0; i < EPOCHS; i++) {
    Affine a3;
    Affine a4;
    union {
      // Fit in stackspace!
      Affine a5;
      Scalar s2;
    } u;

    // Test1: On curve after scaling
    assert(affine_is_on_curve(&A[i][0]));
    assert(affine_is_on_curve(&A[i][1]));
    assert(affine_is_on_curve(&A[i][2]));

    // Test2: Addition is commutative
    //     A0 + A1 == A1 + A0
    affine_add(&a3, &A[i][0], &A[i][1]); // a3 = A0 + A1
    affine_add(&a4, &A[i][1], &A[i][0]); // a4 = A1 + A0
    assert(affine_eq(&a3, &a4));
    assert(affine_is_on_curve(&a3));

    printf("    {\n");
    if (ledger_gen) {
      print_affine_as_ledger_cstruct(&a3);
    }
    else {
      print_affine_as_cstruct(&a3);
    }

    // Test3: Scaling commutes with adding scalars
    //     G*(S0 + S1) == G*S0 + G*S1
    scalar_add(u.s2, S[i][0], S[i][1]);
    generate_pubkey(&a3, u.s2);          // a3 = G*(S0 + S1)
    affine_add(&a4, &A[i][0], &A[i][1]); // a4 = G*S0 + G*S1
    assert(affine_eq(&a3, &a4));
    assert(affine_is_on_curve(&a3));

    if (ledger_gen) {
      print_affine_as_ledger_cstruct(&a3);
    }
    else {
      print_affine_as_cstruct(&a3);
    }

    // Test4: Scaling commutes with multiplying scalars
    //    G*(S0*S1) == S0*(G*S1)
    scalar_mul(u.s2, S[i][0], S[i][1]);
    generate_pubkey(&a3, u.s2);                // a3 = G*(S0*S1)
    affine_scalar_mul(&a4, S[i][0], &A[i][1]); // a4 = S0*(G*S1)
    assert(affine_eq(&a3, &a4));
    assert(affine_is_on_curve(&a3));

    if (ledger_gen) {
      print_affine_as_ledger_cstruct(&a3);
    }
    else {
      print_affine_as_cstruct(&a3);
    }

    // Test5: Scaling commutes with negation
    //    G*(-S0) == -(G*S0)
    scalar_negate(u.s2, S[i][0]);
    generate_pubkey(&a3, u.s2);   // a3 = G*(-S0)
    affine_negate(&a4, &A[i][0]); // a4 = -(G*S0)
    assert(affine_eq(&a3, &a4));
    assert(affine_is_on_curve(&a3));

    if (ledger_gen) {
      print_affine_as_ledger_cstruct(&a3);
    }
    else {
      print_affine_as_cstruct(&a3);
    }

    // Test6: Addition is associative
    //     (A0 + A1) + A2 == A0 + (A1 + A2)
    affine_add(&a3, &A[i][0], &A[i][1]);
    affine_add(&a4, &a3, &A[i][2]);      // a4 = (A0 + A1) + A2
    affine_add(&a3, &A[i][1], &A[i][2]);
    affine_add(&u.a5, &A[i][0], &a3);    // a5 = A0 + (A1 + A2)
    assert(affine_eq(&a4, &u.a5));
    assert(affine_is_on_curve(&a4));

    if (ledger_gen) {
      print_affine_as_ledger_cstruct(&a4);
    }
    else {
      print_affine_as_cstruct(&a4);
    }
    printf("    },\n");
  }
  printf("};\n\n");
  printf("bool curve_checks(void);\n\n");

  if (ledger_gen) {
     printf("\n");
     printf("** Copy the above constants and curve_checks.c into the ledger project\n");
     printf("\n");
  }
}

typedef struct poseidon_test {
  int   input_len;
  char *input[10];
  char *output;
} PoseidonTest;

#define ARRAY_SAFE(...) __VA_ARGS__
#define ASSERT_POSEIDON_EQ(type, input, len, out) { \
  char *inputs[len] = input; \
  Field fields[len]; \
  for (size_t i = 0; i < len; i++) { \
    assert(field_from_hex(fields[i], inputs[i])); \
  } \
  Scalar target; \
  assert(scalar_from_hex(target, out)); \
  PoseidonCtx ctx; \
  assert(poseidon_init(&ctx, type, NULLNET_ID)); \
  poseidon_update(&ctx, fields, ARRAY_LEN(fields)); \
  Scalar output; \
  poseidon_digest(output, &ctx); \
  if (memcmp(output, target, sizeof(output)) != 0) { \
    char buf[65]; \
    fprintf(stderr, " output: %s\n", scalar_to_hex(buf, ARRAY_LEN(buf), output)); \
    fprintf(stderr, " target: %s\n", scalar_to_hex(buf, ARRAY_LEN(buf), target)); \
    assert(memcmp(output, target, sizeof(output)) == 0); \
  } \
}

void test_scalars() {
    Scalar s;
    assert(scalar_from_hex(s, "d2f75185842484ba5a1a4e0ba5f3870ed48782cc4f89a8228f5eaf75e1833906"));
    assert(scalar_from_hex(s, "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff3f"));
    assert(!scalar_from_hex(s, "0000000000000000000000000000000000000000000000000000000000000040"));
    assert(!scalar_from_hex(s, "01000000ed302d991bf94c09fc98462200000000000000000000000000000040"));
}

void test_fields() {
    Field f;
    assert(field_from_hex(f, "a4e2beebb09bd02ad42bbccc11051e8262b6ef50445d8382b253e91ab1557a0d"));
    assert(field_from_hex(f, "df698e389c6f1987ffe186d806f8163738f5bf22e8be02572cce99dc6a4ab030"));
    assert(field_from_hex(f, "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff3f"));
    assert(!field_from_hex(f, "0000000000000000000000000000000000000000000000000000000000000040"));
    assert(!field_from_hex(f, "01000000ed302d991bf94c09fc98462200000000000000000000000000000040"));
}

void test_poseidon() {
    ASSERT_POSEIDON_EQ(
      POSEIDON_3W,
      ARRAY_SAFE({
      }),
      0,
      "1b3251b6912d82edc78bbb0a5c88f0c6fde1781bc3e654123fa6862a4c63e617"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3W,
      ARRAY_SAFE({
        "df698e389c6f1987ffe186d806f8163738f5bf22e8be02572cce99dc6a4ab030"
      }),
      1,
      "f9b1b6c5f8c98017c6b35ac74bc689b6533d6dbbee1fd868831b637a43ea720c"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3W,
      ARRAY_SAFE({
        "56b648a5a85619814900a6b40375676803fe16fb1ad2d1fb79115eb1b52ac026",
        "f26a8a03d9c9bbd9c6b2a1324d2a3f4d894bafe25a7e4ad1a498705f4026ff2f"
      }),
      2,
      "<KEY>"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3W,
      ARRAY_SAFE({
        "<KEY>",
        "a4e2beebb09bd02ad42bbccc11051e8262b6ef50445d8382b253e91ab1557a0d",
        "7dfc23a1242d9c0d6eb16e924cfba342bb2fccf36b8cbaf296851f2e6c469639"
      }),
      3,
      "f94b39a919aab06f43f4a4b5a3e965b719a4dbd2b9cd26d2bba4197b10286b35"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3W,
      ARRAY_SAFE({
        "<KEY>",
        "5e33065d1801131b64d13038ff9693a7ef6283f24ec8c19438d112ff59d50f04",
        "<KEY>",
        "3456d0313a30d7ccb23bd71ed6aa70ab234dad683d8187b677aef73f42f4f52e"
      }),
      4,
      "cc1ccfa964fd6ef9ff1994beb53cfce9ebe1212847ce30e4c64f0777875aec34"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3W,
      ARRAY_SAFE({
        "<KEY>",
        "2d106fb21a262f85fd400a995c6d74bad48d8adab2554046871c215e585b072b",
        "8300e93ee8587956534d0756bb2aa575e5878c670cff5c8e3e55c62632333c06",
        "879c32da31566f6d16afdefff94cba5260fec1057e97f19fc9a61dc2c54a6417",
        "<KEY>"
      }),
      5,
      "<KEY>"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_5W,
      ARRAY_SAFE({
      }),
      0,
      "01ca17b5913ca7a42adfd9353676cd9a939effb71e3246fd78a2d9283c664529"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_5W,
      ARRAY_SAFE({
        "df698e389c6f1987ffe186d806f8163738f5bf22e8be02572cce99dc6a4ab030"
      }),
      1,
      "e7d279a184604c5ae038be9d7e62a23b75373825614f3b8175db6378e4fbc622"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_5W,
      ARRAY_SAFE({
        "56b648a5a85619814900a6b40375676803fe16fb1ad2d1fb79115eb1b52ac026",
        "f26a8a03d9c9bbd9c6b2a1324d2a3f4d894bafe25a7e4ad1a498705f4026ff2f"
      }),
      2,
      "5c3f7b7b0bd53a6713b23b5c84bc6842831acd1c6a322806706167f767ee360c"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_5W,
      ARRAY_SAFE({
        "075c41fa23e4690694df5ded43624fd60ab7ee6ec6dd48f44dc71bc206cecb26",
        "a4e2beebb09bd02ad42bbccc11051e8262b6ef50445d8382b253e91ab1557a0d",
        "7dfc23a1242d9c0d6eb16e924cfba342bb2fccf36b8cbaf296851f2e6c469639"
      }),
      3,
      "e600482c4ef466db52ee02bf64cc9dd71a5a5e63eb94ff37033a10bce618a42d"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_5W,
      ARRAY_SAFE({
        "a1a659b14e80d47318c6fcdbbd388de4272d5c2815eb458cf4f196d52403b639",
        "5e33065d1801131b64d13038ff9693a7ef6283f24ec8c19438d112ff59d50f04",
        "38a8f4d0a9b6d0facdc4e825f6a2ba2b85401d5de119bf9f2bcb908235683e06",
        "3456d0313a30d7ccb23bd71ed6aa70ab234dad683d8187b677aef73f42f4f52e"
      }),
      4,
      "14278226e4fa816ef6444773268a8cf10c84ac3b8e7a62323f2f768a6d6c8537"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_5W,
      ARRAY_SAFE({
        "<KEY>",
        "2d106fb21a262f85fd400a995c6d74bad48d8adab2554046871c215e585b072b",
        "8300e93ee8587956534d0756bb2aa575e5878c670cff5c8e3e55c62632333c06",
        "879c32da31566f6d16afdefff94cba5260fec1057e97f19fc9a61dc2c54a6417",
        "9c0aa6e5501cfb2d08aeaea5b3cddac2c9bee85d13324118b44bafb63a59611e"
      }),
      5,
      "9775860a0bfff072224efdc657c239a81526ba2d4a46d95925bf868b7672d02b"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3,
      ARRAY_SAFE({
      }),
      0,
      "87b24ed3fe1f35af6497c504acd6de35f06bd9c2e2490a1b5012715719de8d05"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3,
      ARRAY_SAFE({
        "df698e389c6f1987ffe186d806f8163738f5bf22e8be02572cce99dc6a4ab030"
      }),
      1,
      "d2f75185842484ba5a1a4e0ba5f3870ed48782cc4f89a8228f5eaf75e1833906"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3,
      ARRAY_SAFE({
        "56b648a5a85619814900a6b40375676803fe16fb1ad2d1fb79115eb1b52ac026",
        "f26a8a03d9c9bbd9c6b2a1324d2a3f4d894bafe25a7e4ad1a498705f4026ff2f"
      }),
      2,
      "922d4e7f5802aee157ae13afb8c7a4aadca06913b9d36a9d1f20f5edb70e2c30"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3,
      ARRAY_SAFE({
        "<KEY>",
        "a4e2beebb09bd02ad42bbccc11051e8262b6ef50445d8382b253e91ab1557a0d",
        "<KEY>"
      }),
      3,
      "<KEY>"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3,
      ARRAY_SAFE({
        "<KEY>",
        "5e33065d1801131b64d13038ff9693a7ef6283f24ec8c19438d112ff59d50f04",
        "<KEY>",
        "3456d0313a30d7ccb23bd71ed6aa70ab234dad683d8187b677aef73f42f4f52e"
      }),
      4,
      "415aab36a9011fa8218bd67be746c7a8fd9ba83d01d1ca669574c60caef12d30"
    );

    ASSERT_POSEIDON_EQ(
      POSEIDON_3,
      ARRAY_SAFE({
        "<KEY>",
        "2d106fb21a262f85fd400a995c6d74bad48d8adab2554046871c215e585b072b",
        "8300e93ee8587956534d0756bb2aa575e5878c670cff5c8e3e55c62632333c06",
        "879c32da31566f6d16afdefff94cba5260fec1057e97f19fc9a61dc2c54a6417",
        "<KEY>"
      }),
      5,
      "9d69ee732cfe073cc9417aef734293002c8db0c69b1e814cfa7a858e7c995d33"
    );
}

void test_get_address() {
      if (_ledger_gen) {
        printf("    # Address generation tests\n");
        printf("    #\n");
        printf("    #     These tests were automatically generated from the Mina c-reference-signer\n");
        printf("    #\n");
        printf("    #     Details:  https://github.com/MinaProtocol/c-reference-signer/README.markdown\n");
        printf("    #     Generate: ./unit_tests ledger_gen\n");
        printf("\n");
      }

      assert(check_get_address("0",
                               "164244176fddb5d769b7de2027469d027ad428fadcc0c02396e6280142efb718",
                               "<KEY>"));

      assert(check_get_address("1",
                               "3ca187a58f09da346844964310c7e0dd948a9105702b716f4d732e042e0c172e",
                               "<KEY>"));

      assert(check_get_address("2",
                               "<KEY>",
                               "<KEY>"));

      assert(check_get_address("3",
                               "1dee867358d4000f1dafa5978341fb515f89eeddbe450bd57df091f1e63d4444",
                               "<KEY>"));

      assert(check_get_address("49370",
                               "20f84123a26e58dd32b0ea3c80381f35cd01bc22a20346cc65b0a67ae48532ba",
                               "B62qkiT4kgCawkSEF84ga5kP9QnhmTJEYzcfgGuk6okAJtSBfVcjm1M"));

      assert(check_get_address("0x312a",
                               "3414fc16e86e6ac272fda03cf8dcb4d7d47af91b4b726494dab43bf773ce1779",
                               "<KEY>"));
}

void test_sign_tx() {
      if (_ledger_gen) {
        printf("    # Sign transaction tests\n");
        printf("    #\n");
        printf("    #     These tests were automatically generated from the Mina c-reference-signer\n");
        printf("    #\n");
        printf("    #     Details:  https://github.com/MinaProtocol/c-reference-signer/README.markdown\n");
        printf("    #     Generate: ./unit_tests ledger_gen\n");
        printf("\n");
      }

      uint8_t network_ids[2] = { TESTNET_ID, MAINNET_ID };

      char* signatures[2][8] = {
        {
          "11a36a8dfe5b857b95a2a7b7b17c62c3ea33411ae6f4eb3a907064aecae353c60794f1d0288322fe3f8bb69d6fabd4fd7c15f8d09f8783b2f087a80407e299af",
          "<KEY>",
          "2b4d0bffcb57981d11a93c05b17672b7be700d42af8496e1ba344394da5d0b0b0432c1e8a77ee1bd4b8ef6449297f7ed4956b81df95bdc6ac95d128984f77205",
          "25bb730a25ce7180b1e5766ff8cc67452631ee46e2d255bccab8662e5f1f0c850a4bb90b3e7399e935fff7f1a06195c6ef89891c0260331b9f381a13e5507a4c",
          "30797d7d0426e54ff195d1f94dc412300f900cc9e84990603939a77b3a4d2fc11ebab12857b47c481c182abe147279732549f0fd49e68d5541f825e9d1e6fa04",
          "07e9f88fc671ed06781f9edb233fdbdee20fa32303015e795747ad9e43fcb47b3ce34e27e31f7c667756403df3eb4ce670d9175dd0ae8490b273485b71c56066",
          "1ff9f77fed4711e0ebe2a7a46a7b1988d1b62a850774bf299ec71a24d5ebfdd81d04a570e4811efe867adefe3491ba8b210f24bd0ec8577df72212d61b569b15",
          "26ca6b95dee29d956b813afa642a6a62cd89b1929320ed6b099fd191a217b08d2c9a54ba1c95e5000b44b93cfbd3b625e20e95636f1929311473c10858a27f09"
        },
        {
          "<KEY>",
          "204eb1a37e56d0255921edd5a7903c210730b289a622d45ed63a52d9e3e461d13dfcf301da98e218563893e6b30fa327600c5ff0788108652a06b970823a4124",
          "<KEY>",
          "058ed7fb4e17d9d400acca06fe20ca8efca2af4ac9a3ed279911b0bf93c45eea0e8961519b703c2fd0e431061d8997cac4a7574e622c0675227d27ce2ff357d9",
          "0904e9521a95334e3f6757cb0007ec8af3322421954255e8d263d0616910b04d213344f8ec020a4b873747d1cbb07296510315a2ec76e52150a4c765520d387f",
          "<KEY>",
          "<KEY>",
          "093f9ef0e4e051279da0a3ded85553847590ab739ee1bfd59e5bb30f98ed8a001a7a60d8506e2572164b7a525617a09f17e1756ac37555b72e01b90f37271595",
        }
      };

      for (size_t i = 0; i < 2; ++i) {
        uint8_t network_id = network_ids[i];
        assert(check_sign_tx("0",
                            "164244176fddb5d769b7de2027469d027ad428fadcc0c02396e6280142efb718",
                            "B62qicipYxyEHu7QjUqS7QvBipTs5CzgkYZZZkPoKVYBu6tnDUcE9Zt",
                            1729000000000,
                            2000000000,
                            16,
                            271828,
                            "Hello Mina!",
                            false,
                            signatures[i][0],
                            network_id));

        assert(check_sign_tx("12586",
                            "3414fc16e86e6ac272fda03cf8dcb4d7d47af91b4b726494dab43bf773ce1779",
                            "B62qrKG4Z8hnzZqp1AL8WsQhQYah3quN1qUj3SyfJA8Lw135qWWg1mi",
                            314159265359,
                            1618033988,
                            0,
                            4294967295,
                            "",
                            false,
                            signatures[i][1],
                            network_id));

        assert(check_sign_tx("12586",
                            "3414fc16e86e6ac272fda03cf8dcb4d7d47af91b4b726494dab43bf773ce1779",
                            "B62qoqiAgERjCjXhofXiD7cMLJSKD8hE8ZtMh4jX5MPNgKB4CFxxm1N",
                            271828182845904,
                            100000,
                            5687,
                            4294967295,
                            "01234567890123456789012345678901",
                            false,
                            signatures[i][2],
                            network_id));

        assert(check_sign_tx("3",
                            "1dee867358d4000f1dafa5978341fb515f89eeddbe450bd57df091f1e63d4444",
                            "B62qnzbXmRNo9q32n4SNu2mpB8e7FYYLH8NmaX6oFCBYjjQ8SbD7uzV",
                            0,
                            2000000000,
                            0,
                            1982,
                            "",
                            false,
                            signatures[i][3],
                            network_id));

        // Sign delegation tx tests

        assert(check_sign_tx("0",
                            "164244176fddb5d769b7de2027469d027ad428fadcc0c02396e6280142efb718",
                            "B62qicipYxyEHu7QjUqS7QvBipTs5CzgkYZZZkPoKVYBu6tnDUcE9Zt",
                            0,
                            2000000000,
                            16,
                            1337,
                            "Delewho?",
                            true,
                            signatures[i][4],
                            network_id));

        assert(check_sign_tx("49370",
                            "20f84123a26e58dd32b0ea3c80381f35cd01bc22a20346cc65b0a67ae48532ba",
                            "B62qnzbXmRNo9q32n4SNu2mpB8e7FYYLH8NmaX6oFCBYjjQ8SbD7uzV",
                            0,
                            2000000000,
                            0,
                            4294967295,
                            "",
                            true,
                            signatures[i][5],
                            network_id));

        assert(check_sign_tx("12586",
                            "3414fc16e86e6ac272fda03cf8dcb4d7d47af91b4b726494dab43bf773ce1779",
                            "B62qkiT4kgCawkSEF84ga5kP9QnhmTJEYzcfgGuk6okAJtSBfVcjm1M",
                            0,
                            42000000000,
                            1,
                            4294967295,
                            "more delegates, more fun........",
                            true,
                            signatures[i][6],
                            network_id));

        assert(check_sign_tx("2",
                            "336eb4a19b3d8905824b0f2254fb495573be302c17582748bf7e101965aa4774",
                            "B62qicipYxyEHu7QjUqS7QvBipTs5CzgkYZZZkPoKVYBu6tnDUcE9Zt",
                            0,
                            1202056900,
                            0,
                            577216,
                            "",
                            true,
                            signatures[i][7],
                            network_id));
      }

      // Check testnet and mainnet signatures are not equal
      for (size_t i = 0; i < 8; ++i) {
          assert(strncmp(signatures[0][i], signatures[1][i], strlen(signatures[1][i])) != 0);
      }
}

int main(int argc, char* argv[]) {
  printf("Running unit tests\n");

  if (argc > 1) {
    if (strncmp(argv[1], "ledger_gen", 10) == 0) {
        _ledger_gen = true;
    }
    else {
        _verbose = true;
    }
  }
  struct rlimit lim = {1, 1};
  if (setrlimit(RLIMIT_STACK, &lim) == -1) {
    printf("rlimit failed\n");
    return 1;
  }

  // Perform crypto tests
  if (!curve_checks()) {
      // Dump computed c-reference signer constants
      generate_curve_checks(false);
      fprintf(stderr, "!! Curve checks FAILED !! (error above)\n\n");
      exit(211);
  }
  if (_ledger_gen) {
      generate_curve_checks(true);
  }

  // fiat-crypto sqrt not square
  {
    Affine pub;

    Compressed good_pk;
    read_public_key_compressed(&good_pk, "<KEY>");
    assert(decompress(&pub, &good_pk));

    Compressed bad_pk;
    read_public_key_compressed(&bad_pk, "<KEY>");
    assert(!decompress(&pub, &bad_pk));
  }

  test_scalars();

  test_fields();

  test_poseidon();

  test_get_address();

  test_sign_tx();

  printf("Unit tests completed successfully\n");

  return 0;
}


<|start_filename|>poseidon.h<|end_filename|>
/*******************************************************************************
 * Poseidon is a hash function explained in https://eprint.iacr.org/2019/458
 * It requires the following parameters, with p a prime defining a prime field.
 * alpha = smallest prime st gcd(p, alpha) = 1
 * m = number of field elements in the state of the hash function.
 * N = number of rounds the hash function performs on each digest.
 * For m = r + c, the sponge absorbs (via field addition) and squeezes r field
 * elements per iteration, and offers log2(c) bits of security.
 * For our p (definied in crypto.c), we have alpha = 11, m = 3, r = 1, s = 2.
 *
 * Poseidon splits the full rounds into two, putting half before the parital
 * rounds are run, and the other half after. We have :
 * full rounds = 8
 * partial = 30,
 * meaning that the rounds total 38.
 * poseidon.c handles splitting the partial rounds in half and execution order.
 ********************************************************************************/

#pragma once

#include "crypto.h"

#define POSEIDON_3W 0x00
#define POSEIDON_5W 0x01
#define POSEIDON_3  0x02

#define MAX_SPONGE_WIDTH 5

typedef Field State[MAX_SPONGE_WIDTH];

typedef struct poseidon_context_t {
    State  state;
    size_t absorbed;
    size_t sponge_width;
    size_t sponge_rate;
    size_t full_rounds;
    uint8_t sbox_alpha;
    uint8_t type;
    const Field ***round_keys;
    const Field **mds_matrix;
    void (*permutation)(struct poseidon_context_t *);
} PoseidonCtx;

bool poseidon_init(PoseidonCtx *ctx, const uint8_t type, const uint8_t network_id);
void poseidon_update(PoseidonCtx *ctx, const Field *input, size_t len);
void poseidon_digest(Scalar out, PoseidonCtx *ctx);


<|start_filename|>Makefile<|end_filename|>
all: reference_signer unit_tests

OBJS = base10.o \
	base58.o \
	blake2b-ref.o \
	sha256.o \
	crypto.o \
	pasta_fp.o \
	pasta_fq.o \
	poseidon.o \
	utils.o \
	curve_checks.o

reference_signer: $(OBJS) reference_signer.c
	$(CC) -Wall -Werror $@.c -o $@ $(OBJS) -lm

.PRECIOUS: unit_tests
unit_tests: $(OBJS) *.c *.h
	$(CC) -Wall -Werror $@.c -o $@ $(OBJS) -lm
	@./$@

%.o: %.c %.h
	$(CC) -Wall -Werror $< -c

clean:
	rm -rf *.o *.log reference_signer unit_tests


<|start_filename|>crypto.c<|end_filename|>
// Mina schnorr signatures and eliptic curve arithmatic
//
//     * Produces a schnorr signature according to the specification here:
//       https://github.com/MinaProtocol/mina/blob/develop/docs/specs/signatures/description.md
//
//     * Signer reference here: https://github.com/MinaProtocol/signer-reference
//
//     * Curve arithmatic
//         - field_add, field_sub, field_mul, field_sq, field_inv, field_negate, field_pow, field_eq
//         - scalar_add, scalar_sub, scalar_mul, scalar_sq, scalar_pow, scalar_eq
//         - group_add, group_dbl, group_scalar_mul (group elements use projective coordinates)
//         - affine_scalar_mul
//         - affine_from_group
//         - generate_pubkey, generate_keypair
//         - sign
//
//     * Curve details
//         Pasta.Pallas (https://github.com/zcash/pasta)
//         E1/Fp : y^2 = x^3 + 5
//         GROUP_ORDER   = 28948022309329048855892746252171976963363056481941647379679742748393362948097 (Fq, 0x94)
//         FIELD_MODULUS = 28948022309329048855892746252171976963363056481941560715954676764349967630337 (Fp, 0x4c)

// #include <assert.h>

#define THROW exit

#include <assert.h>
#include <inttypes.h>
#include <math.h>

#include "crypto.h"
#include "utils.h"
#include "poseidon.h"
#include "pasta_fp.h"
#include "pasta_fq.h"
#include "blake2.h"
#include "libbase58.h"
#include "sha256.h"

// a = 0, b = 5
static const Field GROUP_COEFF_B = {
  0xa1a55e68ffffffed, 0x74c2a54b4f4982f3, 0xfffffffffffffffd, 0x3fffffffffffffff
};

static const Field FIELD_ONE = {
  0x34786d38fffffffd, 0x992c350be41914ad, 0xffffffffffffffff, 0x3fffffffffffffff
};
static const Field FIELD_THREE = {
  0x6b0ee5d0fffffff5, 0x86f76d2b99b14bd0, 0xfffffffffffffffe, 0x3fffffffffffffff
};
static const Field FIELD_FOUR = {
  0x65a221cfffffff1, 0xfddd093b747d6762, 0xfffffffffffffffd, 0x3fffffffffffffff
};
static const Field FIELD_EIGHT = {
  0x7387134cffffffe1, 0xd973797adfadd5a8, 0xfffffffffffffffb, 0x3fffffffffffffff
};
static const Field FIELD_ZERO = { 0, 0, 0, 0 };
static const Scalar SCALAR_ZERO = { 0, 0, 0, 0 };

// (X : Y : Z) = (0 : 1 : 0)
static const Group GROUP_ZERO = {
    { 0, 0, 0, 0},
    { 0x34786d38fffffffd, 0x992c350be41914ad, 0xffffffffffffffff, 0x3fffffffffffffff },
    { 0, 0, 0, 0}
};

// g_generator = (1 : 12418654782883325593414442427049395787963493412651469444558597405572177144507)
static const Affine AFFINE_ONE = {
    {
        0x34786d38fffffffd, 0x992c350be41914ad, 0xffffffffffffffff, 0x3fffffffffffffff
    },
    {
        0x2f474795455d409d, 0xb443b9b74b8255d9, 0x270c412f2c9a5d66, 0x8e00f71ba43dd6b
    }
};

bool field_from_hex(Field b, const char *hex) {
  if (strnlen(hex, 64) != 64) {
    return false;
  }
  uint8_t bytes[32];
  for (size_t i = 0; i < sizeof(bytes); i++) {
    sscanf(&hex[2*i], "%02hhx", &bytes[i]);
  }

  if (bytes[31] & 0xc0) {
      return false;
  }

  fiat_pasta_fp_to_montgomery(b, (uint64_t *)bytes);
  return true;
}

void field_copy(Field c, const Field a)
{
    fiat_pasta_fp_copy(c, a);
}

bool field_is_odd(const Field y)
{
    uint64_t tmp[4];
    fiat_pasta_fp_from_montgomery(tmp, y);
    return tmp[0] & 1;
}

void field_add(Field c, const Field a, const Field b)
{
    fiat_pasta_fp_add(c, a, b);
}

void field_sub(Field c, const Field a, const Field b)
{
    fiat_pasta_fp_sub(c, a, b);
}

void field_mul(Field c, const Field a, const Field b)
{
    fiat_pasta_fp_mul(c, a, b);
}

void field_sq(Field c, const Field a)
{
    fiat_pasta_fp_square(c, a);
}

void field_pow(Field c, const Field a, const uint8_t b)
{
    field_copy(c, FIELD_ONE);

    if (b == 0) {
      return;
    }

    Field tmp;
    for (size_t i = log2(b) + 1; i > 0; i--) {
        field_copy(tmp, c);
        field_sq(c, tmp);

        if (b & (1 << (i - 1))) {
            field_copy(tmp, c);
            field_mul(c, tmp, a);
        }
    }
}

void field_inv(Field c, const Field a)
{
    fiat_pasta_fp_inv(c, a);
}

void field_negate(Field c, const Field a)
{
    fiat_pasta_fp_opp(c, a);
}

unsigned int field_eq(const Field a, const Field b)
{
    if (fiat_pasta_fp_equals(a, b)) {
      return 1;
    } else {
      return 0;
    }
}

bool scalar_from_hex(Field b, const char *hex) {
  if (strnlen(hex, 64) != 64) {
    return false;
  }
  uint8_t bytes[32];
  for (size_t i = 0; i < sizeof(bytes); i++) {
    sscanf(&hex[2*i], "%02hhx", &bytes[i]);
  }

  if (bytes[31] & 0xc0) {
      return false;
  }

  fiat_pasta_fq_to_montgomery(b, (uint64_t *)bytes);
  return true;
}

void scalar_from_words(Scalar b, const uint64_t words[4])
{
    uint64_t tmp[4];
    memcpy(tmp, words, sizeof(tmp));
    tmp[3] &= (((uint64_t)1 << 62) - 1); // drop top two bits
    fiat_pasta_fq_to_montgomery(b, tmp);
}

void scalar_copy(Scalar b, const Scalar a)
{
    fiat_pasta_fq_copy(b, a);
}

void scalar_add(Scalar c, const Scalar a, const Scalar b)
{
    fiat_pasta_fq_add(c, a, b);
}

void scalar_sub(Scalar c, const Scalar a, const Scalar b)
{
    fiat_pasta_fq_sub(c, a, b);
}

void scalar_mul(Scalar c, const Scalar a, const Scalar b)
{
    fiat_pasta_fq_mul(c, a, b);
}

void scalar_sq(Scalar c, const Scalar a)
{
    fiat_pasta_fq_square(c, a);
}

void scalar_negate(Scalar c, const Scalar a)
{
    fiat_pasta_fq_opp(c, a);
}

bool scalar_eq(const Scalar a, const Scalar b)
{
    return fiat_pasta_fq_equals(a, b);
}

// zero is the only point with Z = 0 in jacobian coordinates
unsigned int is_zero(const Group *p)
{
    return field_eq(p->Z, FIELD_ZERO);
}

unsigned int affine_is_zero(const Affine *p)
{
    return (field_eq(p->x, FIELD_ZERO) && field_eq(p->y, FIELD_ZERO));
}

unsigned int group_is_on_curve(const Group *p)
{
    if (is_zero(p)) {
        return 1;
    }

    Field lhs, rhs;
    if (field_eq(p->Z, FIELD_ONE)) {
        // we can check y^2 == x^3 + ax + b
        field_sq(lhs, p->Y);                // y^2
        field_sq(rhs, p->X);                // x^2
        field_mul(rhs, rhs, p->X);          // x^3
        field_add(rhs, rhs, GROUP_COEFF_B); // x^3 + b
    }
    else {
        // we check (y/z^3)^2 == (x/z^2)^3 + b
        // => y^2 == x^3 + bz^6
        Field x3, z6;
        field_sq(x3, p->X);                 // x^2
        field_mul(x3, x3, p->X);            // x^3
        field_sq(lhs, p->Y);                // y^2
        field_sq(z6, p->Z);                 // z^2
        field_sq(z6, z6);                   // z^4
        field_mul(z6, z6, p->Z);            // z^5
        field_mul(z6, z6, p->Z);            // z^6

        field_mul(rhs, z6, GROUP_COEFF_B);  // bz^6
        field_add(rhs, x3, rhs);            // x^3 + bz^6
    }

    return field_eq(lhs, rhs);
}

void affine_to_group(Group *r, const Affine *p)
{
    if (field_eq(p->x, FIELD_ZERO) && field_eq(p->y, FIELD_ZERO)) {
        memcpy(r->X, FIELD_ZERO, FIELD_BYTES);
        memcpy(r->Y, FIELD_ONE, FIELD_BYTES);
        memcpy(r->Z, FIELD_ZERO, FIELD_BYTES);
        return;
    }

    memcpy(r->X, p->x, FIELD_BYTES);
    memcpy(r->Y, p->y, FIELD_BYTES);
    memcpy(r->Z, FIELD_ONE, FIELD_BYTES);
}

void affine_from_group(Affine *r, const Group *p)
{
    if (field_eq(p->Z, FIELD_ZERO)) {
        memcpy(r->x, FIELD_ZERO, FIELD_BYTES);
        memcpy(r->y, FIELD_ZERO, FIELD_BYTES);
        return;
    }

    Field zi, zi2, zi3;
    field_inv(zi, p->Z);        // 1/Z
    field_mul(zi2, zi, zi);     // 1/Z^2
    field_mul(zi3, zi2, zi);    // 1/Z^3
    field_mul(r->x, p->X, zi2); // X/Z^2
    field_mul(r->y, p->Y, zi3); // Y/Z^3
}

void group_one(Group *a)
{
    affine_to_group(a, &AFFINE_ONE);
}

// https://www.hyperelliptic.org/EFD/g1p/auto-code/shortw/jacobian-0/doubling/dbl-2009-l.op3
// cost 2M + 5S + 6add + 3*2 + 1*3 + 1*8
void group_dbl(Group *r, const Group *p)
{
    if (is_zero(p)) {
        *r = *p;
        return;
    }

    Field a, b, c;
    field_sq(a, p->X);            // a = X1^2
    field_sq(b, p->Y);            // b = Y1^2
    field_sq(c, b);               // c = b^2

    Field d, e, f;
    field_add(r->X, p->X, b);     // t0 = X1 + b
    field_sq(r->Y, r->X);         // t1 = t0^2
    field_sub(r->Z, r->Y, a);     // t2 = t1 - a
    field_sub(r->X, r->Z, c);     // t3 = t2 - c
    field_add(d, r->X, r->X);     // d = 2 * t3
    field_mul(e, FIELD_THREE, a); // e = 3 * a
    field_sq(f, e);               // f = e^2

    field_add(r->Y, d, d);        // t4 = 2 * d
    field_sub(r->X, f, r->Y);     // X = f - t4

    field_sub(r->Y, d, r->X);     // t5 = d - X
    field_mul(f, FIELD_EIGHT, c); // t6 = 8 * c
    field_mul(r->Z, e, r->Y);     // t7 = e * t5
    field_sub(r->Y, r->Z, f);     // Y = t7 - t6

    field_mul(f, p->Y, p->Z);     // t8 = Y1 * Z1
    field_add(r->Z, f, f);        // Z = 2 * t8
}

// https://www.hyperelliptic.org/EFD/g1p/auto-code/shortw/jacobian-0/addition/add-2007-bl.op3
// cost 11M + 5S + 9add + 4*2
void group_add(Group *r, const Group *p, const Group *q)
{
    if (is_zero(p)) {
        *r = *q;
        return;
    }

    if (is_zero(q)) {
        *r = *p;
        return;
    }

    if (field_eq(p->X, q->X) && field_eq(p->Y, q->Y) && field_eq(p->Z, q->Z)) {
        return group_dbl(r, p);
    }

    Field z1z1, z2z2;
    field_sq(z1z1, p->Z);         // Z1Z1 = Z1^2
    field_sq(z2z2, q->Z);         // Z2Z2 = Z2^2

    Field u1, u2, s1, s2;
    field_mul(u1, p->X, z2z2);    // u1 = x1 * z2z2
    field_mul(u2, q->X, z1z1);    // u2 = x2 * z1z1
    field_mul(r->X, q->Z, z2z2);  // t0 = z2 * z2z2
    field_mul(s1, p->Y, r->X);    // s1 = y1 * t0
    field_mul(r->Y, p->Z, z1z1);  // t1 = z1 * z1z1
    field_mul(s2, q->Y, r->Y);    // s2 = y2 * t1

    Field h, i, j, w, v;
    field_sub(h, u2, u1);         // h = u2 - u1
    field_add(r->Z, h, h);        // t2 = 2 * h
    field_sq(i, r->Z);            // i = t2^2
    field_mul(j, h, i);           // j = h * i
    field_sub(r->X, s2, s1);      // t3 = s2 - s1
    field_add(w, r->X, r->X);     // w = 2 * t3
    field_mul(v, u1, i);          // v = u1 * i

    // X3 = w^2 - j - 2*v
    field_sq(r->X, w);            // t4 = w^2
    field_add(r->Y, v, v);        // t5 = 2 * v
    field_sub(r->Z, r->X, j);     // t6 = t4 - j
    field_sub(r->X, r->Z, r->Y);  // t6 - t5

    // Y3 = w * (v - X3) - 2*s1*j
    field_sub(r->Y, v, r->X);     // t7 = v - X3
    field_mul(r->Z, s1, j);       // t8 = s1 * j
    field_add(s1, r->Z, r->Z);    // t9 = 2 * t8
    field_mul(r->Z, w, r->Y);     // t10 = w * t7
    field_sub(r->Y, r->Z, s1);    // w * (v - X3) - 2*s1*j

    // Z3 = ((Z1 + Z2)^2 - Z1Z1 - Z2Z2) * h
    field_add(r->Z, p->Z, q->Z);  // t11 = z1 + z2
    field_sq(s1, r->Z);           // t12 = (z1 + z2)^2
    field_sub(r->Z, s1, z1z1);    // t13 = (z1 + z2)^2 - z1z1
    field_sub(j, r->Z, z2z2);     // t14 = (z1 + z2)^2 - z1z1 - z2z2
    field_mul(r->Z, j, h);        // ((z1 + z2)^2 - z1z1 - z2z2) * h
}

// https://www.hyperelliptic.org/EFD/g1p/auto-code/shortw/jacobian-0/addition/madd-2007-bl.op3
// for p = (X1, Y1, Z1), q = (X2, Y2, Z2); assumes Z2 = 1
// cost 7M + 4S + 9add + 3*2 + 1*4 ?
void group_madd(Group *r, const Group *p, const Group *q)
{
    if (is_zero(p)) {
        *r = *q;
        return;
    }
    if (is_zero(q)) {
        *r = *p;
        return;
    }

    Field z1z1, u2;
    field_sq(z1z1, p->Z);            // z1z1 = Z1^2
    field_mul(u2, q->X, z1z1);       // u2 = X2 * z1z1

    Field s2;
    field_mul(r->X, p->Z, z1z1);     // t0 = Z1 * z1z1
    field_mul(s2, q->Y, r->X);       // s2 = Y2 * t0

    Field h, hh;
    field_sub(h, u2, p->X);          // h = u2 - X1
    field_sq(hh, h);                 // hh = h^2

    Field j, w, v;
    field_mul(r->X, FIELD_FOUR, hh); // i = 4 * hh
    field_mul(j, h, r->X);           // j = h * i
    field_sub(r->Y, s2, p->Y);       // t1 = s2 - Y1
    field_add(w, r->Y, r->Y);        // w = 2 * t1
    field_mul(v, p->X, r->X);        // v = X1 * i

    // X3 = w^2 - J - 2*V
    field_sq(r->X, w);               // t2 = w^2
    field_add(r->Y, v, v);           // t3 = 2*v
    field_sub(r->Z, r->X, j);        // t4 = t2 - j
    field_sub(r->X, r->Z, r->Y);     // X3 = w^2 - j - 2*v = t4 - t3

    // Y3 = w * (V - X3) - 2*Y1*J
    field_sub(r->Y, v, r->X);        // t5 = v - X3
    field_mul(v, p->Y, j);           // t6 = Y1 * j
    field_add(r->Z, v, v);           // t7 = 2 * t6
    field_mul(s2, w, r->Y);          // t8 = w * t5
    field_sub(r->Y, s2, r->Z);       // w * (v - X3) - 2*Y1*j = t8 - t7

    // Z3 = (Z1 + H)^2 - Z1Z1 - HH
    field_add(w, p->Z, h);           // t9 = Z1 + h
    field_sq(v, w);                  // t10 = t9^2
    field_sub(w, v, z1z1);           // t11 = t10 - z1z1
    field_sub(r->Z, w, hh);          // (Z1 + h)^2 - Z1Z1 - hh = t11 - hh
}

void group_scalar_mul(Group *r, const Scalar k, const Group *p)
{
    *r = GROUP_ZERO;
    if (is_zero(p)) {
        return;
    }
    if (scalar_eq(k, SCALAR_ZERO)) {
        return;
    }

    // Group r1 = *p;
    Group tmp;

    uint64_t k_bits[4];
    fiat_pasta_fq_from_montgomery(k_bits, k);

    // Not constant time
    for (size_t i = 0; i < FIELD_SIZE_IN_BITS; ++i) {
        size_t j = FIELD_SIZE_IN_BITS - 1 - i;
        size_t limb_idx = j / 64;
        size_t in_limb_idx = (j % 64);
        bool di = (k_bits[limb_idx] >> in_limb_idx) & 1;

        group_dbl(&tmp, r);

        if (di) {
          group_add(r, &tmp, p);
        } else {
          field_copy(r->X, tmp.X);
          field_copy(r->Y, tmp.Y);
          field_copy(r->Z, tmp.Z);
        }
    }
}

void group_negate(Group *q, const Group *p)
{
    field_copy(q->X, p->X);
    field_negate(q->Y, p->Y);
    field_copy(q->Z, p->Z);
}

void affine_scalar_mul(Affine *r, const Scalar k, const Affine *p)
{
    Group pp, pr;
    affine_to_group(&pp, p);
    group_scalar_mul(&pr, k, &pp);
    affine_from_group(r, &pr);
}

bool affine_eq(const Affine *p, const Affine *q)
{
    return field_eq(p->x, q->x) && field_eq(p->y, q->y);
}

void affine_add(Affine *r, const Affine *p, const Affine *q)
{
    Group gr, gp, gq;
    affine_to_group(&gp, p);
    affine_to_group(&gq, q);
    group_add(&gr, &gp, &gq);
    affine_from_group(r, &gr);
}

void affine_negate(Affine *q, const Affine *p)
{
    Group gq, gp;
    affine_to_group(&gp, p);
    group_negate(&gq, &gp);
    affine_from_group(q, &gq);
}

bool affine_is_on_curve(const Affine *p)
{
    Group gp;
    affine_to_group(&gp, p);
    return group_is_on_curve(&gp);
}

void roinput_print_fields(const ROInput *input) {
  for (size_t i = 0; i < LIMBS_PER_FIELD * input->fields_len; ++i) {
    printf("fs[%zu] = 0x%" PRIx64 "\n", i, input->fields[i]);
  }
}

void roinput_print_bits(const ROInput *input) {
  for (size_t i = 0; i < input->bits_len; ++i) {
    printf("bs[%zu] = %u\n", i, packed_bit_array_get(input->bits, i));
  }
}

// input for poseidon
void roinput_add_field(ROInput *input, const Field a) {
  int remaining = (int)input->fields_capacity - (int)input->fields_len;
  if (remaining < 1) {
    printf("fields at capacity\n");
    exit(1);
  }

  size_t offset = LIMBS_PER_FIELD * input->fields_len;

  fiat_pasta_fp_copy(input->fields + offset, a);

  input->fields_len += 1;
}

void roinput_add_bit(ROInput *input, bool b) {
  int remaining = (int)input->bits_capacity - (int)input->bits_len;

  if (remaining < 1) {
    printf("add_bit: bits at capacity\n");
    exit(1);
  }

  size_t offset = input->bits_len;

  packed_bit_array_set(input->bits, offset, b);
  input->bits_len += 1;
}

void roinput_add_scalar(ROInput *input, const Scalar a) {
  int remaining = (int)input->bits_capacity - (int)input->bits_len;
  const size_t len = FIELD_SIZE_IN_BITS;

  uint64_t scalar_bigint[4];
  fiat_pasta_fq_from_montgomery(scalar_bigint, a);

  if (remaining < len) {
    printf("add_scalar: bits at capacity\n");
    exit(1);
  }

  size_t offset = input->bits_len;
  for (size_t i = 0; i < len; ++i) {
    size_t limb_idx = i / 64;
    size_t in_limb_idx = (i % 64);
    bool b = (scalar_bigint[limb_idx] >> in_limb_idx) & 1;
    packed_bit_array_set(input->bits, offset + i, b);
  }

  input->bits_len += len;
}

void roinput_add_bytes(ROInput *input, const uint8_t *bytes, size_t len) {
  int remaining = (int)input->bits_capacity - (int)input->bits_len;
  if (remaining < 8 * len) {
    printf("add_bytes: bits at capacity (bytes)\n");
    exit(1);
  }

  // LSB bits
  size_t k = input->bits_len;
  for (size_t i = 0; i < len; ++i) {
    const uint8_t b = bytes[i];

    for (size_t j = 0; j < 8; ++j) {
      packed_bit_array_set(input->bits, k, (b >> j) & 1);
      ++k;
    }
  }

  input->bits_len += 8 * len;
}

void roinput_add_uint32(ROInput *input, const uint32_t x) {
  const size_t NUM_BYTES = 4;
  uint8_t le[NUM_BYTES];

  for (size_t i = 0; i < NUM_BYTES; ++i) {
    le[i] = (uint8_t) (0xff & (x >> (8 * i)));
  }

  roinput_add_bytes(input, le, NUM_BYTES);
}

void roinput_add_uint64(ROInput *input, const uint64_t x) {
  const size_t NUM_BYTES = 8;
  uint8_t le[NUM_BYTES];

  for (size_t i = 0; i < NUM_BYTES; ++i) {
    le[i] = (uint8_t) (0xff & (x >> (8 * i)));
  }

  roinput_add_bytes(input, le, NUM_BYTES);
}

void roinput_to_bytes(uint8_t *out, const ROInput *input) {
  size_t bit_idx = 0;

  Field tmp;

  // first the field elements, then the bitstrings
  for (size_t i = 0; i < input->fields_len; ++i) {
    fiat_pasta_fp_from_montgomery(tmp, input->fields + (i * LIMBS_PER_FIELD));

    for (size_t j = 0; j < FIELD_SIZE_IN_BITS; ++j) {
      size_t limb_idx = j / 64;
      size_t in_limb_idx = (j % 64);
      bool b = (tmp[limb_idx] >> in_limb_idx) & 1;

      packed_bit_array_set(
          out
          , bit_idx
          , b);
      bit_idx += 1;
    }
  }

  for (size_t i = 0; i < input->bits_len; ++i) {
    packed_bit_array_set(out, bit_idx, packed_bit_array_get(input->bits, i));
    bit_idx += 1;
  }
}

size_t roinput_to_fields(uint64_t *out, const ROInput *input) {
  size_t output_len = 0;

  // Copy over the field elements
  for (size_t i = 0; i < input->fields_len; ++i) {
    size_t offset = i * LIMBS_PER_FIELD;
    fiat_pasta_fp_copy(out + offset, input->fields + offset);
  }
  output_len += input->fields_len;

  size_t bits_consumed = 0;

  // pack in the bits
  uint64_t* next_chunk = out + input->fields_len * LIMBS_PER_FIELD;
  const size_t MAX_CHUNK_SIZE = FIELD_SIZE_IN_BITS - 1;
  while (bits_consumed < input->bits_len) {
    uint64_t chunk_non_montgomery[4] = { 0, 0, 0, 0 };

    size_t remaining = input->bits_len - bits_consumed;
    size_t chunk_size_in_bits = remaining >= MAX_CHUNK_SIZE ? MAX_CHUNK_SIZE : remaining;

    for (size_t i = 0; i < chunk_size_in_bits; ++i) {
      size_t limb_idx = i / 64;
      size_t in_limb_idx = (i % 64);
      size_t b = packed_bit_array_get(input->bits, bits_consumed + i);

      chunk_non_montgomery[limb_idx] =  chunk_non_montgomery[limb_idx] | (((uint64_t) b) << in_limb_idx);
    }
    fiat_pasta_fp_to_montgomery(next_chunk, chunk_non_montgomery);

    output_len += 1;
    bits_consumed += chunk_size_in_bits;
    next_chunk += LIMBS_PER_FIELD;
  }

  return output_len;
}

void generate_keypair(Keypair *keypair, uint32_t account)
{
    if (!keypair) {
        THROW(INVALID_PARAMETER);
    }

    uint64_t priv_non_montgomery[4] = { 0, 0, 0, 0 };
    FILE* fr = fopen("/dev/urandom", "r");
    if (!fr) perror("urandom"), exit(EXIT_FAILURE);
    fread((void*)priv_non_montgomery, sizeof(uint8_t), 32, fr);
    fclose(fr), fr = NULL;

    // Make sure the private key is in [0, p)
    //
    // Note: Mina does rejection sampling to obtain a private key in
    // [0, p), where the field modulus
    //
    //     p = 28948022309329048855892746252171976963363056481941560715954676764349967630337
    //
    // Due to constraints, this implementation take a different
    // approach and just unsets the top two bits of the 256bit bip44
    // secret, so
    //
    //     max = 28948022309329048855892746252171976963317496166410141009864396001978282409983.
    //
    // If p < max then we could still generate invalid private keys
    // (although it's highly unlikely), but
    //
    //     p - max = 45560315531419706090280762371685220354
    //
    // Thus, we cannot generate invalid private keys and instead lose an
    // insignificant amount of entropy.

    priv_non_montgomery[3] &= (((uint64_t)1 << 62) - 1); // drop top two bits
    fiat_pasta_fq_to_montgomery(keypair->priv, priv_non_montgomery);

    affine_scalar_mul(&keypair->pub, keypair->priv, &AFFINE_ONE);

    return;
}

void generate_pubkey(Affine *pub_key, const Scalar priv_key)
{
    affine_scalar_mul(pub_key, priv_key, &AFFINE_ONE);
}

bool generate_address(char *address, const size_t len, const Affine *pub_key)
{
    address[0] = '\0';

    assert (len == MINA_ADDRESS_LEN);
    if (len != MINA_ADDRESS_LEN) {
        return false;
    }

    struct bytes {
        uint8_t version;
        uint8_t payload[35];
        uint8_t checksum[4];
    } raw;

    raw.version    = 0xcb; // version for base58 check
    raw.payload[0] = 0x01; // non_zero_curve_point version
    raw.payload[1] = 0x01; // compressed_poly version

    // x-coordinate
    fiat_pasta_fp_from_montgomery((uint64_t *)&raw.payload[2], pub_key->x);

    // y-coordinate parity
    raw.payload[34] = field_is_odd(pub_key->y);

    uint8_t hash1[SHA256_BLOCK_SIZE];
    sha256_hash(&raw, 36, hash1, sizeof(hash1));

    uint8_t hash2[SHA256_BLOCK_SIZE];
    sha256_hash(hash1, sizeof(hash1), hash2, sizeof(hash2));

    memcpy(raw.checksum, hash2, 4);

    // Encode as address
    size_t out_len = len;
    bool result = b58enc(address, &out_len, &raw, sizeof(raw));
    address[MINA_ADDRESS_LEN - 1] = '\0';
    assert(out_len == len);
    if (out_len != len) {
        return false;
    }
    return result;
}

void message_derive(Scalar out, const Keypair *kp, const ROInput *msg, uint8_t network_id)
{
    ROInput input;
    uint64_t input_fields[LIMBS_PER_FIELD * (msg->fields_capacity + 2)];
    uint8_t input_bits[msg->bits_capacity/8 + SCALAR_BYTES + 1];
    size_t bits_capacity = 8 * sizeof(input_bits);
    uint8_t input_bytes[sizeof(input_fields) + sizeof(input_bits)];
    bzero(input_bytes, sizeof(input_bytes));

    input.fields = input_fields;
    input.bits = input_bits;

    for (size_t i = 0; i < msg->fields_len * LIMBS_PER_FIELD; ++i) {
      input.fields[i] = msg->fields[i];
    }
    memcpy(input.bits, msg->bits, sizeof(uint8_t) * ((msg->bits_len + 7) / 8));

    input.fields_len = msg->fields_len;
    input.bits_len = msg->bits_len;
    input.fields_capacity = 5;
    input.bits_capacity = bits_capacity;

    roinput_add_field(&input, kp->pub.x);
    roinput_add_field(&input, kp->pub.y);
    roinput_add_scalar(&input, kp->priv);
    roinput_add_bytes(&input, &network_id, 1);

    size_t input_size_in_bits = input.bits_len + FIELD_SIZE_IN_BITS * input.fields_len;
    size_t input_size_in_bytes = (input_size_in_bits + 7) / 8;
    assert(input_size_in_bytes <= sizeof(input_bytes));
    roinput_to_bytes(input_bytes, &input);

    uint8_t hash_out[32];
    blake2b(hash_out, 32, input_bytes, input_size_in_bytes, NULL, 0);

    // take 254 bits / drop the top 2 bits
    packed_bit_array_set(hash_out, 255, 0);
    packed_bit_array_set(hash_out, 254, 0);

    uint64_t tmp[4] = { 0, 0, 0, 0 };
    for (size_t i = 0; i < 4; ++i) {
      // 8 bytes
      for (size_t j = 0; j < 8; ++j) {
        tmp[i] |= ((uint64_t) hash_out[8*i + j]) << (8 * j);
      }
    }
    fiat_pasta_fq_to_montgomery(out, tmp);
}

void message_hash(Scalar out, const Affine *pub, const Field rx, const ROInput *msg, const uint8_t hash_type, const uint8_t network_id)
{
    ROInput input;

    uint64_t input_fields[LIMBS_PER_FIELD * (msg->fields_capacity + 3)];
    uint8_t input_bits[msg->bits_capacity/8];

    input.fields_capacity = msg->fields_capacity + 3;
    input.bits_capacity = 8 * sizeof(input_bits);
    assert(msg->bits_len <= input.bits_capacity);

    input.fields = input_fields;
    input.bits = input_bits;
    input.fields_len = msg->fields_len;
    input.bits_len = msg->bits_len;

    memcpy(input.fields, msg->fields, sizeof(uint64_t) * LIMBS_PER_FIELD * msg->fields_len);
    memcpy(input.bits, msg->bits, sizeof(uint8_t) * ((msg->bits_len + 7) / 8));

    roinput_add_field(&input, pub->x);
    roinput_add_field(&input, pub->y);
    roinput_add_field(&input, rx);

    // Initial sponge state
    PoseidonCtx ctx;
    poseidon_init(&ctx, hash_type, network_id);

    Field packed_elements[input.fields_len + (size_t)ceil((float)input.bits_len/(FIELD_SIZE_IN_BITS - 1))];
    size_t packed_elements_len = roinput_to_fields((uint64_t *)packed_elements, &input);
    assert(packed_elements_len == sizeof(packed_elements)/FIELD_BYTES);

    poseidon_update(&ctx, (Field *)packed_elements, packed_elements_len);
    poseidon_digest(out, &ctx);
}

#define FULL_BITS_LEN (FEE_BITS + TOKEN_ID_BITS + 1 + NONCE_BITS + GLOBAL_SLOT_BITS + MEMO_BITS + TAG_BITS + 1 + 1 + TOKEN_ID_BITS + AMOUNT_BITS + 1)
#define FULL_BITS_BYTES ((FULL_BITS_LEN + 7) / 8)

void compress(Compressed *compressed, const Affine *pt) {
  fiat_pasta_fp_copy(compressed->x, pt->x);

  Field y_bigint;
  fiat_pasta_fp_from_montgomery(y_bigint, pt->y);

  compressed->is_odd = y_bigint[0] & 1;
}

bool decompress(Affine *pt, const Compressed *compressed) {
  fiat_pasta_fp_copy(pt->x, compressed->x);

  Field x2;
  fiat_pasta_fp_square(x2, pt->x);
  Field x3;
  fiat_pasta_fp_mul(x3, x2, pt->x); // x^3
  Field y2;
  fiat_pasta_fp_add(y2, x3, GROUP_COEFF_B);

  Field y_pre;
  if (!fiat_pasta_fp_sqrt(y_pre, y2)) {
    return false;
  }
  Field y_pre_bigint;
  fiat_pasta_fp_from_montgomery(y_pre_bigint, y_pre);

  const bool y_pre_odd = (y_pre_bigint[0] & 1);
  if (y_pre_odd == compressed->is_odd) {
    fiat_pasta_fp_copy(pt->y, y_pre);
  } else {
    fiat_pasta_fp_opp(pt->y, y_pre);
  }

  return true;
}

void read_public_key_compressed(Compressed *out, const char *pubkeyBase58) {
  size_t pubkeyBytesLen = 40;
  unsigned char pubkeyBytes[40];
  b58tobin(pubkeyBytes, &pubkeyBytesLen, pubkeyBase58, 0);

  uint64_t x_coord_non_montgomery[4] = { 0, 0, 0, 0 };

  size_t offset = 3;
  for (size_t i = 0; i < 4; ++i) {
    const size_t BYTES_PER_LIMB = 8;
    // 8 bytes per limb
    for (size_t j = 0; j < BYTES_PER_LIMB; ++j) {
      size_t k = offset + BYTES_PER_LIMB * i + j;
      x_coord_non_montgomery[i] |= ( ((uint64_t) pubkeyBytes[k]) << (8 * j));
    }
  }

  fiat_pasta_fp_to_montgomery(out->x, x_coord_non_montgomery);
  out->is_odd = (bool) pubkeyBytes[offset + 32];
}

void prepare_memo(uint8_t *out, const char *s) {
  size_t len = strlen(s);
  out[0] = 1;
  out[1] = len; // length
  for (size_t i = 0; i < len; ++i) {
    out[2 + i] = s[i];
  }
  for (size_t i = 2 + len; i < MEMO_BYTES; ++i) {
    out[i] = 0;
  }
}

bool verify(Signature *sig, const Compressed *pub_compressed, const Transaction *transaction, uint8_t network_id)
{
    // Convert transaction to ROInput
    uint64_t input_fields[4 * 3];
    uint8_t input_bits[FULL_BITS_BYTES];
    ROInput input;
    input.fields_capacity = 3;
    input.bits_capacity = 8 * FULL_BITS_BYTES;
    input.fields = input_fields;
    input.bits = input_bits;
    input.fields_len = 0;
    input.bits_len = 0;

    roinput_add_field(&input, transaction->fee_payer_pk.x);
    roinput_add_field(&input, transaction->source_pk.x);
    roinput_add_field(&input, transaction->receiver_pk.x);

    roinput_add_uint64(&input, transaction->fee);
    roinput_add_uint64(&input, transaction->fee_token);
    roinput_add_bit(&input, transaction->fee_payer_pk.is_odd);
    roinput_add_uint32(&input, transaction->nonce);
    roinput_add_uint32(&input, transaction->valid_until);
    roinput_add_bytes(&input, transaction->memo, MEMO_BYTES);
    for (size_t i = 0; i < 3; ++i) {
      roinput_add_bit(&input, transaction->tag[i]);
    }
    roinput_add_bit(&input, transaction->source_pk.is_odd);
    roinput_add_bit(&input, transaction->receiver_pk.is_odd);
    roinput_add_uint64(&input, transaction->token_id);
    roinput_add_uint64(&input, transaction->amount);
    roinput_add_bit(&input, transaction->token_locked);

    Affine pub;
    if (!decompress(&pub, pub_compressed)) {
      return false;
    }

    Scalar e;
    message_hash(e, &pub, sig->rx, &input, POSEIDON_3W, network_id);

    Group g;
    affine_to_group(&g, &AFFINE_ONE);

    Group sg;
    group_scalar_mul(&sg, sig->s, &g);

    Group pub_proj;
    affine_to_group(&pub_proj, &pub);
    Group epub;
    group_scalar_mul(&epub, e, &pub_proj);

    Group neg_epub;
    fiat_pasta_fp_copy(neg_epub.X, epub.X);
    fiat_pasta_fp_opp(neg_epub.Y, epub.Y);
    fiat_pasta_fp_copy(neg_epub.Z, epub.Z);

    Group r;
    group_add(&r, &sg, &neg_epub);

    Affine raff;
    affine_from_group(&raff, &r);

    Field ry_bigint;
    fiat_pasta_fp_from_montgomery(ry_bigint, raff.y);

    const bool ry_even = (ry_bigint[0] & 1) == 0;

    return (ry_even && fiat_pasta_fp_equals(raff.x, sig->rx));
}

void sign(Signature *sig, const Keypair *kp, const Transaction *transaction, uint8_t network_id)
{
    // Convert transaction to ROInput
    uint64_t input_fields[4 * 3];
    uint8_t input_bits[FULL_BITS_BYTES];
    ROInput input;
    input.fields_capacity = 3;
    input.bits_capacity = 8 * FULL_BITS_BYTES;
    input.fields = input_fields;
    input.bits = input_bits;
    input.fields_len = 0;
    input.bits_len = 0;

    roinput_add_field(&input, transaction->fee_payer_pk.x);
    roinput_add_field(&input, transaction->source_pk.x);
    roinput_add_field(&input, transaction->receiver_pk.x);

    roinput_add_uint64(&input, transaction->fee);
    roinput_add_uint64(&input, transaction->fee_token);
    roinput_add_bit(&input, transaction->fee_payer_pk.is_odd);
    roinput_add_uint32(&input, transaction->nonce);
    roinput_add_uint32(&input, transaction->valid_until);
    roinput_add_bytes(&input, transaction->memo, MEMO_BYTES);
    for (size_t i = 0; i < 3; ++i) {
      roinput_add_bit(&input, transaction->tag[i]);
    }
    roinput_add_bit(&input, transaction->source_pk.is_odd);
    roinput_add_bit(&input, transaction->receiver_pk.is_odd);
    roinput_add_uint64(&input, transaction->token_id);
    roinput_add_uint64(&input, transaction->amount);
    roinput_add_bit(&input, transaction->token_locked);

    Scalar k;
    message_derive(k, kp, &input, network_id);

    uint64_t k_nonzero;
    fiat_pasta_fq_nonzero(&k_nonzero, k);
    if (! k_nonzero) {
      exit(1);
    }

    // r = k*g
    Affine r;
    affine_scalar_mul(&r, k, &AFFINE_ONE);

    field_copy(sig->rx, r.x);

    if (field_is_odd(r.y)) {
        // negate (k = -k)
        Scalar tmp;
        fiat_pasta_fq_copy(tmp, k);
        scalar_negate(k, tmp);
    }

    Scalar e;
    message_hash(e, &kp->pub, r.x, &input, POSEIDON_3W, network_id);

    // s = k + e*sk
    Scalar e_priv;
    scalar_mul(e_priv, e, kp->priv);
    scalar_add(sig->s, k, e_priv);
}


<|start_filename|>poseidon.c<|end_filename|>
/*******************************************************************************
 * Poseidon is used to hash to a field in the schnorr signature scheme we use.
 * In order to be efficiently computed within the snark, it is computed using
 * the base field of the elliptic curve, and the result is then used as a
 * scalar field element, to scale the elliptic curve point. We do all of the
 * computation in this file in the base field, but output the result as a scalar.
 ********************************************************************************/

#include <assert.h>

#include "crypto.h"
#include "pasta_fp.h"
#include "pasta_fq.h"
#include "poseidon.h"
#include "poseidon_params_3w.h"
#include "poseidon_params_5w.h"
#include "poseidon_params_3.h"

#define SPONGE_BYTES(sponge_width) (sizeof(Field)*sponge_width)
#define ROUND_KEY(ctx, round, idx) *(Field *)(ctx->round_keys + (round*ctx->sponge_width + idx)*LIMBS_PER_FIELD)
#define MATRIX_ELT(m, row, col, width) *(Field *)(m + (row*width + col)*LIMBS_PER_FIELD)

static void matrix_mul(State s1, const Field **m, const size_t width)
{
    Field tmp;

    State s2;
    bzero(s2, sizeof(s2));
    for (size_t row = 0; row < width; row++) {
        // Inner product
        for (size_t col = 0; col < width; col++) {
            Field t0;
            field_mul(t0, s1[col], MATRIX_ELT(m, row, col, width));
            field_copy(tmp, s2[row]);
            field_add(s2[row], tmp, t0);
        }
    }

    for (size_t col = 0; col < width; col++) {
        field_copy(s1[col], s2[col]);
    }
}

// 3-wire poseidon permutation function
static void permutation_3w(PoseidonCtx *ctx)
{
    Field tmp;

    // Full rounds only
    for (size_t r = 0; r < ctx->full_rounds; r++) {
        // ark
        for (size_t i = 0; i < ctx->sponge_width; i++) {
            field_copy(tmp, ctx->state[i]);
            field_add(ctx->state[i], tmp, ROUND_KEY(ctx, r, i));
        }

        // sbox
        for (size_t i = 0; i < ctx->sponge_width; i++) {
            field_copy(tmp, ctx->state[i]);
            field_pow(ctx->state[i], tmp, ctx->sbox_alpha);
        }

        // mds
        matrix_mul(ctx->state, ctx->mds_matrix, ctx->sponge_width);
    }

    // Final ark
    for (size_t i = 0; i < ctx->sponge_width; i++) {
        field_copy(tmp, ctx->state[i]);
        field_add(ctx->state[i], tmp, ROUND_KEY(ctx, ctx->full_rounds, i));
    }
}

static void permutation(PoseidonCtx *ctx)
{
    Field tmp;

    // Full rounds only
    for (size_t r = 0; r < ctx->full_rounds; r++) {
        // sbox
        for (unsigned int i = 0; i < ctx->sponge_width; i++) {
            field_copy(tmp, ctx->state[i]);
            field_pow(ctx->state[i], tmp, ctx->sbox_alpha);
        }

        // mds
        matrix_mul(ctx->state, ctx->mds_matrix, ctx->sponge_width);

        // ark
        for (unsigned int i = 0; i < ctx->sponge_width; i++) {
            field_copy(tmp, ctx->state[i]);
            field_add(ctx->state[i], tmp, ROUND_KEY(ctx, r, i));
        }
    }
}

struct poseidon_config_t {
    size_t sponge_width;
    size_t sponge_rate;
    size_t full_rounds;
    size_t sbox_alpha;
    const Field ***round_keys;
    const Field **mds_matrix;
    const Field *sponge_iv[2];
    void (*permutation)(PoseidonCtx *);
} _poseidon_config[3] = {
    // 0x00 - POSEIDON_3W
    {
        .sponge_width = SPONGE_WIDTH_3W,
        .sponge_rate  = SPONGE_RATE_3W,
        .full_rounds  = ROUND_COUNT_3W - 1,
        .sbox_alpha   = SBOX_ALPHA_3W,
        .round_keys   = (const Field ***)round_keys_3w,
        .mds_matrix   = (const Field **)mds_matrix_3w,
        .sponge_iv    = {
            (const Field *)testnet_iv_3w,
            (const Field *)mainnet_iv_3w
        },
        .permutation = permutation_3w
    },
    // 0x01 - POSEIDON_5W
    {
        .sponge_width = SPONGE_WIDTH_5W,
        .sponge_rate  = SPONGE_RATE_5W,
        .full_rounds  = ROUND_COUNT_5W,
        .sbox_alpha   = SBOX_ALPHA_5W,
        .round_keys   = (const Field ***)round_keys_5w,
        .mds_matrix   = (const Field **)mds_matrix_5w,
        .sponge_iv    = {
            (const Field *)testnet_iv_5w,
            (const Field *)mainnet_iv_5w
        },
        .permutation = permutation
    },
    // 0x02 - POSEIDON_3
    {
        .sponge_width = SPONGE_WIDTH_3,
        .sponge_rate  = SPONGE_RATE_3,
        .full_rounds  = ROUND_COUNT_3,
        .sbox_alpha   = SBOX_ALPHA_3,
        .round_keys   = (const Field ***)round_keys_3,
        .mds_matrix   = (const Field **)mds_matrix_3,
        .sponge_iv    = {
            (const Field *)testnet_iv_3,
            (const Field *)mainnet_iv_3
        },
        .permutation = permutation
    }
};

bool poseidon_init(PoseidonCtx *ctx, const uint8_t type, const uint8_t network_id)
{
    if (!ctx) {
      return false;
    }

    if (type != POSEIDON_3W &&
        type != POSEIDON_5W &&
        type != POSEIDON_3) {
        return false;
    }

    if (network_id != TESTNET_ID &&
        network_id != MAINNET_ID &&
        network_id != NULLNET_ID) {
        return false;
    }

    ctx->sponge_width = _poseidon_config[type].sponge_width;
    ctx->sponge_rate  = _poseidon_config[type].sponge_rate;
    ctx->full_rounds  = _poseidon_config[type].full_rounds;
    ctx->sbox_alpha   = _poseidon_config[type].sbox_alpha;
    ctx->round_keys   = _poseidon_config[type].round_keys;
    ctx->mds_matrix   = _poseidon_config[type].mds_matrix;
    ctx->permutation  = _poseidon_config[type].permutation;

    if (network_id != NULLNET_ID) {
        memcpy(ctx->state, _poseidon_config[type].sponge_iv[network_id],
               SPONGE_BYTES(ctx->sponge_width));
    }
    else {
        bzero(ctx->state, SPONGE_BYTES(ctx->sponge_width));
    }

    ctx->absorbed = 0;

    return true;
}

void poseidon_update(PoseidonCtx *ctx, const Field *input, size_t len)
{
    Field tmp;
    for (size_t i = 0; i < len; i++) {
        if (ctx->absorbed == ctx->sponge_rate) {
            ctx->permutation(ctx);
            ctx->absorbed = 0;
        }
        field_copy(tmp, ctx->state[ctx->absorbed]);
        field_add(ctx->state[ctx->absorbed], tmp, input[i]);
        ctx->absorbed++;
    }
}

// Squeezing poseidon returns the first element of its current state.
void poseidon_digest(Scalar out, PoseidonCtx *ctx) {
    ctx->permutation(ctx);

    uint64_t tmp[4];
    fiat_pasta_fp_from_montgomery(tmp, ctx->state[0]);

    // since the difference in modulus between the two fields is < 2^125,
    // with high probability, a random value from one field will fit in the
    // other field.
    fiat_pasta_fq_to_montgomery(out, tmp);
}
