Lines Matching refs:uint32_t
23 extern uint128_t FStar_UInt128_shift_right(uint128_t x0, uint32_t x1);
36 uint64_t b0_ = b0 + (uint64_t)19U * (b4 >> (uint32_t)51U); in Hacl_Bignum_Modulo_carry_top()
43 uint32_t i; in Hacl_Bignum_Fproduct_copy_from_wide_()
44 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_copy_from_wide_()
54 uint32_t i; in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
55 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
65 uint32_t i; in Hacl_Bignum_Fproduct_carry_wide_()
66 for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) in Hacl_Bignum_Fproduct_carry_wide_()
68 uint32_t ctr = i; in Hacl_Bignum_Fproduct_carry_wide_()
70 uint128_t tctrp1 = tmp[ctr + (uint32_t)1U]; in Hacl_Bignum_Fproduct_carry_wide_()
72 uint128_t c = tctr >> (uint32_t)51U; in Hacl_Bignum_Fproduct_carry_wide_()
74 tmp[ctr + (uint32_t)1U] = tctrp1 + c; in Hacl_Bignum_Fproduct_carry_wide_()
83 uint32_t i; in Hacl_Bignum_Fmul_shift_reduce()
84 for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) in Hacl_Bignum_Fmul_shift_reduce()
86 uint32_t ctr = (uint32_t)5U - i - (uint32_t)1U; in Hacl_Bignum_Fmul_shift_reduce()
87 uint64_t z = output[ctr - (uint32_t)1U]; in Hacl_Bignum_Fmul_shift_reduce()
99 uint32_t i; in Hacl_Bignum_Fmul_mul_shift_reduce_()
102 uint32_t i0; in Hacl_Bignum_Fmul_mul_shift_reduce_()
103 for (i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0 = i0 + (uint32_t)1U) in Hacl_Bignum_Fmul_mul_shift_reduce_()
110 i = (uint32_t)4U; in Hacl_Bignum_Fmul_mul_shift_reduce_()
118 memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]); in Hacl_Bignum_Fmul_fmul()
119 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U); in Hacl_Bignum_Fmul_fmul()
123 uint32_t _i; in Hacl_Bignum_Fmul_fmul()
124 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fmul_fmul()
141 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U); in Hacl_Bignum_Fmul_fmul()
148 i1_ = i1 + (i0 >> (uint32_t)51U); in Hacl_Bignum_Fmul_fmul()
194 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U); in Hacl_Bignum_Fsquare_fsquare_()
201 i1_ = i1 + (i0 >> (uint32_t)51U); in Hacl_Bignum_Fsquare_fsquare_()
207 Hacl_Bignum_Fsquare_fsquare_times_(uint64_t *input, uint128_t *tmp, uint32_t count1) in Hacl_Bignum_Fsquare_fsquare_times_()
209 uint32_t i; in Hacl_Bignum_Fsquare_fsquare_times_()
211 for (i = (uint32_t)1U; i < count1; i = i + (uint32_t)1U) in Hacl_Bignum_Fsquare_fsquare_times_()
216 Hacl_Bignum_Fsquare_fsquare_times(uint64_t *output, uint64_t *input, uint32_t count1) in Hacl_Bignum_Fsquare_fsquare_times()
218 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U); in Hacl_Bignum_Fsquare_fsquare_times()
222 uint32_t _i; in Hacl_Bignum_Fsquare_fsquare_times()
223 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fsquare_fsquare_times()
226 memcpy(output, input, (uint32_t)5U * sizeof input[0U]); in Hacl_Bignum_Fsquare_fsquare_times()
231 inline static void Hacl_Bignum_Fsquare_fsquare_times_inplace(uint64_t *output, uint32_t count1) in Hacl_Bignum_Fsquare_fsquare_times_inplace()
233 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U); in Hacl_Bignum_Fsquare_fsquare_times_inplace()
237 uint32_t _i; in Hacl_Bignum_Fsquare_fsquare_times_inplace()
238 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_Fsquare_fsquare_times_inplace()
249 uint64_t *t00 = buf + (uint32_t)5U; in Hacl_Bignum_Crecip_crecip()
250 uint64_t *b0 = buf + (uint32_t)10U; in Hacl_Bignum_Crecip_crecip()
258 Hacl_Bignum_Fsquare_fsquare_times(a0, z, (uint32_t)1U); in Hacl_Bignum_Crecip_crecip()
259 Hacl_Bignum_Fsquare_fsquare_times(t00, a0, (uint32_t)2U); in Hacl_Bignum_Crecip_crecip()
262 Hacl_Bignum_Fsquare_fsquare_times(t00, a0, (uint32_t)1U); in Hacl_Bignum_Crecip_crecip()
264 Hacl_Bignum_Fsquare_fsquare_times(t00, b0, (uint32_t)5U); in Hacl_Bignum_Crecip_crecip()
265 t01 = buf + (uint32_t)5U; in Hacl_Bignum_Crecip_crecip()
266 b1 = buf + (uint32_t)10U; in Hacl_Bignum_Crecip_crecip()
267 c0 = buf + (uint32_t)15U; in Hacl_Bignum_Crecip_crecip()
269 Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)10U); in Hacl_Bignum_Crecip_crecip()
271 Hacl_Bignum_Fsquare_fsquare_times(t01, c0, (uint32_t)20U); in Hacl_Bignum_Crecip_crecip()
273 Hacl_Bignum_Fsquare_fsquare_times_inplace(t01, (uint32_t)10U); in Hacl_Bignum_Crecip_crecip()
275 Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)50U); in Hacl_Bignum_Crecip_crecip()
277 t0 = buf + (uint32_t)5U; in Hacl_Bignum_Crecip_crecip()
278 b = buf + (uint32_t)10U; in Hacl_Bignum_Crecip_crecip()
279 c = buf + (uint32_t)15U; in Hacl_Bignum_Crecip_crecip()
281 Hacl_Bignum_Fsquare_fsquare_times(t0, c, (uint32_t)100U); in Hacl_Bignum_Crecip_crecip()
283 Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)50U); in Hacl_Bignum_Crecip_crecip()
285 Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)5U); in Hacl_Bignum_Crecip_crecip()
291 uint32_t i; in Hacl_Bignum_fsum()
292 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fsum()
308 memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]); in Hacl_Bignum_fdifference()
320 uint32_t i; in Hacl_Bignum_fdifference()
321 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fdifference()
332 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U); in Hacl_Bignum_fscalar()
336 uint32_t _i; in Hacl_Bignum_fscalar()
337 for (_i = 0U; _i < (uint32_t)5U; ++_i) in Hacl_Bignum_fscalar()
346 uint32_t i; in Hacl_Bignum_fscalar()
347 for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) in Hacl_Bignum_fscalar()
357 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U); in Hacl_Bignum_fscalar()
376 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()
378 uint32_t i = ctr - (uint32_t)1U; in Hacl_EC_Point_swap_conditional_step()
389 Hacl_EC_Point_swap_conditional_(uint64_t *a, uint64_t *b, uint64_t swap1, uint32_t ctr) in Hacl_EC_Point_swap_conditional_()
391 if (!(ctr == (uint32_t)0U)) in Hacl_EC_Point_swap_conditional_()
393 uint32_t i; in Hacl_EC_Point_swap_conditional_()
395 i = ctr - (uint32_t)1U; in Hacl_EC_Point_swap_conditional_()
403 Hacl_EC_Point_swap_conditional_(a, b, swap1, (uint32_t)5U); in Hacl_EC_Point_swap_conditional()
404 Hacl_EC_Point_swap_conditional_(a + (uint32_t)5U, b + (uint32_t)5U, swap1, (uint32_t)5U); in Hacl_EC_Point_swap_conditional()
409 memcpy(output, input, (uint32_t)5U * sizeof input[0U]); in Hacl_EC_Point_copy()
410 memcpy(output + (uint32_t)5U, in Hacl_EC_Point_copy()
411 input + (uint32_t)5U, in Hacl_EC_Point_copy()
412 (uint32_t)5U * sizeof (input + (uint32_t)5U)[0U]); in Hacl_EC_Point_copy()
418 uint8_t *x00 = input + (uint32_t)6U; in Hacl_EC_Format_fexpand()
420 uint8_t *x01 = input + (uint32_t)12U; in Hacl_EC_Format_fexpand()
422 uint8_t *x02 = input + (uint32_t)19U; in Hacl_EC_Format_fexpand()
424 uint8_t *x0 = input + (uint32_t)24U; in Hacl_EC_Format_fexpand()
427 uint64_t output1 = i1 >> (uint32_t)3U & (uint64_t)0x7ffffffffffffU; in Hacl_EC_Format_fexpand()
428 uint64_t output2 = i2 >> (uint32_t)6U & (uint64_t)0x7ffffffffffffU; in Hacl_EC_Format_fexpand()
429 uint64_t output3 = i3 >> (uint32_t)1U & (uint64_t)0x7ffffffffffffU; in Hacl_EC_Format_fexpand()
430 uint64_t output4 = i4 >> (uint32_t)12U & (uint64_t)0x7ffffffffffffU; in Hacl_EC_Format_fexpand()
445 uint64_t t1_ = t1 + (t0 >> (uint32_t)51U); in Hacl_EC_Format_fcontract_first_carry_pass()
447 uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_first_carry_pass()
449 uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_first_carry_pass()
451 uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_first_carry_pass()
473 uint64_t t1_ = t1 + (t0 >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_pass()
475 uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_pass()
477 uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_pass()
479 uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_pass()
499 i1_ = i1 + (i0 >> (uint32_t)51U); in Hacl_EC_Format_fcontract_second_carry_full()
536 uint64_t o0 = t1 << (uint32_t)51U | t0; in Hacl_EC_Format_fcontract_store()
537 uint64_t o1 = t2 << (uint32_t)38U | t1 >> (uint32_t)13U; in Hacl_EC_Format_fcontract_store()
538 uint64_t o2 = t3 << (uint32_t)25U | t2 >> (uint32_t)26U; in Hacl_EC_Format_fcontract_store()
539 uint64_t o3 = t4 << (uint32_t)12U | t3 >> (uint32_t)39U; in Hacl_EC_Format_fcontract_store()
541 uint8_t *b1 = output + (uint32_t)8U; in Hacl_EC_Format_fcontract_store()
542 uint8_t *b2 = output + (uint32_t)16U; in Hacl_EC_Format_fcontract_store()
543 uint8_t *b3 = output + (uint32_t)24U; in Hacl_EC_Format_fcontract_store()
561 uint64_t *z = point + (uint32_t)5U; in Hacl_EC_Format_scalar_of_point()
564 uint64_t *sc = buf + (uint32_t)5U; in Hacl_EC_Format_scalar_of_point()
581 uint64_t *z2 = pp + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
583 uint64_t *z3 = ppq + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
585 uint64_t *z = p + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
587 uint64_t *zprime = pq + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
590 uint64_t *origxprime0 = buf + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
591 uint64_t *xxprime0 = buf + (uint32_t)25U; in Hacl_EC_AddAndDouble_fmonty()
592 uint64_t *zzprime0 = buf + (uint32_t)30U; in Hacl_EC_AddAndDouble_fmonty()
603 memcpy(origx, x, (uint32_t)5U * sizeof x[0U]); in Hacl_EC_AddAndDouble_fmonty()
606 memcpy(origxprime0, xprime, (uint32_t)5U * sizeof xprime[0U]); in Hacl_EC_AddAndDouble_fmonty()
611 origxprime = buf + (uint32_t)5U; in Hacl_EC_AddAndDouble_fmonty()
612 xx0 = buf + (uint32_t)15U; in Hacl_EC_AddAndDouble_fmonty()
613 zz0 = buf + (uint32_t)20U; in Hacl_EC_AddAndDouble_fmonty()
614 xxprime = buf + (uint32_t)25U; in Hacl_EC_AddAndDouble_fmonty()
615 zzprime = buf + (uint32_t)30U; in Hacl_EC_AddAndDouble_fmonty()
616 zzzprime = buf + (uint32_t)35U; in Hacl_EC_AddAndDouble_fmonty()
617 memcpy(origxprime, xxprime, (uint32_t)5U * sizeof xxprime[0U]); in Hacl_EC_AddAndDouble_fmonty()
620 Hacl_Bignum_Fsquare_fsquare_times(x3, xxprime, (uint32_t)1U); in Hacl_EC_AddAndDouble_fmonty()
621 Hacl_Bignum_Fsquare_fsquare_times(zzzprime, zzprime, (uint32_t)1U); in Hacl_EC_AddAndDouble_fmonty()
623 Hacl_Bignum_Fsquare_fsquare_times(xx0, x, (uint32_t)1U); in Hacl_EC_AddAndDouble_fmonty()
624 Hacl_Bignum_Fsquare_fsquare_times(zz0, z, (uint32_t)1U); in Hacl_EC_AddAndDouble_fmonty()
625 zzz = buf + (uint32_t)10U; in Hacl_EC_AddAndDouble_fmonty()
626 xx = buf + (uint32_t)15U; in Hacl_EC_AddAndDouble_fmonty()
627 zz = buf + (uint32_t)20U; in Hacl_EC_AddAndDouble_fmonty()
646 uint64_t bit0 = (uint64_t)(byt >> (uint32_t)7U); in Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step()
650 bit = (uint64_t)(byt >> (uint32_t)7U); in Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step()
666 byt1 = byt << (uint32_t)1U; in Hacl_EC_Ladder_SmallLoop_cmult_small_loop_double_step()
678 uint32_t i in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
681 if (!(i == (uint32_t)0U)) in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
683 uint32_t i_ = i - (uint32_t)1U; in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
686 byt_ = byt << (uint32_t)2U; in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
699 uint32_t i in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
702 if (!(i == (uint32_t)0U)) in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
704 uint32_t i1 = i - (uint32_t)1U; in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
706 Hacl_EC_Ladder_SmallLoop_cmult_small_loop(nq, nqpq, nq2, nqpq2, q, byte, (uint32_t)4U); in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
715 uint64_t *nqpq = point_buf + (uint32_t)10U; in Hacl_EC_Ladder_cmult()
716 uint64_t *nq2 = point_buf + (uint32_t)20U; in Hacl_EC_Ladder_cmult()
717 uint64_t *nqpq2 = point_buf + (uint32_t)30U; in Hacl_EC_Ladder_cmult()
720 Hacl_EC_Ladder_BigLoop_cmult_big_loop(n1, nq, nqpq, nq2, nqpq2, q, (uint32_t)32U); in Hacl_EC_Ladder_cmult()
728 uint64_t *z = buf0 + (uint32_t)5U; in Hacl_Curve25519_crypto_scalarmult()
741 memcpy(e, secret, (uint32_t)32U * sizeof secret[0U]); in Hacl_Curve25519_crypto_scalarmult()