34   uint64_t b0 = b[0U];  in Hacl_Bignum_Modulo_carry_top()
38   b[0U] = b0_;  in Hacl_Bignum_Modulo_carry_top()
44   for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)  in Hacl_Bignum_Fproduct_copy_from_wide_()
55   for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)  in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
66   for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U)  in Hacl_Bignum_Fproduct_carry_wide_()
84     for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U)  in Hacl_Bignum_Fmul_shift_reduce()
91   output[0U] = tmp;  in Hacl_Bignum_Fmul_shift_reduce()
92   b0 = output[0U];  in Hacl_Bignum_Fmul_shift_reduce()
93   output[0U] = (uint64_t)19U * b0;  in Hacl_Bignum_Fmul_shift_reduce()
103     for (i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0 = i0 + (uint32_t)1U)  in Hacl_Bignum_Fmul_mul_shift_reduce_()
117   uint64_t tmp[5U] = { 0U };  in Hacl_Bignum_Fmul_fmul()
118   memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);  in Hacl_Bignum_Fmul_fmul()
124       for (_i = 0U; _i < (uint32_t)5U; ++_i)  in Hacl_Bignum_Fmul_fmul()
125         t[_i] = (uint128_t)(uint64_t)0U;  in Hacl_Bignum_Fmul_fmul()
139       b0 = t[0U];  in Hacl_Bignum_Fmul_fmul()
143       t[0U] = b0_;  in Hacl_Bignum_Fmul_fmul()
145       i0 = output[0U];  in Hacl_Bignum_Fmul_fmul()
149       output[0U] = i0_;  in Hacl_Bignum_Fmul_fmul()
157   uint64_t r0 = output[0U];  in Hacl_Bignum_Fsquare_fsquare__()
172   tmp[0U] = s0;  in Hacl_Bignum_Fsquare_fsquare__()
192   b0 = tmp[0U];  in Hacl_Bignum_Fsquare_fsquare_()
196   tmp[0U] = b0_;  in Hacl_Bignum_Fsquare_fsquare_()
198   i0 = output[0U];  in Hacl_Bignum_Fsquare_fsquare_()
202   output[0U] = i0_;  in Hacl_Bignum_Fsquare_fsquare_()
223       for (_i = 0U; _i < (uint32_t)5U; ++_i)  in Hacl_Bignum_Fsquare_fsquare_times()
224         t[_i] = (uint128_t)(uint64_t)0U;  in Hacl_Bignum_Fsquare_fsquare_times()
226     memcpy(output, input, (uint32_t)5U * sizeof input[0U]);  in Hacl_Bignum_Fsquare_fsquare_times()
238       for (_i = 0U; _i < (uint32_t)5U; ++_i)  in Hacl_Bignum_Fsquare_fsquare_times_inplace()
239         t[_i] = (uint128_t)(uint64_t)0U;  in Hacl_Bignum_Fsquare_fsquare_times_inplace()
247   uint64_t buf[20U] = { 0U };  in Hacl_Bignum_Crecip_crecip()
292   for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)  in Hacl_Bignum_fsum()
302   uint64_t tmp[5U] = { 0U };  in Hacl_Bignum_fdifference()
308   memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]);  in Hacl_Bignum_fdifference()
309   b0 = tmp[0U];  in Hacl_Bignum_fdifference()
314   tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U;  in Hacl_Bignum_fdifference()
321     for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)  in Hacl_Bignum_fdifference()
337       for (_i = 0U; _i < (uint32_t)5U; ++_i)  in Hacl_Bignum_fscalar()
338         tmp[_i] = (uint128_t)(uint64_t)0U;  in Hacl_Bignum_fscalar()
347         for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)  in Hacl_Bignum_fscalar()
355       b0 = tmp[0U];  in Hacl_Bignum_fscalar()
359       tmp[0U] = b0_;  in Hacl_Bignum_fscalar()
391   if (!(ctr == (uint32_t)0U))  in Hacl_EC_Point_swap_conditional_()
402   uint64_t swap1 = (uint64_t)0U - iswap;  in Hacl_EC_Point_swap_conditional()
409   memcpy(output, input, (uint32_t)5U * sizeof input[0U]);  in Hacl_EC_Point_copy()
412     (uint32_t)5U * sizeof (input + (uint32_t)5U)[0U]);  in Hacl_EC_Point_copy()
431   output[0U] = output0;  in Hacl_EC_Format_fexpand()
440   uint64_t t0 = input[0U];  in Hacl_EC_Format_fcontract_first_carry_pass()
453   input[0U] = t0_;  in Hacl_EC_Format_fcontract_first_carry_pass()
468   uint64_t t0 = input[0U];  in Hacl_EC_Format_fcontract_second_carry_pass()
481   input[0U] = t0_;  in Hacl_EC_Format_fcontract_second_carry_pass()
496   i0 = input[0U];  in Hacl_EC_Format_fcontract_second_carry_full()
500   input[0U] = i0_;  in Hacl_EC_Format_fcontract_second_carry_full()
506   uint64_t a0 = input[0U];  in Hacl_EC_Format_fcontract_trim()
522   input[0U] = a0_;  in Hacl_EC_Format_fcontract_trim()
531   uint64_t t0 = input[0U];  in Hacl_EC_Format_fcontract_store()
562   uint64_t buf[10U] = { 0U };  in Hacl_EC_Format_scalar_of_point()
588   uint64_t buf[40U] = { 0U };  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()
617   memcpy(origxprime, xxprime, (uint32_t)5U * sizeof xxprime[0U]);  in Hacl_EC_AddAndDouble_fmonty()
681   if (!(i == (uint32_t)0U))  in Hacl_EC_Ladder_SmallLoop_cmult_small_loop()
702   if (!(i == (uint32_t)0U))  in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
713   uint64_t point_buf[40U] = { 0U };  in Hacl_EC_Ladder_cmult()
719   nq[0U] = (uint64_t)1U;  in Hacl_EC_Ladder_cmult()
726   uint64_t buf0[10U] = { 0U };  in Hacl_Curve25519_crypto_scalarmult()
731   z[0U] = (uint64_t)1U;  in Hacl_Curve25519_crypto_scalarmult()
734     uint8_t e[32U] = { 0U };  in Hacl_Curve25519_crypto_scalarmult()
741     memcpy(e, secret, (uint32_t)32U * sizeof secret[0U]);  in Hacl_Curve25519_crypto_scalarmult()
742     e0 = e[0U];  in Hacl_Curve25519_crypto_scalarmult()
747     e[0U] = e01;  in Hacl_Curve25519_crypto_scalarmult()
751       uint64_t buf[15U] = { 0U };  in Hacl_Curve25519_crypto_scalarmult()
754       x[0U] = (uint64_t)1U;  in Hacl_Curve25519_crypto_scalarmult()