Lines Matching refs:tmp
71 inline static void Hacl_Bignum_Fproduct_carry_wide_(FStar_UInt128_uint128 *tmp) in Hacl_Bignum_Fproduct_carry_wide_() argument
77 FStar_UInt128_uint128 tctr = tmp[ctr]; in Hacl_Bignum_Fproduct_carry_wide_()
78 FStar_UInt128_uint128 tctrp1 = tmp[ctr + (uint32_t)1U]; in Hacl_Bignum_Fproduct_carry_wide_()
81 tmp[ctr] = FStar_UInt128_uint64_to_uint128(r0); in Hacl_Bignum_Fproduct_carry_wide_()
82 tmp[ctr + (uint32_t)1U] = FStar_UInt128_add(tctrp1, c); in Hacl_Bignum_Fproduct_carry_wide_()
88 uint64_t tmp = output[4U]; in Hacl_Bignum_Fmul_shift_reduce() local
99 output[0U] = tmp; in Hacl_Bignum_Fmul_shift_reduce()
129 uint64_t tmp[5U] = { 0U }; in Hacl_Bignum_Fmul_fmul() local
130 memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]); in Hacl_Bignum_Fmul_fmul()
148 Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input2); 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
207 tmp[0U] = s0; in Hacl_Bignum_Fsquare_fsquare__()
208 tmp[1U] = s1; in Hacl_Bignum_Fsquare_fsquare__()
209 tmp[2U] = s2; in Hacl_Bignum_Fsquare_fsquare__()
210 tmp[3U] = s3; in Hacl_Bignum_Fsquare_fsquare__()
211 tmp[4U] = s4; 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_()
225 Hacl_Bignum_Fproduct_carry_wide_(tmp); in Hacl_Bignum_Fsquare_fsquare_()
226 b4 = tmp[4U]; in Hacl_Bignum_Fsquare_fsquare_()
227 b0 = tmp[0U]; in Hacl_Bignum_Fsquare_fsquare_()
233 tmp[4U] = b4_; in Hacl_Bignum_Fsquare_fsquare_()
234 tmp[0U] = b0_; in Hacl_Bignum_Fsquare_fsquare_()
235 Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp); in Hacl_Bignum_Fsquare_fsquare_()
247 FStar_UInt128_uint128 *tmp, 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_()
344 uint64_t tmp[5U] = { 0U }; in Hacl_Bignum_fdifference() local
350 memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]); in Hacl_Bignum_fdifference()
351 b0 = tmp[0U]; in Hacl_Bignum_fdifference()
352 b1 = tmp[1U]; in Hacl_Bignum_fdifference()
353 b2 = tmp[2U]; in Hacl_Bignum_fdifference()
354 b3 = tmp[3U]; in Hacl_Bignum_fdifference()
355 b4 = tmp[4U]; in Hacl_Bignum_fdifference()
356 tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U; in Hacl_Bignum_fdifference()
357 tmp[1U] = b1 + (uint64_t)0x3ffffffffffff8U; in Hacl_Bignum_fdifference()
358 tmp[2U] = b2 + (uint64_t)0x3ffffffffffff8U; in Hacl_Bignum_fdifference()
359 tmp[3U] = b3 + (uint64_t)0x3ffffffffffff8U; in Hacl_Bignum_fdifference()
360 tmp[4U] = b4 + (uint64_t)0x3ffffffffffff8U; in Hacl_Bignum_fdifference()
366 uint64_t yi = tmp[i]; in Hacl_Bignum_fdifference()
376 FStar_UInt128_uint128 tmp[5U]; in Hacl_Bignum_fscalar() local
380 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); in Hacl_Bignum_fscalar()
392 tmp[i] = FStar_UInt128_mul_wide(xi, s); in Hacl_Bignum_fscalar()
395 Hacl_Bignum_Fproduct_carry_wide_(tmp); in Hacl_Bignum_fscalar()
396 b4 = tmp[4U]; in Hacl_Bignum_fscalar()
397 b0 = tmp[0U]; in Hacl_Bignum_fscalar()
403 tmp[4U] = b4_; in Hacl_Bignum_fscalar()
404 tmp[0U] = b0_; in Hacl_Bignum_fscalar()
405 Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp); in Hacl_Bignum_fscalar()