INNER CODE UNIT · C

x1

gost-engine/engine · ecp_id_GostR3410_2001_CryptoPro_A_ParamSet.c:171

    x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
    x2 = (fiat_id_GostR3410_2001_CryptoPro_A_ParamSet_int1)(x1 >> 52);
    x3 = (x1 & UINT64_C(0xfffffffffffff));
    *out1 = x3;
    *out2 = (fiat_id_GostR3410_2001_CryptoPro_A_ParamSet_uint1)(0x0 - x2);
}

/*
 * The function fiat_id_GostR3410_2001_CryptoPro_A_ParamSet_addcarryx_u51 is an addition with carry.
 * Postconditions:
 *   out1 = (arg1 + arg2 + arg3) mod 2^51
 *   out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋
 *
 * Input Bounds:
 *   arg1: [0x0 ~> 0x1]
 *   arg2: [0x0 ~> 0x7ffffffffffff]
 *   arg3: [0x0 ~> 0x7ffffffffffff]
 * Output Bounds:

View source record →