Lines Matching refs:hi
111 static uint64_t FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s) in FStar_UInt128_add_u64_shift_left() argument
113 return (hi << s) + (lo >> (FStar_UInt128_u32_64 - s)); in FStar_UInt128_add_u64_shift_left()
116 static uint64_t FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s) in FStar_UInt128_add_u64_shift_left_respec() argument
118 return FStar_UInt128_add_u64_shift_left(hi, lo, s); in FStar_UInt128_add_u64_shift_left_respec()
155 static uint64_t FStar_UInt128_add_u64_shift_right(uint64_t hi, uint64_t lo, uint32_t s) in FStar_UInt128_add_u64_shift_right() argument
157 return (lo >> s) + (hi << (FStar_UInt128_u32_64 - s)); in FStar_UInt128_add_u64_shift_right()
160 static uint64_t FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s) in FStar_UInt128_add_u64_shift_right_respec() argument
162 return FStar_UInt128_add_u64_shift_right(hi, lo, s); in FStar_UInt128_add_u64_shift_right_respec()
336 static uint64_t FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo) in FStar_UInt128_u32_combine() argument
338 return lo + (hi << FStar_UInt128_u32_32); in FStar_UInt128_u32_combine()
384 static uint64_t FStar_UInt128_u32_combine_(uint64_t hi, uint64_t lo) in FStar_UInt128_u32_combine_() argument
386 return lo + (hi << FStar_UInt128_u32_32); in FStar_UInt128_u32_combine_()