Home
last modified time | relevance | path

Searched refs:FStar_UInt128_uint128 (Results 1 – 4 of 4) sorted by relevance

/mbedtls-latest/3rdparty/everest/include/everest/kremlib/
DFStar_UInt128.h20 uint64_t FStar_UInt128___proj__Mkuint128__item__low(FStar_UInt128_uint128 projectee);
22 uint64_t FStar_UInt128___proj__Mkuint128__item__high(FStar_UInt128_uint128 projectee);
24 typedef FStar_UInt128_uint128 FStar_UInt128_t;
26 FStar_UInt128_uint128 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
28 FStar_UInt128_uint128
29 FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
31 FStar_UInt128_uint128 FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
33 FStar_UInt128_uint128 FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
35 FStar_UInt128_uint128
36 FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
[all …]
/mbedtls-latest/3rdparty/everest/library/kremlib/
DFStar_UInt128_extracted.c15 uint64_t FStar_UInt128___proj__Mkuint128__item__low(FStar_UInt128_uint128 projectee) in FStar_UInt128___proj__Mkuint128__item__low()
20 uint64_t FStar_UInt128___proj__Mkuint128__item__high(FStar_UInt128_uint128 projectee) in FStar_UInt128___proj__Mkuint128__item__high()
35 FStar_UInt128_uint128 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_add()
37 FStar_UInt128_uint128 in FStar_UInt128_add()
42 FStar_UInt128_uint128
43 FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_add_underspec()
45 FStar_UInt128_uint128 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()
52 FStar_UInt128_uint128 in FStar_UInt128_add_mod()
57 FStar_UInt128_uint128 FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b) in FStar_UInt128_sub()
[all …]
/mbedtls-latest/3rdparty/everest/library/legacy/
DHacl_Curve25519.c17 extern FStar_UInt128_uint128
18 FStar_UInt128_add(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
20 extern FStar_UInt128_uint128
21 FStar_UInt128_add_mod(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
23 extern FStar_UInt128_uint128
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);
[all …]
/mbedtls-latest/3rdparty/everest/include/everest/kremlin/internal/
Dtypes.h49 typedef __m128i FStar_UInt128_uint128; typedef
51 typedef unsigned __int128 FStar_UInt128_uint128; typedef
56 } FStar_UInt128_uint128; typedef
59 typedef FStar_UInt128_uint128 FStar_UInt128_t, FStar_UInt128_t_, uint128_t;