25 static uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)  in FStar_UInt128_constant_time_carry()
30 static uint64_t FStar_UInt128_carry(uint64_t a, uint64_t b)  in FStar_UInt128_carry()
35 FStar_UInt128_uint128 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_add()
43 FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_add_underspec()
50 FStar_UInt128_uint128 FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_add_mod()
57 FStar_UInt128_uint128 FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_sub()
65 FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_sub_underspec()
73 FStar_UInt128_sub_mod_impl(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_sub_mod_impl()
80 FStar_UInt128_uint128 FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_sub_mod()
85 FStar_UInt128_uint128 FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_logand()
91 FStar_UInt128_uint128 FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_logxor()
97 FStar_UInt128_uint128 FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_logor()
103 FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a)  in FStar_UInt128_lognot()
122 FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s)  in FStar_UInt128_shift_left_small()
137 FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s)  in FStar_UInt128_shift_left_large()
143 FStar_UInt128_uint128 FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s)  in FStar_UInt128_shift_left()
166 FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s)  in FStar_UInt128_shift_right_small()
181 FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s)  in FStar_UInt128_shift_right_large()
187 FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s)  in FStar_UInt128_shift_right()
199 bool FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_eq()
204 bool FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_gt()
209 bool FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_lt()
214 bool FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_gte()
219 bool FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_lte()
224 FStar_UInt128_uint128 FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_eq_mask()
239 FStar_UInt128_uint128 FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)  in FStar_UInt128_gte_mask()
252 FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a)  in FStar_UInt128_uint64_to_uint128()
258 uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a)  in FStar_UInt128_uint128_to_uint64()
329 static uint64_t FStar_UInt128_u64_mod_32(uint64_t a)  in FStar_UInt128_u64_mod_32()