Lines Matching refs:FStar_UInt128_uint128
17 extern FStar_UInt128_uint128
18 FStar_UInt128_add(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
20 extern FStar_UInt128_uint128
21 FStar_UInt128_add_mod(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
23 extern FStar_UInt128_uint128
24 FStar_UInt128_logand(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
26 extern FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 x0, uint32_t x1);
28 extern FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t x0);
30 extern uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 x0);
32 extern FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x0, uint64_t x1);
45 Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, FStar_UInt128_uint128 *input) in Hacl_Bignum_Fproduct_copy_from_wide_()
50 FStar_UInt128_uint128 xi = input[i]; in Hacl_Bignum_Fproduct_copy_from_wide_()
57 FStar_UInt128_uint128 *output, in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
65 FStar_UInt128_uint128 xi = output[i]; in Hacl_Bignum_Fproduct_sum_scalar_multiplication_()
71 inline static void Hacl_Bignum_Fproduct_carry_wide_(FStar_UInt128_uint128 *tmp) in Hacl_Bignum_Fproduct_carry_wide_()
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_()
80 FStar_UInt128_uint128 c = FStar_UInt128_shift_right(tctr, (uint32_t)51U); in Hacl_Bignum_Fproduct_carry_wide_()
106 FStar_UInt128_uint128 *output, in Hacl_Bignum_Fmul_mul_shift_reduce_()
131 KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U); in Hacl_Bignum_Fmul_fmul()
133 FStar_UInt128_uint128 t[5U]; in Hacl_Bignum_Fmul_fmul()
140 FStar_UInt128_uint128 b4; in Hacl_Bignum_Fmul_fmul()
141 FStar_UInt128_uint128 b0; in Hacl_Bignum_Fmul_fmul()
142 FStar_UInt128_uint128 b4_; in Hacl_Bignum_Fmul_fmul()
143 FStar_UInt128_uint128 b0_; 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__()
182 FStar_UInt128_uint128 in Hacl_Bignum_Fsquare_fsquare__()
187 FStar_UInt128_uint128 in Hacl_Bignum_Fsquare_fsquare__()
192 FStar_UInt128_uint128 in Hacl_Bignum_Fsquare_fsquare__()
197 FStar_UInt128_uint128 in Hacl_Bignum_Fsquare_fsquare__()
202 FStar_UInt128_uint128 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_()
216 FStar_UInt128_uint128 b4; in Hacl_Bignum_Fsquare_fsquare_()
217 FStar_UInt128_uint128 b0; in Hacl_Bignum_Fsquare_fsquare_()
218 FStar_UInt128_uint128 b4_; in Hacl_Bignum_Fsquare_fsquare_()
219 FStar_UInt128_uint128 b0_; in Hacl_Bignum_Fsquare_fsquare_()
247 FStar_UInt128_uint128 *tmp, in Hacl_Bignum_Fsquare_fsquare_times_()
260 KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U); in Hacl_Bignum_Fsquare_fsquare_times()
262 FStar_UInt128_uint128 t[5U]; in Hacl_Bignum_Fsquare_fsquare_times()
275 KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U); in Hacl_Bignum_Fsquare_fsquare_times_inplace()
277 FStar_UInt128_uint128 t[5U]; in Hacl_Bignum_Fsquare_fsquare_times_inplace()
374 KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U); in Hacl_Bignum_fscalar()
376 FStar_UInt128_uint128 tmp[5U]; in Hacl_Bignum_fscalar()
383 FStar_UInt128_uint128 b4; in Hacl_Bignum_fscalar()
384 FStar_UInt128_uint128 b0; in Hacl_Bignum_fscalar()
385 FStar_UInt128_uint128 b4_; in Hacl_Bignum_fscalar()
386 FStar_UInt128_uint128 b0_; in Hacl_Bignum_fscalar()