fiat_25519_uint1
static FIAT_25519_FIAT_INLINE void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
fiat_25519_uint1 x1;
*out2 = (fiat_25519_uint1)(0x0 - x2);
fiat_25519_uint1 x145;
static FIAT_25519_FIAT_INLINE void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
fiat_25519_uint1 x1;
x145 = (fiat_25519_uint1)(x144 >> 25);
fiat_25519_uint1 x118;
x118 = (fiat_25519_uint1)(x117 >> 25);
x12 = ((fiat_25519_uint1)(x11 >> 26) + (x2 & UINT32_C(0x1ffffff)));
x15 = ((fiat_25519_uint1)(x12 >> 25) + (x3 & UINT32_C(0x3ffffff)));
fiat_25519_uint1 x2;
fiat_25519_uint1 x4;
fiat_25519_uint1 x6;
fiat_25519_uint1 x8;
fiat_25519_uint1 x10;
fiat_25519_uint1 x12;
fiat_25519_uint1 x14;
fiat_25519_uint1 x16;
fiat_25519_uint1 x18;
fiat_25519_uint1 x20;
fiat_25519_uint1 x23;
fiat_25519_uint1 x25;
fiat_25519_uint1 x27;
fiat_25519_uint1 x29;
fiat_25519_uint1 x31;
fiat_25519_uint1 x33;
fiat_25519_uint1 x35;
fiat_25519_uint1 x37;
fiat_25519_uint1 x39;
fiat_25519_uint1 x41;
fiat_25519_uint1 x50;
fiat_25519_uint1 x89;
x89 = (fiat_25519_uint1)(x87 >> 8);
x50 = (fiat_25519_uint1)(x49 >> 51);
fiat_25519_uint1 x48;
x48 = (fiat_25519_uint1)(x47 >> 51);
x7 = ((fiat_25519_uint1)(x6 >> 51) + (x2 & UINT64_C(0x7ffffffffffff)));
x10 = ((fiat_25519_uint1)(x7 >> 51) + (x3 & UINT64_C(0x7ffffffffffff)));
fiat_25519_uint1 x2;
fiat_25519_uint1 x4;
fiat_25519_uint1 x6;
fiat_25519_uint1 x8;
fiat_25519_uint1 x10;
fiat_25519_uint1 x13;
fiat_25519_uint1 x15;
fiat_25519_uint1 x17;
fiat_25519_uint1 x19;
fiat_25519_uint1 x21;
fiat_25519_uint1 x65;
x65 = (fiat_25519_uint1)(x63 >> 8);
static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
fiat_25519_uint1 x3;
x3 = (fiat_25519_uint1)(x1 >> 51);
static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
fiat_25519_uint1 x3;
x3 = (fiat_25519_uint1)(x1 >> 26);
static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
*out2 = (fiat_25519_uint1)(0x0 - x2);
static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
fiat_25519_uint1 x3;
x3 = (fiat_25519_uint1)(x1 >> 25);
static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
*out2 = (fiat_25519_uint1)(0x0 - x2);