Searched refs:FStar_UInt128_uint128_to_uint64 (Results 1 – 4 of 4) sorted by relevance
30 extern uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 x0);51 output[i] = FStar_UInt128_uint128_to_uint64(xi); in Hacl_Bignum_Fproduct_copy_from_wide_()79 uint64_t r0 = FStar_UInt128_uint128_to_uint64(tctr) & (uint64_t)0x7ffffffffffffU; in Hacl_Bignum_Fproduct_carry_wide_()156 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_Fmul_fmul()232 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_Fsquare_fsquare_()402 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_fscalar()
68 uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a);
258 uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a) in FStar_UInt128_uint128_to_uint64() function
27 extern uint64_t FStar_UInt128_uint128_to_uint64(uint128_t x0);