Externals: Update mbedtls to 2.28.0

2026-06-19 01:16:48 -07:00 · 2022-04-02 19:30:22 -04:00
parent c9896e1c4b
commit d8a5a8827e
256 changed files with 67342 additions and 15594 deletions
@@ -10,7 +10,7 @@ set(MBEDTLS_LIBRARIES ${MBEDTLS_LIBRARY} ${MBEDX509_LIBRARY} ${MBEDCRYPTO_LIBRAR
 set(CMAKE_REQUIRED_INCLUDES ${MBEDTLS_INCLUDE_DIRS})
 check_cxx_source_compiles("
 	#include <mbedtls/version.h>
-	#if MBEDTLS_VERSION_NUMBER < 0x02040000
+	#if MBEDTLS_VERSION_NUMBER < 0x021C0000
 	#error \"Your mbed TLS version is too old.\"
 	#endif
 	int main() {}"
@@ -0,0 +1 @@
+/Makefile
@@ -0,0 +1,17 @@
+list (APPEND thirdparty_src)
+list (APPEND thirdparty_lib)
+list (APPEND thirdparty_inc_public)
+list (APPEND thirdparty_inc)
+list (APPEND thirdparty_def)
+
+execute_process(COMMAND ${MBEDTLS_PYTHON_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/config.py -f ${CMAKE_CURRENT_SOURCE_DIR}/../include/mbedtls/config.h get MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED RESULT_VARIABLE result)
+
+if(${result} EQUAL 0)
+    add_subdirectory(everest)
+endif()
+
+set(thirdparty_src ${thirdparty_src} PARENT_SCOPE)
+set(thirdparty_lib ${thirdparty_lib} PARENT_SCOPE)
+set(thirdparty_inc_public ${thirdparty_inc_public} PARENT_SCOPE)
+set(thirdparty_inc ${thirdparty_inc} PARENT_SCOPE)
+set(thirdparty_def ${thirdparty_def} PARENT_SCOPE)
@@ -0,0 +1,2 @@
+THIRDPARTY_DIR = $(dir $(lastword $(MAKEFILE_LIST)))
+include $(THIRDPARTY_DIR)/everest/Makefile.inc
@@ -0,0 +1,2 @@
+*.o
+Makefile
@@ -0,0 +1,28 @@
+list (APPEND everest_src)
+list (APPEND everest_inc_public)
+list (APPEND everest_inc)
+list (APPEND everest_def)
+
+set(everest_src
+  ${CMAKE_CURRENT_SOURCE_DIR}/library/everest.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/library/x25519.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/library/Hacl_Curve25519_joined.c
+)
+
+list(APPEND everest_inc_public ${CMAKE_CURRENT_SOURCE_DIR}/include)
+list(APPEND everest_inc ${CMAKE_CURRENT_SOURCE_DIR}/include/everest ${CMAKE_CURRENT_SOURCE_DIR}/include/everest/kremlib)
+
+if(INSTALL_MBEDTLS_HEADERS)
+
+  install(DIRECTORY include/everest
+    DESTINATION include
+    FILE_PERMISSIONS OWNER_READ OWNER_WRITE GROUP_READ WORLD_READ
+    DIRECTORY_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE
+    FILES_MATCHING PATTERN "*.h")
+
+endif(INSTALL_MBEDTLS_HEADERS)
+
+set(thirdparty_src ${thirdparty_src} ${everest_src} PARENT_SCOPE)
+set(thirdparty_inc_public ${thirdparty_inc_public} ${everest_inc_public} PARENT_SCOPE)
+set(thirdparty_inc ${thirdparty_inc} ${everest_inc} PARENT_SCOPE)
+set(thirdparty_def ${thirdparty_def} ${everest_def} PARENT_SCOPE)
@@ -0,0 +1,6 @@
+THIRDPARTY_INCLUDES+=-I../3rdparty/everest/include -I../3rdparty/everest/include/everest -I../3rdparty/everest/include/everest/kremlib
+
+THIRDPARTY_CRYPTO_OBJECTS+= \
+	../3rdparty/everest/library/everest.o \
+	../3rdparty/everest/library/x25519.o \
+	../3rdparty/everest/library/Hacl_Curve25519_joined.o
@@ -0,0 +1,5 @@
+The files in this directory stem from [Project Everest](https://project-everest.github.io/) and are distributed under the Apache 2.0 license.
+
+This is a formally verified implementation of Curve25519-based handshakes. The C code is automatically derived from the (verified) [original implementation](https://github.com/project-everest/hacl-star/tree/master/code/curve25519) in the [F* language](https://github.com/fstarlang/fstar) by [KreMLin](https://github.com/fstarlang/kremlin). In addition to the improved safety and security of the implementation, it is also significantly faster than the default implementation of Curve25519 in mbedTLS.
+
+The caveat is that not all platforms are supported, although the version in `everest/library/legacy` should work on most systems. The main issue is that some platforms do not provide a 128-bit integer type and KreMLin therefore has to use additional (also verified) code to simulate them, resulting in less of a performance gain overall. Explictly supported platforms are currently `x86` and `x86_64` using gcc or clang, and Visual C (2010 and later).
@@ -0,0 +1,21 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+/* This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
+ * KreMLin invocation: /mnt/e/everest/verify/kremlin/krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrcLh -minimal -fbuiltin-uint128 -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrcLh -minimal -I /mnt/e/everest/verify/hacl-star/code/lib/kremlin -I /mnt/e/everest/verify/kremlin/kremlib/compat -I /mnt/e/everest/verify/hacl-star/specs -I /mnt/e/everest/verify/hacl-star/specs/old -I . -ccopt -march=native -verbose -ldopt -flto -tmpdir x25519-c -I ../bignum -bundle Hacl.Curve25519=* -minimal -add-include "kremlib.h" -skip-compilation x25519-c/out.krml -o x25519-c/Hacl_Curve25519.c
+ * F* version: 059db0c8
+ * KreMLin version: 916c37ac
+ */
+
+
+
+#ifndef __Hacl_Curve25519_H
+#define __Hacl_Curve25519_H
+
+
+#include "kremlib.h"
+
+void Hacl_Curve25519_crypto_scalarmult(uint8_t *mypublic, uint8_t *secret, uint8_t *basepoint);
+
+#define __Hacl_Curve25519_H_DEFINED
+#endif
@@ -0,0 +1,234 @@
+/*
+ *  Interface to code from Project Everest
+ *
+ *  Copyright 2016-2018 INRIA and Microsoft Corporation
+ *  SPDX-License-Identifier: Apache-2.0
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License"); you may
+ *  not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+ *  WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *  This file is part of Mbed TLS (https://tls.mbed.org).
+ */
+
+#ifndef MBEDTLS_EVEREST_H
+#define MBEDTLS_EVEREST_H
+
+#include "everest/x25519.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/**
+ * Defines the source of the imported EC key.
+ */
+typedef enum
+{
+    MBEDTLS_EVEREST_ECDH_OURS,   /**< Our key. */
+    MBEDTLS_EVEREST_ECDH_THEIRS, /**< The key of the peer. */
+} mbedtls_everest_ecdh_side;
+
+typedef struct {
+    mbedtls_x25519_context ctx;
+} mbedtls_ecdh_context_everest;
+
+
+/**
+ * \brief           This function sets up the ECDH context with the information
+ *                  given.
+ *
+ *                  This function should be called after mbedtls_ecdh_init() but
+ *                  before mbedtls_ecdh_make_params(). There is no need to call
+ *                  this function before mbedtls_ecdh_read_params().
+ *
+ *                  This is the first function used by a TLS server for ECDHE
+ *                  ciphersuites.
+ *
+ * \param ctx       The ECDH context to set up.
+ * \param grp_id    The group id of the group to set up the context for.
+ *
+ * \return          \c 0 on success.
+ */
+int mbedtls_everest_setup( mbedtls_ecdh_context_everest *ctx, int grp_id );
+
+/**
+ * \brief           This function frees a context.
+ *
+ * \param ctx       The context to free.
+ */
+void mbedtls_everest_free( mbedtls_ecdh_context_everest *ctx );
+
+/**
+ * \brief           This function generates a public key and a TLS
+ *                  ServerKeyExchange payload.
+ *
+ *                  This is the second function used by a TLS server for ECDHE
+ *                  ciphersuites. (It is called after mbedtls_ecdh_setup().)
+ *
+ * \note            This function assumes that the ECP group (grp) of the
+ *                  \p ctx context has already been properly set,
+ *                  for example, using mbedtls_ecp_group_load().
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param olen      The number of characters written.
+ * \param buf       The destination buffer.
+ * \param blen      The length of the destination buffer.
+ * \param f_rng     The RNG function.
+ * \param p_rng     The RNG context.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ */
+int mbedtls_everest_make_params( mbedtls_ecdh_context_everest *ctx, size_t *olen,
+                                 unsigned char *buf, size_t blen,
+                                 int( *f_rng )( void *, unsigned char *, size_t ),
+                                 void *p_rng );
+
+/**
+ * \brief           This function parses and processes a TLS ServerKeyExhange
+ *                  payload.
+ *
+ *                  This is the first function used by a TLS client for ECDHE
+ *                  ciphersuites.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param buf       The pointer to the start of the input buffer.
+ * \param end       The address for one Byte past the end of the buffer.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ *
+ */
+int mbedtls_everest_read_params( mbedtls_ecdh_context_everest *ctx,
+                                 const unsigned char **buf, const unsigned char *end );
+
+/**
+ * \brief           This function parses and processes a TLS ServerKeyExhange
+ *                  payload.
+ *
+ *                  This is the first function used by a TLS client for ECDHE
+ *                  ciphersuites.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param buf       The pointer to the start of the input buffer.
+ * \param end       The address for one Byte past the end of the buffer.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ *
+ */
+int mbedtls_everest_read_params( mbedtls_ecdh_context_everest *ctx,
+                                 const unsigned char **buf, const unsigned char *end );
+
+/**
+ * \brief           This function sets up an ECDH context from an EC key.
+ *
+ *                  It is used by clients and servers in place of the
+ *                  ServerKeyEchange for static ECDH, and imports ECDH
+ *                  parameters from the EC key information of a certificate.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context to set up.
+ * \param key       The EC key to use.
+ * \param side      Defines the source of the key: 1: Our key, or
+ *                  0: The key of the peer.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ *
+ */
+int mbedtls_everest_get_params( mbedtls_ecdh_context_everest *ctx, const mbedtls_ecp_keypair *key,
+                                mbedtls_everest_ecdh_side side );
+
+/**
+ * \brief           This function generates a public key and a TLS
+ *                  ClientKeyExchange payload.
+ *
+ *                  This is the second function used by a TLS client for ECDH(E)
+ *                  ciphersuites.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param olen      The number of Bytes written.
+ * \param buf       The destination buffer.
+ * \param blen      The size of the destination buffer.
+ * \param f_rng     The RNG function.
+ * \param p_rng     The RNG context.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ */
+int mbedtls_everest_make_public( mbedtls_ecdh_context_everest *ctx, size_t *olen,
+                                 unsigned char *buf, size_t blen,
+                                 int( *f_rng )( void *, unsigned char *, size_t ),
+                                 void *p_rng );
+
+/**
+ * \brief       This function parses and processes a TLS ClientKeyExchange
+ *              payload.
+ *
+ *              This is the third function used by a TLS server for ECDH(E)
+ *              ciphersuites. (It is called after mbedtls_ecdh_setup() and
+ *              mbedtls_ecdh_make_params().)
+ *
+ * \see         ecp.h
+ *
+ * \param ctx   The ECDH context.
+ * \param buf   The start of the input buffer.
+ * \param blen  The length of the input buffer.
+ *
+ * \return      \c 0 on success.
+ * \return      An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ */
+int mbedtls_everest_read_public( mbedtls_ecdh_context_everest *ctx,
+                                 const unsigned char *buf, size_t blen );
+
+/**
+ * \brief           This function derives and exports the shared secret.
+ *
+ *                  This is the last function used by both TLS client
+ *                  and servers.
+ *
+ * \note            If \p f_rng is not NULL, it is used to implement
+ *                  countermeasures against side-channel attacks.
+ *                  For more information, see mbedtls_ecp_mul().
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The ECDH context.
+ * \param olen      The number of Bytes written.
+ * \param buf       The destination buffer.
+ * \param blen      The length of the destination buffer.
+ * \param f_rng     The RNG function.
+ * \param p_rng     The RNG context.
+ *
+ * \return          \c 0 on success.
+ * \return          An \c MBEDTLS_ERR_ECP_XXX error code on failure.
+ */
+int mbedtls_everest_calc_secret( mbedtls_ecdh_context_everest *ctx, size_t *olen,
+                                 unsigned char *buf, size_t blen,
+                                 int( *f_rng )( void *, unsigned char *, size_t ),
+                                 void *p_rng );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* MBEDTLS_EVEREST_H */
@@ -0,0 +1,29 @@
+/*
+ *  Copyright 2016-2018 INRIA and Microsoft Corporation
+ *
+ *  SPDX-License-Identifier: Apache-2.0
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License"); you may
+ *  not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *  http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+ *  WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ *
+ *  This file is part of Mbed TLS (https://tls.mbed.org) and
+ *  originated from Project Everest (https://project-everest.github.io/)
+ */
+
+#ifndef __KREMLIB_H
+#define __KREMLIB_H
+
+#include "kremlin/internal/target.h"
+#include "kremlin/internal/types.h"
+#include "kremlin/c_endianness.h"
+
+#endif     /* __KREMLIB_H */
@@ -0,0 +1,204 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KREMLIN_ENDIAN_H
+#define __KREMLIN_ENDIAN_H
+
+#include <string.h>
+#include <inttypes.h>
+
+/******************************************************************************/
+/* Implementing C.fst (part 2: endian-ness macros)                            */
+/******************************************************************************/
+
+/* ... for Linux */
+#if defined(__linux__) || defined(__CYGWIN__)
+#  include <endian.h>
+
+/* ... for OSX */
+#elif defined(__APPLE__)
+#  include <libkern/OSByteOrder.h>
+#  define htole64(x) OSSwapHostToLittleInt64(x)
+#  define le64toh(x) OSSwapLittleToHostInt64(x)
+#  define htobe64(x) OSSwapHostToBigInt64(x)
+#  define be64toh(x) OSSwapBigToHostInt64(x)
+
+#  define htole16(x) OSSwapHostToLittleInt16(x)
+#  define le16toh(x) OSSwapLittleToHostInt16(x)
+#  define htobe16(x) OSSwapHostToBigInt16(x)
+#  define be16toh(x) OSSwapBigToHostInt16(x)
+
+#  define htole32(x) OSSwapHostToLittleInt32(x)
+#  define le32toh(x) OSSwapLittleToHostInt32(x)
+#  define htobe32(x) OSSwapHostToBigInt32(x)
+#  define be32toh(x) OSSwapBigToHostInt32(x)
+
+/* ... for Solaris */
+#elif defined(__sun__)
+#  include <sys/byteorder.h>
+#  define htole64(x) LE_64(x)
+#  define le64toh(x) LE_64(x)
+#  define htobe64(x) BE_64(x)
+#  define be64toh(x) BE_64(x)
+
+#  define htole16(x) LE_16(x)
+#  define le16toh(x) LE_16(x)
+#  define htobe16(x) BE_16(x)
+#  define be16toh(x) BE_16(x)
+
+#  define htole32(x) LE_32(x)
+#  define le32toh(x) LE_32(x)
+#  define htobe32(x) BE_32(x)
+#  define be32toh(x) BE_32(x)
+
+/* ... for the BSDs */
+#elif defined(__FreeBSD__) || defined(__NetBSD__) || defined(__DragonFly__)
+#  include <sys/endian.h>
+#elif defined(__OpenBSD__)
+#  include <endian.h>
+
+/* ... for Windows (MSVC)... not targeting XBOX 360! */
+#elif defined(_MSC_VER)
+
+#  include <stdlib.h>
+#  define htobe16(x) _byteswap_ushort(x)
+#  define htole16(x) (x)
+#  define be16toh(x) _byteswap_ushort(x)
+#  define le16toh(x) (x)
+
+#  define htobe32(x) _byteswap_ulong(x)
+#  define htole32(x) (x)
+#  define be32toh(x) _byteswap_ulong(x)
+#  define le32toh(x) (x)
+
+#  define htobe64(x) _byteswap_uint64(x)
+#  define htole64(x) (x)
+#  define be64toh(x) _byteswap_uint64(x)
+#  define le64toh(x) (x)
+
+/* ... for Windows (GCC-like, e.g. mingw or clang) */
+#elif (defined(_WIN32) || defined(_WIN64)) &&                                  \
+    (defined(__GNUC__) || defined(__clang__))
+
+#  define htobe16(x) __builtin_bswap16(x)
+#  define htole16(x) (x)
+#  define be16toh(x) __builtin_bswap16(x)
+#  define le16toh(x) (x)
+
+#  define htobe32(x) __builtin_bswap32(x)
+#  define htole32(x) (x)
+#  define be32toh(x) __builtin_bswap32(x)
+#  define le32toh(x) (x)
+
+#  define htobe64(x) __builtin_bswap64(x)
+#  define htole64(x) (x)
+#  define be64toh(x) __builtin_bswap64(x)
+#  define le64toh(x) (x)
+
+/* ... generic big-endian fallback code */
+#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
+
+/* byte swapping code inspired by:
+ * https://github.com/rweather/arduinolibs/blob/master/libraries/Crypto/utility/EndianUtil.h
+ * */
+
+#  define htobe32(x) (x)
+#  define be32toh(x) (x)
+#  define htole32(x)                                                           \
+    (__extension__({                                                           \
+      uint32_t _temp = (x);                                                    \
+      ((_temp >> 24) & 0x000000FF) | ((_temp >> 8) & 0x0000FF00) |             \
+          ((_temp << 8) & 0x00FF0000) | ((_temp << 24) & 0xFF000000);          \
+    }))
+#  define le32toh(x) (htole32((x)))
+
+#  define htobe64(x) (x)
+#  define be64toh(x) (x)
+#  define htole64(x)                                                           \
+    (__extension__({                                                           \
+      uint64_t __temp = (x);                                                   \
+      uint32_t __low = htobe32((uint32_t)__temp);                              \
+      uint32_t __high = htobe32((uint32_t)(__temp >> 32));                     \
+      (((uint64_t)__low) << 32) | __high;                                      \
+    }))
+#  define le64toh(x) (htole64((x)))
+
+/* ... generic little-endian fallback code */
+#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+
+#  define htole32(x) (x)
+#  define le32toh(x) (x)
+#  define htobe32(x)                                                           \
+    (__extension__({                                                           \
+      uint32_t _temp = (x);                                                    \
+      ((_temp >> 24) & 0x000000FF) | ((_temp >> 8) & 0x0000FF00) |             \
+          ((_temp << 8) & 0x00FF0000) | ((_temp << 24) & 0xFF000000);          \
+    }))
+#  define be32toh(x) (htobe32((x)))
+
+#  define htole64(x) (x)
+#  define le64toh(x) (x)
+#  define htobe64(x)                                                           \
+    (__extension__({                                                           \
+      uint64_t __temp = (x);                                                   \
+      uint32_t __low = htobe32((uint32_t)__temp);                              \
+      uint32_t __high = htobe32((uint32_t)(__temp >> 32));                     \
+      (((uint64_t)__low) << 32) | __high;                                      \
+    }))
+#  define be64toh(x) (htobe64((x)))
+
+/* ... couldn't determine endian-ness of the target platform */
+#else
+#  error "Please define __BYTE_ORDER__!"
+
+#endif /* defined(__linux__) || ... */
+
+/* Loads and stores. These avoid undefined behavior due to unaligned memory
+ * accesses, via memcpy. */
+
+inline static uint16_t load16(uint8_t *b) {
+  uint16_t x;
+  memcpy(&x, b, 2);
+  return x;
+}
+
+inline static uint32_t load32(uint8_t *b) {
+  uint32_t x;
+  memcpy(&x, b, 4);
+  return x;
+}
+
+inline static uint64_t load64(uint8_t *b) {
+  uint64_t x;
+  memcpy(&x, b, 8);
+  return x;
+}
+
+inline static void store16(uint8_t *b, uint16_t i) {
+  memcpy(b, &i, 2);
+}
+
+inline static void store32(uint8_t *b, uint32_t i) {
+  memcpy(b, &i, 4);
+}
+
+inline static void store64(uint8_t *b, uint64_t i) {
+  memcpy(b, &i, 8);
+}
+
+#define load16_le(b) (le16toh(load16(b)))
+#define store16_le(b, i) (store16(b, htole16(i)))
+#define load16_be(b) (be16toh(load16(b)))
+#define store16_be(b, i) (store16(b, htobe16(i)))
+
+#define load32_le(b) (le32toh(load32(b)))
+#define store32_le(b, i) (store32(b, htole32(i)))
+#define load32_be(b) (be32toh(load32(b)))
+#define store32_be(b, i) (store32(b, htobe32(i)))
+
+#define load64_le(b) (le64toh(load64(b)))
+#define store64_le(b, i) (store64(b, htole64(i)))
+#define load64_be(b) (be64toh(load64(b)))
+#define store64_be(b, i) (store64(b, htobe64(i)))
+
+#endif
@@ -0,0 +1,16 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KREMLIN_BUILTIN_H
+#define __KREMLIN_BUILTIN_H
+
+/* For alloca, when using KreMLin's -falloca */
+#if (defined(_WIN32) || defined(_WIN64))
+#  include <malloc.h>
+#endif
+
+/* If some globals need to be initialized before the main, then kremlin will
+ * generate and try to link last a function with this type: */
+void kremlinit_globals(void);
+
+#endif
@@ -0,0 +1,46 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KREMLIN_CALLCONV_H
+#define __KREMLIN_CALLCONV_H
+
+/******************************************************************************/
+/* Some macros to ease compatibility                                          */
+/******************************************************************************/
+
+/* We want to generate __cdecl safely without worrying about it being undefined.
+ * When using MSVC, these are always defined. When using MinGW, these are
+ * defined too. They have no meaning for other platforms, so we define them to
+ * be empty macros in other situations. */
+#ifndef _MSC_VER
+#ifndef __cdecl
+#define __cdecl
+#endif
+#ifndef __stdcall
+#define __stdcall
+#endif
+#ifndef __fastcall
+#define __fastcall
+#endif
+#endif
+
+/* Since KreMLin emits the inline keyword unconditionally, we follow the
+ * guidelines at https://gcc.gnu.org/onlinedocs/gcc/Inline.html and make this
+ * __inline__ to ensure the code compiles with -std=c90 and earlier. */
+#ifdef __GNUC__
+#  define inline __inline__
+#endif
+
+/* GCC-specific attribute syntax; everyone else gets the standard C inline
+ * attribute. */
+#ifdef __GNU_C__
+#  ifndef __clang__
+#    define force_inline inline __attribute__((always_inline))
+#  else
+#    define force_inline inline
+#  endif
+#else
+#  define force_inline inline
+#endif
+
+#endif
@@ -0,0 +1,34 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef KRML_COMPAT_H
+#define KRML_COMPAT_H
+
+#include <inttypes.h>
+
+/* A series of macros that define C implementations of types that are not Low*,
+ * to facilitate porting programs to Low*. */
+
+typedef const char *Prims_string;
+
+typedef struct {
+  uint32_t length;
+  const char *data;
+} FStar_Bytes_bytes;
+
+typedef int32_t Prims_pos, Prims_nat, Prims_nonzero, Prims_int,
+    krml_checked_int_t;
+
+#define RETURN_OR(x)                                                           \
+  do {                                                                         \
+    int64_t __ret = x;                                                         \
+    if (__ret < INT32_MIN || INT32_MAX < __ret) {                              \
+      KRML_HOST_PRINTF(                                                        \
+          "Prims.{int,nat,pos} integer overflow at %s:%d\n", __FILE__,         \
+          __LINE__);                                                           \
+      KRML_HOST_EXIT(252);                                                     \
+    }                                                                          \
+    return (int32_t)__ret;                                                     \
+  } while (0)
+
+#endif
@@ -0,0 +1,57 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KREMLIN_DEBUG_H
+#define __KREMLIN_DEBUG_H
+
+#include <inttypes.h>
+
+#include "kremlin/internal/target.h"
+
+/******************************************************************************/
+/* Debugging helpers - intended only for KreMLin developers                   */
+/******************************************************************************/
+
+/* In support of "-wasm -d force-c": we might need this function to be
+ * forward-declared, because the dependency on WasmSupport appears very late,
+ * after SimplifyWasm, and sadly, after the topological order has been done. */
+void WasmSupport_check_buffer_size(uint32_t s);
+
+/* A series of GCC atrocities to trace function calls (kremlin's [-d c-calls]
+ * option). Useful when trying to debug, say, Wasm, to compare traces. */
+/* clang-format off */
+#ifdef __GNUC__
+#define KRML_FORMAT(X) _Generic((X),                                           \
+  uint8_t : "0x%08" PRIx8,                                                     \
+  uint16_t: "0x%08" PRIx16,                                                    \
+  uint32_t: "0x%08" PRIx32,                                                    \
+  uint64_t: "0x%08" PRIx64,                                                    \
+  int8_t  : "0x%08" PRIx8,                                                     \
+  int16_t : "0x%08" PRIx16,                                                    \
+  int32_t : "0x%08" PRIx32,                                                    \
+  int64_t : "0x%08" PRIx64,                                                    \
+  default : "%s")
+
+#define KRML_FORMAT_ARG(X) _Generic((X),                                       \
+  uint8_t : X,                                                                 \
+  uint16_t: X,                                                                 \
+  uint32_t: X,                                                                 \
+  uint64_t: X,                                                                 \
+  int8_t  : X,                                                                 \
+  int16_t : X,                                                                 \
+  int32_t : X,                                                                 \
+  int64_t : X,                                                                 \
+  default : "unknown")
+/* clang-format on */
+
+#  define KRML_DEBUG_RETURN(X)                                                 \
+    ({                                                                         \
+      __auto_type _ret = (X);                                                  \
+      KRML_HOST_PRINTF("returning: ");                                         \
+      KRML_HOST_PRINTF(KRML_FORMAT(_ret), KRML_FORMAT_ARG(_ret));              \
+      KRML_HOST_PRINTF(" \n");                                                 \
+      _ret;                                                                    \
+    })
+#endif
+
+#endif
@@ -0,0 +1,102 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KREMLIN_TARGET_H
+#define __KREMLIN_TARGET_H
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <stdbool.h>
+#include <inttypes.h>
+#include <limits.h>
+
+#include "kremlin/internal/callconv.h"
+
+/******************************************************************************/
+/* Macros that KreMLin will generate.                                         */
+/******************************************************************************/
+
+/* For "bare" targets that do not have a C stdlib, the user might want to use
+ * [-add-early-include '"mydefinitions.h"'] and override these. */
+#ifndef KRML_HOST_PRINTF
+#  define KRML_HOST_PRINTF printf
+#endif
+
+#if (                                                                          \
+    (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) &&             \
+    (!(defined KRML_HOST_EPRINTF)))
+#  define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
+#endif
+
+#ifndef KRML_HOST_EXIT
+#  define KRML_HOST_EXIT exit
+#endif
+
+#ifndef KRML_HOST_MALLOC
+#  define KRML_HOST_MALLOC malloc
+#endif
+
+#ifndef KRML_HOST_CALLOC
+#  define KRML_HOST_CALLOC calloc
+#endif
+
+#ifndef KRML_HOST_FREE
+#  define KRML_HOST_FREE free
+#endif
+
+#ifndef KRML_HOST_TIME
+
+#  include <time.h>
+
+/* Prims_nat not yet in scope */
+inline static int32_t krml_time() {
+  return (int32_t)time(NULL);
+}
+
+#  define KRML_HOST_TIME krml_time
+#endif
+
+/* In statement position, exiting is easy. */
+#define KRML_EXIT                                                              \
+  do {                                                                         \
+    KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \
+    KRML_HOST_EXIT(254);                                                       \
+  } while (0)
+
+/* In expression position, use the comma-operator and a malloc to return an
+ * expression of the right size. KreMLin passes t as the parameter to the macro.
+ */
+#define KRML_EABORT(t, msg)                                                    \
+  (KRML_HOST_PRINTF("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, msg),  \
+   KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t))))
+
+/* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
+ * *elements*. Do an ugly, run-time check (some of which KreMLin can eliminate).
+ */
+
+#ifdef __GNUC__
+#  define _KRML_CHECK_SIZE_PRAGMA                                              \
+    _Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
+#else
+#  define _KRML_CHECK_SIZE_PRAGMA
+#endif
+
+#define KRML_CHECK_SIZE(size_elt, sz)                                          \
+  do {                                                                         \
+    _KRML_CHECK_SIZE_PRAGMA                                                    \
+    if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) {                  \
+      KRML_HOST_PRINTF(                                                        \
+          "Maximum allocatable size exceeded, aborting before overflow at "    \
+          "%s:%d\n",                                                           \
+          __FILE__, __LINE__);                                                 \
+      KRML_HOST_EXIT(253);                                                     \
+    }                                                                          \
+  } while (0)
+
+#if defined(_MSC_VER) && _MSC_VER < 1900
+#  define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
+#else
+#  define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
+#endif
+
+#endif
@@ -0,0 +1,61 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef KRML_TYPES_H
+#define KRML_TYPES_H
+
+#include <inttypes.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+/* Types which are either abstract, meaning that have to be implemented in C, or
+ * which are models, meaning that they are swapped out at compile-time for
+ * hand-written C types (in which case they're marked as noextract). */
+
+typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_;
+typedef int64_t FStar_Int64_t, FStar_Int64_t_;
+typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_;
+typedef int32_t FStar_Int32_t, FStar_Int32_t_;
+typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_;
+typedef int16_t FStar_Int16_t, FStar_Int16_t_;
+typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_;
+typedef int8_t FStar_Int8_t, FStar_Int8_t_;
+
+/* Only useful when building Kremlib, because it's in the dependency graph of
+ * FStar.Int.Cast. */
+typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_;
+typedef int64_t FStar_Int63_t, FStar_Int63_t_;
+
+typedef double FStar_Float_float;
+typedef uint32_t FStar_Char_char;
+typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write;
+
+typedef void *FStar_Dyn_dyn;
+
+typedef const char *C_String_t, *C_String_t_;
+
+typedef int exit_code;
+typedef FILE *channel;
+
+typedef unsigned long long TestLib_cycles;
+
+typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan;
+
+/* The uint128 type is a special case since we offer several implementations of
+ * it, depending on the compiler and whether the user wants the verified
+ * implementation or not. */
+#if !defined(KRML_VERIFIED_UINT128) && defined(_MSC_VER) && defined(_M_X64)
+#  include <emmintrin.h>
+typedef __m128i FStar_UInt128_uint128;
+#elif !defined(KRML_VERIFIED_UINT128) && !defined(_MSC_VER)
+typedef unsigned __int128 FStar_UInt128_uint128;
+#else
+typedef struct FStar_UInt128_uint128_s {
+  uint64_t low;
+  uint64_t high;
+} FStar_UInt128_uint128;
+#endif
+
+typedef FStar_UInt128_uint128 FStar_UInt128_t, FStar_UInt128_t_, uint128_t;
+
+#endif
--- a/Show More
+++ b/Show More