third_party/fiat/p521_64.h
static void fiat_secp521r1_carry_sub(
    fiat_secp521r1_tight_field_element out1,
    const fiat_secp521r1_tight_field_element arg1,
    const fiat_secp521r1_tight_field_element arg2) {
    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;
    uint64_t x14;
    uint64_t x15;
    uint64_t x16;
    uint64_t x17;
    uint64_t x18;
    uint64_t x19;
    uint64_t x20;
    x1 = ((UINT64_C(0x7fffffffffffffe) + (arg1[0])) - (arg2[0]));
    x2 = ((x1 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[1])) - (arg2[1])));
    x3 = ((x2 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[2])) - (arg2[2])));
    x4 = ((x3 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[3])) - (arg2[3])));
    x5 = ((x4 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[4])) - (arg2[4])));
    x6 = ((x5 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[5])) - (arg2[5])));
    x7 = ((x6 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[6])) - (arg2[6])));
    x8 = ((x7 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[7])) - (arg2[7])));
    x9 = ((x8 >> 58) + ((UINT64_C(0x3fffffffffffffe) + (arg1[8])) - (arg2[8])));
    x10 = ((x1 & UINT64_C(0x3ffffffffffffff)) + (x9 >> 57));
    x11 = ((fiat_secp521r1_uint1)(x10 >> 58) +
           (x2 & UINT64_C(0x3ffffffffffffff)));
    x12 = (x10 & UINT64_C(0x3ffffffffffffff));
    x13 = (x11 & UINT64_C(0x3ffffffffffffff));
    x14 = ((fiat_secp521r1_uint1)(x11 >> 58) +
           (x3 & UINT64_C(0x3ffffffffffffff)));
    x15 = (x4 & UINT64_C(0x3ffffffffffffff));
    x16 = (x5 & UINT64_C(0x3ffffffffffffff));
    x17 = (x6 & UINT64_C(0x3ffffffffffffff));
    x18 = (x7 & UINT64_C(0x3ffffffffffffff));
    x19 = (x8 & UINT64_C(0x3ffffffffffffff));
    x20 = (x9 & UINT64_C(0x1ffffffffffffff));
    out1[0] = x12;
    out1[1] = x13;
    out1[2] = x14;
    out1[3] = x15;
    out1[4] = x16;
    out1[5] = x17;
    out1[6] = x18;
    out1[7] = x19;
    out1[8] = x20;
}
/*
 * The function fiat_secp521r1_carry_sub subtracts two field elements.
 *
 * Postconditions:
 *   eval out1 mod m = (eval arg1 - eval arg2) mod m
 *
 */
The function fiat_secp521r1_carry_sub subtracts two field elements.
Postconditions:
eval out1 mod m = (eval arg1 - eval arg2) mod m
The function fiat_secp521r1_carry_sub subtracts two field elements . Postconditions : eval out1 mod m = ( eval arg1 - eval arg2 ) mod m
static void fiat_secp521r1_carry_sub(
    fiat_secp521r1_tight_field_element out1,
    const fiat_secp521r1_tight_field_element arg1,
    const fiat_secp521r1_tight_field_element arg2) {
    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;
    uint64_t x14;
    uint64_t x15;
    uint64_t x16;
    uint64_t x17;
    uint64_t x18;
    uint64_t x19;
    uint64_t x20;
    x1 = ((UINT64_C(0x7fffffffffffffe) + (arg1[0])) - (arg2[0]));
    x2 = ((x1 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[1])) - (arg2[1])));
    x3 = ((x2 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[2])) - (arg2[2])));
    x4 = ((x3 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[3])) - (arg2[3])));
    x5 = ((x4 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[4])) - (arg2[4])));
    x6 = ((x5 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[5])) - (arg2[5])));
    x7 = ((x6 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[6])) - (arg2[6])));
    x8 = ((x7 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[7])) - (arg2[7])));
    x9 = ((x8 >> 58) + ((UINT64_C(0x3fffffffffffffe) + (arg1[8])) - (arg2[8])));
    x10 = ((x1 & UINT64_C(0x3ffffffffffffff)) + (x9 >> 57));
    x11 = ((fiat_secp521r1_uint1)(x10 >> 58) +
           (x2 & UINT64_C(0x3ffffffffffffff)));
    x12 = (x10 & UINT64_C(0x3ffffffffffffff));
    x13 = (x11 & UINT64_C(0x3ffffffffffffff));
    x14 = ((fiat_secp521r1_uint1)(x11 >> 58) +
           (x3 & UINT64_C(0x3ffffffffffffff)));
    x15 = (x4 & UINT64_C(0x3ffffffffffffff));
    x16 = (x5 & UINT64_C(0x3ffffffffffffff));
    x17 = (x6 & UINT64_C(0x3ffffffffffffff));
    x18 = (x7 & UINT64_C(0x3ffffffffffffff));
    x19 = (x8 & UINT64_C(0x3ffffffffffffff));
    x20 = (x9 & UINT64_C(0x1ffffffffffffff));
    out1[0] = x12;
    out1[1] = x13;
    out1[2] = x14;
    out1[3] = x15;
    out1[4] = x16;
    out1[5] = x17;
    out1[6] = x18;
    out1[7] = x19;
    out1[8] = x20;
}
static void fiat_secp521r1_carry_sub ( fiat_secp521r1_tight_field_element out1 , const fiat_secp521r1_tight_field_element arg1 , const fiat_secp521r1_tight_field_element arg2 ) { 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 ; uint64_t x14 ; uint64_t x15 ; uint64_t x16 ; uint64_t x17 ; uint64_t x18 ; uint64_t x19 ; uint64_t x20 ; x1 = ( ( UINT64_C ( 0x7fffffffffffffe ) + ( arg1 [ 0 ] ) ) - ( arg2 [ 0 ] ) ) ; x2 = ( ( x1 >> 58 ) + ( ( UINT64_C ( 0x7fffffffffffffe ) + ( arg1 [ 1 ] ) ) - ( arg2 [ 1 ] ) ) ) ; x3 = ( ( x2 >> 58 ) + ( ( UINT64_C ( 0x7fffffffffffffe ) + ( arg1 [ 2 ] ) ) - ( arg2 [ 2 ] ) ) ) ; x4 = ( ( x3 >> 58 ) + ( ( UINT64_C ( 0x7fffffffffffffe ) + ( arg1 [ 3 ] ) ) - ( arg2 [ 3 ] ) ) ) ; x5 = ( ( x4 >> 58 ) + ( ( UINT64_C ( 0x7fffffffffffffe ) + ( arg1 [ 4 ] ) ) - ( arg2 [ 4 ] ) ) ) ; x6 = ( ( x5 >> 58 ) + ( ( UINT64_C ( 0x7fffffffffffffe ) + ( arg1 [ 5 ] ) ) - ( arg2 [ 5 ] ) ) ) ; x7 = ( ( x6 >> 58 ) + ( ( UINT64_C ( 0x7fffffffffffffe ) + ( arg1 [ 6 ] ) ) - ( arg2 [ 6 ] ) ) ) ; x8 = ( ( x7 >> 58 ) + ( ( UINT64_C ( 0x7fffffffffffffe ) + ( arg1 [ 7 ] ) ) - ( arg2 [ 7 ] ) ) ) ; x9 = ( ( x8 >> 58 ) + ( ( UINT64_C ( 0x3fffffffffffffe ) + ( arg1 [ 8 ] ) ) - ( arg2 [ 8 ] ) ) ) ; x10 = ( ( x1 & UINT64_C ( 0x3ffffffffffffff ) ) + ( x9 >> 57 ) ) ; x11 = ( ( fiat_secp521r1_uint1 ) ( x10 >> 58 ) + ( x2 & UINT64_C ( 0x3ffffffffffffff ) ) ) ; x12 = ( x10 & UINT64_C ( 0x3ffffffffffffff ) ) ; x13 = ( x11 & UINT64_C ( 0x3ffffffffffffff ) ) ; x14 = ( ( fiat_secp521r1_uint1 ) ( x11 >> 58 ) + ( x3 & UINT64_C ( 0x3ffffffffffffff ) ) ) ; x15 = ( x4 & UINT64_C ( 0x3ffffffffffffff ) ) ; x16 = ( x5 & UINT64_C ( 0x3ffffffffffffff ) ) ; x17 = ( x6 & UINT64_C ( 0x3ffffffffffffff ) ) ; x18 = ( x7 & UINT64_C ( 0x3ffffffffffffff ) ) ; x19 = ( x8 & UINT64_C ( 0x3ffffffffffffff ) ) ; x20 = ( x9 & UINT64_C ( 0x1ffffffffffffff ) ) ; out1 [ 0 ] = x12 ; out1 [ 1 ] = x13 ; out1 [ 2 ] = x14 ; out1 [ 3 ] = x15 ; out1 [ 4 ] = x16 ; out1 [ 5 ] = x17 ; out1 [ 6 ] = x18 ; out1 [ 7 ] = x19 ; out1 [ 8 ] = x20 ; }
The function fiat_secp521r1_carry_sub subtracts two field elements.
The function fiat_secp521r1_carry_sub subtracts two field elements .