Lines Matching refs:uint128_t
17 extern uint128_t FStar_UInt128_add(uint128_t x0, uint128_t x1);
19 extern uint128_t FStar_UInt128_add_mod(uint128_t x0, uint128_t x1);
21 extern uint128_t FStar_UInt128_logand(uint128_t x0, uint128_t x1);
23 extern uint128_t FStar_UInt128_shift_right(uint128_t x0, uint32_t x1);
25 extern uint128_t FStar_UInt128_uint64_to_uint128(uint64_t x0);
27 extern uint64_t FStar_UInt128_uint128_to_uint64(uint128_t x0);
29 extern uint128_t FStar_UInt128_mul_wide(uint64_t x0, uint64_t x1);
41 inline static void Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, uint128_t *input)
46 uint128_t xi = input[i];
52 Hacl_Bignum_Fproduct_sum_scalar_multiplication_(uint128_t *output, uint64_t *input, uint64_t s)
57 uint128_t xi = output[i];
59 output[i] = xi + (uint128_t)yi * s;
63 inline static void Hacl_Bignum_Fproduct_carry_wide_(uint128_t *tmp)
69 uint128_t tctr = tmp[ctr];
70 uint128_t tctrp1 = tmp[ctr + (uint32_t)1U];
72 uint128_t c = tctr >> (uint32_t)51U;
73 tmp[ctr] = (uint128_t)r0;
97 Hacl_Bignum_Fmul_mul_shift_reduce_(uint128_t *output, uint64_t *input, uint64_t *input2)
119 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U);
121 uint128_t t[5U];
125 t[_i] = (uint128_t)(uint64_t)0U;
128 uint128_t b4;
129 uint128_t b0;
130 uint128_t b4_;
131 uint128_t b0_;
140 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU;
141 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U);
155 inline static void Hacl_Bignum_Fsquare_fsquare__(uint128_t *tmp, uint64_t *output)
167 uint128_t s0 = (uint128_t)r0 * r0 + (uint128_t)d4 * r1 + (uint128_t)d2 * r3;
168 uint128_t s1 = (uint128_t)d0 * r1 + (uint128_t)d4 * r2 + (uint128_t)(r3 * (uint64_t)19U) * r3;
169 uint128_t s2 = (uint128_t)d0 * r2 + (uint128_t)r1 * r1 + (uint128_t)d4 * r3;
170 uint128_t s3 = (uint128_t)d0 * r3 + (uint128_t)d1 * r2 + (uint128_t)r4 * d419;
171 uint128_t s4 = (uint128_t)d0 * r4 + (uint128_t)d1 * r3 + (uint128_t)r2 * r2;
179 inline static void Hacl_Bignum_Fsquare_fsquare_(uint128_t *tmp, uint64_t *output)
181 uint128_t b4;
182 uint128_t b0;
183 uint128_t b4_;
184 uint128_t b0_;
193 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU;
194 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U);
207 Hacl_Bignum_Fsquare_fsquare_times_(uint64_t *input, uint128_t *tmp, uint32_t count1)
218 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U);
220 uint128_t t[5U];
224 t[_i] = (uint128_t)(uint64_t)0U;
233 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U);
235 uint128_t t[5U];
239 t[_i] = (uint128_t)(uint64_t)0U;
332 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U);
334 uint128_t tmp[5U];
338 tmp[_i] = (uint128_t)(uint64_t)0U;
341 uint128_t b4;
342 uint128_t b0;
343 uint128_t b4_;
344 uint128_t b0_;
350 tmp[i] = (uint128_t)xi * s;
356 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU;
357 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U);