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