Lines Matching refs:b4_
38 uint64_t b4_ = b4 & (uint64_t)0x7ffffffffffffU; in Hacl_Bignum_Modulo_carry_top() local
40 b[4U] = b4_; in Hacl_Bignum_Modulo_carry_top()
142 FStar_UInt128_uint128 b4_; in Hacl_Bignum_Fmul_fmul() local
152 b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)); in Hacl_Bignum_Fmul_fmul()
157 t[4U] = b4_; in Hacl_Bignum_Fmul_fmul()
218 FStar_UInt128_uint128 b4_; in Hacl_Bignum_Fsquare_fsquare_() local
228 b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)); in Hacl_Bignum_Fsquare_fsquare_()
233 tmp[4U] = b4_; in Hacl_Bignum_Fsquare_fsquare_()
385 FStar_UInt128_uint128 b4_; in Hacl_Bignum_fscalar() local
398 b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)); in Hacl_Bignum_fscalar()
403 tmp[4U] = b4_; in Hacl_Bignum_fscalar()