INNER CODE UNIT · C

x1

gost-engine/engine · ecp_id_GostR3410_2001_CryptoPro_A_ParamSet.c:143

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

/*
 * The function fiat_id_GostR3410_2001_CryptoPro_A_ParamSet_subborrowx_u52 is a subtraction with borrow.
 * Postconditions:
 *   out1 = (-arg1 + arg2 + -arg3) mod 2^52
 *   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^52⌋
 *
 * Input Bounds:
 *   arg1: [0x0 ~> 0x1]
 *   arg2: [0x0 ~> 0xfffffffffffff]
 *   arg3: [0x0 ~> 0xfffffffffffff]
 * Output Bounds:

View source record →