41 inline static void Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, uint128_t *input)  in Hacl_Bignum_Fproduct_copy_from_wide_()  argument
46     uint128_t xi = input[i];  in Hacl_Bignum_Fproduct_copy_from_wide_()
52 Hacl_Bignum_Fproduct_sum_scalar_multiplication_(uint128_t *output, uint64_t *input, uint64_t s)  in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()  argument
58     uint64_t yi = input[i];  in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
97 Hacl_Bignum_Fmul_mul_shift_reduce_(uint128_t *output, uint64_t *input, uint64_t *input2)  in Hacl_Bignum_Fmul_mul_shift_reduce_()  argument
106       Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i0);  in Hacl_Bignum_Fmul_mul_shift_reduce_()
107       Hacl_Bignum_Fmul_shift_reduce(input);  in Hacl_Bignum_Fmul_mul_shift_reduce_()
112   Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);  in Hacl_Bignum_Fmul_mul_shift_reduce_()
115 inline static void Hacl_Bignum_Fmul_fmul(uint64_t *output, uint64_t *input, uint64_t *input2)  in Hacl_Bignum_Fmul_fmul()  argument
118   memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);  in Hacl_Bignum_Fmul_fmul()
207 Hacl_Bignum_Fsquare_fsquare_times_(uint64_t *input, uint128_t *tmp, uint32_t count1)  in Hacl_Bignum_Fsquare_fsquare_times_()  argument
210   Hacl_Bignum_Fsquare_fsquare_(tmp, input);  in Hacl_Bignum_Fsquare_fsquare_times_()
212     Hacl_Bignum_Fsquare_fsquare_(tmp, input);  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()  argument
226     memcpy(output, input, (uint32_t)5U * sizeof input[0U]);  in Hacl_Bignum_Fsquare_fsquare_times()
370 inline static void Hacl_Bignum_crecip(uint64_t *output, uint64_t *input)  in Hacl_Bignum_crecip()  argument
372   Hacl_Bignum_Crecip_crecip(output, input);  in Hacl_Bignum_crecip()
407 static void Hacl_EC_Point_copy(uint64_t *output, uint64_t *input)  in Hacl_EC_Point_copy()  argument
409   memcpy(output, input, (uint32_t)5U * sizeof input[0U]);  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()
415 static void Hacl_EC_Format_fexpand(uint64_t *output, uint8_t *input)  in Hacl_EC_Format_fexpand()  argument
417   uint64_t i0 = load64_le(input);  in Hacl_EC_Format_fexpand()
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()
438 static void Hacl_EC_Format_fcontract_first_carry_pass(uint64_t *input)  in Hacl_EC_Format_fcontract_first_carry_pass()  argument
440   uint64_t t0 = input[0U];  in Hacl_EC_Format_fcontract_first_carry_pass()
441   uint64_t t1 = input[1U];  in Hacl_EC_Format_fcontract_first_carry_pass()
442   uint64_t t2 = input[2U];  in Hacl_EC_Format_fcontract_first_carry_pass()
443   uint64_t t3 = input[3U];  in Hacl_EC_Format_fcontract_first_carry_pass()
444   uint64_t t4 = input[4U];  in Hacl_EC_Format_fcontract_first_carry_pass()
453   input[0U] = t0_;  in Hacl_EC_Format_fcontract_first_carry_pass()
454   input[1U] = t1__;  in Hacl_EC_Format_fcontract_first_carry_pass()
455   input[2U] = t2__;  in Hacl_EC_Format_fcontract_first_carry_pass()
456   input[3U] = t3__;  in Hacl_EC_Format_fcontract_first_carry_pass()
457   input[4U] = t4_;  in Hacl_EC_Format_fcontract_first_carry_pass()
460 static void Hacl_EC_Format_fcontract_first_carry_full(uint64_t *input)  in Hacl_EC_Format_fcontract_first_carry_full()  argument
462   Hacl_EC_Format_fcontract_first_carry_pass(input);  in Hacl_EC_Format_fcontract_first_carry_full()
463   Hacl_Bignum_Modulo_carry_top(input);  in Hacl_EC_Format_fcontract_first_carry_full()
466 static void Hacl_EC_Format_fcontract_second_carry_pass(uint64_t *input)  in Hacl_EC_Format_fcontract_second_carry_pass()  argument
468   uint64_t t0 = input[0U];  in Hacl_EC_Format_fcontract_second_carry_pass()
469   uint64_t t1 = input[1U];  in Hacl_EC_Format_fcontract_second_carry_pass()
470   uint64_t t2 = input[2U];  in Hacl_EC_Format_fcontract_second_carry_pass()
471   uint64_t t3 = input[3U];  in Hacl_EC_Format_fcontract_second_carry_pass()
472   uint64_t t4 = input[4U];  in Hacl_EC_Format_fcontract_second_carry_pass()
481   input[0U] = t0_;  in Hacl_EC_Format_fcontract_second_carry_pass()
482   input[1U] = t1__;  in Hacl_EC_Format_fcontract_second_carry_pass()
483   input[2U] = t2__;  in Hacl_EC_Format_fcontract_second_carry_pass()
484   input[3U] = t3__;  in Hacl_EC_Format_fcontract_second_carry_pass()
485   input[4U] = t4_;  in Hacl_EC_Format_fcontract_second_carry_pass()
488 static void Hacl_EC_Format_fcontract_second_carry_full(uint64_t *input)  in Hacl_EC_Format_fcontract_second_carry_full()  argument
494   Hacl_EC_Format_fcontract_second_carry_pass(input);  in Hacl_EC_Format_fcontract_second_carry_full()
495   Hacl_Bignum_Modulo_carry_top(input);  in Hacl_EC_Format_fcontract_second_carry_full()
496   i0 = input[0U];  in Hacl_EC_Format_fcontract_second_carry_full()
497   i1 = input[1U];  in Hacl_EC_Format_fcontract_second_carry_full()
500   input[0U] = i0_;  in Hacl_EC_Format_fcontract_second_carry_full()
501   input[1U] = i1_;  in Hacl_EC_Format_fcontract_second_carry_full()
504 static void Hacl_EC_Format_fcontract_trim(uint64_t *input)  in Hacl_EC_Format_fcontract_trim()  argument
506   uint64_t a0 = input[0U];  in Hacl_EC_Format_fcontract_trim()
507   uint64_t a1 = input[1U];  in Hacl_EC_Format_fcontract_trim()
508   uint64_t a2 = input[2U];  in Hacl_EC_Format_fcontract_trim()
509   uint64_t a3 = input[3U];  in Hacl_EC_Format_fcontract_trim()
510   uint64_t a4 = input[4U];  in Hacl_EC_Format_fcontract_trim()
522   input[0U] = a0_;  in Hacl_EC_Format_fcontract_trim()
523   input[1U] = a1_;  in Hacl_EC_Format_fcontract_trim()
524   input[2U] = a2_;  in Hacl_EC_Format_fcontract_trim()
525   input[3U] = a3_;  in Hacl_EC_Format_fcontract_trim()
526   input[4U] = a4_;  in Hacl_EC_Format_fcontract_trim()
529 static void Hacl_EC_Format_fcontract_store(uint8_t *output, uint64_t *input)  in Hacl_EC_Format_fcontract_store()  argument
531   uint64_t t0 = input[0U];  in Hacl_EC_Format_fcontract_store()
532   uint64_t t1 = input[1U];  in Hacl_EC_Format_fcontract_store()
533   uint64_t t2 = input[2U];  in Hacl_EC_Format_fcontract_store()
534   uint64_t t3 = input[3U];  in Hacl_EC_Format_fcontract_store()
535   uint64_t t4 = input[4U];  in Hacl_EC_Format_fcontract_store()
550 static void Hacl_EC_Format_fcontract(uint8_t *output, uint64_t *input)  in Hacl_EC_Format_fcontract()  argument
552   Hacl_EC_Format_fcontract_first_carry_full(input);  in Hacl_EC_Format_fcontract()
553   Hacl_EC_Format_fcontract_second_carry_full(input);  in Hacl_EC_Format_fcontract()
554   Hacl_EC_Format_fcontract_trim(input);  in Hacl_EC_Format_fcontract()
555   Hacl_EC_Format_fcontract_store(output, input);  in Hacl_EC_Format_fcontract()