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