Lines Matching refs:uint32_t
26 extern FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 x0, uint32_t x1);
39 uint64_t b0_ = b0 + (uint64_t)19U * (b4 >> (uint32_t)51U); in Hacl_Bignum_Modulo_carry_top()
47 uint32_t i; in Hacl_Bignum_Fproduct_copy_from_wide_()
48 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_copy_from_wide_()
62 uint32_t i; in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
63 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
73 uint32_t i; in Hacl_Bignum_Fproduct_carry_wide_()
74 for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_carry_wide_()
76 uint32_t ctr = i; in Hacl_Bignum_Fproduct_carry_wide_()
78 FStar_UInt128_uint128 tctrp1 = tmp[ctr + (uint32_t)1U]; in Hacl_Bignum_Fproduct_carry_wide_()
80 FStar_UInt128_uint128 c = FStar_UInt128_shift_right(tctr, (uint32_t)51U); in Hacl_Bignum_Fproduct_carry_wide_()
82 tmp[ctr + (uint32_t)1U] = FStar_UInt128_add(tctrp1, c); in Hacl_Bignum_Fproduct_carry_wide_()
91 uint32_t i; in Hacl_Bignum_Fmul_shift_reduce()
92 for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) in Hacl_Bignum_Fmul_shift_reduce()
94 uint32_t ctr = (uint32_t)5U - i - (uint32_t)1U; in Hacl_Bignum_Fmul_shift_reduce()
95 uint64_t z = output[ctr - (uint32_t)1U]; in Hacl_Bignum_Fmul_shift_reduce()
111 uint32_t i; in Hacl_Bignum_Fmul_mul_shift_reduce_()
114 uint32_t i0; in Hacl_Bignum_Fmul_mul_shift_reduce_()
115 for (i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0 = i0 + (uint32_t)1U) in Hacl_Bignum_Fmul_mul_shift_reduce_()
122 i = (uint32_t)4U; in Hacl_Bignum_Fmul_mul_shift_reduce_()
130 memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]); in Hacl_Bignum_Fmul_fmul()
131 KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U); in Hacl_Bignum_Fmul_fmul()
135 uint32_t _i; in Hacl_Bignum_Fmul_fmul()
136 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fmul_fmul()
156 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_Fmul_fmul()
163 i1_ = i1 + (i0 >> (uint32_t)51U); in Hacl_Bignum_Fmul_fmul()
232 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_Fsquare_fsquare_()
239 i1_ = i1 + (i0 >> (uint32_t)51U); in Hacl_Bignum_Fsquare_fsquare_()
248 uint32_t count1 in Hacl_Bignum_Fsquare_fsquare_times_()
251 uint32_t i; in Hacl_Bignum_Fsquare_fsquare_times_()
253 for (i = (uint32_t)1U; i < count1; i = i + (uint32_t)1U) in Hacl_Bignum_Fsquare_fsquare_times_()
258 Hacl_Bignum_Fsquare_fsquare_times(uint64_t *output, uint64_t *input, uint32_t count1) in Hacl_Bignum_Fsquare_fsquare_times()
260 KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U); in Hacl_Bignum_Fsquare_fsquare_times()
264 uint32_t _i; in Hacl_Bignum_Fsquare_fsquare_times()
265 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fsquare_fsquare_times()
268 memcpy(output, input, (uint32_t)5U * sizeof input[0U]); in Hacl_Bignum_Fsquare_fsquare_times()
273 inline static void Hacl_Bignum_Fsquare_fsquare_times_inplace(uint64_t *output, uint32_t count1) in Hacl_Bignum_Fsquare_fsquare_times_inplace()
275 KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U); in Hacl_Bignum_Fsquare_fsquare_times_inplace()
279 uint32_t _i; in Hacl_Bignum_Fsquare_fsquare_times_inplace()
280 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fsquare_fsquare_times_inplace()
291 uint64_t *t00 = buf + (uint32_t)5U; in Hacl_Bignum_Crecip_crecip()
292 uint64_t *b0 = buf + (uint32_t)10U; in Hacl_Bignum_Crecip_crecip()
300 Hacl_Bignum_Fsquare_fsquare_times(a0, z, (uint32_t)1U); in Hacl_Bignum_Crecip_crecip()
301 Hacl_Bignum_Fsquare_fsquare_times(t00, a0, (uint32_t)2U); in Hacl_Bignum_Crecip_crecip()
304 Hacl_Bignum_Fsquare_fsquare_times(t00, a0, (uint32_t)1U); in Hacl_Bignum_Crecip_crecip()
306 Hacl_Bignum_Fsquare_fsquare_times(t00, b0, (uint32_t)5U); in Hacl_Bignum_Crecip_crecip()
307 t01 = buf + (uint32_t)5U; in Hacl_Bignum_Crecip_crecip()
308 b1 = buf + (uint32_t)10U; in Hacl_Bignum_Crecip_crecip()
309 c0 = buf + (uint32_t)15U; in Hacl_Bignum_Crecip_crecip()
311 Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)10U); in Hacl_Bignum_Crecip_crecip()
313 Hacl_Bignum_Fsquare_fsquare_times(t01, c0, (uint32_t)20U); in Hacl_Bignum_Crecip_crecip()
315 Hacl_Bignum_Fsquare_fsquare_times_inplace(t01, (uint32_t)10U); in Hacl_Bignum_Crecip_crecip()
317 Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)50U); in Hacl_Bignum_Crecip_crecip()
319 t0 = buf + (uint32_t)5U; in Hacl_Bignum_Crecip_crecip()
320 b = buf + (uint32_t)10U; in Hacl_Bignum_Crecip_crecip()
321 c = buf + (uint32_t)15U; in Hacl_Bignum_Crecip_crecip()
323 Hacl_Bignum_Fsquare_fsquare_times(t0, c, (uint32_t)100U); in Hacl_Bignum_Crecip_crecip()
325 Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)50U); in Hacl_Bignum_Crecip_crecip()
327 Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)5U); in Hacl_Bignum_Crecip_crecip()
333 uint32_t i; in Hacl_Bignum_fsum()
334 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fsum()
350 memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]); in Hacl_Bignum_fdifference()
362 uint32_t i; in Hacl_Bignum_fdifference()
363 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fdifference()
374 KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U); in Hacl_Bignum_fscalar()
378 uint32_t _i; in Hacl_Bignum_fscalar()
379 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_fscalar()
388 uint32_t i; in Hacl_Bignum_fscalar()
389 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fscalar()
402 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_fscalar()
421 Hacl_EC_Point_swap_conditional_step(uint64_t *a, uint64_t *b, uint64_t swap1, uint32_t ctr) in Hacl_EC_Point_swap_conditional_step()
423 uint32_t i = ctr - (uint32_t)1U; in Hacl_EC_Point_swap_conditional_step()
434 Hacl_EC_Point_swap_conditional_(uint64_t *a, uint64_t *b, uint64_t swap1, uint32_t ctr) in Hacl_EC_Point_swap_conditional_()
436 if (!(ctr == (uint32_t)0U)) in Hacl_EC_Point_swap_conditional_()
438 uint32_t i; in Hacl_EC_Point_swap_conditional_()
440 i = ctr - (uint32_t)1U; in Hacl_EC_Point_swap_conditional_()
448 Hacl_EC_Point_swap_conditional_(a, b, swap1, (uint32_t)5U); in Hacl_EC_Point_swap_conditional()
449 Hacl_EC_Point_swap_conditional_(a + (uint32_t)5U, b + (uint32_t)5U, swap1, (uint32_t)5U); in Hacl_EC_Point_swap_conditional()
454 memcpy(output, input, (uint32_t)5U * sizeof input[0U]); in Hacl_EC_Point_copy()
455 memcpy(output + (uint32_t)5U, in Hacl_EC_Point_copy()
456 input + (uint32_t)5U, in Hacl_EC_Point_copy()
457 (uint32_t)5U * sizeof (input + (uint32_t)5U)[0U]); in Hacl_EC_Point_copy()
463 uint8_t *x00 = input + (uint32_t)6U; in Hacl_EC_Format_fexpand()
465 uint8_t *x01 = input + (uint32_t)12U; in Hacl_EC_Format_fexpand()
467 uint8_t *x02 = input + (uint32_t)19U; in Hacl_EC_Format_fexpand()
469 uint8_t *x0 = input + (uint32_t)24U; in Hacl_EC_Format_fexpand()
472 uint64_t output1 = i1 >> (uint32_t)3U & (uint64_t)0x7ffffffffffffU; in Hacl_EC_Format_fexpand()
473 uint64_t output2 = i2 >> (uint32_t)6U & (uint64_t)0x7ffffffffffffU; in Hacl_EC_Format_fexpand()
474 uint64_t output3 = i3 >> (uint32_t)1U & (uint64_t)0x7ffffffffffffU; in Hacl_EC_Format_fexpand()
475 uint64_t output4 = i4 >> (uint32_t)12U & (uint64_t)0x7ffffffffffffU; in Hacl_EC_Format_fexpand()
490 uint64_t t1_ = t1 + (t0 >> (uint32_t)51U); in Hacl_EC_Format_fcontract_first_carry_pass()
492 uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_first_carry_pass()
494 uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_first_carry_pass()
496 uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_first_carry_pass()
518 uint64_t t1_ = t1 + (t0 >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_pass()
520 uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_pass()
522 uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_pass()
524 uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_pass()
544 i1_ = i1 + (i0 >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_full()
581 uint64_t o0 = t1 << (uint32_t)51U | t0; in Hacl_EC_Format_fcontract_store()
582 uint64_t o1 = t2 << (uint32_t)38U | t1 >> (uint32_t)13U; in Hacl_EC_Format_fcontract_store()
583 uint64_t o2 = t3 << (uint32_t)25U | t2 >> (uint32_t)26U; in Hacl_EC_Format_fcontract_store()
584 uint64_t o3 = t4 << (uint32_t)12U | t3 >> (uint32_t)39U; in Hacl_EC_Format_fcontract_store()
586 uint8_t *b1 = output + (uint32_t)8U; in Hacl_EC_Format_fcontract_store()
587 uint8_t *b2 = output + (uint32_t)16U; in Hacl_EC_Format_fcontract_store()
588 uint8_t *b3 = output + (uint32_t)24U; in Hacl_EC_Format_fcontract_store()
606 uint64_t *z = point + (uint32_t)5U; in Hacl_EC_Format_scalar_of_point()
609 uint64_t *sc = buf + (uint32_t)5U; in Hacl_EC_Format_scalar_of_point()
626 uint64_t *z2 = pp + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
628 uint64_t *z3 = ppq + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
630 uint64_t *z = p + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
632 uint64_t *zprime = pq + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
635 uint64_t *origxprime0 = buf + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
636 uint64_t *xxprime0 = buf + (uint32_t)25U; in Hacl_EC_AddAndDouble_fmonty()
637 uint64_t *zzprime0 = buf + (uint32_t)30U; 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()
656 origxprime = buf + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
657 xx0 = buf + (uint32_t)15U; in Hacl_EC_AddAndDouble_fmonty()
658 zz0 = buf + (uint32_t)20U; in Hacl_EC_AddAndDouble_fmonty()
659 xxprime = buf + (uint32_t)25U; in Hacl_EC_AddAndDouble_fmonty()
660 zzprime = buf + (uint32_t)30U; in Hacl_EC_AddAndDouble_fmonty()
661 zzzprime = buf + (uint32_t)35U; in Hacl_EC_AddAndDouble_fmonty()
662 memcpy(origxprime, xxprime, (uint32_t)5U * sizeof xxprime[0U]); in Hacl_EC_AddAndDouble_fmonty()
665 Hacl_Bignum_Fsquare_fsquare_times(x3, xxprime, (uint32_t)1U); in Hacl_EC_AddAndDouble_fmonty()
666 Hacl_Bignum_Fsquare_fsquare_times(zzzprime, zzprime, (uint32_t)1U); in Hacl_EC_AddAndDouble_fmonty()
668 Hacl_Bignum_Fsquare_fsquare_times(xx0, x, (uint32_t)1U); in Hacl_EC_AddAndDouble_fmonty()
669 Hacl_Bignum_Fsquare_fsquare_times(zz0, z, (uint32_t)1U); in Hacl_EC_AddAndDouble_fmonty()
670 zzz = buf + (uint32_t)10U; in Hacl_EC_AddAndDouble_fmonty()
671 xx = buf + (uint32_t)15U; in Hacl_EC_AddAndDouble_fmonty()
672 zz = buf + (uint32_t)20U; in Hacl_EC_AddAndDouble_fmonty()
691 uint64_t bit0 = (uint64_t)(byt >> (uint32_t)7U); in Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step()
695 bit = (uint64_t)(byt >> (uint32_t)7U); in Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step()
711 byt1 = byt << (uint32_t)1U; in Hacl_EC_Ladder_SmallLoop_cmult_small_loop_double_step()
723 uint32_t i in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
726 if (!(i == (uint32_t)0U)) in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
728 uint32_t i_ = i - (uint32_t)1U; in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
731 byt_ = byt << (uint32_t)2U; in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
744 uint32_t i in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
747 if (!(i == (uint32_t)0U)) in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
749 uint32_t i1 = i - (uint32_t)1U; in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
751 Hacl_EC_Ladder_SmallLoop_cmult_small_loop(nq, nqpq, nq2, nqpq2, q, byte, (uint32_t)4U); in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
760 uint64_t *nqpq = point_buf + (uint32_t)10U; in Hacl_EC_Ladder_cmult()
761 uint64_t *nq2 = point_buf + (uint32_t)20U; in Hacl_EC_Ladder_cmult()
762 uint64_t *nqpq2 = point_buf + (uint32_t)30U; in Hacl_EC_Ladder_cmult()
765 Hacl_EC_Ladder_BigLoop_cmult_big_loop(n1, nq, nqpq, nq2, nqpq2, q, (uint32_t)32U); in Hacl_EC_Ladder_cmult()
773 uint64_t *z = buf0 + (uint32_t)5U; in Hacl_Curve25519_crypto_scalarmult()
786 memcpy(e, secret, (uint32_t)32U * sizeof secret[0U]); in Hacl_Curve25519_crypto_scalarmult()