Lines Matching refs:a
25 static uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b) in FStar_UInt128_constant_time_carry() argument
27 return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t)63U; in FStar_UInt128_constant_time_carry()
30 static uint64_t FStar_UInt128_carry(uint64_t a, uint64_t b) in FStar_UInt128_carry() argument
32 return FStar_UInt128_constant_time_carry(a, b); in FStar_UInt128_carry()
35 FStar_UInt128_uint128 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_add() argument
38 flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) }; in FStar_UInt128_add()
43 FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_add_underspec() argument
46 flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) }; 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() argument
53 flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) }; in FStar_UInt128_add_mod()
57 FStar_UInt128_uint128 FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_sub() argument
60 flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) }; in FStar_UInt128_sub()
65 FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_sub_underspec() argument
68 flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) }; 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() argument
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()
80 FStar_UInt128_uint128 FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_sub_mod() argument
82 return FStar_UInt128_sub_mod_impl(a, 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() argument
87 FStar_UInt128_uint128 flat = { a.low & b.low, a.high & b.high }; in FStar_UInt128_logand()
91 FStar_UInt128_uint128 FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_logxor() argument
93 FStar_UInt128_uint128 flat = { a.low ^ b.low, a.high ^ b.high }; in FStar_UInt128_logxor()
97 FStar_UInt128_uint128 FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_logor() argument
99 FStar_UInt128_uint128 flat = { a.low | b.low, a.high | b.high }; in FStar_UInt128_logor()
103 FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a) in FStar_UInt128_lognot() argument
105 FStar_UInt128_uint128 flat = { ~a.low, ~a.high }; in FStar_UInt128_lognot()
122 FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s) in FStar_UInt128_shift_left_small() argument
126 return a; in FStar_UInt128_shift_left_small()
131 flat = { a.low << s, FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, 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() argument
139 FStar_UInt128_uint128 flat = { (uint64_t)0U, a.low << (s - FStar_UInt128_u32_64) }; 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() argument
147 return FStar_UInt128_shift_left_small(a, s); in FStar_UInt128_shift_left()
151 return FStar_UInt128_shift_left_large(a, 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() argument
170 return a; in FStar_UInt128_shift_right_small()
175 flat = { FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s), a.high >> 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() argument
183 FStar_UInt128_uint128 flat = { a.high >> (s - FStar_UInt128_u32_64), (uint64_t)0U }; 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() argument
191 return FStar_UInt128_shift_right_small(a, s); in FStar_UInt128_shift_right()
195 return FStar_UInt128_shift_right_large(a, s); in FStar_UInt128_shift_right()
199 bool FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_eq() argument
201 return a.low == b.low && a.high == b.high; in FStar_UInt128_eq()
204 bool FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_gt() argument
206 return a.high > b.high || (a.high == b.high && a.low > b.low); in FStar_UInt128_gt()
209 bool FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_lt() argument
211 return a.high < b.high || (a.high == b.high && a.low < b.low); in FStar_UInt128_lt()
214 bool FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_gte() argument
216 return a.high > b.high || (a.high == b.high && a.low >= b.low); in FStar_UInt128_gte()
219 bool FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_lte() argument
221 return a.high < b.high || (a.high == b.high && a.low <= b.low); 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() argument
229 FStar_UInt64_eq_mask(a.low, in FStar_UInt128_eq_mask()
231 & FStar_UInt64_eq_mask(a.high, b.high), in FStar_UInt128_eq_mask()
232 FStar_UInt64_eq_mask(a.low, in FStar_UInt128_eq_mask()
234 & FStar_UInt64_eq_mask(a.high, b.high) 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() argument
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()
252 FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a) in FStar_UInt128_uint64_to_uint128() argument
254 FStar_UInt128_uint128 flat = { a, (uint64_t)0U }; in FStar_UInt128_uint64_to_uint128()
258 uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a) in FStar_UInt128_uint128_to_uint64() argument
260 return a.low; in FStar_UInt128_uint128_to_uint64()
329 static uint64_t FStar_UInt128_u64_mod_32(uint64_t a) in FStar_UInt128_u64_mod_32() argument
331 return a & (uint64_t)0xffffffffU; in FStar_UInt128_u64_mod_32()