!64 #I5OMGR:解决冲突升级版本1010

Merge pull request !64 from liyufan/master

.gitee/ISSUE_TEMPLATE.zh-CN.md

-### 该问题是怎么引起的？
-
-
-
-### 重现步骤
-
-
-
-### 报错信息
-    
-    

.gitee/PULL_REQUEST_TEMPLATE.zh-CN.md

-### 相关的Issue
-
-  
-### 原因（目的、解决的问题等）
-
-
-### 描述（做了什么，变更了什么）
-
-
-### 测试用例（新增、改动、可能影响的功能）
-    
-    

.github/ISSUE_TEMPLATE/bug_report.md

+---
+name: Bug report
+about: To report a bug, please fill this form.
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+### Summary
+
+
+
+### System information
+
+Mbed TLS version (number or commit id): 
+Operating system and version: 
+Configuration (if not default, please attach `mbedtls_config.h`): 
+Compiler and options (if you used a pre-built binary, please indicate how you obtained it): 
+Additional environment information: 
+
+### Expected behavior
+
+
+
+### Actual behavior
+
+
+
+### Steps to reproduce
+
+
+
+### Additional information
+

.github/ISSUE_TEMPLATE/config.yml

+blank_issues_enabled: false
+contact_links:
+    - name: Mbed TLS security team
+      url: mailto:mbed-tls-security@lists.trustedfirmware.org
+      about: Report a security vulnerability.
+    - name: Mbed TLS mailing list
+      url: https://lists.trustedfirmware.org/mailman/listinfo/mbed-tls
+      about: Mbed TLS community support and general discussion.

.github/ISSUE_TEMPLATE/feature_request.md

+---
+name: Enhancement request
+about: To request an enhancement, please fill this form.
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+### Suggested enhancement
+
+
+
+### Justification
+
+Mbed TLS needs this because 
+

.github/issue_template.md

-Note: This is just a template, so feel free to use/remove the unnecessary things
-
-### Description
-- Type: Bug | Enhancement\Feature Request | Question
-- Priority: Blocker | Major | Minor
-
----------------------------------------------------------------
-## Bug
-
-**OS**  
-Mbed OS|linux|windows|
-
-**mbed TLS build:**  
-Version: x.x.x or git commit id  
-OS version: x.x.x  
-Configuration: please attach config.h file where possible  
-Compiler and options (if you used a pre-built binary, please indicate how you obtained it):  
-Additional environment information:  
-
-**Peer device TLS stack and version**  
-OpenSSL|GnuTls|Chrome|NSS(Firefox)|SecureChannel (IIS/Internet Explorer/Edge)|Other  
-Version:  
-
-**Expected behavior**   
-
-**Actual behavior**  
-
-**Steps to reproduce**  
-
-----------------------------------------------------------------
-## Enhancement\Feature Request
-
-**Justification - why does the library need this feature?**  
-
-**Suggested enhancement**  
-
------------------------------------------------------------------
-
-## Question
-
-**Please first check for answers in the [Mbed TLS knowledge Base](https://tls.mbed.org/kb), and preferably file an issue in the [Mbed TLS support forum](https://forums.mbed.com/c/mbed-tls)**  

.gitignore

@@ -18,6 +18,7 @@ Testing
 Coverage
 *.gcno
 *.gcda
+coverage-summary.txt
 
 # generated by scripts/memory.sh
 massif-*
@@ -31,9 +32,18 @@ massif-*
 # Python build artifacts:
 *.pyc
 
+# CMake generates *.dir/ folders for in-tree builds (used by MSVC projects), ignore all of those:
+*.dir/
+
+# Microsoft CMake extension for Visual Studio Code generates a build directory by default
+/build/
+
 # Generated documentation:
 /apidoc
 
+# PSA Crypto compliance test repo, cloned by test_psa_compliance.py
+/psa-arch-tests
+
 # Editor navigation files:
 /GPATH
 /GRTAGS

.mypy.ini

+[mypy]
+mypy_path = scripts
+namespace_packages = True
+warn_unused_configs = True

.pylintrc

+[MASTER]
+init-hook='import sys; sys.path.append("scripts")'
+
 [BASIC]
 # We're ok with short funtion argument names.
 # [invalid-name]
@@ -12,9 +15,9 @@ bad-functions=input
 # [missing-docstring]
 docstring-min-length=10
 
-# Allow longer methods than the default.
+# No upper limit on method names. Pylint <2.1.0 has an upper limit of 30.
 # [invalid-name]
-method-rgx=[a-z_][a-z0-9_]{2,35}$
+method-rgx=[a-z_][a-z0-9_]{2,}$
 
 # Allow module names containing a dash (but no underscore or uppercase letter).
 # They are whole programs, not meant to be included by another module.
@@ -23,7 +26,7 @@ module-rgx=(([a-z_][a-z0-9_]*)|([A-Z][a-zA-Z0-9]+)|[a-z][-0-9a-z]+)$
 
 # Some functions don't need docstrings.
 # [missing-docstring]
-no-docstring-rgx=(run_)main$
+no-docstring-rgx=(run_)?main$
 
 # We're ok with short local or global variable names.
 # [invalid-name]

.travis.yml

-language: c
-compiler: gcc
+# Declare python as our language. This way we get our chosen Python version,
+# and pip is available. Gcc and clang are available anyway.
+language: python
+python: 3.5
 sudo: false
 cache: ccache
 
@@ -14,27 +16,36 @@ jobs:
           - graphviz
           - gcc-arm-none-eabi
           - libnewlib-arm-none-eabi
-      language: python # Needed to get pip for Python 3
-      python: 3.5 # version from Ubuntu 16.04
-      install:
-        - pip install pylint==2.4.4
+          - gcc-arm-linux-gnueabi
+          - libc6-dev-armel-cross
       script:
         - tests/scripts/all.sh -k 'check_*'
         - tests/scripts/all.sh -k test_default_out_of_box
-        - tests/scripts/test-ref-configs.pl
-        - tests/scripts/all.sh -k build_arm_none_eabi_gcc_arm5vte build_arm_none_eabi_gcc_m0plus
+        - tests/scripts/all.sh -k test_ref_configs
+        - tests/scripts/all.sh -k build_arm_linux_gnueabi_gcc_arm5vte build_arm_none_eabi_gcc_m0plus
 
     - name: full configuration
       script:
         - tests/scripts/all.sh -k test_full_cmake_gcc_asan
 
-    - name: check compilation guards
-      script:
-        - tests/scripts/all.sh -k 'test_depends_*' 'build_key_exchanges'
-
     - name: Windows
       os: windows
+      # The language 'python' is currently unsupported on the
+      # Windows Build Environment. And 'generic' causes the job to get stuck
+      # on "Booting virtual machine".
+      language: c
+      before_install:
+        - choco install python --version=3.5.4
+      env:
+        # Add the directory where the Choco packages go
+        - PATH=/c/Python35:/c/Python35/Scripts:$PATH
+        - PYTHON=python.exe
       script:
+        - type perl; perl --version
+        - type python; python --version
+        - scripts/make_generated_files.bat
+        # Logs appear out of sequence on Windows. Give time to catch up.
+        - sleep 5
         - scripts/windows_msbuild.bat v141 # Visual Studio 2017
 
 after_failure:
@@ -45,6 +56,9 @@ env:
     - SEED=1
     - secure: "FrI5d2s+ckckC17T66c8jm2jV6i2DkBPU5nyWzwbedjmEBeocREfQLd/x8yKpPzLDz7ghOvr+/GQvsPPn0dVkGlNzm3Q+hGHc/ujnASuUtGrcuMM+0ALnJ3k4rFr9xEvjJeWb4SmhJO5UCAZYvTItW4k7+bj9L+R6lt3TzQbXzg="
 
+install:
+  - $PYTHON scripts/min_requirements.py
+
 addons:
   apt:
     packages:

3rdparty/.gitignore

+/Makefile

3rdparty/CMakeLists.txt

+execute_process(COMMAND ${MBEDTLS_PYTHON_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/config.py -f ${CMAKE_CURRENT_SOURCE_DIR}/../include/mbedtls/mbedtls_config.h get MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED RESULT_VARIABLE result)
+
+if(${result} EQUAL 0)
+    add_subdirectory(everest)
+endif()

3rdparty/Makefile.inc

+THIRDPARTY_DIR = $(dir $(lastword $(MAKEFILE_LIST)))
+include $(THIRDPARTY_DIR)/everest/Makefile.inc

3rdparty/everest/.gitignore

+*.o
+Makefile

3rdparty/everest/CMakeLists.txt

+add_library(everest
+  library/everest.c
+  library/x25519.c
+  library/Hacl_Curve25519_joined.c)
+
+target_include_directories(everest
+  PUBLIC $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>
+         $<BUILD_INTERFACE:${MBEDTLS_DIR}/include>
+         $<INSTALL_INTERFACE:include>
+  PRIVATE include/everest
+          include/everest/kremlib
+          ${MBEDTLS_DIR}/library/)
+
+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)
+
+install(TARGETS everest
+  EXPORT MbedTLSTargets
+  DESTINATION ${LIB_INSTALL_DIR}
+  PERMISSIONS OWNER_READ OWNER_WRITE GROUP_READ WORLD_READ)

3rdparty/everest/Makefile.inc

+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

3rdparty/everest/README.md

+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).

3rdparty/everest/include/everest/Hacl_Curve25519.h

+/* 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

3rdparty/everest/include/everest/everest.h

+/*
+ *  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 */

3rdparty/everest/include/everest/kremlib.h

+/*
+ *  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 */

3rdparty/everest/include/everest/kremlib/FStar_UInt128.h

+/* 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: ../krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrB9w -minimal -fparentheses -fcurly-braces -fno-shadow -header copyright-header.txt -minimal -tmpdir dist/uint128 -skip-compilation -extract-uints -add-include <inttypes.h> -add-include <stdbool.h> -add-include "kremlin/internal/types.h" -bundle FStar.UInt128=* extracted/prims.krml extracted/FStar_Pervasives_Native.krml extracted/FStar_Pervasives.krml extracted/FStar_Mul.krml extracted/FStar_Squash.krml extracted/FStar_Classical.krml extracted/FStar_StrongExcludedMiddle.krml extracted/FStar_FunctionalExtensionality.krml extracted/FStar_List_Tot_Base.krml extracted/FStar_List_Tot_Properties.krml extracted/FStar_List_Tot.krml extracted/FStar_Seq_Base.krml extracted/FStar_Seq_Properties.krml extracted/FStar_Seq.krml extracted/FStar_Math_Lib.krml extracted/FStar_Math_Lemmas.krml extracted/FStar_BitVector.krml extracted/FStar_UInt.krml extracted/FStar_UInt32.krml extracted/FStar_Int.krml extracted/FStar_Int16.krml extracted/FStar_Preorder.krml extracted/FStar_Ghost.krml extracted/FStar_ErasedLogic.krml extracted/FStar_UInt64.krml extracted/FStar_Set.krml extracted/FStar_PropositionalExtensionality.krml extracted/FStar_PredicateExtensionality.krml extracted/FStar_TSet.krml extracted/FStar_Monotonic_Heap.krml extracted/FStar_Heap.krml extracted/FStar_Map.krml extracted/FStar_Monotonic_HyperHeap.krml extracted/FStar_Monotonic_HyperStack.krml extracted/FStar_HyperStack.krml extracted/FStar_Monotonic_Witnessed.krml extracted/FStar_HyperStack_ST.krml extracted/FStar_HyperStack_All.krml extracted/FStar_Date.krml extracted/FStar_Universe.krml extracted/FStar_GSet.krml extracted/FStar_ModifiesGen.krml extracted/LowStar_Monotonic_Buffer.krml extracted/LowStar_Buffer.krml extracted/Spec_Loops.krml extracted/LowStar_BufferOps.krml extracted/C_Loops.krml extracted/FStar_UInt8.krml extracted/FStar_Kremlin_Endianness.krml extracted/FStar_UInt63.krml extracted/FStar_Exn.krml extracted/FStar_ST.krml extracted/FStar_All.krml extracted/FStar_Dyn.krml extracted/FStar_Int63.krml extracted/FStar_Int64.krml extracted/FStar_Int32.krml extracted/FStar_Int8.krml extracted/FStar_UInt16.krml extracted/FStar_Int_Cast.krml extracted/FStar_UInt128.krml extracted/C_Endianness.krml extracted/FStar_List.krml extracted/FStar_Float.krml extracted/FStar_IO.krml extracted/C.krml extracted/FStar_Char.krml extracted/FStar_String.krml extracted/LowStar_Modifies.krml extracted/C_String.krml extracted/FStar_Bytes.krml extracted/FStar_HyperStack_IO.krml extracted/C_Failure.krml extracted/TestLib.krml extracted/FStar_Int_Cast_Full.krml
+ * F* version: 059db0c8
+ * KreMLin version: 916c37ac
+ */
+
+
+
+#ifndef __FStar_UInt128_H
+#define __FStar_UInt128_H
+
+
+#include <inttypes.h>
+#include <stdbool.h>
+#include "kremlin/internal/types.h"
+
+uint64_t FStar_UInt128___proj__Mkuint128__item__low(FStar_UInt128_uint128 projectee);
+
+uint64_t FStar_UInt128___proj__Mkuint128__item__high(FStar_UInt128_uint128 projectee);
+
+typedef FStar_UInt128_uint128 FStar_UInt128_t;
+
+FStar_UInt128_uint128 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128
+FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128
+FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a);
+
+FStar_UInt128_uint128 FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s);
+
+FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s);
+
+bool FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+bool FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+bool FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+bool FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+bool FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a);
+
+uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Plus_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Plus_Question_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Plus_Percent_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Subtraction_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Subtraction_Question_Hat)(
+  FStar_UInt128_uint128 x0,
+  FStar_UInt128_uint128 x1
+);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Subtraction_Percent_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Amp_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Hat_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Bar_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Less_Less_Hat)(FStar_UInt128_uint128 x0, uint32_t x1);
+
+extern FStar_UInt128_uint128
+(*FStar_UInt128_op_Greater_Greater_Hat)(FStar_UInt128_uint128 x0, uint32_t x1);
+
+extern bool (*FStar_UInt128_op_Equals_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern bool
+(*FStar_UInt128_op_Greater_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern bool (*FStar_UInt128_op_Less_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern bool
+(*FStar_UInt128_op_Greater_Equals_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+extern bool
+(*FStar_UInt128_op_Less_Equals_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
+
+FStar_UInt128_uint128 FStar_UInt128_mul32(uint64_t x, uint32_t y);
+
+FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x, uint64_t y);
+
+#define __FStar_UInt128_H_DEFINED
+#endif

3rdparty/everest/include/everest/kremlib/FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.h

+/* 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: ../krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrB9w -minimal -fparentheses -fcurly-braces -fno-shadow -header copyright-header.txt -minimal -tmpdir dist/minimal -skip-compilation -extract-uints -add-include <inttypes.h> -add-include <stdbool.h> -add-include "kremlin/internal/compat.h" -add-include "kremlin/internal/types.h" -bundle FStar.UInt64+FStar.UInt32+FStar.UInt16+FStar.UInt8=* extracted/prims.krml extracted/FStar_Pervasives_Native.krml extracted/FStar_Pervasives.krml extracted/FStar_Mul.krml extracted/FStar_Squash.krml extracted/FStar_Classical.krml extracted/FStar_StrongExcludedMiddle.krml extracted/FStar_FunctionalExtensionality.krml extracted/FStar_List_Tot_Base.krml extracted/FStar_List_Tot_Properties.krml extracted/FStar_List_Tot.krml extracted/FStar_Seq_Base.krml extracted/FStar_Seq_Properties.krml extracted/FStar_Seq.krml extracted/FStar_Math_Lib.krml extracted/FStar_Math_Lemmas.krml extracted/FStar_BitVector.krml extracted/FStar_UInt.krml extracted/FStar_UInt32.krml extracted/FStar_Int.krml extracted/FStar_Int16.krml extracted/FStar_Preorder.krml extracted/FStar_Ghost.krml extracted/FStar_ErasedLogic.krml extracted/FStar_UInt64.krml extracted/FStar_Set.krml extracted/FStar_PropositionalExtensionality.krml extracted/FStar_PredicateExtensionality.krml extracted/FStar_TSet.krml extracted/FStar_Monotonic_Heap.krml extracted/FStar_Heap.krml extracted/FStar_Map.krml extracted/FStar_Monotonic_HyperHeap.krml extracted/FStar_Monotonic_HyperStack.krml extracted/FStar_HyperStack.krml extracted/FStar_Monotonic_Witnessed.krml extracted/FStar_HyperStack_ST.krml extracted/FStar_HyperStack_All.krml extracted/FStar_Date.krml extracted/FStar_Universe.krml extracted/FStar_GSet.krml extracted/FStar_ModifiesGen.krml extracted/LowStar_Monotonic_Buffer.krml extracted/LowStar_Buffer.krml extracted/Spec_Loops.krml extracted/LowStar_BufferOps.krml extracted/C_Loops.krml extracted/FStar_UInt8.krml extracted/FStar_Kremlin_Endianness.krml extracted/FStar_UInt63.krml extracted/FStar_Exn.krml extracted/FStar_ST.krml extracted/FStar_All.krml extracted/FStar_Dyn.krml extracted/FStar_Int63.krml extracted/FStar_Int64.krml extracted/FStar_Int32.krml extracted/FStar_Int8.krml extracted/FStar_UInt16.krml extracted/FStar_Int_Cast.krml extracted/FStar_UInt128.krml extracted/C_Endianness.krml extracted/FStar_List.krml extracted/FStar_Float.krml extracted/FStar_IO.krml extracted/C.krml extracted/FStar_Char.krml extracted/FStar_String.krml extracted/LowStar_Modifies.krml extracted/C_String.krml extracted/FStar_Bytes.krml extracted/FStar_HyperStack_IO.krml extracted/C_Failure.krml extracted/TestLib.krml extracted/FStar_Int_Cast_Full.krml
+ * F* version: 059db0c8
+ * KreMLin version: 916c37ac
+ */
+
+
+
+#ifndef __FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8_H
+#define __FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8_H
+
+
+#include <inttypes.h>
+#include <stdbool.h>
+#include "kremlin/internal/compat.h"
+#include "kremlin/internal/types.h"
+
+extern Prims_int FStar_UInt64_n;
+
+extern Prims_int FStar_UInt64_v(uint64_t x0);
+
+extern uint64_t FStar_UInt64_uint_to_t(Prims_int x0);
+
+extern uint64_t FStar_UInt64_add(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_add_underspec(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_add_mod(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_sub(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_sub_underspec(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_sub_mod(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_mul(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_mul_underspec(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_mul_mod(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_mul_div(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_div(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_rem(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_logand(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_logxor(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_logor(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_lognot(uint64_t x0);
+
+extern uint64_t FStar_UInt64_shift_right(uint64_t x0, uint32_t x1);
+
+extern uint64_t FStar_UInt64_shift_left(uint64_t x0, uint32_t x1);
+
+extern bool FStar_UInt64_eq(uint64_t x0, uint64_t x1);
+
+extern bool FStar_UInt64_gt(uint64_t x0, uint64_t x1);
+
+extern bool FStar_UInt64_gte(uint64_t x0, uint64_t x1);
+
+extern bool FStar_UInt64_lt(uint64_t x0, uint64_t x1);
+
+extern bool FStar_UInt64_lte(uint64_t x0, uint64_t x1);
+
+extern uint64_t FStar_UInt64_minus(uint64_t x0);
+
+extern uint32_t FStar_UInt64_n_minus_one;
+
+uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b);
+
+uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b);
+
+extern Prims_string FStar_UInt64_to_string(uint64_t x0);
+
+extern uint64_t FStar_UInt64_of_string(Prims_string x0);
+
+extern Prims_int FStar_UInt32_n;
+
+extern Prims_int FStar_UInt32_v(uint32_t x0);
+
+extern uint32_t FStar_UInt32_uint_to_t(Prims_int x0);
+
+extern uint32_t FStar_UInt32_add(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_add_underspec(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_add_mod(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_sub(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_sub_underspec(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_sub_mod(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_mul(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_mul_underspec(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_mul_mod(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_mul_div(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_div(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_rem(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_logand(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_logxor(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_logor(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_lognot(uint32_t x0);
+
+extern uint32_t FStar_UInt32_shift_right(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_shift_left(uint32_t x0, uint32_t x1);
+
+extern bool FStar_UInt32_eq(uint32_t x0, uint32_t x1);
+
+extern bool FStar_UInt32_gt(uint32_t x0, uint32_t x1);
+
+extern bool FStar_UInt32_gte(uint32_t x0, uint32_t x1);
+
+extern bool FStar_UInt32_lt(uint32_t x0, uint32_t x1);
+
+extern bool FStar_UInt32_lte(uint32_t x0, uint32_t x1);
+
+extern uint32_t FStar_UInt32_minus(uint32_t x0);
+
+extern uint32_t FStar_UInt32_n_minus_one;
+
+uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b);
+
+uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b);
+
+extern Prims_string FStar_UInt32_to_string(uint32_t x0);
+
+extern uint32_t FStar_UInt32_of_string(Prims_string x0);
+
+extern Prims_int FStar_UInt16_n;
+
+extern Prims_int FStar_UInt16_v(uint16_t x0);
+
+extern uint16_t FStar_UInt16_uint_to_t(Prims_int x0);
+
+extern uint16_t FStar_UInt16_add(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_add_underspec(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_add_mod(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_sub(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_sub_underspec(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_sub_mod(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_mul(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_mul_underspec(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_mul_mod(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_mul_div(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_div(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_rem(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_logand(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_logxor(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_logor(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_lognot(uint16_t x0);
+
+extern uint16_t FStar_UInt16_shift_right(uint16_t x0, uint32_t x1);
+
+extern uint16_t FStar_UInt16_shift_left(uint16_t x0, uint32_t x1);
+
+extern bool FStar_UInt16_eq(uint16_t x0, uint16_t x1);
+
+extern bool FStar_UInt16_gt(uint16_t x0, uint16_t x1);
+
+extern bool FStar_UInt16_gte(uint16_t x0, uint16_t x1);
+
+extern bool FStar_UInt16_lt(uint16_t x0, uint16_t x1);
+
+extern bool FStar_UInt16_lte(uint16_t x0, uint16_t x1);
+
+extern uint16_t FStar_UInt16_minus(uint16_t x0);
+
+extern uint32_t FStar_UInt16_n_minus_one;
+
+uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b);
+
+uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b);
+
+extern Prims_string FStar_UInt16_to_string(uint16_t x0);
+
+extern uint16_t FStar_UInt16_of_string(Prims_string x0);
+
+extern Prims_int FStar_UInt8_n;
+
+extern Prims_int FStar_UInt8_v(uint8_t x0);
+
+extern uint8_t FStar_UInt8_uint_to_t(Prims_int x0);
+
+extern uint8_t FStar_UInt8_add(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_add_underspec(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_add_mod(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_sub(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_sub_underspec(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_sub_mod(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_mul(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_mul_underspec(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_mul_mod(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_mul_div(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_div(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_rem(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_logand(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_logxor(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_logor(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_lognot(uint8_t x0);
+
+extern uint8_t FStar_UInt8_shift_right(uint8_t x0, uint32_t x1);
+
+extern uint8_t FStar_UInt8_shift_left(uint8_t x0, uint32_t x1);
+
+extern bool FStar_UInt8_eq(uint8_t x0, uint8_t x1);
+
+extern bool FStar_UInt8_gt(uint8_t x0, uint8_t x1);
+
+extern bool FStar_UInt8_gte(uint8_t x0, uint8_t x1);
+
+extern bool FStar_UInt8_lt(uint8_t x0, uint8_t x1);
+
+extern bool FStar_UInt8_lte(uint8_t x0, uint8_t x1);
+
+extern uint8_t FStar_UInt8_minus(uint8_t x0);
+
+extern uint32_t FStar_UInt8_n_minus_one;
+
+uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b);
+
+uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b);
+
+extern Prims_string FStar_UInt8_to_string(uint8_t x0);
+
+extern uint8_t FStar_UInt8_of_string(Prims_string x0);
+
+typedef uint8_t FStar_UInt8_byte;
+
+#define __FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8_H_DEFINED
+#endif

3rdparty/everest/include/everest/vs2010/Hacl_Curve25519.h

+/* 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 -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

3rdparty/everest/include/everest/vs2010/inttypes.h

+/*
+ *  Custom inttypes.h for VS2010 KreMLin requires these definitions,
+ *  but VS2010 doesn't provide them.
+ *
+ *  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 _INTTYPES_H_VS2010
+#define _INTTYPES_H_VS2010
+
+#include <stdint.h>
+
+#ifdef _MSC_VER
+#define inline __inline
+#endif
+
+/* VS2010 unsigned long == 8 bytes */
+
+#define PRIu64 "I64u"
+
+#endif

3rdparty/everest/include/everest/vs2010/stdbool.h

+/*
+ *  Custom stdbool.h for VS2010 KreMLin requires these definitions,
+ *  but VS2010 doesn't provide them.
+ *
+ *  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 _STDBOOL_H_VS2010
+#define _STDBOOL_H_VS2010
+
+typedef int bool;
+
+static bool true = 1;
+static bool false = 0;
+
+#endif

3rdparty/everest/include/everest/x25519.h

+/*
+ *  ECDH with curve-optimized implementation multiplexing
+ *
+ *  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_X25519_H
+#define MBEDTLS_X25519_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#define MBEDTLS_ECP_TLS_CURVE25519 0x1d
+#define MBEDTLS_X25519_KEY_SIZE_BYTES 32
+
+/**
+ * Defines the source of the imported EC key.
+ */
+typedef enum
+{
+    MBEDTLS_X25519_ECDH_OURS,   /**< Our key. */
+    MBEDTLS_X25519_ECDH_THEIRS, /**< The key of the peer. */
+} mbedtls_x25519_ecdh_side;
+
+/**
+ * \brief           The x25519 context structure.
+ */
+typedef struct
+{
+  unsigned char our_secret[MBEDTLS_X25519_KEY_SIZE_BYTES];
+  unsigned char peer_point[MBEDTLS_X25519_KEY_SIZE_BYTES];
+} mbedtls_x25519_context;
+
+/**
+ * \brief           This function initializes an x25519 context.
+ *
+ * \param ctx       The x25519 context to initialize.
+ */
+void mbedtls_x25519_init( mbedtls_x25519_context *ctx );
+
+/**
+ * \brief           This function frees a context.
+ *
+ * \param ctx       The context to free.
+ */
+void mbedtls_x25519_free( mbedtls_x25519_context *ctx );
+
+/**
+ * \brief           This function generates a public key and a TLS
+ *                  ServerKeyExchange payload.
+ *
+ *                  This is the first function used by a TLS server for x25519.
+ *
+ *
+ * \param ctx       The x25519 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_x25519_make_params( mbedtls_x25519_context *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 ServerKeyExchange
+ *                  payload.
+ *
+ *
+ * \param ctx       The x25519 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_x25519_read_params( mbedtls_x25519_context *ctx,
+                        const unsigned char **buf, const unsigned char *end );
+
+/**
+ * \brief           This function sets up an x25519 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 x25519 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_x25519_get_params( mbedtls_x25519_context *ctx, const mbedtls_ecp_keypair *key,
+                               mbedtls_x25519_ecdh_side side );
+
+/**
+ * \brief           This function derives and exports the shared secret.
+ *
+ *                  This is the last function used by both TLS client
+ *                  and servers.
+ *
+ *
+ * \param ctx       The x25519 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_x25519_calc_secret( mbedtls_x25519_context *ctx, size_t *olen,
+                        unsigned char *buf, size_t blen,
+                        int( *f_rng )(void *, unsigned char *, size_t),
+                        void *p_rng );
+
+/**
+ * \brief           This function generates a public key and a TLS
+ *                  ClientKeyExchange payload.
+ *
+ *                  This is the second function used by a TLS client for x25519.
+ *
+ * \see             ecp.h
+ *
+ * \param ctx       The x25519 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_x25519_make_public( mbedtls_x25519_context *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 second function used by a TLS server for x25519.
+ *
+ * \see         ecp.h
+ *
+ * \param ctx   The x25519 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_x25519_read_public( mbedtls_x25519_context *ctx,
+                        const unsigned char *buf, size_t blen );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* x25519.h */

3rdparty/everest/library/Hacl_Curve25519_joined.c

+/*
+ *  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)
+ */
+
+#include "common.h"
+
+#if defined(MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED)
+
+#if defined(__SIZEOF_INT128__) && (__SIZEOF_INT128__ == 16)
+#define MBEDTLS_HAVE_INT128
+#endif
+
+#if defined(MBEDTLS_HAVE_INT128)
+#include "Hacl_Curve25519.c"
+#else
+#define KRML_VERIFIED_UINT128
+#include "kremlib/FStar_UInt128_extracted.c"
+#include "legacy/Hacl_Curve25519.c"
+#endif
+
+#include "kremlib/FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.c"
+
+#endif /* defined(MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED) */
+

3rdparty/everest/library/everest.c

+/*
+ *  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).
+ */
+
+#include "common.h"
+
+#include <string.h>
+
+#include "mbedtls/ecdh.h"
+
+#include "everest/x25519.h"
+#include "everest/everest.h"
+
+#if defined(MBEDTLS_PLATFORM_C)
+#include "mbedtls/platform.h"
+#else
+#define mbedtls_calloc calloc
+#define mbedtls_free   free
+#endif
+
+#if defined(MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED)
+
+int mbedtls_everest_setup( mbedtls_ecdh_context_everest *ctx, int grp_id )
+{
+    if( grp_id != MBEDTLS_ECP_DP_CURVE25519 )
+        return MBEDTLS_ERR_ECP_BAD_INPUT_DATA;
+    mbedtls_x25519_init( &ctx->ctx );
+    return 0;
+}
+
+void mbedtls_everest_free( mbedtls_ecdh_context_everest *ctx )
+{
+    mbedtls_x25519_free( &ctx->ctx );
+}
+
+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 )
+{
+    mbedtls_x25519_context *x25519_ctx = &ctx->ctx;
+    return mbedtls_x25519_make_params( x25519_ctx, olen, buf, blen, f_rng, p_rng );
+}
+
+int mbedtls_everest_read_params( mbedtls_ecdh_context_everest *ctx,
+                                 const unsigned char **buf,
+                                 const unsigned char *end )
+{
+    mbedtls_x25519_context *x25519_ctx = &ctx->ctx;
+    return mbedtls_x25519_read_params( x25519_ctx, buf, end );
+}
+
+int mbedtls_everest_get_params( mbedtls_ecdh_context_everest *ctx,
+                                const mbedtls_ecp_keypair *key,
+                                mbedtls_everest_ecdh_side side )
+{
+    mbedtls_x25519_context *x25519_ctx = &ctx->ctx;
+    mbedtls_x25519_ecdh_side s = side == MBEDTLS_EVEREST_ECDH_OURS ?
+                                            MBEDTLS_X25519_ECDH_OURS :
+                                            MBEDTLS_X25519_ECDH_THEIRS;
+    return mbedtls_x25519_get_params( x25519_ctx, key, s );
+}
+
+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 )
+{
+    mbedtls_x25519_context *x25519_ctx = &ctx->ctx;
+    return mbedtls_x25519_make_public( x25519_ctx, olen, buf, blen, f_rng, p_rng );
+}
+
+int mbedtls_everest_read_public( mbedtls_ecdh_context_everest *ctx,
+                                 const unsigned char *buf, size_t blen )
+{
+    mbedtls_x25519_context *x25519_ctx = &ctx->ctx;
+    return mbedtls_x25519_read_public ( x25519_ctx, buf, blen );
+}
+
+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 )
+{
+    mbedtls_x25519_context *x25519_ctx = &ctx->ctx;
+    return mbedtls_x25519_calc_secret( x25519_ctx, olen, buf, blen, f_rng, p_rng );
+}
+
+#endif /* MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED */
+

3rdparty/everest/library/kremlib/FStar_UInt128_extracted.c

+/* 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: ../krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrB9w -minimal -fparentheses -fcurly-braces -fno-shadow -header copyright-header.txt -minimal -tmpdir extracted -warn-error +9+11 -skip-compilation -extract-uints -add-include <inttypes.h> -add-include "kremlib.h" -add-include "kremlin/internal/compat.h" extracted/prims.krml extracted/FStar_Pervasives_Native.krml extracted/FStar_Pervasives.krml extracted/FStar_Mul.krml extracted/FStar_Squash.krml extracted/FStar_Classical.krml extracted/FStar_StrongExcludedMiddle.krml extracted/FStar_FunctionalExtensionality.krml extracted/FStar_List_Tot_Base.krml extracted/FStar_List_Tot_Properties.krml extracted/FStar_List_Tot.krml extracted/FStar_Seq_Base.krml extracted/FStar_Seq_Properties.krml extracted/FStar_Seq.krml extracted/FStar_Math_Lib.krml extracted/FStar_Math_Lemmas.krml extracted/FStar_BitVector.krml extracted/FStar_UInt.krml extracted/FStar_UInt32.krml extracted/FStar_Int.krml extracted/FStar_Int16.krml extracted/FStar_Preorder.krml extracted/FStar_Ghost.krml extracted/FStar_ErasedLogic.krml extracted/FStar_UInt64.krml extracted/FStar_Set.krml extracted/FStar_PropositionalExtensionality.krml extracted/FStar_PredicateExtensionality.krml extracted/FStar_TSet.krml extracted/FStar_Monotonic_Heap.krml extracted/FStar_Heap.krml extracted/FStar_Map.krml extracted/FStar_Monotonic_HyperHeap.krml extracted/FStar_Monotonic_HyperStack.krml extracted/FStar_HyperStack.krml extracted/FStar_Monotonic_Witnessed.krml extracted/FStar_HyperStack_ST.krml extracted/FStar_HyperStack_All.krml extracted/FStar_Date.krml extracted/FStar_Universe.krml extracted/FStar_GSet.krml extracted/FStar_ModifiesGen.krml extracted/LowStar_Monotonic_Buffer.krml extracted/LowStar_Buffer.krml extracted/Spec_Loops.krml extracted/LowStar_BufferOps.krml extracted/C_Loops.krml extracted/FStar_UInt8.krml extracted/FStar_Kremlin_Endianness.krml extracted/FStar_UInt63.krml extracted/FStar_Exn.krml extracted/FStar_ST.krml extracted/FStar_All.krml extracted/FStar_Dyn.krml extracted/FStar_Int63.krml extracted/FStar_Int64.krml extracted/FStar_Int32.krml extracted/FStar_Int8.krml extracted/FStar_UInt16.krml extracted/FStar_Int_Cast.krml extracted/FStar_UInt128.krml extracted/C_Endianness.krml extracted/FStar_List.krml extracted/FStar_Float.krml extracted/FStar_IO.krml extracted/C.krml extracted/FStar_Char.krml extracted/FStar_String.krml extracted/LowStar_Modifies.krml extracted/C_String.krml extracted/FStar_Bytes.krml extracted/FStar_HyperStack_IO.krml extracted/C_Failure.krml extracted/TestLib.krml extracted/FStar_Int_Cast_Full.krml
+ * F* version: 059db0c8
+ * KreMLin version: 916c37ac
+ */
+
+
+#include "FStar_UInt128.h"
+#include "kremlin/c_endianness.h"
+#include "FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.h"
+
+uint64_t FStar_UInt128___proj__Mkuint128__item__low(FStar_UInt128_uint128 projectee)
+{
+  return projectee.low;
+}
+
+uint64_t FStar_UInt128___proj__Mkuint128__item__high(FStar_UInt128_uint128 projectee)
+{
+  return projectee.high;
+}
+
+static uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)
+{
+  return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t)63U;
+}
+
+static uint64_t FStar_UInt128_carry(uint64_t a, uint64_t b)
+{
+  return FStar_UInt128_constant_time_carry(a, b);
+}
+
+FStar_UInt128_uint128 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128
+  flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };
+  return flat;
+}
+
+FStar_UInt128_uint128
+FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128
+  flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128
+  flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128
+  flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) };
+  return flat;
+}
+
+FStar_UInt128_uint128
+FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128
+  flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) };
+  return flat;
+}
+
+static FStar_UInt128_uint128
+FStar_UInt128_sub_mod_impl(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128
+  flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return FStar_UInt128_sub_mod_impl(a, b);
+}
+
+FStar_UInt128_uint128 FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 flat = { a.low & b.low, a.high & b.high };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 flat = { a.low ^ b.low, a.high ^ b.high };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 flat = { a.low | b.low, a.high | b.high };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a)
+{
+  FStar_UInt128_uint128 flat = { ~a.low, ~a.high };
+  return flat;
+}
+
+static uint32_t FStar_UInt128_u32_64 = (uint32_t)64U;
+
+static uint64_t FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s)
+{
+  return (hi << s) + (lo >> (FStar_UInt128_u32_64 - s));
+}
+
+static uint64_t FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s)
+{
+  return FStar_UInt128_add_u64_shift_left(hi, lo, s);
+}
+
+static FStar_UInt128_uint128
+FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s)
+{
+  if (s == (uint32_t)0U)
+  {
+    return a;
+  }
+  else
+  {
+    FStar_UInt128_uint128
+    flat = { a.low << s, FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s) };
+    return flat;
+  }
+}
+
+static FStar_UInt128_uint128
+FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s)
+{
+  FStar_UInt128_uint128 flat = { (uint64_t)0U, a.low << (s - FStar_UInt128_u32_64) };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s)
+{
+  if (s < FStar_UInt128_u32_64)
+  {
+    return FStar_UInt128_shift_left_small(a, s);
+  }
+  else
+  {
+    return FStar_UInt128_shift_left_large(a, s);
+  }
+}
+
+static uint64_t FStar_UInt128_add_u64_shift_right(uint64_t hi, uint64_t lo, uint32_t s)
+{
+  return (lo >> s) + (hi << (FStar_UInt128_u32_64 - s));
+}
+
+static uint64_t FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s)
+{
+  return FStar_UInt128_add_u64_shift_right(hi, lo, s);
+}
+
+static FStar_UInt128_uint128
+FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s)
+{
+  if (s == (uint32_t)0U)
+  {
+    return a;
+  }
+  else
+  {
+    FStar_UInt128_uint128
+    flat = { FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s), a.high >> s };
+    return flat;
+  }
+}
+
+static FStar_UInt128_uint128
+FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s)
+{
+  FStar_UInt128_uint128 flat = { a.high >> (s - FStar_UInt128_u32_64), (uint64_t)0U };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s)
+{
+  if (s < FStar_UInt128_u32_64)
+  {
+    return FStar_UInt128_shift_right_small(a, s);
+  }
+  else
+  {
+    return FStar_UInt128_shift_right_large(a, s);
+  }
+}
+
+bool FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.low == b.low && a.high == b.high;
+}
+
+bool FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.high > b.high || (a.high == b.high && a.low > b.low);
+}
+
+bool FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.high < b.high || (a.high == b.high && a.low < b.low);
+}
+
+bool FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.high > b.high || (a.high == b.high && a.low >= b.low);
+}
+
+bool FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.high < b.high || (a.high == b.high && a.low <= b.low);
+}
+
+FStar_UInt128_uint128 FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128
+  flat =
+    {
+      FStar_UInt64_eq_mask(a.low,
+        b.low)
+      & FStar_UInt64_eq_mask(a.high, b.high),
+      FStar_UInt64_eq_mask(a.low,
+        b.low)
+      & FStar_UInt64_eq_mask(a.high, b.high)
+    };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128
+  flat =
+    {
+      (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high))
+      | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low)),
+      (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high))
+      | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low))
+    };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a)
+{
+  FStar_UInt128_uint128 flat = { a, (uint64_t)0U };
+  return flat;
+}
+
+uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a)
+{
+  return a.low;
+}
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Plus_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_add;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Plus_Question_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_add_underspec;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Plus_Percent_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_add_mod;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Subtraction_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_sub;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Subtraction_Question_Hat)(
+  FStar_UInt128_uint128 x0,
+  FStar_UInt128_uint128 x1
+) = FStar_UInt128_sub_underspec;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Subtraction_Percent_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_sub_mod;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Amp_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_logand;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Hat_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_logxor;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Bar_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_logor;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Less_Less_Hat)(FStar_UInt128_uint128 x0, uint32_t x1) =
+  FStar_UInt128_shift_left;
+
+FStar_UInt128_uint128
+(*FStar_UInt128_op_Greater_Greater_Hat)(FStar_UInt128_uint128 x0, uint32_t x1) =
+  FStar_UInt128_shift_right;
+
+bool
+(*FStar_UInt128_op_Equals_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_eq;
+
+bool
+(*FStar_UInt128_op_Greater_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_gt;
+
+bool
+(*FStar_UInt128_op_Less_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_lt;
+
+bool
+(*FStar_UInt128_op_Greater_Equals_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_gte;
+
+bool
+(*FStar_UInt128_op_Less_Equals_Hat)(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1) =
+  FStar_UInt128_lte;
+
+static uint64_t FStar_UInt128_u64_mod_32(uint64_t a)
+{
+  return a & (uint64_t)0xffffffffU;
+}
+
+static uint32_t FStar_UInt128_u32_32 = (uint32_t)32U;
+
+static uint64_t FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo)
+{
+  return lo + (hi << FStar_UInt128_u32_32);
+}
+
+FStar_UInt128_uint128 FStar_UInt128_mul32(uint64_t x, uint32_t y)
+{
+  FStar_UInt128_uint128
+  flat =
+    {
+      FStar_UInt128_u32_combine((x >> FStar_UInt128_u32_32)
+        * (uint64_t)y
+        + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> FStar_UInt128_u32_32),
+        FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * (uint64_t)y)),
+      ((x >> FStar_UInt128_u32_32)
+      * (uint64_t)y
+      + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> FStar_UInt128_u32_32))
+      >> FStar_UInt128_u32_32
+    };
+  return flat;
+}
+
+typedef struct K___uint64_t_uint64_t_uint64_t_uint64_t_s
+{
+  uint64_t fst;
+  uint64_t snd;
+  uint64_t thd;
+  uint64_t f3;
+}
+K___uint64_t_uint64_t_uint64_t_uint64_t;
+
+static K___uint64_t_uint64_t_uint64_t_uint64_t
+FStar_UInt128_mul_wide_impl_t_(uint64_t x, uint64_t y)
+{
+  K___uint64_t_uint64_t_uint64_t_uint64_t
+  flat =
+    {
+      FStar_UInt128_u64_mod_32(x),
+      FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y)),
+      x
+      >> FStar_UInt128_u32_32,
+      (x >> FStar_UInt128_u32_32)
+      * FStar_UInt128_u64_mod_32(y)
+      + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32)
+    };
+  return flat;
+}
+
+static uint64_t FStar_UInt128_u32_combine_(uint64_t hi, uint64_t lo)
+{
+  return lo + (hi << FStar_UInt128_u32_32);
+}
+
+static FStar_UInt128_uint128 FStar_UInt128_mul_wide_impl(uint64_t x, uint64_t y)
+{
+  K___uint64_t_uint64_t_uint64_t_uint64_t scrut = FStar_UInt128_mul_wide_impl_t_(x, y);
+  uint64_t u1 = scrut.fst;
+  uint64_t w3 = scrut.snd;
+  uint64_t x_ = scrut.thd;
+  uint64_t t_ = scrut.f3;
+  FStar_UInt128_uint128
+  flat =
+    {
+      FStar_UInt128_u32_combine_(u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_),
+        w3),
+      x_
+      * (y >> FStar_UInt128_u32_32)
+      + (t_ >> FStar_UInt128_u32_32)
+      + ((u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_)) >> FStar_UInt128_u32_32)
+    };
+  return flat;
+}
+
+FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x, uint64_t y)
+{
+  return FStar_UInt128_mul_wide_impl(x, y);
+}
+

3rdparty/everest/library/kremlib/FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.c

+/* 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: ../krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrB9w -minimal -fparentheses -fcurly-braces -fno-shadow -header copyright-header.txt -minimal -tmpdir dist/minimal -skip-compilation -extract-uints -add-include <inttypes.h> -add-include <stdbool.h> -add-include "kremlin/internal/compat.h" -add-include "kremlin/internal/types.h" -bundle FStar.UInt64+FStar.UInt32+FStar.UInt16+FStar.UInt8=* extracted/prims.krml extracted/FStar_Pervasives_Native.krml extracted/FStar_Pervasives.krml extracted/FStar_Mul.krml extracted/FStar_Squash.krml extracted/FStar_Classical.krml extracted/FStar_StrongExcludedMiddle.krml extracted/FStar_FunctionalExtensionality.krml extracted/FStar_List_Tot_Base.krml extracted/FStar_List_Tot_Properties.krml extracted/FStar_List_Tot.krml extracted/FStar_Seq_Base.krml extracted/FStar_Seq_Properties.krml extracted/FStar_Seq.krml extracted/FStar_Math_Lib.krml extracted/FStar_Math_Lemmas.krml extracted/FStar_BitVector.krml extracted/FStar_UInt.krml extracted/FStar_UInt32.krml extracted/FStar_Int.krml extracted/FStar_Int16.krml extracted/FStar_Preorder.krml extracted/FStar_Ghost.krml extracted/FStar_ErasedLogic.krml extracted/FStar_UInt64.krml extracted/FStar_Set.krml extracted/FStar_PropositionalExtensionality.krml extracted/FStar_PredicateExtensionality.krml extracted/FStar_TSet.krml extracted/FStar_Monotonic_Heap.krml extracted/FStar_Heap.krml extracted/FStar_Map.krml extracted/FStar_Monotonic_HyperHeap.krml extracted/FStar_Monotonic_HyperStack.krml extracted/FStar_HyperStack.krml extracted/FStar_Monotonic_Witnessed.krml extracted/FStar_HyperStack_ST.krml extracted/FStar_HyperStack_All.krml extracted/FStar_Date.krml extracted/FStar_Universe.krml extracted/FStar_GSet.krml extracted/FStar_ModifiesGen.krml extracted/LowStar_Monotonic_Buffer.krml extracted/LowStar_Buffer.krml extracted/Spec_Loops.krml extracted/LowStar_BufferOps.krml extracted/C_Loops.krml extracted/FStar_UInt8.krml extracted/FStar_Kremlin_Endianness.krml extracted/FStar_UInt63.krml extracted/FStar_Exn.krml extracted/FStar_ST.krml extracted/FStar_All.krml extracted/FStar_Dyn.krml extracted/FStar_Int63.krml extracted/FStar_Int64.krml extracted/FStar_Int32.krml extracted/FStar_Int8.krml extracted/FStar_UInt16.krml extracted/FStar_Int_Cast.krml extracted/FStar_UInt128.krml extracted/C_Endianness.krml extracted/FStar_List.krml extracted/FStar_Float.krml extracted/FStar_IO.krml extracted/C.krml extracted/FStar_Char.krml extracted/FStar_String.krml extracted/LowStar_Modifies.krml extracted/C_String.krml extracted/FStar_Bytes.krml extracted/FStar_HyperStack_IO.krml extracted/C_Failure.krml extracted/TestLib.krml extracted/FStar_Int_Cast_Full.krml
+ * F* version: 059db0c8
+ * KreMLin version: 916c37ac
+ */
+
+
+#include "FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.h"
+
+uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
+{
+  uint64_t x = a ^ b;
+  uint64_t minus_x = ~x + (uint64_t)1U;
+  uint64_t x_or_minus_x = x | minus_x;
+  uint64_t xnx = x_or_minus_x >> (uint32_t)63U;
+  return xnx - (uint64_t)1U;
+}
+
+uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b)
+{
+  uint64_t x = a;
+  uint64_t y = b;
+  uint64_t x_xor_y = x ^ y;
+  uint64_t x_sub_y = x - y;
+  uint64_t x_sub_y_xor_y = x_sub_y ^ y;
+  uint64_t q = x_xor_y | x_sub_y_xor_y;
+  uint64_t x_xor_q = x ^ q;
+  uint64_t x_xor_q_ = x_xor_q >> (uint32_t)63U;
+  return x_xor_q_ - (uint64_t)1U;
+}
+
+uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b)
+{
+  uint32_t x = a ^ b;
+  uint32_t minus_x = ~x + (uint32_t)1U;
+  uint32_t x_or_minus_x = x | minus_x;
+  uint32_t xnx = x_or_minus_x >> (uint32_t)31U;
+  return xnx - (uint32_t)1U;
+}
+
+uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b)
+{
+  uint32_t x = a;
+  uint32_t y = b;
+  uint32_t x_xor_y = x ^ y;
+  uint32_t x_sub_y = x - y;
+  uint32_t x_sub_y_xor_y = x_sub_y ^ y;
+  uint32_t q = x_xor_y | x_sub_y_xor_y;
+  uint32_t x_xor_q = x ^ q;
+  uint32_t x_xor_q_ = x_xor_q >> (uint32_t)31U;
+  return x_xor_q_ - (uint32_t)1U;
+}
+
+uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b)
+{
+  uint16_t x = a ^ b;
+  uint16_t minus_x = ~x + (uint16_t)1U;
+  uint16_t x_or_minus_x = x | minus_x;
+  uint16_t xnx = x_or_minus_x >> (uint32_t)15U;
+  return xnx - (uint16_t)1U;
+}
+
+uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b)
+{
+  uint16_t x = a;
+  uint16_t y = b;
+  uint16_t x_xor_y = x ^ y;
+  uint16_t x_sub_y = x - y;
+  uint16_t x_sub_y_xor_y = x_sub_y ^ y;
+  uint16_t q = x_xor_y | x_sub_y_xor_y;
+  uint16_t x_xor_q = x ^ q;
+  uint16_t x_xor_q_ = x_xor_q >> (uint32_t)15U;
+  return x_xor_q_ - (uint16_t)1U;
+}
+
+uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b)
+{
+  uint8_t x = a ^ b;
+  uint8_t minus_x = ~x + (uint8_t)1U;
+  uint8_t x_or_minus_x = x | minus_x;
+  uint8_t xnx = x_or_minus_x >> (uint32_t)7U;
+  return xnx - (uint8_t)1U;
+}
+
+uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b)
+{
+  uint8_t x = a;
+  uint8_t y = b;
+  uint8_t x_xor_y = x ^ y;
+  uint8_t x_sub_y = x - y;
+  uint8_t x_sub_y_xor_y = x_sub_y ^ y;
+  uint8_t q = x_xor_y | x_sub_y_xor_y;
+  uint8_t x_xor_q = x ^ q;
+  uint8_t x_xor_q_ = x_xor_q >> (uint32_t)7U;
+  return x_xor_q_ - (uint8_t)1U;
+}
+

3rdparty/everest/library/x25519.c

+/*
+ *  ECDH with curve-optimized implementation multiplexing
+ *
+ *  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)
+ */
+
+#include "common.h"
+
+#if defined(MBEDTLS_ECDH_C) && defined(MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED)
+
+#include <mbedtls/ecdh.h>
+
+#if !(defined(__SIZEOF_INT128__) && (__SIZEOF_INT128__ == 16))
+#define KRML_VERIFIED_UINT128
+#endif
+
+#include <Hacl_Curve25519.h>
+#include <mbedtls/platform_util.h>
+
+#include "x25519.h"
+
+#include <string.h>
+
+/*
+ * Initialize context
+ */
+void mbedtls_x25519_init( mbedtls_x25519_context *ctx )
+{
+    mbedtls_platform_zeroize( ctx, sizeof( mbedtls_x25519_context ) );
+}
+
+/*
+ * Free context
+ */
+void mbedtls_x25519_free( mbedtls_x25519_context *ctx )
+{
+    if( ctx == NULL )
+        return;
+
+    mbedtls_platform_zeroize( ctx->our_secret, MBEDTLS_X25519_KEY_SIZE_BYTES );
+    mbedtls_platform_zeroize( ctx->peer_point, MBEDTLS_X25519_KEY_SIZE_BYTES );
+}
+
+int mbedtls_x25519_make_params( mbedtls_x25519_context *ctx, size_t *olen,
+                        unsigned char *buf, size_t blen,
+                        int( *f_rng )(void *, unsigned char *, size_t),
+                        void *p_rng )
+{
+    int ret = 0;
+
+    uint8_t base[MBEDTLS_X25519_KEY_SIZE_BYTES] = {0};
+
+    if( ( ret = f_rng( p_rng, ctx->our_secret, MBEDTLS_X25519_KEY_SIZE_BYTES ) ) != 0 )
+        return ret;
+
+    *olen = MBEDTLS_X25519_KEY_SIZE_BYTES + 4;
+    if( blen < *olen )
+        return( MBEDTLS_ERR_ECP_BUFFER_TOO_SMALL );
+
+    *buf++ = MBEDTLS_ECP_TLS_NAMED_CURVE;
+    *buf++ = MBEDTLS_ECP_TLS_CURVE25519 >> 8;
+    *buf++ = MBEDTLS_ECP_TLS_CURVE25519 & 0xFF;
+    *buf++ = MBEDTLS_X25519_KEY_SIZE_BYTES;
+
+    base[0] = 9;
+    Hacl_Curve25519_crypto_scalarmult( buf, ctx->our_secret, base );
+
+    base[0] = 0;
+    if( memcmp( buf, base, MBEDTLS_X25519_KEY_SIZE_BYTES) == 0 )
+        return MBEDTLS_ERR_ECP_RANDOM_FAILED;
+
+    return( 0 );
+}
+
+int mbedtls_x25519_read_params( mbedtls_x25519_context *ctx,
+                        const unsigned char **buf, const unsigned char *end )
+{
+    if( end - *buf < MBEDTLS_X25519_KEY_SIZE_BYTES + 1 )
+        return( MBEDTLS_ERR_ECP_BAD_INPUT_DATA );
+
+    if( ( *(*buf)++ != MBEDTLS_X25519_KEY_SIZE_BYTES ) )
+        return( MBEDTLS_ERR_ECP_BAD_INPUT_DATA );
+
+    memcpy( ctx->peer_point, *buf, MBEDTLS_X25519_KEY_SIZE_BYTES );
+    *buf += MBEDTLS_X25519_KEY_SIZE_BYTES;
+    return( 0 );
+}
+
+int mbedtls_x25519_get_params( mbedtls_x25519_context *ctx, const mbedtls_ecp_keypair *key,
+                               mbedtls_x25519_ecdh_side side )
+{
+    size_t olen = 0;
+
+    switch( side ) {
+    case MBEDTLS_X25519_ECDH_THEIRS:
+        return mbedtls_ecp_point_write_binary( &key->grp, &key->Q, MBEDTLS_ECP_PF_COMPRESSED, &olen, ctx->peer_point, MBEDTLS_X25519_KEY_SIZE_BYTES );
+    case MBEDTLS_X25519_ECDH_OURS:
+        return mbedtls_mpi_write_binary_le( &key->d, ctx->our_secret, MBEDTLS_X25519_KEY_SIZE_BYTES );
+    default:
+        return( MBEDTLS_ERR_ECP_BAD_INPUT_DATA );
+    }
+}
+
+int mbedtls_x25519_calc_secret( mbedtls_x25519_context *ctx, size_t *olen,
+                        unsigned char *buf, size_t blen,
+                        int( *f_rng )(void *, unsigned char *, size_t),
+                        void *p_rng )
+{
+    /* f_rng and p_rng are not used here because this implementation does not
+       need blinding since it has constant trace. */
+    (( void )f_rng);
+    (( void )p_rng);
+
+    *olen = MBEDTLS_X25519_KEY_SIZE_BYTES;
+
+    if( blen < *olen )
+        return( MBEDTLS_ERR_ECP_BUFFER_TOO_SMALL );
+
+    Hacl_Curve25519_crypto_scalarmult( buf, ctx->our_secret, ctx->peer_point);
+
+    /* Wipe the DH secret and don't let the peer chose a small subgroup point */
+    mbedtls_platform_zeroize( ctx->our_secret, MBEDTLS_X25519_KEY_SIZE_BYTES );
+
+    if( memcmp( buf, ctx->our_secret, MBEDTLS_X25519_KEY_SIZE_BYTES) == 0 )
+        return MBEDTLS_ERR_ECP_RANDOM_FAILED;
+
+    return( 0 );
+}
+
+int mbedtls_x25519_make_public( mbedtls_x25519_context *ctx, size_t *olen,
+                        unsigned char *buf, size_t blen,
+                        int( *f_rng )(void *, unsigned char *, size_t),
+                        void *p_rng )
+{
+    int ret = 0;
+    unsigned char base[MBEDTLS_X25519_KEY_SIZE_BYTES] = { 0 };
+
+    if( ctx == NULL )
+        return( MBEDTLS_ERR_ECP_BAD_INPUT_DATA );
+
+    if( ( ret = f_rng( p_rng, ctx->our_secret, MBEDTLS_X25519_KEY_SIZE_BYTES ) ) != 0 )
+        return ret;
+
+    *olen = MBEDTLS_X25519_KEY_SIZE_BYTES + 1;
+    if( blen < *olen )
+        return(MBEDTLS_ERR_ECP_BUFFER_TOO_SMALL);
+    *buf++ = MBEDTLS_X25519_KEY_SIZE_BYTES;
+
+    base[0] = 9;
+    Hacl_Curve25519_crypto_scalarmult( buf, ctx->our_secret, base );
+
+    base[0] = 0;
+    if( memcmp( buf, base, MBEDTLS_X25519_KEY_SIZE_BYTES ) == 0 )
+        return MBEDTLS_ERR_ECP_RANDOM_FAILED;
+
+    return( ret );
+}
+
+int mbedtls_x25519_read_public( mbedtls_x25519_context *ctx,
+                        const unsigned char *buf, size_t blen )
+{
+    if( blen < MBEDTLS_X25519_KEY_SIZE_BYTES + 1 )
+        return(MBEDTLS_ERR_ECP_BUFFER_TOO_SMALL);
+    if( (*buf++ != MBEDTLS_X25519_KEY_SIZE_BYTES) )
+        return(MBEDTLS_ERR_ECP_BAD_INPUT_DATA);
+    memcpy( ctx->peer_point, buf, MBEDTLS_X25519_KEY_SIZE_BYTES );
+    return( 0 );
+}
+
+
+#endif /* MBEDTLS_ECDH_C && MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED */

BRANCHES.md

+# Maintained branches
+
+At any point in time, we have a number of maintained branches consisting of:
+
+- The [`master`](https://github.com/ARMmbed/mbedtls/tree/master) branch:
+  this always contains the latest release, including all publicly available
+  security fixes.
+- The [`development`](https://github.com/ARMmbed/mbedtls/tree/development) branch:
+  this is where the current major version of Mbed TLS (version 3.x) is being
+  prepared. It has API changes that make it incompatible with Mbed TLS 2.x,
+  as well as all the new features and bug fixes and security fixes.
+- The [`development_2.x`](https://github.com/ARMmbed/mbedtls/tree/development_2.x) branch:
+  this branch retains the API of Mbed TLS 2.x, and has a subset of the
+  features added after Mbed TLS 2.26.0 and bug fixes and security fixes.
+- One or more long-time support (LTS) branches:
+  these only get bug fixes and security fixes.
+
+We use [Semantic Versioning](https://semver.org/). In particular, we maintain
+API compatibility in the `master` branch across minor version changes (e.g.
+the API of 3.(x+1) is backward compatible with 3.x). We only break API
+compatibility on major version changes (e.g. from 3.x to 4.0). We also maintain
+ABI compatibility within LTS branches; see the next section for details.
+
+## Backwards Compatibility
+
+We maintain API compatibility in released versions of Mbed TLS. If you have
+code that's working and secure with Mbed TLS x.y.z and does not rely on
+undocumented features, then you should be able to re-compile it without
+modification with any later release x.y'.z' with the same major version
+number, and your code will still build, be secure, and work.
+
+Note that new releases of Mbed TLS may extend the API. Here are some
+examples of changes that are common in minor releases of Mbed TLS, and are
+not considered API compatibility breaks:
+
+* Adding or reordering fields in a structure or union.
+* Removing a field from a structure, unless the field is documented as public.
+* Adding items to an enum.
+* Returning an error code that was not previously documented for a function
+  when a new error condition arises.
+* Changing which error code is returned in a case where multiple error
+  conditions apply.
+* Changing the behavior of a function from failing to succeeding, when the
+  change is a reasonable extension of the current behavior, i.e. the
+  addition of a new feature.
+
+There are rare exceptions where we break API compatibility: code that was
+relying on something that became insecure in the meantime (for example,
+crypto that was found to be weak) may need to be changed. In case security
+comes in conflict with backwards compatibility, we will put security first,
+but always attempt to provide a compatibility option.
+
+## Long-time support branches
+
+For the LTS branches, additionally we try very hard to also maintain ABI
+compatibility (same definition as API except with re-linking instead of
+re-compiling) and to avoid any increase in code size or RAM usage, or in the
+minimum version of tools needed to build the code. The only exception, as
+before, is in case those goals would conflict with fixing a security issue, we
+will put security first but provide a compatibility option. (So far we never
+had to break ABI compatibility in an LTS branch, but we occasionally had to
+increase code size for a security fix.)
+
+For contributors, see the [Backwards Compatibility section of
+CONTRIBUTING](CONTRIBUTING.md#backwards-compatibility).
+
+## Current Branches
+
+The following branches are currently maintained:
+
+- [master](https://github.com/ARMmbed/mbedtls/tree/master)
+- [`development`](https://github.com/ARMmbed/mbedtls/)
+- [`development_2.x`](https://github.com/ARMmbed/mbedtls/tree/development_2.x)
+- [`mbedtls-2.16`](https://github.com/ARMmbed/mbedtls/tree/mbedtls-2.16)
+ maintained until at least the end of 2021, see
+  <https://tls.mbed.org/tech-updates/blog/announcing-lts-branch-mbedtls-2.16>
+
+Users are urged to always use the latest version of a maintained branch.

BUGS.md

+## Known issues
+
+Known issues in Mbed TLS are [tracked on GitHub](https://github.com/ARMmbed/mbedtls/issues).
+
+## Reporting a bug
+
+If you think you've found a bug in Mbed TLS, please follow these steps:
+
+1. Make sure you're using the latest version of a
+   [maintained branch](BRANCHES.md): `master`, `development`,
+   or a long-time support branch.
+2. Check [GitHub](https://github.com/ARMmbed/mbedtls/issues) to see if
+   your issue has already been reported. If not, …
+3. If the issue is a security risk (for example: buffer overflow,
+   data leak), please report it confidentially as described in
+   [`SECURITY.md`](SECURITY.md). If not, …
+4. Please [create an issue on on GitHub](https://github.com/ARMmbed/mbedtls/issues).
+
+Please do not use GitHub for support questions. If you want to know
+how to do something with Mbed TLS, please see [`SUPPORT.md`](SUPPORT.md) for available documentation and support channels.

BUILD.gn

@@ -11,10 +11,22 @@
 # 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.
-#
+#
 
 import("//third_party/mbedtls/mbedtls.gni")
 
+MBEDTLS_SOURCES += [
+  "library/debug.c",
+  "library/ssl_cache.c",
+  "library/ssl_cookie.c",
+  "library/ssl_srv.c",
+  "library/ssl_ticket.c",
+  "library/x509_create.c",
+  "library/x509_csr.c",
+  "library/x509write_crt.c",
+  "library/x509write_csr.c",
+]
+
 if (defined(ohos_lite)) {
   import("//build/lite/config/component/lite_component.gni")
   import("//build/lite/ndk/ndk.gni")
@@ -89,19 +101,6 @@ if (defined(ohos_lite)) {
       ]
     }
 
-    MBEDTLS_SOURCES += [
-      "library/debug.c",
-      "library/pkcs11.c",
-      "library/ssl_cache.c",
-      "library/ssl_cookie.c",
-      "library/ssl_srv.c",
-      "library/ssl_ticket.c",
-      "library/x509_create.c",
-      "library/x509_csr.c",
-      "library/x509write_crt.c",
-      "library/x509write_csr.c",
-    ]
-
     static_library("mbedtls_gt") {
       sources = MBEDTLS_SOURCES
       output_name = "mbedtls_gt"

CMakeLists.txt

-cmake_minimum_required(VERSION 2.6)
+#
+# CMake build system design considerations:
+#
+# - Include directories:
+#   + Do not define include directories globally using the include_directories
+#     command but rather at the target level using the
+#     target_include_directories command. That way, it is easier to guarantee
+#     that targets are built using the proper list of include directories.
+#   + Use the PUBLIC and PRIVATE keywords to specifiy the scope of include
+#     directories. That way, a target linking to a library (using the
+#     target_link_librairies command) inherits from the library PUBLIC include
+#     directories and not from the PRIVATE ones.
+# - MBEDTLS_TARGET_PREFIX: CMake targets are designed to be alterable by calling
+#   CMake in order to avoid target name clashes, via the use of
+#   MBEDTLS_TARGET_PREFIX. The value of this variable is prefixed to the
+#   mbedtls, mbedx509, mbedcrypto and apidoc targets.
+#
+
+# We specify a minimum requirement of 3.10.2, but for now use 3.5.1 here
+# until our infrastructure catches up.
+cmake_minimum_required(VERSION 3.5.1)
+
+include(CMakePackageConfigHelpers)
+
+# https://cmake.org/cmake/help/latest/policy/CMP0011.html
+# Setting this policy is required in CMake >= 3.18.0, otherwise a warning is generated. The OLD
+# policy setting is deprecated, and will be removed in future versions.
+cmake_policy(SET CMP0011 NEW)
+# https://cmake.org/cmake/help/latest/policy/CMP0012.html
+# Setting the CMP0012 policy to NEW is required for FindPython3 to work with CMake 3.18.2
+# (there is a bug in this particular version), otherwise, setting the CMP0012 policy is required
+# for CMake versions >= 3.18.3 otherwise a deprecated warning is generated. The OLD policy setting
+# is deprecated and will be removed in future versions.
+cmake_policy(SET CMP0012 NEW)
+
 if(TEST_CPP)
     project("mbed TLS" C CXX)
 else()
     project("mbed TLS" C)
 endif()
 
-option(USE_PKCS11_HELPER_LIBRARY "Build mbed TLS with the pkcs11-helper library." OFF)
-option(ENABLE_ZLIB_SUPPORT "Build mbed TLS with zlib library." OFF)
+# Set the project root directory.
+set(MBEDTLS_DIR ${CMAKE_CURRENT_SOURCE_DIR})
 
 option(ENABLE_PROGRAMS "Build mbed TLS programs." ON)
 
 option(UNSAFE_BUILD "Allow unsafe builds. These builds ARE NOT SECURE." OFF)
+option(MBEDTLS_FATAL_WARNINGS "Compiler warnings treated as errors" ON)
+if(WIN32)
+    option(GEN_FILES "Generate the auto-generated files as needed" OFF)
+else()
+    option(GEN_FILES "Generate the auto-generated files as needed" ON)
+endif()
 
 string(REGEX MATCH "Clang" CMAKE_COMPILER_IS_CLANG "${CMAKE_C_COMPILER_ID}")
 string(REGEX MATCH "GNU" CMAKE_COMPILER_IS_GNU "${CMAKE_C_COMPILER_ID}")
@@ -25,17 +65,6 @@ else()
 endif()
 
 # Warning string - created as a list for compatibility with CMake 2.8
-set(WARNING_BORDER "*******************************************************\n")
-set(NULL_ENTROPY_WARN_L1 "****  WARNING!  MBEDTLS_TEST_NULL_ENTROPY defined!\n")
-set(NULL_ENTROPY_WARN_L2 "****  THIS BUILD HAS NO DEFINED ENTROPY SOURCES\n")
-set(NULL_ENTROPY_WARN_L3 "****  AND IS *NOT* SUITABLE FOR PRODUCTION USE\n")
-
-set(NULL_ENTROPY_WARNING "${WARNING_BORDER}"
-                         "${NULL_ENTROPY_WARN_L1}"
-                         "${NULL_ENTROPY_WARN_L2}"
-                         "${NULL_ENTROPY_WARN_L3}"
-                         "${WARNING_BORDER}")
-
 set(CTR_DRBG_128_BIT_KEY_WARN_L1 "****  WARNING!  MBEDTLS_CTR_DRBG_USE_128_BIT_KEY defined!\n")
 set(CTR_DRBG_128_BIT_KEY_WARN_L2 "****  Using 128-bit keys for CTR_DRBG limits the security of generated\n")
 set(CTR_DRBG_128_BIT_KEY_WARN_L3 "****  keys and operations that use random values generated to 128-bit security\n")
@@ -46,42 +75,36 @@ set(CTR_DRBG_128_BIT_KEY_WARNING "${WARNING_BORDER}"
                          "${CTR_DRBG_128_BIT_KEY_WARN_L3}"
                          "${WARNING_BORDER}")
 
-find_package(PythonInterp)
-find_package(Perl)
-if(PERL_FOUND)
+# Python 3 is only needed here to check for configuration warnings.
+if(NOT CMAKE_VERSION VERSION_LESS 3.15.0)
+    set(Python3_FIND_STRATEGY LOCATION)
+    find_package(Python3 COMPONENTS Interpreter)
+    if(Python3_Interpreter_FOUND)
+        set(MBEDTLS_PYTHON_EXECUTABLE ${Python3_EXECUTABLE})
+    endif()
+else()
+    find_package(PythonInterp 3)
+    if(PYTHONINTERP_FOUND)
+        set(MBEDTLS_PYTHON_EXECUTABLE ${PYTHON_EXECUTABLE})
+    endif()
+endif()
+if(MBEDTLS_PYTHON_EXECUTABLE)
 
     # If 128-bit keys are configured for CTR_DRBG, display an appropriate warning
-    execute_process(COMMAND ${PERL_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/scripts/config.pl -f ${CMAKE_CURRENT_SOURCE_DIR}/include/mbedtls/config.h get MBEDTLS_CTR_DRBG_USE_128_BIT_KEY
+    execute_process(COMMAND ${MBEDTLS_PYTHON_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/scripts/config.py -f ${CMAKE_CURRENT_SOURCE_DIR}/include/mbedtls/mbedtls_config.h get MBEDTLS_CTR_DRBG_USE_128_BIT_KEY
                         RESULT_VARIABLE result)
     if(${result} EQUAL 0)
         message(WARNING ${CTR_DRBG_128_BIT_KEY_WARNING})
     endif()
 
-    # If NULL Entropy is configured, display an appropriate warning
-    execute_process(COMMAND ${PERL_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/scripts/config.pl -f ${CMAKE_CURRENT_SOURCE_DIR}/include/mbedtls/config.h get MBEDTLS_TEST_NULL_ENTROPY
-                        RESULT_VARIABLE result)
-    if(${result} EQUAL 0)
-        message(WARNING ${NULL_ENTROPY_WARNING})
-
-        if(NOT UNSAFE_BUILD)
-            message(FATAL_ERROR "\
-\n\
-Warning! You have enabled MBEDTLS_TEST_NULL_ENTROPY. \
-This option is not safe for production use and negates all security \
-It is intended for development use only. \
-\n\
-To confirm you want to build with this option, re-run cmake with the \
-option: \n\
-  cmake -DUNSAFE_BUILD=ON ")
-
-            return()
-        endif()
-    endif()
 endif()
 
-set(CMAKE_BUILD_TYPE ${CMAKE_BUILD_TYPE}
-    CACHE STRING "Choose the type of build: None Debug Release Coverage ASan ASanDbg MemSan MemSanDbg Check CheckFull"
-    FORCE)
+# If this is the root project add longer list of available CMAKE_BUILD_TYPE values
+if(CMAKE_SOURCE_DIR STREQUAL CMAKE_CURRENT_SOURCE_DIR)
+    set(CMAKE_BUILD_TYPE ${CMAKE_BUILD_TYPE}
+        CACHE STRING "Choose the type of build: None Debug Release Coverage ASan ASanDbg MemSan MemSanDbg Check CheckFull"
+        FORCE)
+endif()
 
 # Create a symbolic link from ${base_name} in the binary directory
 # to the corresponding path in the source directory.
@@ -117,39 +140,72 @@ function(link_to_source base_name)
     endif()
 endfunction(link_to_source)
 
+# Get the filename without the final extension (i.e. convert "a.b.c" to "a.b")
+function(get_name_without_last_ext dest_var full_name)
+    # Split into a list on '.' (but a cmake list is just a ';'-separated string)
+    string(REPLACE "." ";" ext_parts "${full_name}")
+    # Remove the last item if there are more than one
+    list(LENGTH ext_parts ext_parts_len)
+    if (${ext_parts_len} GREATER "1")
+        math(EXPR ext_parts_last_item "${ext_parts_len} - 1")
+        list(REMOVE_AT ext_parts ${ext_parts_last_item})
+    endif()
+    # Convert back to a string by replacing separators with '.'
+    string(REPLACE ";" "." no_ext_name "${ext_parts}")
+    # Copy into the desired variable
+    set(${dest_var} ${no_ext_name} PARENT_SCOPE)
+endfunction(get_name_without_last_ext)
+
 string(REGEX MATCH "Clang" CMAKE_COMPILER_IS_CLANG "${CMAKE_C_COMPILER_ID}")
 
+include(CheckCCompilerFlag)
+
 if(CMAKE_COMPILER_IS_GNU)
     # some warnings we want are not available with old GCC versions
     # note: starting with CMake 2.8 we could use CMAKE_C_COMPILER_VERSION
     execute_process(COMMAND ${CMAKE_C_COMPILER} -dumpversion
                     OUTPUT_VARIABLE GCC_VERSION)
-    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -Wextra -W -Wdeclaration-after-statement -Wwrite-strings")
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -Wextra -Wwrite-strings")
+    if (GCC_VERSION VERSION_GREATER 3.0 OR GCC_VERSION VERSION_EQUAL 3.0)
+        set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wformat=2 -Wno-format-nonliteral")
+    endif()
+    if (GCC_VERSION VERSION_GREATER 4.3 OR GCC_VERSION VERSION_EQUAL 4.3)
+        set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wvla")
+    endif()
     if (GCC_VERSION VERSION_GREATER 4.5 OR GCC_VERSION VERSION_EQUAL 4.5)
         set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wlogical-op")
     endif()
     if (GCC_VERSION VERSION_GREATER 4.8 OR GCC_VERSION VERSION_EQUAL 4.8)
         set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wshadow")
     endif()
+    if (GCC_VERSION VERSION_GREATER 5.0)
+        CHECK_C_COMPILER_FLAG("-Wformat-signedness" C_COMPILER_SUPPORTS_WFORMAT_SIGNEDNESS)
+        if(C_COMPILER_SUPPORTS_WFORMAT_SIGNEDNESS)
+            set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wformat-signedness")
+        endif()
+    endif()
+    if (GCC_VERSION VERSION_GREATER 7.0 OR GCC_VERSION VERSION_EQUAL 7.0)
+      set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wformat-overflow=2 -Wformat-truncation")
+    endif()
     set(CMAKE_C_FLAGS_RELEASE     "-O2")
     set(CMAKE_C_FLAGS_DEBUG       "-O0 -g3")
     set(CMAKE_C_FLAGS_COVERAGE    "-O0 -g3 --coverage")
-    set(CMAKE_C_FLAGS_ASAN        "-Werror -fsanitize=address -fno-common -O3")
-    set(CMAKE_C_FLAGS_ASANDBG     "-Werror -fsanitize=address -fno-common -O1 -g3 -fno-omit-frame-pointer -fno-optimize-sibling-calls ")
-    set(CMAKE_C_FLAGS_CHECK       "-Werror -Os")
+    set(CMAKE_C_FLAGS_ASAN        "-fsanitize=address -fno-common -fsanitize=undefined -fno-sanitize-recover=all -O3")
+    set(CMAKE_C_FLAGS_ASANDBG     "-fsanitize=address -fno-common -fsanitize=undefined -fno-sanitize-recover=all -O1 -g3 -fno-omit-frame-pointer -fno-optimize-sibling-calls")
+    set(CMAKE_C_FLAGS_CHECK       "-Os")
     set(CMAKE_C_FLAGS_CHECKFULL   "${CMAKE_C_FLAGS_CHECK} -Wcast-qual")
 endif(CMAKE_COMPILER_IS_GNU)
 
 if(CMAKE_COMPILER_IS_CLANG)
-    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -Wextra -W -Wdeclaration-after-statement -Wwrite-strings -Wpointer-arith -Wimplicit-fallthrough -Wshadow")
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -Wextra -Wwrite-strings -Wpointer-arith -Wimplicit-fallthrough -Wshadow -Wvla -Wformat=2 -Wno-format-nonliteral")
     set(CMAKE_C_FLAGS_RELEASE     "-O2")
     set(CMAKE_C_FLAGS_DEBUG       "-O0 -g3")
     set(CMAKE_C_FLAGS_COVERAGE    "-O0 -g3 --coverage")
-    set(CMAKE_C_FLAGS_ASAN        "-Werror -fsanitize=address -fno-common -fsanitize=undefined -fno-sanitize-recover=all -O3")
-    set(CMAKE_C_FLAGS_ASANDBG     "-Werror -fsanitize=address -fno-common -fsanitize=undefined -fno-sanitize-recover=all -O1 -g3 -fno-omit-frame-pointer -fno-optimize-sibling-calls ")
-    set(CMAKE_C_FLAGS_MEMSAN      "-Werror -fsanitize=memory -O3")
-    set(CMAKE_C_FLAGS_MEMSANDBG   "-Werror -fsanitize=memory -O1 -g3 -fno-omit-frame-pointer -fno-optimize-sibling-calls -fsanitize-memory-track-origins=2")
-    set(CMAKE_C_FLAGS_CHECK       "-Werror -Os")
+    set(CMAKE_C_FLAGS_ASAN        "-fsanitize=address -fno-common -fsanitize=undefined -fno-sanitize-recover=all -O3")
+    set(CMAKE_C_FLAGS_ASANDBG     "-fsanitize=address -fno-common -fsanitize=undefined -fno-sanitize-recover=all -O1 -g3 -fno-omit-frame-pointer -fno-optimize-sibling-calls")
+    set(CMAKE_C_FLAGS_MEMSAN      "-fsanitize=memory -O3")
+    set(CMAKE_C_FLAGS_MEMSANDBG   "-fsanitize=memory -O1 -g3 -fno-omit-frame-pointer -fno-optimize-sibling-calls -fsanitize-memory-track-origins=2")
+    set(CMAKE_C_FLAGS_CHECK       "-Os")
 endif(CMAKE_COMPILER_IS_CLANG)
 
 if(CMAKE_COMPILER_IS_IAR)
@@ -157,11 +213,25 @@ if(CMAKE_COMPILER_IS_IAR)
 endif(CMAKE_COMPILER_IS_IAR)
 
 if(CMAKE_COMPILER_IS_MSVC)
-    # Strictest warnings, and treat as errors
+    # Strictest warnings
     set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} /W3")
-    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} /WX")
 endif(CMAKE_COMPILER_IS_MSVC)
 
+if(MBEDTLS_FATAL_WARNINGS)
+    if(CMAKE_COMPILER_IS_MSVC)
+        set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} /WX")
+    endif(CMAKE_COMPILER_IS_MSVC)
+
+    if(CMAKE_COMPILER_IS_CLANG OR CMAKE_COMPILER_IS_GNU)
+        set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Werror")
+        if(UNSAFE_BUILD)
+            set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-error=cpp")
+            set(CMAKE_C_FLAGS_ASAN "${CMAKE_C_FLAGS_ASAN} -Wno-error=cpp")
+            set(CMAKE_C_FLAGS_ASANDBG "${CMAKE_C_FLAGS_ASANDBG} -Wno-error=cpp")
+        endif(UNSAFE_BUILD)
+    endif(CMAKE_COMPILER_IS_CLANG OR CMAKE_COMPILER_IS_GNU)
+endif(MBEDTLS_FATAL_WARNINGS)
+
 if(CMAKE_BUILD_TYPE STREQUAL "Coverage")
     if(CMAKE_COMPILER_IS_GNU OR CMAKE_COMPILER_IS_CLANG)
         set(CMAKE_SHARED_LINKER_FLAGS "--coverage")
@@ -173,24 +243,40 @@ else()
     set(LIB_INSTALL_DIR lib)
 endif()
 
-include_directories(include/)
-
-if(ENABLE_ZLIB_SUPPORT)
-    find_package(ZLIB)
+add_subdirectory(include)
 
-    if(ZLIB_FOUND)
-        include_directories(${ZLIB_INCLUDE_DIR})
-    endif(ZLIB_FOUND)
-endif(ENABLE_ZLIB_SUPPORT)
+add_subdirectory(3rdparty)
 
 add_subdirectory(library)
-add_subdirectory(include)
+
+#
+# The C files in tests/src directory contain test code shared among test suites
+# and programs. This shared test code is compiled and linked to test suites and
+# programs objects as a set of compiled objects. The compiled objects are NOT
+# built into a library that the test suite and program objects would link
+# against as they link against the mbedcrypto, mbedx509 and mbedtls libraries.
+# The reason is that such library is expected to have mutual dependencies with
+# the aforementioned libraries and that there is as of today no portable way of
+# handling such dependencies (only toolchain specific solutions).
+#
+# Thus the below definition of the `mbedtls_test` CMake library of objects
+# target. This library of objects is used by tests and programs CMake files
+# to define the test executables.
+#
+if(ENABLE_TESTING OR ENABLE_PROGRAMS)
+    file(GLOB MBEDTLS_TEST_FILES ${CMAKE_CURRENT_SOURCE_DIR}/tests/src/*.c ${CMAKE_CURRENT_SOURCE_DIR}/tests/src/drivers/*.c)
+    add_library(mbedtls_test OBJECT ${MBEDTLS_TEST_FILES})
+    target_include_directories(mbedtls_test
+        PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/tests/include
+        PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/include
+        PRIVATE ${CMAKE_CURRENT_SOURCE_DIR}/library)
+endif()
 
 if(ENABLE_PROGRAMS)
     add_subdirectory(programs)
 endif()
 
-ADD_CUSTOM_TARGET(apidoc
+ADD_CUSTOM_TARGET(${MBEDTLS_TARGET_PREFIX}apidoc
     COMMAND doxygen mbedtls.doxyfile
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/doxygen)
 
@@ -238,3 +324,37 @@ if(ENABLE_TESTING)
                     ${CMAKE_CURRENT_BINARY_DIR}/DartConfiguration.tcl COPYONLY)
     endif()
 endif()
+
+configure_package_config_file(
+    "cmake/MbedTLSConfig.cmake.in"
+    "cmake/MbedTLSConfig.cmake"
+        INSTALL_DESTINATION "cmake")
+
+write_basic_package_version_file(
+    "cmake/MbedTLSConfigVersion.cmake"
+        COMPATIBILITY SameMajorVersion
+        VERSION 3.1.0)
+
+install(
+    FILES "${CMAKE_CURRENT_BINARY_DIR}/cmake/MbedTLSConfig.cmake"
+          "${CMAKE_CURRENT_BINARY_DIR}/cmake/MbedTLSConfigVersion.cmake"
+    DESTINATION "cmake")
+
+export(
+    EXPORT MbedTLSTargets
+    NAMESPACE MbedTLS::
+    FILE "cmake/MbedTLSTargets.cmake")
+
+install(
+    EXPORT MbedTLSTargets
+    NAMESPACE MbedTLS::
+    DESTINATION "cmake"
+    FILE "MbedTLSTargets.cmake")
+
+if(CMAKE_VERSION VERSION_GREATER 3.15 OR CMAKE_VERSION VERSION_EQUAL 3.15)
+    # Do not export the package by default
+    cmake_policy(SET CMP0090 NEW)
+
+    # Make this package visible to the system
+    export(PACKAGE MbedTLS)
+endif()

CONTRIBUTING.md

@@ -22,9 +22,10 @@ Making a Contribution
 1. All new files should include the [Apache-2.0](https://spdx.org/licenses/Apache-2.0.html) standard license header where possible.
 1. Ensure that each commit has at least one `Signed-off-by:` line from the committer. If anyone else contributes to the commit, they should also add their own `Signed-off-by:` line. By adding this line, contributor(s) certify that the contribution is made under the terms of the [Developer Certificate of Origin](dco.txt). The contribution licensing is described in the [License section of the README](README.md#License).
 
-API/ABI Compatibility
----------------------
-The project aims to minimise the impact on users upgrading to newer versions of the library and it should not be necessary for a user to make any changes to their own code to work with a newer version of the library. Unless the user has made an active decision to use newer features, a newer generation of the library or a change has been necessary due to a security issue or other significant software defect, no modifications to their own code should be necessary. To achieve this, API compatibility is maintained between different versions of Mbed TLS on the main development branch and in LTS (Long Term Support) branches.
+Backwards Compatibility
+-----------------------
+
+The project aims to minimise the impact on users upgrading to newer versions of the library and it should not be necessary for a user to make any changes to their own code to work with a newer version of the library. Unless the user has made an active decision to use newer features, a newer generation of the library or a change has been necessary due to a security issue or other significant software defect, no modifications to their own code should be necessary. To achieve this, API compatibility is maintained between different versions of Mbed TLS on the main development branch and in LTS (Long Term Support) branches, as described in [BRANCHES.md](BRANCHES.md).
 
 To minimise such disruption to users, where a change to the interface is required, all changes to the ABI or API, even on the main development branch where new features are added, need to be justifiable by either being a significant enhancement, new feature or bug fix which is best resolved by an interface change.
 
@@ -48,8 +49,10 @@ When backporting to these branches please observe the following rules:
 
 It would be highly appreciated if contributions are backported to LTS branches in addition to the [development branch](https://github.com/ARMmbed/mbedtls/tree/development) by contributors.
 
-Currently maintained LTS branches are:
-1. [mbedtls-2.7](https://github.com/ARMmbed/mbedtls/tree/mbedtls-2.7)
+The list of maintained branches can be found in the [Current Branches section
+of BRANCHES.md](BRANCHES.md#current-branches).
+
+The only currently maintained LTS branch is:
 1. [mbedtls-2.16](https://github.com/ARMmbed/mbedtls/tree/mbedtls-2.16)
 
 

ChangeLog.d/00README.md

@@ -22,7 +22,7 @@ We generally don't include changelog entries for:
 * Changes to parts of the code base that users don't interact with directly,
   such as test code and test data.
 
-Until Mbed TLS 2.16.8, we required changelog entries in more cases.
+Until Mbed TLS 2.24.0, we required changelog entries in more cases.
 Looking at older changelog entries is good practice for how to write a
 changelog entry, but not for deciding whether to write one.
 

ChangeLog.d/fix-pkcs12-null-password.txt

-Bugfix
-   * Fix a potential invalid pointer dereference and infinite loop bugs in
-     pkcs12 functions when the password is empty. Fix the documentation to
-     better describe the inputs to these functions and their possible values.
-     Fixes #5136.
\ No newline at end of file

LICENSE

-Unless specifically indicated otherwise in a file, Mbed TLS files are provided
-under the Apache License 2.0, or the GNU General Public License v2.0 or later
-(SPDX-License-Identifier: Apache-2.0 OR GPL-2.0-or-later).
 
-A copy of these licenses can be found in apache-2.0.txt and gpl-2.0.txt
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   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.

Makefile

-
 DESTDIR=/usr/local
 PREFIX=mbedtls_
+PERL ?= perl
 
 .SILENT:
 
@@ -11,19 +11,55 @@ all: programs tests
 
 no_test: programs
 
-programs: lib
+programs: lib mbedtls_test
 	$(MAKE) -C programs
 
 lib:
 	$(MAKE) -C library
 
-tests: lib
+tests: lib mbedtls_test
 	$(MAKE) -C tests
 
+mbedtls_test:
+	$(MAKE) -C tests mbedtls_test
+
+library/%:
+	$(MAKE) -C library $*
+programs/%:
+	$(MAKE) -C programs $*
+tests/%:
+	$(MAKE) -C tests $*
+
+.PHONY: generated_files
+generated_files: library/generated_files
+generated_files: programs/generated_files
+generated_files: tests/generated_files
+generated_files: visualc_files
+
+.PHONY: visualc_files
+VISUALC_FILES = visualc/VS2010/mbedTLS.sln visualc/VS2010/mbedTLS.vcxproj
+# TODO: $(app).vcxproj for each $(app) in programs/
+visualc_files: $(VISUALC_FILES)
+
+# Ensure that the .c files that generate_visualc_files.pl enumerates are
+# present before it runs. It doesn't matter if the files aren't up-to-date,
+# they just need to be present.
+$(VISUALC_FILES): | library/generated_files
+$(VISUALC_FILES): scripts/generate_visualc_files.pl
+$(VISUALC_FILES): scripts/data_files/vs2010-app-template.vcxproj
+$(VISUALC_FILES): scripts/data_files/vs2010-main-template.vcxproj
+$(VISUALC_FILES): scripts/data_files/vs2010-sln-template.sln
+# TODO: also the list of .c and .h source files, but not their content
+$(VISUALC_FILES):
+	echo "  Gen   $@ ..."
+	$(PERL) scripts/generate_visualc_files.pl
+
 ifndef WINDOWS
 install: no_test
 	mkdir -p $(DESTDIR)/include/mbedtls
 	cp -rp include/mbedtls $(DESTDIR)/include
+	mkdir -p $(DESTDIR)/include/psa
+	cp -rp include/psa $(DESTDIR)/include
 
 	mkdir -p $(DESTDIR)/lib
 	cp -RP library/libmbedtls.*    $(DESTDIR)/lib
@@ -41,6 +77,7 @@ install: no_test
 
 uninstall:
 	rm -rf $(DESTDIR)/include/mbedtls
+	rm -rf $(DESTDIR)/include/psa
 	rm -f $(DESTDIR)/lib/libmbedtls.*
 	rm -f $(DESTDIR)/lib/libmbedx509.*
 	rm -f $(DESTDIR)/lib/libmbedcrypto.*
@@ -54,12 +91,6 @@ uninstall:
 	done
 endif
 
-WARNING_BORDER      =*******************************************************\n
-NULL_ENTROPY_WARN_L1=****  WARNING!  MBEDTLS_TEST_NULL_ENTROPY defined! ****\n
-NULL_ENTROPY_WARN_L2=****  THIS BUILD HAS NO DEFINED ENTROPY SOURCES    ****\n
-NULL_ENTROPY_WARN_L3=****  AND IS *NOT* SUITABLE FOR PRODUCTION USE     ****\n
-
-NULL_ENTROPY_WARNING=\n$(WARNING_BORDER)$(NULL_ENTROPY_WARN_L1)$(NULL_ENTROPY_WARN_L2)$(NULL_ENTROPY_WARN_L3)$(WARNING_BORDER)
 
 WARNING_BORDER_LONG      =**********************************************************************************\n
 CTR_DRBG_128_BIT_KEY_WARN_L1=****  WARNING!  MBEDTLS_CTR_DRBG_USE_128_BIT_KEY defined!                      ****\n
@@ -73,22 +104,32 @@ post_build:
 ifndef WINDOWS
 
 	# If 128-bit keys are configured for CTR_DRBG, display an appropriate warning
-	-scripts/config.pl get MBEDTLS_CTR_DRBG_USE_128_BIT_KEY && ([ $$? -eq 0 ]) && \
+	-scripts/config.py get MBEDTLS_CTR_DRBG_USE_128_BIT_KEY && ([ $$? -eq 0 ]) && \
 	    echo '$(CTR_DRBG_128_BIT_KEY_WARNING)'
 
-	# If NULL Entropy is configured, display an appropriate warning
-	-scripts/config.pl get MBEDTLS_TEST_NULL_ENTROPY && ([ $$? -eq 0 ]) && \
-	    echo '$(NULL_ENTROPY_WARNING)'
 endif
 
-clean:
+clean: clean_more_on_top
 	$(MAKE) -C library clean
 	$(MAKE) -C programs clean
 	$(MAKE) -C tests clean
+
+clean_more_on_top:
 ifndef WINDOWS
 	find . \( -name \*.gcno -o -name \*.gcda -o -name \*.info \) -exec rm {} +
 endif
 
+neat: clean_more_on_top
+	$(MAKE) -C library neat
+	$(MAKE) -C programs neat
+	$(MAKE) -C tests neat
+ifndef WINDOWS
+	rm -f visualc/VS2010/*.vcxproj visualc/VS2010/mbedTLS.sln
+else
+	if exist visualc\VS2010\*.vcxproj del /Q /F visualc\VS2010\*.vcxproj
+	if exist visualc\VS2010\mbedTLS.sln del /Q /F visualc\VS2010\mbedTLS.sln
+endif
+
 check: lib tests
 	$(MAKE) -C tests check
 
@@ -122,7 +163,16 @@ apidoc_clean:
 endif
 
 ## Editor navigation files
-C_SOURCE_FILES = $(wildcard include/*/*.h library/*.[hc] programs/*/*.[hc] tests/suites/*.function)
+C_SOURCE_FILES = $(wildcard \
+	3rdparty/*/include/*/*.h 3rdparty/*/include/*/*/*.h 3rdparty/*/include/*/*/*/*.h \
+	3rdparty/*/*.c 3rdparty/*/*/*.c 3rdparty/*/*/*/*.c 3rdparty/*/*/*/*/*.c \
+	include/*/*.h \
+	library/*.[hc] \
+	programs/*/*.[hc] \
+	tests/include/*/*.h tests/include/*/*/*.h \
+	tests/src/*.c tests/src/*/*.c \
+	tests/suites/*.function \
+)
 # Exuberant-ctags invocation. Other ctags implementations may require different options.
 CTAGS = ctags --langmap=c:+.h.function --line-directives=no -o
 tags: $(C_SOURCE_FILES)

README.OpenSource

-[
-    {
-    "Name": "mbed TLS",
-    "License": "Apache License V2.0; GPL V2.0",
-    "License File": "LICENSE",
-    "Version Number": "2.16.11",
-    "Owner": "shituanhui@huawei.com",
-    "Upstream URL": "https://tls.mbed.org/",
-    "Description": "An open source, portable, easy to use, readable and flexible SSL library."
-    }
-]
-
+[
+    {
+    "Name": "mbed TLS",
+    "License": "Apache License V2.0; GPL V2.0",
+    "License File": "LICENSE",
+    "Version Number": "3.1.0",
+    "Owner": "shituanhui@huawei.com",
+    "Upstream URL": "https://tls.mbed.org/",
+    "Description": "An open source, portable, easy to use, readable and flexible SSL library."
+    }
+]
+

README.md

@@ -3,13 +3,30 @@ README for Mbed TLS
 
 Mbed TLS is a C library that implements cryptographic primitives, X.509 certificate manipulation and the SSL/TLS and DTLS protocols. Its small code footprint makes it suitable for embedded systems.
 
+Mbed TLS includes a reference implementation of the [PSA Cryptography API](#psa-cryptography-api). This is currently a preview for evaluation purposes only.
+
 Configuration
 -------------
 
-Mbed TLS should build out of the box on most systems. Some platform specific options are available in the fully documented configuration file `include/mbedtls/config.h`, which is also the place where features can be selected. This file can be edited manually, or in a more programmatic way using the Perl script `scripts/config.pl` (use `--help` for usage instructions).
+Mbed TLS should build out of the box on most systems. Some platform specific options are available in the fully documented configuration file `include/mbedtls/mbedtls_config.h`, which is also the place where features can be selected. This file can be edited manually, or in a more programmatic way using the Python 3 script `scripts/config.py` (use `--help` for usage instructions).
 
 Compiler options can be set using conventional environment variables such as `CC` and `CFLAGS` when using the Make and CMake build system (see below).
 
+We provide some non-standard configurations focused on specific use cases in the `configs/` directory. You can read more about those in `configs/README.txt`
+
+Documentation
+-------------
+
+Documentation for the Mbed TLS interfaces in the default library configuration is available as part of the [Mbed TLS documentation](https://tls.mbed.org/api/).
+
+To generate a local copy of the library documentation in HTML format, tailored to your compile-time configuration:
+
+1. Make sure that [Doxygen](http://www.doxygen.nl/) is installed.
+1. Run `make apidoc`.
+1. Browse `apidoc/index.html` or `apidoc/modules.html`.
+
+For other sources of documentation, see the [SUPPORT](SUPPORT.md) document.
+
 Compiling
 ---------
 
@@ -17,11 +34,46 @@ There are currently three active build systems used within Mbed TLS releases:
 
 -   GNU Make
 -   CMake
--   Microsoft Visual Studio (Microsoft Visual Studio 2010 or later)
+-   Microsoft Visual Studio
 
 The main systems used for development are CMake and GNU Make. Those systems are always complete and up-to-date. The others should reflect all changes present in the CMake and Make build system, although features may not be ported there automatically.
 
-The Make and CMake build systems create three libraries: libmbedcrypto, libmbedx509, and libmbedtls. Note that libmbedtls depends on libmbedx509 and libmbedcrypto, and libmbedx509 depends on libmbedcrypto. As a result, some linkers will expect flags to be in a specific order, for example the GNU linker wants `-lmbedtls -lmbedx509 -lmbedcrypto`. Also, when loading shared libraries using dlopen(), you'll need to load libmbedcrypto first, then libmbedx509, before you can load libmbedtls.
+The Make and CMake build systems create three libraries: libmbedcrypto, libmbedx509, and libmbedtls. Note that libmbedtls depends on libmbedx509 and libmbedcrypto, and libmbedx509 depends on libmbedcrypto. As a result, some linkers will expect flags to be in a specific order, for example the GNU linker wants `-lmbedtls -lmbedx509 -lmbedcrypto`.
+
+### Tool versions
+
+You need the following tools to build the library with the provided makefiles:
+
+* GNU Make 3.82 or a build tool that CMake supports.
+* A C99 toolchain (compiler, linker, archiver). We actively test with GCC 5.4, Clang 3.8, IAR 8 and Visual Studio 2013. More recent versions should work. Slightly older versions may work.
+* Python 3.6 to generate the test code, and to generate sample programs in the development branch.
+* Perl to run the tests, and to generate some source files in the development branch.
+* CMake 3.10.2 or later (if using CMake).
+* Microsoft Visual Studio 2013 or later (if using Visual Studio).
+* Doxygen 1.8.11 or later (if building the documentation; slightly older versions should work).
+
+### Generated source files in the development branch
+
+The source code of Mbed TLS includes some files that are automatically generated by scripts and whose content depends only on the Mbed TLS source, not on the platform or on the library configuration. These files are not included in the development branch of Mbed TLS, but the generated files are included in official releases. This section explains how to generate the missing files in the development branch.
+
+The following tools are required:
+
+* Perl, for some library source files and for Visual Studio build files.
+* Python 3 and some Python packages, for some library source files, sample programs and test data. To install the necessary packages, run
+    ```
+    python -m pip install -r scripts/basic.requirements.txt
+    ```
+* A C compiler for the host platform, for some test data.
+
+If you are cross-compiling, you must set the `CC` environment variable to a C compiler for the host platform when generating the configuration-independent files.
+
+Any of the following methods are available to generate the configuration-independent files:
+
+* If not cross-compiling, running `make` with any target, or just `make`, will automatically generate required files.
+* On non-Windows systems, when not cross-compiling, CMake will generate the required files automatically.
+* Run `make generated_files` to generate all the configuration-independent files.
+* On Unix/POSIX systems, run `tests/scripts/check-generated-files.sh -u` to generate all the configuration-independent files.
+* On Windows, run `scripts\make_generated_files.bat` to generate all the configuration-independent files.
 
 ### Make
 
@@ -49,7 +101,7 @@ In order to build for a Windows platform, you should use `WINDOWS_BUILD=1` if th
 
 Setting the variable `SHARED` in your environment will build shared libraries in addition to the static libraries. Setting `DEBUG` gives you a debug build. You can override `CFLAGS` and `LDFLAGS` by setting them in your environment or on the make command line; compiler warning options may be overridden separately using `WARNING_CFLAGS`. Some directory-specific options (for example, `-I` directives) are still preserved.
 
-Please note that setting `CFLAGS` overrides its default value of `-O2` and setting `WARNING_CFLAGS` overrides its default value (starting with `-Wall -W`), so if you just want to add some warning options to the default ones, you can do so by setting `CFLAGS=-O2 -Werror` for example. Setting `WARNING_CFLAGS` is useful when you want to get rid of its default content (for example because your compiler doesn't accept `-Wall` as an option). Directory-specific options cannot be overridden from the command line.
+Please note that setting `CFLAGS` overrides its default value of `-O2` and setting `WARNING_CFLAGS` overrides its default value (starting with `-Wall -Wextra`), so if you just want to add some warning options to the default ones, you can do so by setting `CFLAGS=-O2 -Werror` for example. Setting `WARNING_CFLAGS` is useful when you want to get rid of its default content (for example because your compiler doesn't accept `-Wall` as an option). Directory-specific options cannot be overridden from the command line.
 
 Depending on your platform, you might run into some issues. Please check the Makefiles in `library/`, `programs/` and `tests/` for options to manually add or remove for specific platforms. You can also check [the Mbed TLS Knowledge Base](https://tls.mbed.org/kb) for articles on your platform or issue.
 
@@ -61,11 +113,11 @@ In order to build the source using CMake in a separate directory (recommended),
 
     mkdir /path/to/build_dir && cd /path/to/build_dir
     cmake /path/to/mbedtls_source
-    make
+    cmake --build .
 
 In order to run the tests, enter:
 
-    make test
+    ctest
 
 The test suites need Python to be built and Perl to be executed. If you don't have one of these installed, you'll want to disable the test suites with:
 
@@ -131,16 +183,52 @@ Regarding variables, also note that if you set CFLAGS when invoking cmake,
 your value of CFLAGS doesn't override the content provided by cmake (depending
 on the build mode as seen above), it's merely prepended to it.
 
+#### Consuming Mbed TLS
+
+Mbed TLS provides a package config file for consumption as a dependency in other
+CMake projects. You can include Mbed TLS's CMake targets yourself with:
+
+    find_package(MbedTLS)
+
+If prompted, set `MbedTLS_DIR` to `${YOUR_MBEDTLS_INSTALL_DIR}/cmake`. This
+creates the following targets:
+
+- `MbedTLS::mbedcrypto` (Crypto library)
+- `MbedTLS::mbedtls` (TLS library)
+- `MbedTLS::mbedx509` (X509 library)
+
+You can then use these directly through `target_link_libraries()`:
+
+    add_executable(xyz)
+
+    target_link_libraries(xyz
+        PUBLIC MbedTLS::mbedtls
+               MbedTLS::mbedcrypto
+               MbedTLS::mbedx509)
+
+This will link the Mbed TLS libraries to your library or application, and add
+its include directories to your target (transitively, in the case of `PUBLIC` or
+`INTERFACE` link libraries).
+
+#### Mbed TLS as a subproject
+
+Mbed TLS supports being built as a CMake subproject. One can
+use `add_subdirectory()` from a parent CMake project to include Mbed TLS as a
+subproject.
+
 ### Microsoft Visual Studio
 
 The build files for Microsoft Visual Studio are generated for Visual Studio 2010.
 
 The solution file `mbedTLS.sln` contains all the basic projects needed to build the library and all the programs. The files in tests are not generated and compiled, as these need Python and perl environments as well. However, the selftest program in `programs/test/` is still available.
 
+In the development branch of Mbed TLS, the Visual Studio solution files need to be generated first as described in [“Generated source files in the development branch”](#generated-source-files-in-the-development-branch).
+
 Example programs
 ----------------
 
-We've included example programs for a lot of different features and uses in [`programs/`](programs/README.md). Most programs only focus on a single feature or usage scenario, so keep that in mind when copying parts of the code.
+We've included example programs for a lot of different features and uses in [`programs/`](programs/README.md).
+Please note that the goal of these sample programs is to demonstrate specific features of the library, and the code may need to be adapted to build a real-world application.
 
 Tests
 -----
@@ -153,12 +241,7 @@ For machines with a Unix shell and OpenSSL (and optionally GnuTLS) installed, ad
 -   `tests/compat.sh` tests interoperability of every ciphersuite with other implementations.
 -   `tests/scripts/test-ref-configs.pl` test builds in various reduced configurations.
 -   `tests/scripts/key-exchanges.pl` test builds in configurations with a single key exchange enabled
--   `tests/scripts/all.sh` runs a combination of the above tests, plus some more, with various build options (such as ASan, full `config.h`, etc).
-
-Configurations
---------------
-
-We provide some non-standard configurations focused on specific use cases in the `configs/` directory. You can read more about those in `configs/README.txt`
+-   `tests/scripts/all.sh` runs a combination of the above tests, plus some more, with various build options (such as ASan, full `mbedtls_config.h`, etc).
 
 Porting Mbed TLS
 ----------------
@@ -169,12 +252,68 @@ Mbed TLS can be ported to many different architectures, OS's and platforms. Befo
 -   [What external dependencies does Mbed TLS rely on?](https://tls.mbed.org/kb/development/what-external-dependencies-does-mbedtls-rely-on)
 -   [How do I configure Mbed TLS](https://tls.mbed.org/kb/compiling-and-building/how-do-i-configure-mbedtls)
 
+Mbed TLS is mostly written in portable C99; however, it has a few platform requirements that go beyond the standard, but are met by most modern architectures:
+
+- Bytes must be 8 bits.
+- All-bits-zero must be a valid representation of a null pointer.
+- Signed integers must be represented using two's complement.
+- `int` and `size_t` must be at least 32 bits wide.
+- The types `uint8_t`, `uint16_t`, `uint32_t` and their signed equivalents must be available.
+
+PSA cryptography API
+--------------------
+
+### PSA API design
+
+Arm's [Platform Security Architecture (PSA)](https://developer.arm.com/architectures/security-architectures/platform-security-architecture) is a holistic set of threat models, security analyses, hardware and firmware architecture specifications, and an open source firmware reference implementation. PSA provides a recipe, based on industry best practice, that allows security to be consistently designed in, at both a hardware and firmware level.
+
+The [PSA cryptography API](https://armmbed.github.io/mbed-crypto/psa/#application-programming-interface) provides access to a set of cryptographic primitives. It has a dual purpose. First, it can be used in a PSA-compliant platform to build services, such as secure boot, secure storage and secure communication. Second, it can also be used independently of other PSA components on any platform.
+
+The design goals of the PSA cryptography API include:
+
+* The API distinguishes caller memory from internal memory, which allows the library to be implemented in an isolated space for additional security. Library calls can be implemented as direct function calls if isolation is not desired, and as remote procedure calls if isolation is desired.
+* The structure of internal data is hidden to the application, which allows substituting alternative implementations at build time or run time, for example, in order to take advantage of hardware accelerators.
+* All access to the keys happens through key identifiers, which allows support for external cryptoprocessors that is transparent to applications.
+* The interface to algorithms is generic, favoring algorithm agility.
+* The interface is designed to be easy to use and hard to accidentally misuse.
+
+Arm welcomes feedback on the design of the API. If you think something could be improved, please open an issue on our Github repository. Alternatively, if you prefer to provide your feedback privately, please email us at [`mbed-crypto@arm.com`](mailto:mbed-crypto@arm.com). All feedback received by email is treated confidentially.
+
+### PSA API documentation
+
+A browsable copy of the PSA Cryptography API documents is available on the [PSA cryptography interfaces documentation portal](https://armmbed.github.io/mbed-crypto/psa/#application-programming-interface) in [PDF](https://armmbed.github.io/mbed-crypto/PSA_Cryptography_API_Specification.pdf) and [HTML](https://armmbed.github.io/mbed-crypto/html/index.html) formats.
+
+### PSA implementation in Mbed TLS
+
+Mbed TLS includes a reference implementation of the PSA Cryptography API.
+This implementation is not yet as mature as the rest of the library. Some parts of the code have not been reviewed as thoroughly, and some parts of the PSA implementation are not yet well optimized for code size.
+
+The X.509 and TLS code can use PSA cryptography for a limited subset of operations. To enable this support, activate the compilation option `MBEDTLS_USE_PSA_CRYPTO` in `mbedtls_config.h`.
+
+There are currently a few deviations where the library does not yet implement the latest version of the specification. Please refer to the [compliance issues on Github](https://github.com/ARMmbed/mbed-crypto/labels/compliance) for an up-to-date list.
+
+### Upcoming features
+
+Future releases of this library will include:
+
+* A driver programming interface, which makes it possible to use hardware accelerators instead of the default software implementation for chosen algorithms.
+* Support for external keys to be stored and manipulated exclusively in a separate cryptoprocessor.
+* A configuration mechanism to compile only the algorithms you need for your application.
+* A wider set of cryptographic algorithms.
+
 License
 -------
 
-Unless specifically indicated otherwise in a file, Mbed TLS files are provided under the [Apache-2.0](https://spdx.org/licenses/Apache-2.0.html) OR [GPL-2.0-or-later](https://spdx.org/licenses/GPL-2.0-or-later.html) licenses. A copy of these licenses can be found in [apache-2.0.txt](./apache-2.0.txt) and [gpl-2.0.txt](./gpl-2.0.txt). Contributors must accept that their contributions are made under both the Apache-2.0 AND GPL-2.0-or-later licenses.
+Unless specifically indicated otherwise in a file, Mbed TLS files are provided under the [Apache-2.0](https://spdx.org/licenses/Apache-2.0.html) license. See the [LICENSE](LICENSE) file for the full text of this license. Contributors must accept that their contributions are made under both the Apache-2.0 AND [GPL-2.0-or-later](https://spdx.org/licenses/GPL-2.0-or-later.html) licenses. This enables LTS (Long Term Support) branches of the software to be provided under either the Apache-2.0 OR GPL-2.0-or-later licenses.
 
 Contributing
 ------------
 
 We gratefully accept bug reports and contributions from the community. Please see the [contributing guidelines](CONTRIBUTING.md) for details on how to do this.
+
+Contact
+-------
+
+* To report a security vulnerability in Mbed TLS, please email <mbed-tls-security@lists.trustedfirmware.org>. For more information, see [`SECURITY.md`](SECURITY.md).
+* To report a bug or request a feature in Mbed TLS, please [file an issue on GitHub](https://github.com/ARMmbed/mbedtls/issues/new/choose).
+* Please see [`SUPPORT.md`](SUPPORT.md) for other channels for discussion and support about Mbed TLS.

SECURITY.md

+## Reporting Vulneratibilities
+
+If you think you have found an Mbed TLS security vulnerability, then please
+send an email to the security team at
+<mbed-tls-security@lists.trustedfirmware.org>.
+
+## Security Incident Handling Process
+
+Our security process is detailled in our
+[security
+center](https://developer.trustedfirmware.org/w/mbed-tls/security-center/).
+
+Its primary goal is to ensure fixes are ready to be deployed when the issue
+goes public.
+
+## Maintained branches
+
+Only the maintained branches, as listed in [`BRANCHES.md`](BRANCHES.md),
+get security fixes.
+Users are urged to always use the latest version of a maintained branch.

SUPPORT.md

+## Documentation
+
+Here are some useful sources of information about using Mbed TLS:
+
+- API documentation, see the [Documentation section of the
+  README](README.md#License);
+- the `docs` directory in the source tree;
+- the [Mbed TLS knowledge Base](https://tls.mbed.org/kb);
+- the [Mbed TLS mailing-list
+  archives](https://lists.trustedfirmware.org/pipermail/mbed-tls/).
+
+## Asking Questions
+
+If you can't find your answer in the above sources, please use the [Mbed TLS
+mailing list](https://lists.trustedfirmware.org/mailman/listinfo/mbed-tls).

bundle.json

-{
-    "name": "@ohos/mbedtls",
-    "description": "An open source, portable, easy to use, readable and flexible SSL library.",
-    "version": "3.1",
-    "license": "Apache V2,GPL V2.0",
-    "publishAs": "code-segment",
-    "segment": {
-        "destPath": "third_party/mbedtls"
-    },
-    "dirs": {},
-    "scripts": {},
-    "component": {
-        "name": "thirdparty_mbedtls",
-        "subsystem": "",
-        "syscap": [],
-        "features": [],
-        "adapted_system_type": [],
-        "rom": "",
-        "ram": "",
-        "deps": {
-            "components": [],
-            "third_party": []
-        },
-        "build": {
-            "sub_component": [],
-            "inner_kits": [],
-            "test": []
-        }
-    }
+{
+    "name": "@ohos/mbedtls",
+    "description": "An open source, portable, easy to use, readable and flexible SSL library.",
+    "version": "5.0",
+    "license": "Apache V2,GPL V2.0",
+    "publishAs": "code-segment",
+    "segment": {
+        "destPath": "third_party/mbedtls"
+    },
+    "dirs": {},
+    "scripts": {},
+    "component": {
+        "name": "thirdparty_mbedtls",
+        "subsystem": "",
+        "syscap": [],
+        "features": [],
+        "adapted_system_type": [],
+        "rom": "",
+        "ram": "",
+        "deps": {
+            "components": [],
+            "third_party": []
+        },
+        "build": {
+            "sub_component": [],
+            "inner_kits": [],
+            "test": []
+        }
+    }
 }
\ No newline at end of file

cmake/MbedTLSConfig.cmake.in

+@PACKAGE_INIT@
+
+include("${CMAKE_CURRENT_LIST_DIR}/MbedTLSTargets.cmake")

configs/README.txt

@@ -4,12 +4,10 @@ The examples are generally focused on a particular usage case (eg, support for
 a restricted number of ciphersuites) and aim at minimizing resource usage for
 this target. They can be used as a basis for custom configurations.
 
-These files are complete replacements for the default config.h. To use one of
+These files are complete replacements for the default mbedtls_config.h. To use one of
 them, you can pick one of the following methods:
 
-1. Replace the default file include/mbedtls/config.h with the chosen one.
-   (Depending on your compiler, you may need to adjust the line with
-   #include "mbedtls/check_config.h" then.)
+1. Replace the default file include/mbedtls/mbedtls_config.h with the chosen one.
 
 2. Define MBEDTLS_CONFIG_FILE and adjust the include path accordingly.
    For example, using make:

configs/config-ccm-psk-tls1_2.h

@@ -5,13 +5,7 @@
  */
 /*
  *  Copyright The Mbed TLS Contributors
- *  SPDX-License-Identifier: Apache-2.0 OR GPL-2.0-or-later
- *
- *  This file is provided under the Apache License 2.0, or the
- *  GNU General Public License v2.0 or later.
- *
- *  **********
- *  Apache License 2.0:
+ *  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.
@@ -24,27 +18,6 @@
  *  WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
- *
- *  **********
- *
- *  **********
- *  GNU General Public License v2.0 or later:
- *
- *  This program is free software; you can redistribute it and/or modify
- *  it under the terms of the GNU General Public License as published by
- *  the Free Software Foundation; either version 2 of the License, or
- *  (at your option) any later version.
- *
- *  This program is distributed in the hope that it will be useful,
- *  but WITHOUT ANY WARRANTY; without even the implied warranty of
- *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- *  GNU General Public License for more details.
- *
- *  You should have received a copy of the GNU General Public License along
- *  with this program; if not, write to the Free Software Foundation, Inc.,
- *  51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
- *
- *  **********
  */
 /*
  * Minimal configuration for TLS 1.2 with PSK and AES-CCM ciphersuites
@@ -56,8 +29,6 @@
  *
  * See README.txt for usage instructions.
  */
-#ifndef MBEDTLS_CONFIG_H
-#define MBEDTLS_CONFIG_H
 
 /* System support */
 //#define MBEDTLS_HAVE_TIME /* Optionally used in Hello messages */
@@ -75,6 +46,10 @@
 #define MBEDTLS_ENTROPY_C
 #define MBEDTLS_MD_C
 #define MBEDTLS_NET_C
+/* The library does not currently support enabling SHA-224 without SHA-256.
+ * A future version of the library will have this option disabled
+ * by default. */
+#define MBEDTLS_SHA224_C
 #define MBEDTLS_SHA256_C
 #define MBEDTLS_SSL_CLI_C
 #define MBEDTLS_SSL_SRV_C
@@ -106,8 +81,5 @@
  * both ends of the connection!  (See comments in "mbedtls/ssl.h".)
  * The optimal size here depends on the typical size of records.
  */
-#define MBEDTLS_SSL_MAX_CONTENT_LEN             1024
-
-#include "mbedtls/check_config.h"
-
-#endif /* MBEDTLS_CONFIG_H */
+#define MBEDTLS_SSL_IN_CONTENT_LEN             1024
+#define MBEDTLS_SSL_OUT_CONTENT_LEN             1024

configs/config_rsa_aes_cbc.h

@@ -85,3 +85,4 @@
 #include "mbedtls/check_config.h"
 
 #endif /* MBEDTLS_CONFIG_H */
+

docs/.gitignore

+*.html
+*.pdf

docs/architecture/Makefile

+PANDOC = pandoc
+
+default: all
+
+all_markdown = \
+	       mbed-crypto-storage-specification.md \
+	       testing/driver-interface-test-strategy.md \
+	       testing/invasive-testing.md \
+	       testing/test-framework.md \
+	       # This line is intentionally left blank
+
+html: $(all_markdown:.md=.html)
+pdf: $(all_markdown:.md=.pdf)
+all: html pdf
+
+.SUFFIXES:
+.SUFFIXES: .md .html .pdf
+
+.md.html:
+	$(PANDOC) -o $@ $<
+.md.pdf:
+	$(PANDOC) -o $@ $<
+
+clean:
+	rm -f *.html *.pdf
+	rm -f testing/*.html testing/*.pdf