38   flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };  in FStar_UInt128_add()  local
46   flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };  in FStar_UInt128_add_underspec()  local
53   flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };  in FStar_UInt128_add_mod()  local
60   flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) };  in FStar_UInt128_sub()  local
68   flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) };  in FStar_UInt128_sub_underspec()  local
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()  local
87   FStar_UInt128_uint128 flat = { a.low & b.low, a.high & b.high };  in FStar_UInt128_logand()  local
93   FStar_UInt128_uint128 flat = { a.low ^ b.low, a.high ^ b.high };  in FStar_UInt128_logxor()  local
99   FStar_UInt128_uint128 flat = { a.low | b.low, a.high | b.high };  in FStar_UInt128_logor()  local
105   FStar_UInt128_uint128 flat = { ~a.low, ~a.high };  in FStar_UInt128_lognot()  local
131     flat = { a.low << s, FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s) };  in FStar_UInt128_shift_left_small()  local
139   FStar_UInt128_uint128 flat = { (uint64_t)0U, a.low << (s - FStar_UInt128_u32_64) };  in FStar_UInt128_shift_left_large()  local
175     flat = { FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s), a.high >> s };  in FStar_UInt128_shift_right_small()  local
183   FStar_UInt128_uint128 flat = { a.high >> (s - FStar_UInt128_u32_64), (uint64_t)0U };  in FStar_UInt128_shift_right_large()  local
227   flat =  in FStar_UInt128_eq_mask()  local
242   flat =  in FStar_UInt128_gte_mask()  local
254   FStar_UInt128_uint128 flat = { a, (uint64_t)0U };  in FStar_UInt128_uint64_to_uint128()  local
344   flat =  in FStar_UInt128_mul32()  local
371   flat =  in FStar_UInt128_mul_wide_impl_t_()  local
397   flat =  in FStar_UInt128_mul_wide_impl()  local