Lines Matching refs:x0
13 extern uint64_t FStar_UInt64_eq_mask(uint64_t x0, uint64_t x1);
15 extern uint64_t FStar_UInt64_gte_mask(uint64_t x0, uint64_t x1);
18 FStar_UInt128_add(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
21 FStar_UInt128_add_mod(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
24 FStar_UInt128_logand(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
26 extern FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 x0, uint32_t x1);
28 extern FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t x0);
30 extern uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 x0);
32 extern FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x0, uint64_t x1);
469 uint8_t *x0 = input + (uint32_t)24U; in Hacl_EC_Format_fexpand() local
470 uint64_t i4 = load64_le(x0); in Hacl_EC_Format_fexpand()
772 uint64_t *x0 = buf0; in Hacl_Curve25519_crypto_scalarmult() local
775 Hacl_EC_Format_fexpand(x0, basepoint); in Hacl_Curve25519_crypto_scalarmult()