45 Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, FStar_UInt128_uint128 *input)  in Hacl_Bignum_Fproduct_copy_from_wide_()  argument
51     output[i] = FStar_UInt128_uint128_to_uint64(xi);  in Hacl_Bignum_Fproduct_copy_from_wide_()
57   FStar_UInt128_uint128 *output,  in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()  argument
65     FStar_UInt128_uint128 xi = output[i];  in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
67     output[i] = FStar_UInt128_add_mod(xi, FStar_UInt128_mul_wide(yi, s));  in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
86 inline static void Hacl_Bignum_Fmul_shift_reduce(uint64_t *output)  in Hacl_Bignum_Fmul_shift_reduce()  argument
88   uint64_t tmp = output[4U];  in Hacl_Bignum_Fmul_shift_reduce()
95       uint64_t z = output[ctr - (uint32_t)1U];  in Hacl_Bignum_Fmul_shift_reduce()
96       output[ctr] = z;  in Hacl_Bignum_Fmul_shift_reduce()
99   output[0U] = tmp;  in Hacl_Bignum_Fmul_shift_reduce()
100   b0 = output[0U];  in Hacl_Bignum_Fmul_shift_reduce()
101   output[0U] = (uint64_t)19U * b0;  in Hacl_Bignum_Fmul_shift_reduce()
106   FStar_UInt128_uint128 *output,  in Hacl_Bignum_Fmul_mul_shift_reduce_()  argument
118       Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i0);  in Hacl_Bignum_Fmul_mul_shift_reduce_()
124   Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);  in Hacl_Bignum_Fmul_mul_shift_reduce_()
127 inline static void Hacl_Bignum_Fmul_fmul(uint64_t *output, uint64_t *input, uint64_t *input2)  in Hacl_Bignum_Fmul_fmul()  argument
159       Hacl_Bignum_Fproduct_copy_from_wide_(output, t);  in Hacl_Bignum_Fmul_fmul()
160       i0 = output[0U];  in Hacl_Bignum_Fmul_fmul()
161       i1 = output[1U];  in Hacl_Bignum_Fmul_fmul()
164       output[0U] = i0_;  in Hacl_Bignum_Fmul_fmul()
165       output[1U] = i1_;  in Hacl_Bignum_Fmul_fmul()
170 inline static void Hacl_Bignum_Fsquare_fsquare__(FStar_UInt128_uint128 *tmp, uint64_t *output)  in Hacl_Bignum_Fsquare_fsquare__()  argument
172   uint64_t r0 = output[0U];  in Hacl_Bignum_Fsquare_fsquare__()
173   uint64_t r1 = output[1U];  in Hacl_Bignum_Fsquare_fsquare__()
174   uint64_t r2 = output[2U];  in Hacl_Bignum_Fsquare_fsquare__()
175   uint64_t r3 = output[3U];  in Hacl_Bignum_Fsquare_fsquare__()
176   uint64_t r4 = output[4U];  in Hacl_Bignum_Fsquare_fsquare__()
214 inline static void Hacl_Bignum_Fsquare_fsquare_(FStar_UInt128_uint128 *tmp, uint64_t *output)  in Hacl_Bignum_Fsquare_fsquare_()  argument
224   Hacl_Bignum_Fsquare_fsquare__(tmp, output);  in Hacl_Bignum_Fsquare_fsquare_()
235   Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp);  in Hacl_Bignum_Fsquare_fsquare_()
236   i0 = output[0U];  in Hacl_Bignum_Fsquare_fsquare_()
237   i1 = output[1U];  in Hacl_Bignum_Fsquare_fsquare_()
240   output[0U] = i0_;  in Hacl_Bignum_Fsquare_fsquare_()
241   output[1U] = i1_;  in Hacl_Bignum_Fsquare_fsquare_()
258 Hacl_Bignum_Fsquare_fsquare_times(uint64_t *output, uint64_t *input, uint32_t count1)  in Hacl_Bignum_Fsquare_fsquare_times()  argument
268     memcpy(output, input, (uint32_t)5U * sizeof input[0U]);  in Hacl_Bignum_Fsquare_fsquare_times()
269     Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1);  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()  argument
283     Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1);  in Hacl_Bignum_Fsquare_fsquare_times_inplace()
372 inline static void Hacl_Bignum_fscalar(uint64_t *output, uint64_t *b, uint64_t s)  in Hacl_Bignum_fscalar()  argument
405       Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp);  in Hacl_Bignum_fscalar()
410 inline static void Hacl_Bignum_fmul(uint64_t *output, uint64_t *a, uint64_t *b)  in Hacl_Bignum_fmul()  argument
412   Hacl_Bignum_Fmul_fmul(output, a, b);  in Hacl_Bignum_fmul()
415 inline static void Hacl_Bignum_crecip(uint64_t *output, uint64_t *input)  in Hacl_Bignum_crecip()  argument
417   Hacl_Bignum_Crecip_crecip(output, input);  in Hacl_Bignum_crecip()
452 static void Hacl_EC_Point_copy(uint64_t *output, uint64_t *input)  in Hacl_EC_Point_copy()  argument
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()
460 static void Hacl_EC_Format_fexpand(uint64_t *output, uint8_t *input)  in Hacl_EC_Format_fexpand()  argument
476   output[0U] = output0;  in Hacl_EC_Format_fexpand()
477   output[1U] = output1;  in Hacl_EC_Format_fexpand()
478   output[2U] = output2;  in Hacl_EC_Format_fexpand()
479   output[3U] = output3;  in Hacl_EC_Format_fexpand()
480   output[4U] = output4;  in Hacl_EC_Format_fexpand()
574 static void Hacl_EC_Format_fcontract_store(uint8_t *output, uint64_t *input)  in Hacl_EC_Format_fcontract_store()  argument
585   uint8_t *b0 = output;  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()
595 static void Hacl_EC_Format_fcontract(uint8_t *output, uint64_t *input)  in Hacl_EC_Format_fcontract()  argument
600   Hacl_EC_Format_fcontract_store(output, input);  in Hacl_EC_Format_fcontract()