22   return projectee.high;  in FStar_UInt128___proj__Mkuint128__item__high()
38   flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };  in FStar_UInt128_add()
46   flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };  in FStar_UInt128_add_underspec()
53   flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };  in FStar_UInt128_add_mod()
60   flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) };  in FStar_UInt128_sub()
68   flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) };  in FStar_UInt128_sub_underspec()
76   flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) };  in FStar_UInt128_sub_mod_impl()
87   FStar_UInt128_uint128 flat = { a.low & b.low, a.high & b.high };  in FStar_UInt128_logand()
93   FStar_UInt128_uint128 flat = { a.low ^ b.low, a.high ^ b.high };  in FStar_UInt128_logxor()
99   FStar_UInt128_uint128 flat = { a.low | b.low, a.high | b.high };  in FStar_UInt128_logor()
105   FStar_UInt128_uint128 flat = { ~a.low, ~a.high };  in FStar_UInt128_lognot()
131     flat = { a.low << s, FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s) };  in FStar_UInt128_shift_left_small()
175     flat = { FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s), a.high >> s };  in FStar_UInt128_shift_right_small()
183   FStar_UInt128_uint128 flat = { a.high >> (s - FStar_UInt128_u32_64), (uint64_t)0U };  in FStar_UInt128_shift_right_large()
201   return a.low == b.low && a.high == b.high;  in FStar_UInt128_eq()
206   return a.high > b.high || (a.high == b.high && a.low > b.low);  in FStar_UInt128_gt()
211   return a.high < b.high || (a.high == b.high && a.low < b.low);  in FStar_UInt128_lt()
216   return a.high > b.high || (a.high == b.high && a.low >= b.low);  in FStar_UInt128_gte()
221   return a.high < b.high || (a.high == b.high && a.low <= b.low);  in FStar_UInt128_lte()
231       & FStar_UInt64_eq_mask(a.high, b.high),  in FStar_UInt128_eq_mask()
234       & FStar_UInt64_eq_mask(a.high, b.high)  in FStar_UInt128_eq_mask()
244       (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high))  in FStar_UInt128_gte_mask()
245       | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low)),  in FStar_UInt128_gte_mask()
246       (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high))  in FStar_UInt128_gte_mask()
247       | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low))  in FStar_UInt128_gte_mask()