ECDH: Everest: Remove unnecessary file
diff --git a/3rdparty/everest/library/kremlib/fstar_uint128.c b/3rdparty/everest/library/kremlib/fstar_uint128.c
deleted file mode 100644
index cadfbc7..0000000
--- a/3rdparty/everest/library/kremlib/fstar_uint128.c
+++ /dev/null
@@ -1,216 +0,0 @@
-/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
- Licensed under the Apache 2.0 License. */
-
-/******************************************************************************/
-/* Machine integers (128-bit arithmetic) */
-/******************************************************************************/
-
-/* This header makes KreMLin-generated C code work with:
- * - the default setting where we assume the target compiler defines __int128
- * - the setting where we use FStar.UInt128's implementation instead; in that
- * case, generated C files must be compiled with -DKRML_VERIFIED_UINT128
- * - a refinement of the case above, wherein all structures are passed by
- * reference, a.k.a. "-fnostruct-passing", meaning that the KreMLin-generated
- * must be compiled with -DKRML_NOSTRUCT_PASSING
- * Note: no MSVC support in this file.
- */
-
-#include "FStar_UInt128.h"
-#include "kremlin/c_endianness.h"
-#include "FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.h"
-
-#if !defined(KRML_VERIFIED_UINT128) && !defined(_MSC_VER)
-
-/* GCC + using native unsigned __int128 support */
-
-uint128_t load128_le(uint8_t *b) {
- uint128_t l = (uint128_t)load64_le(b);
- uint128_t h = (uint128_t)load64_le(b + 8);
- return (h << 64 | l);
-}
-
-void store128_le(uint8_t *b, uint128_t n) {
- store64_le(b, (uint64_t)n);
- store64_le(b + 8, (uint64_t)(n >> 64));
-}
-
-uint128_t load128_be(uint8_t *b) {
- uint128_t h = (uint128_t)load64_be(b);
- uint128_t l = (uint128_t)load64_be(b + 8);
- return (h << 64 | l);
-}
-
-void store128_be(uint8_t *b, uint128_t n) {
- store64_be(b, (uint64_t)(n >> 64));
- store64_be(b + 8, (uint64_t)n);
-}
-
-uint128_t FStar_UInt128_add(uint128_t x, uint128_t y) {
- return x + y;
-}
-
-uint128_t FStar_UInt128_mul(uint128_t x, uint128_t y) {
- return x * y;
-}
-
-uint128_t FStar_UInt128_add_mod(uint128_t x, uint128_t y) {
- return x + y;
-}
-
-uint128_t FStar_UInt128_sub(uint128_t x, uint128_t y) {
- return x - y;
-}
-
-uint128_t FStar_UInt128_sub_mod(uint128_t x, uint128_t y) {
- return x - y;
-}
-
-uint128_t FStar_UInt128_logand(uint128_t x, uint128_t y) {
- return x & y;
-}
-
-uint128_t FStar_UInt128_logor(uint128_t x, uint128_t y) {
- return x | y;
-}
-
-uint128_t FStar_UInt128_logxor(uint128_t x, uint128_t y) {
- return x ^ y;
-}
-
-uint128_t FStar_UInt128_lognot(uint128_t x) {
- return ~x;
-}
-
-uint128_t FStar_UInt128_shift_left(uint128_t x, uint32_t y) {
- return x << y;
-}
-
-uint128_t FStar_UInt128_shift_right(uint128_t x, uint32_t y) {
- return x >> y;
-}
-
-uint128_t FStar_UInt128_uint64_to_uint128(uint64_t x) {
- return (uint128_t)x;
-}
-
-uint64_t FStar_UInt128_uint128_to_uint64(uint128_t x) {
- return (uint64_t)x;
-}
-
-uint128_t FStar_UInt128_mul_wide(uint64_t x, uint64_t y) {
- return ((uint128_t) x) * y;
-}
-
-uint128_t FStar_UInt128_eq_mask(uint128_t x, uint128_t y) {
- uint64_t mask =
- FStar_UInt64_eq_mask((uint64_t)(x >> 64), (uint64_t)(y >> 64)) &
- FStar_UInt64_eq_mask(x, y);
- return ((uint128_t)mask) << 64 | mask;
-}
-
-uint128_t FStar_UInt128_gte_mask(uint128_t x, uint128_t y) {
- uint64_t mask =
- (FStar_UInt64_gte_mask(x >> 64, y >> 64) &
- ~(FStar_UInt64_eq_mask(x >> 64, y >> 64))) |
- (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask(x, y));
- return ((uint128_t)mask) << 64 | mask;
-}
-
-uint128_t FStar_Int_Cast_Full_uint64_to_uint128(uint64_t x) {
- return x;
-}
-
-uint64_t FStar_Int_Cast_Full_uint128_to_uint64(uint128_t x) {
- return x;
-}
-
-#elif !defined(_MSC_VER) && defined(KRML_VERIFIED_UINT128)
-
-/* Verified uint128 implementation. */
-
-/* Access 64-bit fields within the int128. */
-#define HIGH64_OF(x) ((x)->high)
-#define LOW64_OF(x) ((x)->low)
-
-typedef FStar_UInt128_uint128 FStar_UInt128_t_, uint128_t;
-
-/* A series of definitions written using pointers. */
-
-void load128_le_(uint8_t *b, uint128_t *r) {
- LOW64_OF(r) = load64_le(b);
- HIGH64_OF(r) = load64_le(b + 8);
-}
-
-void store128_le_(uint8_t *b, uint128_t *n) {
- store64_le(b, LOW64_OF(n));
- store64_le(b + 8, HIGH64_OF(n));
-}
-
-void load128_be_(uint8_t *b, uint128_t *r) {
- HIGH64_OF(r) = load64_be(b);
- LOW64_OF(r) = load64_be(b + 8);
-}
-
-void store128_be_(uint8_t *b, uint128_t *n) {
- store64_be(b, HIGH64_OF(n));
- store64_be(b + 8, LOW64_OF(n));
-}
-
-void
-FStar_Int_Cast_Full_uint64_to_uint128_(uint64_t x, uint128_t *dst) {
- /* C89 */
- LOW64_OF(dst) = x;
- HIGH64_OF(dst) = 0;
-}
-
-uint64_t FStar_Int_Cast_Full_uint128_to_uint64_(uint128_t *x) {
- return LOW64_OF(x);
-}
-
-# ifndef KRML_NOSTRUCT_PASSING
-
-uint128_t load128_le(uint8_t *b) {
- uint128_t r;
- load128_le_(b, &r);
- return r;
-}
-
-void store128_le(uint8_t *b, uint128_t n) {
- store128_le_(b, &n);
-}
-
-uint128_t load128_be(uint8_t *b) {
- uint128_t r;
- load128_be_(b, &r);
- return r;
-}
-
-void store128_be(uint8_t *b, uint128_t n) {
- store128_be_(b, &n);
-}
-
-uint128_t FStar_Int_Cast_Full_uint64_to_uint128(uint64_t x) {
- uint128_t dst;
- FStar_Int_Cast_Full_uint64_to_uint128_(x, &dst);
- return dst;
-}
-
-uint64_t FStar_Int_Cast_Full_uint128_to_uint64(uint128_t x) {
- return FStar_Int_Cast_Full_uint128_to_uint64_(&x);
-}
-
-# else /* !defined(KRML_STRUCT_PASSING) */
-
-# define print128 print128_
-# define load128_le load128_le_
-# define store128_le store128_le_
-# define load128_be load128_be_
-# define store128_be store128_be_
-# define FStar_Int_Cast_Full_uint128_to_uint64 \
- FStar_Int_Cast_Full_uint128_to_uint64_
-# define FStar_Int_Cast_Full_uint64_to_uint128 \
- FStar_Int_Cast_Full_uint64_to_uint128_
-
-# endif /* KRML_STRUCT_PASSING */
-
-#endif
diff --git a/library/Makefile b/library/Makefile
index 30663ea..ee9ca38 100644
--- a/library/Makefile
+++ b/library/Makefile
@@ -108,7 +108,6 @@
../3rdparty/everest/library/everest.o \
../3rdparty/everest/library/Hacl_Curve25519.o \
../3rdparty/everest/library/x25519.o \
- ../3rdparty/everest/library/kremlib/fstar_uint128.o \
../3rdparty/everest/library/kremlib/FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.o
.SILENT:
diff --git a/visualc/VS2010/mbedTLS.vcxproj b/visualc/VS2010/mbedTLS.vcxproj
index fade3d1..2206bb1 100644
--- a/visualc/VS2010/mbedTLS.vcxproj
+++ b/visualc/VS2010/mbedTLS.vcxproj
@@ -302,7 +302,6 @@
<ClCompile Include="..\..\library\xtea.c" />
<ClCompile Include="..\..\3rdparty\everest\library\everest.c" />
<ClCompile Include="..\..\3rdparty\everest\library\x25519.c" />
- <ClCompile Include="..\..\3rdparty\everest\library\kremlib\fstar_uint128.c" />
<ClCompile Include="..\..\3rdparty\everest\library\kremlib\FStar_UInt128_extracted.c" />
<ClCompile Include="..\..\3rdparty\everest\library\kremlib\FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.c" />
<ClCompile Include="..\..\3rdparty\everest\library\vs2010\Hacl_Curve25519.c" />