Searched refs:FStar_UInt128_u64_mod_32 (Results 1 – 1 of 1) sorted by relevance
329 static uint64_t FStar_UInt128_u64_mod_32(uint64_t a) in FStar_UInt128_u64_mod_32() function348 + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> FStar_UInt128_u32_32), in FStar_UInt128_mul32()349 FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * (uint64_t)y)), in FStar_UInt128_mul32()352 + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> FStar_UInt128_u32_32)) in FStar_UInt128_mul32()373 FStar_UInt128_u64_mod_32(x), in FStar_UInt128_mul_wide_impl_t_()374 FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y)), in FStar_UInt128_mul_wide_impl_t_()378 * FStar_UInt128_u64_mod_32(y) in FStar_UInt128_mul_wide_impl_t_()379 + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32) in FStar_UInt128_mul_wide_impl_t_()399 FStar_UInt128_u32_combine_(u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_), in FStar_UInt128_mul_wide_impl()404 + ((u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_)) >> FStar_UInt128_u32_32) in FStar_UInt128_mul_wide_impl()