Lines Matching refs:U
37 uint64_t b0 = b[0U]; in Hacl_Bignum_Modulo_carry_top()
41 b[0U] = b0_; in Hacl_Bignum_Modulo_carry_top()
48 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_copy_from_wide_()
63 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
74 for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_carry_wide_()
92 for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) in Hacl_Bignum_Fmul_shift_reduce()
99 output[0U] = tmp; in Hacl_Bignum_Fmul_shift_reduce()
100 b0 = output[0U]; in Hacl_Bignum_Fmul_shift_reduce()
101 output[0U] = (uint64_t)19U * b0; in Hacl_Bignum_Fmul_shift_reduce()
115 for (i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0 = i0 + (uint32_t)1U) in Hacl_Bignum_Fmul_mul_shift_reduce_()
129 uint64_t tmp[5U] = { 0U }; in Hacl_Bignum_Fmul_fmul()
130 memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]); in Hacl_Bignum_Fmul_fmul()
136 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fmul_fmul()
137 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); in Hacl_Bignum_Fmul_fmul()
151 b0 = t[0U]; in Hacl_Bignum_Fmul_fmul()
158 t[0U] = b0_; in Hacl_Bignum_Fmul_fmul()
160 i0 = output[0U]; in Hacl_Bignum_Fmul_fmul()
164 output[0U] = i0_; in Hacl_Bignum_Fmul_fmul()
172 uint64_t r0 = output[0U]; in Hacl_Bignum_Fsquare_fsquare__()
207 tmp[0U] = s0; in Hacl_Bignum_Fsquare_fsquare__()
227 b0 = tmp[0U]; in Hacl_Bignum_Fsquare_fsquare_()
234 tmp[0U] = b0_; in Hacl_Bignum_Fsquare_fsquare_()
236 i0 = output[0U]; in Hacl_Bignum_Fsquare_fsquare_()
240 output[0U] = i0_; in Hacl_Bignum_Fsquare_fsquare_()
265 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fsquare_fsquare_times()
266 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); in Hacl_Bignum_Fsquare_fsquare_times()
268 memcpy(output, input, (uint32_t)5U * sizeof input[0U]); in Hacl_Bignum_Fsquare_fsquare_times()
280 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fsquare_fsquare_times_inplace()
281 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); in Hacl_Bignum_Fsquare_fsquare_times_inplace()
289 uint64_t buf[20U] = { 0U }; in Hacl_Bignum_Crecip_crecip()
334 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fsum()
344 uint64_t tmp[5U] = { 0U }; in Hacl_Bignum_fdifference()
350 memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]); in Hacl_Bignum_fdifference()
351 b0 = tmp[0U]; in Hacl_Bignum_fdifference()
356 tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U; in Hacl_Bignum_fdifference()
363 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fdifference()
379 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_fscalar()
380 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); in Hacl_Bignum_fscalar()
389 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fscalar()
397 b0 = tmp[0U]; in Hacl_Bignum_fscalar()
404 tmp[0U] = b0_; in Hacl_Bignum_fscalar()
436 if (!(ctr == (uint32_t)0U)) in Hacl_EC_Point_swap_conditional_()
447 uint64_t swap1 = (uint64_t)0U - iswap; in Hacl_EC_Point_swap_conditional()
454 memcpy(output, input, (uint32_t)5U * sizeof input[0U]); in Hacl_EC_Point_copy()
457 (uint32_t)5U * sizeof (input + (uint32_t)5U)[0U]); in Hacl_EC_Point_copy()
476 output[0U] = output0; in Hacl_EC_Format_fexpand()
485 uint64_t t0 = input[0U]; in Hacl_EC_Format_fcontract_first_carry_pass()
498 input[0U] = t0_; in Hacl_EC_Format_fcontract_first_carry_pass()
513 uint64_t t0 = input[0U]; in Hacl_EC_Format_fcontract_second_carry_pass()
526 input[0U] = t0_; in Hacl_EC_Format_fcontract_second_carry_pass()
541 i0 = input[0U]; in Hacl_EC_Format_fcontract_second_carry_full()
545 input[0U] = i0_; in Hacl_EC_Format_fcontract_second_carry_full()
551 uint64_t a0 = input[0U]; in Hacl_EC_Format_fcontract_trim()
567 input[0U] = a0_; in Hacl_EC_Format_fcontract_trim()
576 uint64_t t0 = input[0U]; in Hacl_EC_Format_fcontract_store()
607 uint64_t buf[10U] = { 0U }; in Hacl_EC_Format_scalar_of_point()
633 uint64_t buf[40U] = { 0U }; in Hacl_EC_AddAndDouble_fmonty()
648 memcpy(origx, x, (uint32_t)5U * sizeof x[0U]); in Hacl_EC_AddAndDouble_fmonty()
651 memcpy(origxprime0, xprime, (uint32_t)5U * sizeof xprime[0U]); in Hacl_EC_AddAndDouble_fmonty()
662 memcpy(origxprime, xxprime, (uint32_t)5U * sizeof xxprime[0U]); in Hacl_EC_AddAndDouble_fmonty()
726 if (!(i == (uint32_t)0U)) in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
747 if (!(i == (uint32_t)0U)) in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
758 uint64_t point_buf[40U] = { 0U }; in Hacl_EC_Ladder_cmult()
764 nq[0U] = (uint64_t)1U; in Hacl_EC_Ladder_cmult()
771 uint64_t buf0[10U] = { 0U }; in Hacl_Curve25519_crypto_scalarmult()
776 z[0U] = (uint64_t)1U; in Hacl_Curve25519_crypto_scalarmult()
779 uint8_t e[32U] = { 0U }; in Hacl_Curve25519_crypto_scalarmult()
786 memcpy(e, secret, (uint32_t)32U * sizeof secret[0U]); in Hacl_Curve25519_crypto_scalarmult()
787 e0 = e[0U]; in Hacl_Curve25519_crypto_scalarmult()
792 e[0U] = e01; in Hacl_Curve25519_crypto_scalarmult()
796 uint64_t buf[15U] = { 0U }; in Hacl_Curve25519_crypto_scalarmult()
799 x[0U] = (uint64_t)1U; in Hacl_Curve25519_crypto_scalarmult()