update hacl to ad60c9d98c9ce8f6a4fa13090511fa4b3a2c137b (#426)

cryspen · Sep 27, 2023 · bb6620a · bb6620a
1 parent c6d3969
commit bb6620a
Show file tree

Hide file tree

Showing 142 changed files with 2,244 additions and 2,003 deletions.
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
@@ -40,7 +40,7 @@ jobs:
       matrix:
         os:
           - macos-latest
-          - ubuntu-latest
+          # - ubuntu-latest Disabling Ubuntu for now as long as bindgen is broken
           - windows-latest
 
     runs-on: ${{ matrix.os }}
@@ -95,7 +95,7 @@ jobs:
         bits: [32, 64]
         os:
           - macos-latest
-          - ubuntu-latest
+          # - ubuntu-latest disable for now
           - windows-latest
         exclude:
           - bits: 32
@@ -122,7 +122,7 @@ jobs:
       - if: matrix.os == 'ubuntu-latest'
         run: |
           sudo apt-get update
-          sudo apt-get install ninja-build gcc-multilib g++-multilib
+          sudo apt-get install ninja-build gcc-multilib g++-multilib clang-15
           rustup target add i686-unknown-linux-gnu
 
       - name: Setup | Developer Command Prompt (x86)

diff --git a/config/default_config.cmake b/config/default_config.cmake
@@ -7,10 +7,10 @@ set(SOURCES_std
 	${PROJECT_SOURCE_DIR}/src/Hacl_HMAC.c
 	${PROJECT_SOURCE_DIR}/src/Hacl_Hash_SHA2.c
 	${PROJECT_SOURCE_DIR}/src/Hacl_Hash_Blake2.c
-	${PROJECT_SOURCE_DIR}/src/Lib_Memzero0.c
 	${PROJECT_SOURCE_DIR}/src/Hacl_Ed25519.c
 	${PROJECT_SOURCE_DIR}/src/Hacl_EC_Ed25519.c
 	${PROJECT_SOURCE_DIR}/src/Hacl_Hash_Base.c
+	${PROJECT_SOURCE_DIR}/src/Lib_Memzero0.c
 	${PROJECT_SOURCE_DIR}/src/Hacl_Streaming_Blake2.c
 	${PROJECT_SOURCE_DIR}/src/Hacl_Bignum256_32.c
 	${PROJECT_SOURCE_DIR}/src/Hacl_Bignum.c
@@ -42,10 +42,10 @@ set(SOURCES_std
 	${PROJECT_SOURCE_DIR}/src/Hacl_Frodo64.c
 	${PROJECT_SOURCE_DIR}/src/EverCrypt_DRBG.c
 	${PROJECT_SOURCE_DIR}/src/Lib_RandomBuffer_System.c
-	${PROJECT_SOURCE_DIR}/src/Lib_Memzero0.c
 	${PROJECT_SOURCE_DIR}/src/EverCrypt_HMAC.c
 	${PROJECT_SOURCE_DIR}/src/EverCrypt_Hash.c
 	${PROJECT_SOURCE_DIR}/src/EverCrypt_AutoConfig2.c
+	${PROJECT_SOURCE_DIR}/src/Lib_Memzero0.c
 	${PROJECT_SOURCE_DIR}/src/EverCrypt_Ed25519.c
 	${PROJECT_SOURCE_DIR}/src/EverCrypt_Curve25519.c
 	${PROJECT_SOURCE_DIR}/src/EverCrypt_HKDF.c
@@ -124,7 +124,6 @@ set(INCLUDES
 	${PROJECT_SOURCE_DIR}/include/Hacl_HMAC.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Hash_SHA2.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2.h
-	${PROJECT_SOURCE_DIR}/include/Lib_Memzero0.h
 	${PROJECT_SOURCE_DIR}/include/internal/Hacl_Ed25519.h
 	${PROJECT_SOURCE_DIR}/include/internal/Hacl_Hash_SHA2.h
 	${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA2.h
@@ -143,6 +142,7 @@ set(INCLUDES
 	${PROJECT_SOURCE_DIR}/include/internal/Hacl_Hash_Blake2.h
 	${PROJECT_SOURCE_DIR}/include/internal/Hacl_Impl_Blake2_Constants.h
 	${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_Blake2.h
+	${PROJECT_SOURCE_DIR}/include/lib_memzero0.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Blake2.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2b_256.h
 	${PROJECT_SOURCE_DIR}/include/libintvector.h
@@ -265,7 +265,6 @@ set(PUBLIC_INCLUDES
 	${PROJECT_SOURCE_DIR}/include/Hacl_HMAC.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Hash_SHA2.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2.h
-	${PROJECT_SOURCE_DIR}/include/Lib_Memzero0.h
 	${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_SHA2.h
 	${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Curve25519_51.h
 	${PROJECT_SOURCE_DIR}/include/lib_intrinsics.h
@@ -276,6 +275,7 @@ set(PUBLIC_INCLUDES
 	${PROJECT_SOURCE_DIR}/include/Hacl_EC_Ed25519.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Base.h
 	${PROJECT_SOURCE_DIR}/include/internal/../Hacl_Hash_Blake2.h
+	${PROJECT_SOURCE_DIR}/include/lib_memzero0.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Streaming_Blake2.h
 	${PROJECT_SOURCE_DIR}/include/Hacl_Hash_Blake2b_256.h
 	${PROJECT_SOURCE_DIR}/include/libintvector.h

diff --git a/include/EverCrypt_AEAD.h b/include/EverCrypt_AEAD.h
@@ -42,6 +42,10 @@ extern "C" {
 
 typedef struct EverCrypt_AEAD_state_s_s EverCrypt_AEAD_state_s;
 
+/**
+Both encryption and decryption require a state that holds the key.
+The state may be reused as many times as desired.
+*/
 bool EverCrypt_AEAD_uu___is_Ek(Spec_Agile_AEAD_alg a, EverCrypt_AEAD_state_s projectee);
 
 /**

diff --git a/include/EverCrypt_DRBG.h b/include/EverCrypt_DRBG.h
@@ -36,7 +36,6 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "Lib_RandomBuffer_System.h"
-#include "Lib_Memzero0.h"
 #include "Hacl_Streaming_Types.h"
 #include "Hacl_HMAC_DRBG.h"
 

diff --git a/include/Hacl_Frodo1344.h b/include/Hacl_Frodo1344.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo1344_crypto_bytes;

diff --git a/include/Hacl_Frodo64.h b/include/Hacl_Frodo64.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 /*

diff --git a/include/Hacl_Frodo640.h b/include/Hacl_Frodo640.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo640_crypto_bytes;

diff --git a/include/Hacl_Frodo976.h b/include/Hacl_Frodo976.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo976_crypto_bytes;

diff --git a/include/Hacl_Hash_Blake2.h b/include/Hacl_Hash_Blake2.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Krmllib.h"
 
 void Hacl_Blake2b_32_blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn);

diff --git a/include/Hacl_Hash_Blake2b_256.h b/include/Hacl_Hash_Blake2b_256.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Krmllib.h"
 #include "libintvector.h"
 

diff --git a/include/Hacl_Hash_Blake2s_128.h b/include/Hacl_Hash_Blake2s_128.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "libintvector.h"
 
 void

diff --git a/include/Hacl_Krmllib.h b/include/Hacl_Krmllib.h
@@ -35,9 +35,9 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b);
+static KRML_NOINLINE uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b);
 
-static inline uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b);
+static KRML_NOINLINE uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b);
 
 static inline FStar_UInt128_uint128
 FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);

diff --git a/include/Lib_Memzero0.h b/include/Lib_Memzero0.h
diff --git a/include/TestLib.h b/include/TestLib.h
@@ -55,7 +55,8 @@ extern void TestLib_checku32(uint32_t uu___, uint32_t uu___1);
 
 extern void TestLib_checku64(uint64_t uu___, uint64_t uu___1);
 
-extern void TestLib_compare_and_print(C_String_t uu___, uint8_t *b1, uint8_t *b2, uint32_t l);
+extern void
+TestLib_compare_and_print(Prims_string uu___, uint8_t *b1, uint8_t *b2, uint32_t l);
 
 extern uint8_t *TestLib_unsafe_malloc(uint32_t l);
 

diff --git a/include/internal/Hacl_Bignum_Base.h b/include/internal/Hacl_Bignum_Base.h
@@ -401,6 +401,7 @@ Hacl_Bignum_Multiplication_bn_sqr_u32(uint32_t aLen, uint32_t *a, uint32_t *res)
     res[i0 + i0] = r;
   }
   uint32_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u32(aLen + aLen, res, res, res);
+  KRML_HOST_IGNORE(c0);
   KRML_CHECK_SIZE(sizeof (uint32_t), aLen + aLen);
   uint32_t tmp[aLen + aLen];
   memset(tmp, 0U, (aLen + aLen) * sizeof (uint32_t));
@@ -413,6 +414,7 @@ Hacl_Bignum_Multiplication_bn_sqr_u32(uint32_t aLen, uint32_t *a, uint32_t *res)
     tmp[(uint32_t)2U * i + (uint32_t)1U] = hi;
   }
   uint32_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u32(aLen + aLen, res, tmp, res);
+  KRML_HOST_IGNORE(c1);
 }
 
 static inline void
@@ -450,6 +452,7 @@ Hacl_Bignum_Multiplication_bn_sqr_u64(uint32_t aLen, uint64_t *a, uint64_t *res)
     res[i0 + i0] = r;
   }
   uint64_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u64(aLen + aLen, res, res, res);
+  KRML_HOST_IGNORE(c0);
   KRML_CHECK_SIZE(sizeof (uint64_t), aLen + aLen);
   uint64_t tmp[aLen + aLen];
   memset(tmp, 0U, (aLen + aLen) * sizeof (uint64_t));
@@ -462,6 +465,7 @@ Hacl_Bignum_Multiplication_bn_sqr_u64(uint32_t aLen, uint64_t *a, uint64_t *res)
     tmp[(uint32_t)2U * i + (uint32_t)1U] = hi;
   }
   uint64_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u64(aLen + aLen, res, tmp, res);
+  KRML_HOST_IGNORE(c1);
 }
 
 #if defined(__cplusplus)

diff --git a/include/internal/Hacl_Krmllib.h b/include/internal/Hacl_Krmllib.h
@@ -37,13 +37,13 @@ extern "C" {
 
 #include "../Hacl_Krmllib.h"
 
-static inline uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b);
+static KRML_NOINLINE uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b);
 
-static inline uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b);
+static KRML_NOINLINE uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b);
 
-static inline uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b);
+static KRML_NOINLINE uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b);
 
-static inline uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b);
+static KRML_NOINLINE uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b);
 
 static inline FStar_UInt128_uint128
 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);

diff --git a/include/lib_intrinsics.h b/include/lib_intrinsics.h
@@ -8,15 +8,20 @@
 #endif
 #endif
 
-#if defined(HACL_CAN_COMPILE_INTRINSICS)
-#if defined(_MSC_VER)
-#include <immintrin.h>
-#else
-#include <x86intrin.h>
-#endif
-#endif
+/*
+   GCC versions prior to 5.5 incorrectly optimize certain intrinsics.
+
+   See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81300
+
+   CLANG versions prior to 5 crash on certain intrinsics.
+
+   See https://bugs.llvm.org/show_bug.cgi?id=24943
+*/
 
-#if !defined(HACL_CAN_COMPILE_INTRINSICS)
+#if !defined(HACL_CAN_COMPILE_INTRINSICS) || \
+    (defined(__clang__) && (__clang_major__ < 5)) || \
+    (defined(__GNUC__) && !defined(__clang__) &&  \
+     (__GNUC__ < 5 || (__GNUC__ == 5 && (__GNUC_MINOR__ < 5))))
 
 #include "Hacl_IntTypes_Intrinsics.h"
 
@@ -25,58 +30,63 @@
 #include "Hacl_IntTypes_Intrinsics_128.h"
 
 #define Lib_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4) \
-  (Hacl_IntTypes_Intrinsics_128_add_carry_u64(x1, x2, x3, x4))
+    (Hacl_IntTypes_Intrinsics_128_add_carry_u64(x1, x2, x3, x4))
 
 #define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4) \
-  (Hacl_IntTypes_Intrinsics_128_sub_borrow_u64(x1, x2, x3, x4))
+    (Hacl_IntTypes_Intrinsics_128_sub_borrow_u64(x1, x2, x3, x4))
 
 #else
 
 #define Lib_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4) \
-  (Hacl_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4))
+    (Hacl_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4))
 
 #define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4) \
-  (Hacl_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4))
+    (Hacl_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4))
 
 #endif // defined(HACL_CAN_COMPILE_UINT128)
 
 #define Lib_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4) \
-  (Hacl_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4))
+    (Hacl_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4))
 
 #define Lib_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4) \
-  (Hacl_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4))
+    (Hacl_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4))
 
 #else // !defined(HACL_CAN_COMPILE_INTRINSICS)
 
+#if defined(_MSC_VER)
+#include <immintrin.h>
+#else
+#include <x86intrin.h>
+#endif
+
 #define Lib_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4) \
-  (_addcarry_u32(x1, x2, x3, (unsigned int *) x4))
+    (_addcarry_u32(x1, x2, x3, (unsigned int *)x4))
 
 #define Lib_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4) \
-  (_addcarry_u64(x1, x2, x3, (long long unsigned int *) x4))
-
+    (_addcarry_u64(x1, x2, x3, (long long unsigned int *)x4))
 
 /*
    GCC versions prior to 7.2 pass arguments to _subborrow_u{32,64}
    in an incorrect order.
 
    See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81294
 */
-#if defined(__GNUC__) && !defined (__clang__) && \
-  (__GNUC__ < 7 || (__GNUC__ == 7 && (__GNUC_MINOR__ < 2)))
+#if defined(__GNUC__) && !defined(__clang__) && \
+    (__GNUC__ < 7 || (__GNUC__ == 7 && (__GNUC_MINOR__ < 2)))
 
 #define Lib_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4) \
-  (_subborrow_u32(x1, x3, x2, (unsigned int *) x4))
+    (_subborrow_u32(x1, x3, x2, (unsigned int *)x4))
 
 #define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4) \
-  (_subborrow_u64(x1, x3, x2, (long long unsigned int *) x4))
+    (_subborrow_u64(x1, x3, x2, (long long unsigned int *)x4))
 
 #else
 
-#define Lib_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4)  \
-  (_subborrow_u32(x1, x2, x3, (unsigned int *) x4))
+#define Lib_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4) \
+    (_subborrow_u32(x1, x2, x3, (unsigned int *)x4))
 
-#define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4)  \
-  (_subborrow_u64(x1, x2, x3, (long long unsigned int *) x4))
+#define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4) \
+    (_subborrow_u64(x1, x2, x3, (long long unsigned int *)x4))
 
 #endif // GCC < 7.2
 

diff --git a/include/lib_memzero0.h b/include/lib_memzero0.h
@@ -0,0 +1,5 @@
+#include <inttypes.h>
+
+void Lib_Memzero0_memzero0(void *dst, uint64_t len);
+
+#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t))