Lines Matching refs:input
45 Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, FStar_UInt128_uint128 *input) in Hacl_Bignum_Fproduct_copy_from_wide_() argument
50 FStar_UInt128_uint128 xi = input[i]; in Hacl_Bignum_Fproduct_copy_from_wide_()
58 uint64_t *input, in Hacl_Bignum_Fproduct_sum_scalar_multiplication_() argument
66 uint64_t yi = input[i]; in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
107 uint64_t *input, 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_()
119 Hacl_Bignum_Fmul_shift_reduce(input); 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
130 memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]); in Hacl_Bignum_Fmul_fmul()
246 uint64_t *input, in Hacl_Bignum_Fsquare_fsquare_times_() argument
252 Hacl_Bignum_Fsquare_fsquare_(tmp, input); in Hacl_Bignum_Fsquare_fsquare_times_()
254 Hacl_Bignum_Fsquare_fsquare_(tmp, input); in Hacl_Bignum_Fsquare_fsquare_times_()
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()
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()
456 input + (uint32_t)5U, in Hacl_EC_Point_copy()
457 (uint32_t)5U * sizeof (input + (uint32_t)5U)[0U]); in Hacl_EC_Point_copy()
460 static void Hacl_EC_Format_fexpand(uint64_t *output, uint8_t *input) in Hacl_EC_Format_fexpand() argument
462 uint64_t i0 = load64_le(input); in Hacl_EC_Format_fexpand()
463 uint8_t *x00 = input + (uint32_t)6U; in Hacl_EC_Format_fexpand()
465 uint8_t *x01 = input + (uint32_t)12U; in Hacl_EC_Format_fexpand()
467 uint8_t *x02 = input + (uint32_t)19U; in Hacl_EC_Format_fexpand()
469 uint8_t *x0 = input + (uint32_t)24U; in Hacl_EC_Format_fexpand()
483 static void Hacl_EC_Format_fcontract_first_carry_pass(uint64_t *input) in Hacl_EC_Format_fcontract_first_carry_pass() argument
485 uint64_t t0 = input[0U]; in Hacl_EC_Format_fcontract_first_carry_pass()
486 uint64_t t1 = input[1U]; in Hacl_EC_Format_fcontract_first_carry_pass()
487 uint64_t t2 = input[2U]; in Hacl_EC_Format_fcontract_first_carry_pass()
488 uint64_t t3 = input[3U]; in Hacl_EC_Format_fcontract_first_carry_pass()
489 uint64_t t4 = input[4U]; in Hacl_EC_Format_fcontract_first_carry_pass()
498 input[0U] = t0_; in Hacl_EC_Format_fcontract_first_carry_pass()
499 input[1U] = t1__; in Hacl_EC_Format_fcontract_first_carry_pass()
500 input[2U] = t2__; in Hacl_EC_Format_fcontract_first_carry_pass()
501 input[3U] = t3__; in Hacl_EC_Format_fcontract_first_carry_pass()
502 input[4U] = t4_; in Hacl_EC_Format_fcontract_first_carry_pass()
505 static void Hacl_EC_Format_fcontract_first_carry_full(uint64_t *input) in Hacl_EC_Format_fcontract_first_carry_full() argument
507 Hacl_EC_Format_fcontract_first_carry_pass(input); in Hacl_EC_Format_fcontract_first_carry_full()
508 Hacl_Bignum_Modulo_carry_top(input); in Hacl_EC_Format_fcontract_first_carry_full()
511 static void Hacl_EC_Format_fcontract_second_carry_pass(uint64_t *input) in Hacl_EC_Format_fcontract_second_carry_pass() argument
513 uint64_t t0 = input[0U]; in Hacl_EC_Format_fcontract_second_carry_pass()
514 uint64_t t1 = input[1U]; in Hacl_EC_Format_fcontract_second_carry_pass()
515 uint64_t t2 = input[2U]; in Hacl_EC_Format_fcontract_second_carry_pass()
516 uint64_t t3 = input[3U]; in Hacl_EC_Format_fcontract_second_carry_pass()
517 uint64_t t4 = input[4U]; in Hacl_EC_Format_fcontract_second_carry_pass()
526 input[0U] = t0_; in Hacl_EC_Format_fcontract_second_carry_pass()
527 input[1U] = t1__; in Hacl_EC_Format_fcontract_second_carry_pass()
528 input[2U] = t2__; in Hacl_EC_Format_fcontract_second_carry_pass()
529 input[3U] = t3__; in Hacl_EC_Format_fcontract_second_carry_pass()
530 input[4U] = t4_; in Hacl_EC_Format_fcontract_second_carry_pass()
533 static void Hacl_EC_Format_fcontract_second_carry_full(uint64_t *input) in Hacl_EC_Format_fcontract_second_carry_full() argument
539 Hacl_EC_Format_fcontract_second_carry_pass(input); in Hacl_EC_Format_fcontract_second_carry_full()
540 Hacl_Bignum_Modulo_carry_top(input); in Hacl_EC_Format_fcontract_second_carry_full()
541 i0 = input[0U]; in Hacl_EC_Format_fcontract_second_carry_full()
542 i1 = input[1U]; in Hacl_EC_Format_fcontract_second_carry_full()
545 input[0U] = i0_; in Hacl_EC_Format_fcontract_second_carry_full()
546 input[1U] = i1_; in Hacl_EC_Format_fcontract_second_carry_full()
549 static void Hacl_EC_Format_fcontract_trim(uint64_t *input) in Hacl_EC_Format_fcontract_trim() argument
551 uint64_t a0 = input[0U]; in Hacl_EC_Format_fcontract_trim()
552 uint64_t a1 = input[1U]; in Hacl_EC_Format_fcontract_trim()
553 uint64_t a2 = input[2U]; in Hacl_EC_Format_fcontract_trim()
554 uint64_t a3 = input[3U]; in Hacl_EC_Format_fcontract_trim()
555 uint64_t a4 = input[4U]; in Hacl_EC_Format_fcontract_trim()
567 input[0U] = a0_; in Hacl_EC_Format_fcontract_trim()
568 input[1U] = a1_; in Hacl_EC_Format_fcontract_trim()
569 input[2U] = a2_; in Hacl_EC_Format_fcontract_trim()
570 input[3U] = a3_; in Hacl_EC_Format_fcontract_trim()
571 input[4U] = a4_; in Hacl_EC_Format_fcontract_trim()
574 static void Hacl_EC_Format_fcontract_store(uint8_t *output, uint64_t *input) in Hacl_EC_Format_fcontract_store() argument
576 uint64_t t0 = input[0U]; in Hacl_EC_Format_fcontract_store()
577 uint64_t t1 = input[1U]; in Hacl_EC_Format_fcontract_store()
578 uint64_t t2 = input[2U]; in Hacl_EC_Format_fcontract_store()
579 uint64_t t3 = input[3U]; in Hacl_EC_Format_fcontract_store()
580 uint64_t t4 = input[4U]; 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
597 Hacl_EC_Format_fcontract_first_carry_full(input); in Hacl_EC_Format_fcontract()
598 Hacl_EC_Format_fcontract_second_carry_full(input); in Hacl_EC_Format_fcontract()
599 Hacl_EC_Format_fcontract_trim(input); in Hacl_EC_Format_fcontract()
600 Hacl_EC_Format_fcontract_store(output, input); in Hacl_EC_Format_fcontract()