INNER CODE UNIT · C

x2

gost-engine/engine · ecp_id_GostR3410_2001_CryptoPro_A_ParamSet.c:253

    x2 = ((fiat_id_GostR3410_2001_CryptoPro_A_ParamSet_int1)(0x0 - x1) &
          UINT64_C(0xffffffffffffffff));
    x3 =
        ((fiat_id_GostR3410_2001_CryptoPro_A_ParamSet_value_barrier_u64(x2) &
          arg3) |
         (fiat_id_GostR3410_2001_CryptoPro_A_ParamSet_value_barrier_u64((~x2)) &
          arg2));
    *out1 = x3;
}

/*
 * The function fiat_id_GostR3410_2001_CryptoPro_A_ParamSet_carry_mul multiplies two field elements and reduces the result.
 * Postconditions:
 *   eval out1 mod m = (eval arg1 * eval arg2) mod m
 *
 * Input Bounds:
 *   arg1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
 *   arg2: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]

View source record →