Lines Matching refs:b4
36 uint64_t b4 = b[4U]; in Hacl_Bignum_Modulo_carry_top() local
38 uint64_t b4_ = b4 & (uint64_t)0x7ffffffffffffU; in Hacl_Bignum_Modulo_carry_top()
39 uint64_t b0_ = b0 + (uint64_t)19U * (b4 >> (uint32_t)51U); in Hacl_Bignum_Modulo_carry_top()
140 FStar_UInt128_uint128 b4; in Hacl_Bignum_Fmul_fmul() local
150 b4 = t[4U]; in Hacl_Bignum_Fmul_fmul()
152 b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)); in Hacl_Bignum_Fmul_fmul()
156 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_Fmul_fmul()
216 FStar_UInt128_uint128 b4; in Hacl_Bignum_Fsquare_fsquare_() local
226 b4 = tmp[4U]; in Hacl_Bignum_Fsquare_fsquare_()
228 b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)); in Hacl_Bignum_Fsquare_fsquare_()
232 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_Fsquare_fsquare_()
349 uint64_t b4; in Hacl_Bignum_fdifference() local
355 b4 = tmp[4U]; in Hacl_Bignum_fdifference()
360 tmp[4U] = b4 + (uint64_t)0x3ffffffffffff8U; in Hacl_Bignum_fdifference()
383 FStar_UInt128_uint128 b4; in Hacl_Bignum_fscalar() local
396 b4 = tmp[4U]; in Hacl_Bignum_fscalar()
398 b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)); in Hacl_Bignum_fscalar()
402 FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); in Hacl_Bignum_fscalar()