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) in Hacl_Bignum_Fproduct_copy_from_wide_()
46 uint128_t xi = input[i]; in Hacl_Bignum_Fproduct_copy_from_wide_()
52 Hacl_Bignum_Fproduct_sum_scalar_multiplication_(uint128_t *output, uint64_t *input, uint64_t s) in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
57 uint128_t xi = output[i]; in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
59 output[i] = xi + (uint128_t)yi * s; in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
63 inline static void Hacl_Bignum_Fproduct_carry_wide_(uint128_t *tmp) in Hacl_Bignum_Fproduct_carry_wide_()
69 uint128_t tctr = tmp[ctr]; in Hacl_Bignum_Fproduct_carry_wide_()
70 uint128_t tctrp1 = tmp[ctr + (uint32_t)1U]; in Hacl_Bignum_Fproduct_carry_wide_()
72 uint128_t c = tctr >> (uint32_t)51U; in Hacl_Bignum_Fproduct_carry_wide_()
73 tmp[ctr] = (uint128_t)r0; in Hacl_Bignum_Fproduct_carry_wide_()
97 Hacl_Bignum_Fmul_mul_shift_reduce_(uint128_t *output, uint64_t *input, uint64_t *input2) in Hacl_Bignum_Fmul_mul_shift_reduce_()
119 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U); in Hacl_Bignum_Fmul_fmul()
121 uint128_t t[5U]; in Hacl_Bignum_Fmul_fmul()
125 t[_i] = (uint128_t)(uint64_t)0U; in Hacl_Bignum_Fmul_fmul()
128 uint128_t b4; in Hacl_Bignum_Fmul_fmul()
129 uint128_t b0; in Hacl_Bignum_Fmul_fmul()
130 uint128_t b4_; in Hacl_Bignum_Fmul_fmul()
131 uint128_t b0_; in Hacl_Bignum_Fmul_fmul()
140 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU; in Hacl_Bignum_Fmul_fmul()
141 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U); in Hacl_Bignum_Fmul_fmul()
155 inline static void Hacl_Bignum_Fsquare_fsquare__(uint128_t *tmp, uint64_t *output) in Hacl_Bignum_Fsquare_fsquare__()
167 uint128_t s0 = (uint128_t)r0 * r0 + (uint128_t)d4 * r1 + (uint128_t)d2 * r3; in Hacl_Bignum_Fsquare_fsquare__()
168 uint128_t s1 = (uint128_t)d0 * r1 + (uint128_t)d4 * r2 + (uint128_t)(r3 * (uint64_t)19U) * r3; in Hacl_Bignum_Fsquare_fsquare__()
169 uint128_t s2 = (uint128_t)d0 * r2 + (uint128_t)r1 * r1 + (uint128_t)d4 * r3; in Hacl_Bignum_Fsquare_fsquare__()
170 uint128_t s3 = (uint128_t)d0 * r3 + (uint128_t)d1 * r2 + (uint128_t)r4 * d419; in Hacl_Bignum_Fsquare_fsquare__()
171 uint128_t s4 = (uint128_t)d0 * r4 + (uint128_t)d1 * r3 + (uint128_t)r2 * r2; in Hacl_Bignum_Fsquare_fsquare__()
179 inline static void Hacl_Bignum_Fsquare_fsquare_(uint128_t *tmp, uint64_t *output) in Hacl_Bignum_Fsquare_fsquare_()
181 uint128_t b4; in Hacl_Bignum_Fsquare_fsquare_()
182 uint128_t b0; in Hacl_Bignum_Fsquare_fsquare_()
183 uint128_t b4_; in Hacl_Bignum_Fsquare_fsquare_()
184 uint128_t b0_; in Hacl_Bignum_Fsquare_fsquare_()
193 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU; in Hacl_Bignum_Fsquare_fsquare_()
194 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U); in Hacl_Bignum_Fsquare_fsquare_()
207 Hacl_Bignum_Fsquare_fsquare_times_(uint64_t *input, uint128_t *tmp, uint32_t count1) in Hacl_Bignum_Fsquare_fsquare_times_()
218 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U); in Hacl_Bignum_Fsquare_fsquare_times()
220 uint128_t t[5U]; in Hacl_Bignum_Fsquare_fsquare_times()
224 t[_i] = (uint128_t)(uint64_t)0U; in Hacl_Bignum_Fsquare_fsquare_times()
233 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U); in Hacl_Bignum_Fsquare_fsquare_times_inplace()
235 uint128_t t[5U]; in Hacl_Bignum_Fsquare_fsquare_times_inplace()
239 t[_i] = (uint128_t)(uint64_t)0U; in Hacl_Bignum_Fsquare_fsquare_times_inplace()
332 KRML_CHECK_SIZE(sizeof (uint128_t), (uint32_t)5U); in Hacl_Bignum_fscalar()
334 uint128_t tmp[5U]; in Hacl_Bignum_fscalar()
338 tmp[_i] = (uint128_t)(uint64_t)0U; in Hacl_Bignum_fscalar()
341 uint128_t b4; in Hacl_Bignum_fscalar()
342 uint128_t b0; in Hacl_Bignum_fscalar()
343 uint128_t b4_; in Hacl_Bignum_fscalar()
344 uint128_t b0_; in Hacl_Bignum_fscalar()
350 tmp[i] = (uint128_t)xi * s; in Hacl_Bignum_fscalar()
356 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU; in Hacl_Bignum_fscalar()
357 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U); in Hacl_Bignum_fscalar()