124 Externals/mbedtls/3rdparty/everest/include/everest/kremlib/FStar_UInt128.h
View file
@@ -0,0 +1,124 @@
/* 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
280 ...arty/everest/include/everest/kremlib/FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.h
View file
@@ -0,0 +1,280 @@
/* 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
204 Externals/mbedtls/3rdparty/everest/include/everest/kremlin/c_endianness.h
View file
@@ -0,0 +1,204 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

#ifndef __KREMLIN_ENDIAN_H
#define __KREMLIN_ENDIAN_H

#include <string.h>
#include <inttypes.h>

/******************************************************************************/
/* Implementing C.fst (part 2: endian-ness macros) */
/******************************************************************************/

/* ... for Linux */
#if defined(__linux__) || defined(__CYGWIN__)
# include <endian.h>

/* ... for OSX */
#elif defined(__APPLE__)
# include <libkern/OSByteOrder.h>
# define htole64(x) OSSwapHostToLittleInt64(x)
# define le64toh(x) OSSwapLittleToHostInt64(x)
# define htobe64(x) OSSwapHostToBigInt64(x)
# define be64toh(x) OSSwapBigToHostInt64(x)

# define htole16(x) OSSwapHostToLittleInt16(x)
# define le16toh(x) OSSwapLittleToHostInt16(x)
# define htobe16(x) OSSwapHostToBigInt16(x)
# define be16toh(x) OSSwapBigToHostInt16(x)

# define htole32(x) OSSwapHostToLittleInt32(x)
# define le32toh(x) OSSwapLittleToHostInt32(x)
# define htobe32(x) OSSwapHostToBigInt32(x)
# define be32toh(x) OSSwapBigToHostInt32(x)

/* ... for Solaris */
#elif defined(__sun__)
# include <sys/byteorder.h>
# define htole64(x) LE_64(x)
# define le64toh(x) LE_64(x)
# define htobe64(x) BE_64(x)
# define be64toh(x) BE_64(x)

# define htole16(x) LE_16(x)
# define le16toh(x) LE_16(x)
# define htobe16(x) BE_16(x)
# define be16toh(x) BE_16(x)

# define htole32(x) LE_32(x)
# define le32toh(x) LE_32(x)
# define htobe32(x) BE_32(x)
# define be32toh(x) BE_32(x)

/* ... for the BSDs */
#elif defined(__FreeBSD__) || defined(__NetBSD__) || defined(__DragonFly__)
# include <sys/endian.h>
#elif defined(__OpenBSD__)
# include <endian.h>

/* ... for Windows (MSVC)... not targeting XBOX 360! */
#elif defined(_MSC_VER)

# include <stdlib.h>
# define htobe16(x) _byteswap_ushort(x)
# define htole16(x) (x)
# define be16toh(x) _byteswap_ushort(x)
# define le16toh(x) (x)

# define htobe32(x) _byteswap_ulong(x)
# define htole32(x) (x)
# define be32toh(x) _byteswap_ulong(x)
# define le32toh(x) (x)

# define htobe64(x) _byteswap_uint64(x)
# define htole64(x) (x)
# define be64toh(x) _byteswap_uint64(x)
# define le64toh(x) (x)

/* ... for Windows (GCC-like, e.g. mingw or clang) */
#elif (defined(_WIN32) || defined(_WIN64)) && \
(defined(__GNUC__) || defined(__clang__))

# define htobe16(x) __builtin_bswap16(x)
# define htole16(x) (x)
# define be16toh(x) __builtin_bswap16(x)
# define le16toh(x) (x)

# define htobe32(x) __builtin_bswap32(x)
# define htole32(x) (x)
# define be32toh(x) __builtin_bswap32(x)
# define le32toh(x) (x)

# define htobe64(x) __builtin_bswap64(x)
# define htole64(x) (x)
# define be64toh(x) __builtin_bswap64(x)
# define le64toh(x) (x)

/* ... generic big-endian fallback code */
#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__

/* byte swapping code inspired by:
* https://github.com/rweather/arduinolibs/blob/master/libraries/Crypto/utility/EndianUtil.h
* */

# define htobe32(x) (x)
# define be32toh(x) (x)
# define htole32(x) \
(__extension__({ \
uint32_t _temp = (x); \
((_temp >> 24) & 0x000000FF) | ((_temp >> 8) & 0x0000FF00) | \
((_temp << 8) & 0x00FF0000) | ((_temp << 24) & 0xFF000000); \
}))
# define le32toh(x) (htole32((x)))

# define htobe64(x) (x)
# define be64toh(x) (x)
# define htole64(x) \
(__extension__({ \
uint64_t __temp = (x); \
uint32_t __low = htobe32((uint32_t)__temp); \
uint32_t __high = htobe32((uint32_t)(__temp >> 32)); \
(((uint64_t)__low) << 32) | __high; \
}))
# define le64toh(x) (htole64((x)))

/* ... generic little-endian fallback code */
#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__

# define htole32(x) (x)
# define le32toh(x) (x)
# define htobe32(x) \
(__extension__({ \
uint32_t _temp = (x); \
((_temp >> 24) & 0x000000FF) | ((_temp >> 8) & 0x0000FF00) | \
((_temp << 8) & 0x00FF0000) | ((_temp << 24) & 0xFF000000); \
}))
# define be32toh(x) (htobe32((x)))

# define htole64(x) (x)
# define le64toh(x) (x)
# define htobe64(x) \
(__extension__({ \
uint64_t __temp = (x); \
uint32_t __low = htobe32((uint32_t)__temp); \
uint32_t __high = htobe32((uint32_t)(__temp >> 32)); \
(((uint64_t)__low) << 32) | __high; \
}))
# define be64toh(x) (htobe64((x)))

/* ... couldn't determine endian-ness of the target platform */
#else
# error "Please define __BYTE_ORDER__!"

#endif /* defined(__linux__) || ... */

/* Loads and stores. These avoid undefined behavior due to unaligned memory
* accesses, via memcpy. */

inline static uint16_t load16(uint8_t *b) {
uint16_t x;
memcpy(&x, b, 2);
return x;
}

inline static uint32_t load32(uint8_t *b) {
uint32_t x;
memcpy(&x, b, 4);
return x;
}

inline static uint64_t load64(uint8_t *b) {
uint64_t x;
memcpy(&x, b, 8);
return x;
}

inline static void store16(uint8_t *b, uint16_t i) {
memcpy(b, &i, 2);
}

inline static void store32(uint8_t *b, uint32_t i) {
memcpy(b, &i, 4);
}

inline static void store64(uint8_t *b, uint64_t i) {
memcpy(b, &i, 8);
}

#define load16_le(b) (le16toh(load16(b)))
#define store16_le(b, i) (store16(b, htole16(i)))
#define load16_be(b) (be16toh(load16(b)))
#define store16_be(b, i) (store16(b, htobe16(i)))

#define load32_le(b) (le32toh(load32(b)))
#define store32_le(b, i) (store32(b, htole32(i)))
#define load32_be(b) (be32toh(load32(b)))
#define store32_be(b, i) (store32(b, htobe32(i)))

#define load64_le(b) (le64toh(load64(b)))
#define store64_le(b, i) (store64(b, htole64(i)))
#define load64_be(b) (be64toh(load64(b)))
#define store64_be(b, i) (store64(b, htobe64(i)))

#endif
16 Externals/mbedtls/3rdparty/everest/include/everest/kremlin/internal/builtin.h
View file
@@ -0,0 +1,16 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

#ifndef __KREMLIN_BUILTIN_H
#define __KREMLIN_BUILTIN_H

/* For alloca, when using KreMLin's -falloca */
#if (defined(_WIN32) || defined(_WIN64))
# include <malloc.h>
#endif

/* If some globals need to be initialized before the main, then kremlin will
* generate and try to link last a function with this type: */
void kremlinit_globals(void);

#endif
46 Externals/mbedtls/3rdparty/everest/include/everest/kremlin/internal/callconv.h
View file
@@ -0,0 +1,46 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

#ifndef __KREMLIN_CALLCONV_H
#define __KREMLIN_CALLCONV_H

/******************************************************************************/
/* Some macros to ease compatibility */
/******************************************************************************/

/* We want to generate __cdecl safely without worrying about it being undefined.
* When using MSVC, these are always defined. When using MinGW, these are
* defined too. They have no meaning for other platforms, so we define them to
* be empty macros in other situations. */
#ifndef _MSC_VER
#ifndef __cdecl
#define __cdecl
#endif
#ifndef __stdcall
#define __stdcall
#endif
#ifndef __fastcall
#define __fastcall
#endif
#endif

/* Since KreMLin emits the inline keyword unconditionally, we follow the
* guidelines at https://gcc.gnu.org/onlinedocs/gcc/Inline.html and make this
* __inline__ to ensure the code compiles with -std=c90 and earlier. */
#ifdef __GNUC__
# define inline __inline__
#endif

/* GCC-specific attribute syntax; everyone else gets the standard C inline
* attribute. */
#ifdef __GNU_C__
# ifndef __clang__
# define force_inline inline __attribute__((always_inline))
# else
# define force_inline inline
# endif
#else
# define force_inline inline
#endif

#endif
34 Externals/mbedtls/3rdparty/everest/include/everest/kremlin/internal/compat.h
View file
@@ -0,0 +1,34 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

#ifndef KRML_COMPAT_H
#define KRML_COMPAT_H

#include <inttypes.h>

/* A series of macros that define C implementations of types that are not Low*,
* to facilitate porting programs to Low*. */

typedef const char *Prims_string;

typedef struct {
uint32_t length;
const char *data;
} FStar_Bytes_bytes;

typedef int32_t Prims_pos, Prims_nat, Prims_nonzero, Prims_int,
krml_checked_int_t;

#define RETURN_OR(x) \
do { \
int64_t __ret = x; \
if (__ret < INT32_MIN || INT32_MAX < __ret) { \
KRML_HOST_PRINTF( \
"Prims.{int,nat,pos} integer overflow at %s:%d\n", __FILE__, \
__LINE__); \
KRML_HOST_EXIT(252); \
} \
return (int32_t)__ret; \
} while (0)

#endif
57 Externals/mbedtls/3rdparty/everest/include/everest/kremlin/internal/debug.h
View file
@@ -0,0 +1,57 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

#ifndef __KREMLIN_DEBUG_H
#define __KREMLIN_DEBUG_H

#include <inttypes.h>

#include "kremlin/internal/target.h"

/******************************************************************************/
/* Debugging helpers - intended only for KreMLin developers */
/******************************************************************************/

/* In support of "-wasm -d force-c": we might need this function to be
* forward-declared, because the dependency on WasmSupport appears very late,
* after SimplifyWasm, and sadly, after the topological order has been done. */
void WasmSupport_check_buffer_size(uint32_t s);

/* A series of GCC atrocities to trace function calls (kremlin's [-d c-calls]
* option). Useful when trying to debug, say, Wasm, to compare traces. */
/* clang-format off */
#ifdef __GNUC__
#define KRML_FORMAT(X) _Generic((X), \
uint8_t : "0x%08" PRIx8, \
uint16_t: "0x%08" PRIx16, \
uint32_t: "0x%08" PRIx32, \
uint64_t: "0x%08" PRIx64, \
int8_t : "0x%08" PRIx8, \
int16_t : "0x%08" PRIx16, \
int32_t : "0x%08" PRIx32, \
int64_t : "0x%08" PRIx64, \
default : "%s")

#define KRML_FORMAT_ARG(X) _Generic((X), \
uint8_t : X, \
uint16_t: X, \
uint32_t: X, \
uint64_t: X, \
int8_t : X, \
int16_t : X, \
int32_t : X, \
int64_t : X, \
default : "unknown")
/* clang-format on */

# define KRML_DEBUG_RETURN(X) \
({ \
__auto_type _ret = (X); \
KRML_HOST_PRINTF("returning: "); \
KRML_HOST_PRINTF(KRML_FORMAT(_ret), KRML_FORMAT_ARG(_ret)); \
KRML_HOST_PRINTF(" \n"); \
_ret; \
})
#endif

#endif
102 Externals/mbedtls/3rdparty/everest/include/everest/kremlin/internal/target.h
View file
@@ -0,0 +1,102 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

#ifndef __KREMLIN_TARGET_H
#define __KREMLIN_TARGET_H

#include <stdlib.h>
#include <stdio.h>
#include <stdbool.h>
#include <inttypes.h>
#include <limits.h>

#include "kremlin/internal/callconv.h"

/******************************************************************************/
/* Macros that KreMLin will generate. */
/******************************************************************************/

/* For "bare" targets that do not have a C stdlib, the user might want to use
* [-add-early-include '"mydefinitions.h"'] and override these. */
#ifndef KRML_HOST_PRINTF
# define KRML_HOST_PRINTF printf
#endif

#if ( \
(defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \
(!(defined KRML_HOST_EPRINTF)))
# define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
#endif

#ifndef KRML_HOST_EXIT
# define KRML_HOST_EXIT exit
#endif

#ifndef KRML_HOST_MALLOC
# define KRML_HOST_MALLOC malloc
#endif

#ifndef KRML_HOST_CALLOC
# define KRML_HOST_CALLOC calloc
#endif

#ifndef KRML_HOST_FREE
# define KRML_HOST_FREE free
#endif

#ifndef KRML_HOST_TIME

# include <time.h>

/* Prims_nat not yet in scope */
inline static int32_t krml_time() {
return (int32_t)time(NULL);
}

# define KRML_HOST_TIME krml_time
#endif

/* In statement position, exiting is easy. */
#define KRML_EXIT \
do { \
KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \
KRML_HOST_EXIT(254); \
} while (0)

/* In expression position, use the comma-operator and a malloc to return an
* expression of the right size. KreMLin passes t as the parameter to the macro.
*/
#define KRML_EABORT(t, msg) \
(KRML_HOST_PRINTF("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, msg), \
KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t))))

/* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
* *elements*. Do an ugly, run-time check (some of which KreMLin can eliminate).
*/

#ifdef __GNUC__
# define _KRML_CHECK_SIZE_PRAGMA \
_Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
#else
# define _KRML_CHECK_SIZE_PRAGMA
#endif

#define KRML_CHECK_SIZE(size_elt, sz) \
do { \
_KRML_CHECK_SIZE_PRAGMA \
if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \
KRML_HOST_PRINTF( \
"Maximum allocatable size exceeded, aborting before overflow at " \
"%s:%d\n", \
__FILE__, __LINE__); \
KRML_HOST_EXIT(253); \
} \
} while (0)

#if defined(_MSC_VER) && _MSC_VER < 1900
# define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
#else
# define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
#endif

#endif
61 Externals/mbedtls/3rdparty/everest/include/everest/kremlin/internal/types.h
View file
@@ -0,0 +1,61 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

#ifndef KRML_TYPES_H
#define KRML_TYPES_H

#include <inttypes.h>
#include <stdio.h>
#include <stdlib.h>

/* Types which are either abstract, meaning that have to be implemented in C, or
* which are models, meaning that they are swapped out at compile-time for
* hand-written C types (in which case they're marked as noextract). */

typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_;
typedef int64_t FStar_Int64_t, FStar_Int64_t_;
typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_;
typedef int32_t FStar_Int32_t, FStar_Int32_t_;
typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_;
typedef int16_t FStar_Int16_t, FStar_Int16_t_;
typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_;
typedef int8_t FStar_Int8_t, FStar_Int8_t_;

/* Only useful when building Kremlib, because it's in the dependency graph of
* FStar.Int.Cast. */
typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_;
typedef int64_t FStar_Int63_t, FStar_Int63_t_;

typedef double FStar_Float_float;
typedef uint32_t FStar_Char_char;
typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write;

typedef void *FStar_Dyn_dyn;

typedef const char *C_String_t, *C_String_t_;

typedef int exit_code;
typedef FILE *channel;

typedef unsigned long long TestLib_cycles;

typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan;

/* The uint128 type is a special case since we offer several implementations of
* it, depending on the compiler and whether the user wants the verified
* implementation or not. */
#if !defined(KRML_VERIFIED_UINT128) && defined(_MSC_VER) && defined(_M_X64)
# include <emmintrin.h>
typedef __m128i FStar_UInt128_uint128;
#elif !defined(KRML_VERIFIED_UINT128) && !defined(_MSC_VER)
typedef unsigned __int128 FStar_UInt128_uint128;
#else
typedef struct FStar_UInt128_uint128_s {
uint64_t low;
uint64_t high;
} FStar_UInt128_uint128;
#endif

typedef FStar_UInt128_uint128 FStar_UInt128_t, FStar_UInt128_t_, uint128_t;

#endif
5 Externals/mbedtls/3rdparty/everest/include/everest/kremlin/internal/wasmsupport.h
View file
@@ -0,0 +1,5 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

/* This file is automatically included when compiling with -wasm -d force-c */
#define WasmSupport_check_buffer_size(X)
21 Externals/mbedtls/3rdparty/everest/include/everest/vs2010/Hacl_Curve25519.h
View file
@@ -0,0 +1,21 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */

/* This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
* KreMLin invocation: /mnt/e/everest/verify/kremlin/krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrcLh -minimal -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
36 Externals/mbedtls/3rdparty/everest/include/everest/vs2010/inttypes.h
View file
@@ -0,0 +1,36 @@
/*
* 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
31 Externals/mbedtls/3rdparty/everest/include/everest/vs2010/stdbool.h
View file
@@ -0,0 +1,31 @@
/*
* 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
190 Externals/mbedtls/3rdparty/everest/include/everest/x25519.h
View file
@@ -0,0 +1,190 @@
/*
* 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 */
760 Externals/mbedtls/3rdparty/everest/library/Hacl_Curve25519.c
View file

Large diffs are not rendered by default.

41 Externals/mbedtls/3rdparty/everest/library/Hacl_Curve25519_joined.c
View file
@@ -0,0 +1,41 @@
/*
* 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) */

107 Externals/mbedtls/3rdparty/everest/library/everest.c
View file
@@ -0,0 +1,107 @@
/*
* 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 */

413 Externals/mbedtls/3rdparty/everest/library/kremlib/FStar_UInt128_extracted.c
View file

Large diffs are not rendered by default.

100 ...tls/3rdparty/everest/library/kremlib/FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.c
View file
@@ -0,0 +1,100 @@
/* 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;
}

805 Externals/mbedtls/3rdparty/everest/library/legacy/Hacl_Curve25519.c
View file

Large diffs are not rendered by default.

186 Externals/mbedtls/3rdparty/everest/library/x25519.c
View file
@@ -0,0 +1,186 @@
/*
* 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 */
240 Externals/mbedtls/CMakeLists.txt
View file
@@ -1,55 +1,250 @@
#
# 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.
# + Note: there is currently one remaining include_directories command in the
# CMake files. It is related to ZLIB support which is planned to be removed.
# When the support is removed, the associated include_directories command
# will be removed as well as this note.
# - 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.
#

cmake_minimum_required(VERSION 2.8.12)
project("mbed TLS" C)

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)
# 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()

# Set the project root directory.
set(MBEDTLS_DIR ${CMAKE_CURRENT_SOURCE_DIR})

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)

option(ENABLE_PROGRAMS "Build mbed TLS programs." OFF)

option(UNSAFE_BUILD "Allow unsafe builds. These builds ARE NOT SECURE." OFF)
option(MBEDTLS_FATAL_WARNINGS "Compiler warnings treated as errors" ON)

string(REGEX MATCH "Clang" CMAKE_COMPILER_IS_CLANG "${CMAKE_C_COMPILER_ID}")
string(REGEX MATCH "GNU" CMAKE_COMPILER_IS_GNU "${CMAKE_C_COMPILER_ID}")
string(REGEX MATCH "IAR" CMAKE_COMPILER_IS_IAR "${CMAKE_C_COMPILER_ID}")
string(REGEX MATCH "MSVC" CMAKE_COMPILER_IS_MSVC "${CMAKE_C_COMPILER_ID}")

# the test suites currently have compile errors with MSVC
if(CMAKE_COMPILER_IS_MSVC)
option(ENABLE_TESTING "Build mbed TLS tests." OFF)
else()
option(ENABLE_TESTING "Build mbed TLS tests." OFF)
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")

set(CTR_DRBG_128_BIT_KEY_WARNING "${WARNING_BORDER}"
"${CTR_DRBG_128_BIT_KEY_WARN_L1}"
"${CTR_DRBG_128_BIT_KEY_WARN_L2}"
"${CTR_DRBG_128_BIT_KEY_WARN_L3}"
"${WARNING_BORDER}")

# 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 ${MBEDTLS_PYTHON_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/scripts/config.py -f ${CMAKE_CURRENT_SOURCE_DIR}/include/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 ${MBEDTLS_PYTHON_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/scripts/config.py -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()

# 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.
function(link_to_source base_name)
# Get OS dependent path to use in `execute_process`
if (CMAKE_HOST_WIN32)
#mklink is an internal command of cmd.exe it can only work with \
string(REPLACE "/" "\\" link "${CMAKE_CURRENT_BINARY_DIR}/${base_name}")
string(REPLACE "/" "\\" target "${CMAKE_CURRENT_SOURCE_DIR}/${base_name}")
else()
set(link "${CMAKE_CURRENT_BINARY_DIR}/${base_name}")
set(target "${CMAKE_CURRENT_SOURCE_DIR}/${base_name}")
endif()

if (NOT EXISTS ${link})
if (CMAKE_HOST_UNIX)
set(command ln -s ${target} ${link})
else()
if (IS_DIRECTORY ${target})
set(command cmd.exe /c mklink /j ${link} ${target})
else()
set(command cmd.exe /c mklink /h ${link} ${target})
endif()
endif()

execute_process(COMMAND ${command}
RESULT_VARIABLE result
ERROR_VARIABLE output)

if (NOT ${result} EQUAL 0)
message(FATAL_ERROR "Could not create symbolic link for: ${target} --> ${output}")
endif()
endif()
endfunction(link_to_source)

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)
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} --warn_about_c_style_casts --warnings_are_errors -Ohz")
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")
@@ -61,6 +256,17 @@ else()
set(LIB_INSTALL_DIR lib)
endif()

include_directories(include/)
if(ENABLE_ZLIB_SUPPORT)
find_package(ZLIB)

if(ZLIB_FOUND)
include_directories(${ZLIB_INCLUDE_DIR})
endif(ZLIB_FOUND)
endif(ENABLE_ZLIB_SUPPORT)

add_subdirectory(include)

add_subdirectory(3rdparty)
list(APPEND libs ${thirdparty_lib})

add_subdirectory(library)
204 Externals/mbedtls/LICENSE
View file
@@ -1,2 +1,202 @@
Unless specifically indicated otherwise in a file, files are licensed
under the Apache 2.0 license, as can be found in: apache-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.
202 Externals/mbedtls/apache-2.0.txt
View file

This file was deleted.

8 Externals/mbedtls/include/CMakeLists.txt
View file
@@ -3,14 +3,20 @@ option(INSTALL_MBEDTLS_HEADERS "Install mbed TLS headers." ON)
if(INSTALL_MBEDTLS_HEADERS)

file(GLOB headers "mbedtls/*.h")
file(GLOB psa_headers "psa/*.h")

install(FILES ${headers}
DESTINATION include/mbedtls
PERMISSIONS OWNER_READ OWNER_WRITE GROUP_READ WORLD_READ)

install(FILES ${psa_headers}
DESTINATION include/psa
PERMISSIONS OWNER_READ OWNER_WRITE GROUP_READ WORLD_READ)

endif(INSTALL_MBEDTLS_HEADERS)

# Make config.h available in an out-of-source build. ssl-opt.sh requires it.
if (NOT ${CMAKE_CURRENT_BINARY_DIR} STREQUAL ${CMAKE_CURRENT_SOURCE_DIR})
if (ENABLE_TESTING AND NOT ${CMAKE_CURRENT_BINARY_DIR} STREQUAL ${CMAKE_CURRENT_SOURCE_DIR})
link_to_source(mbedtls)
link_to_source(psa)
endif()