41 inline static void Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, uint128_t *input)  in Hacl_Bignum_Fproduct_copy_from_wide_()  argument
47     output[i] = (uint64_t)xi;  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
57     uint128_t xi = output[i];  in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
59     output[i] = xi + (uint128_t)yi * s;  in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
78 inline static void Hacl_Bignum_Fmul_shift_reduce(uint64_t *output)  in Hacl_Bignum_Fmul_shift_reduce()  argument
80   uint64_t tmp = output[4U];  in Hacl_Bignum_Fmul_shift_reduce()
87       uint64_t z = output[ctr - (uint32_t)1U];  in Hacl_Bignum_Fmul_shift_reduce()
88       output[ctr] = z;  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()
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_()
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
144       Hacl_Bignum_Fproduct_copy_from_wide_(output, t);  in Hacl_Bignum_Fmul_fmul()
145       i0 = output[0U];  in Hacl_Bignum_Fmul_fmul()
146       i1 = output[1U];  in Hacl_Bignum_Fmul_fmul()
149       output[0U] = i0_;  in Hacl_Bignum_Fmul_fmul()
150       output[1U] = i1_;  in Hacl_Bignum_Fmul_fmul()
155 inline static void Hacl_Bignum_Fsquare_fsquare__(uint128_t *tmp, uint64_t *output)  in Hacl_Bignum_Fsquare_fsquare__()  argument
157   uint64_t r0 = output[0U];  in Hacl_Bignum_Fsquare_fsquare__()
158   uint64_t r1 = output[1U];  in Hacl_Bignum_Fsquare_fsquare__()
159   uint64_t r2 = output[2U];  in Hacl_Bignum_Fsquare_fsquare__()
160   uint64_t r3 = output[3U];  in Hacl_Bignum_Fsquare_fsquare__()
161   uint64_t r4 = output[4U];  in Hacl_Bignum_Fsquare_fsquare__()
179 inline static void Hacl_Bignum_Fsquare_fsquare_(uint128_t *tmp, uint64_t *output)  in Hacl_Bignum_Fsquare_fsquare_()  argument
189   Hacl_Bignum_Fsquare_fsquare__(tmp, output);  in Hacl_Bignum_Fsquare_fsquare_()
197   Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp);  in Hacl_Bignum_Fsquare_fsquare_()
198   i0 = output[0U];  in Hacl_Bignum_Fsquare_fsquare_()
199   i1 = output[1U];  in Hacl_Bignum_Fsquare_fsquare_()
202   output[0U] = i0_;  in Hacl_Bignum_Fsquare_fsquare_()
203   output[1U] = i1_;  in Hacl_Bignum_Fsquare_fsquare_()
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()
227     Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1);  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()  argument
241     Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1);  in Hacl_Bignum_Fsquare_fsquare_times_inplace()
330 inline static void Hacl_Bignum_fscalar(uint64_t *output, uint64_t *b, uint64_t s)  in Hacl_Bignum_fscalar()  argument
360       Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp);  in Hacl_Bignum_fscalar()
365 inline static void Hacl_Bignum_fmul(uint64_t *output, uint64_t *a, uint64_t *b)  in Hacl_Bignum_fmul()  argument
367   Hacl_Bignum_Fmul_fmul(output, a, b);  in Hacl_Bignum_fmul()
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()
410   memcpy(output + (uint32_t)5U,  in Hacl_EC_Point_copy()
415 static void Hacl_EC_Format_fexpand(uint64_t *output, uint8_t *input)  in Hacl_EC_Format_fexpand()  argument
431   output[0U] = output0;  in Hacl_EC_Format_fexpand()
432   output[1U] = output1;  in Hacl_EC_Format_fexpand()
433   output[2U] = output2;  in Hacl_EC_Format_fexpand()
434   output[3U] = output3;  in Hacl_EC_Format_fexpand()
435   output[4U] = output4;  in Hacl_EC_Format_fexpand()
529 static void Hacl_EC_Format_fcontract_store(uint8_t *output, uint64_t *input)  in Hacl_EC_Format_fcontract_store()  argument
540   uint8_t *b0 = output;  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()
550 static void Hacl_EC_Format_fcontract(uint8_t *output, uint64_t *input)  in Hacl_EC_Format_fcontract()  argument
555   Hacl_EC_Format_fcontract_store(output, input);  in Hacl_EC_Format_fcontract()