update HACL to 1b30697fc2b0d8d5e2f541eccfd3fb52b45b905c (#429)

CMakeLists.txt

@@ -93,12 +93,9 @@ if(NOT MSVC)
         # -pedantic
         # -Wconversion
         # -Wsign-conversion
-        # -Werror=gcc-compat
         $<$<CONFIG:DEBUG>:-g>
         $<$<CONFIG:DEBUG>:-Og>
         $<$<CONFIG:RELEASE>:-O3>
-        # $<$<CONFIG:RELEASE>:-g>
-        # $<$<CONFIG:RELEASE>:-Wno-deprecated-declarations>
     )
 endif()
 
@@ -337,6 +334,9 @@ configure_file(config/Config.h.in config.h)
 # Now combine everything into the hacl library
 # # Dynamic library
 add_library(hacl SHARED ${SOURCES_std} ${VALE_OBJECTS})
+if(NOT MSVC)
+    target_compile_options(hacl PRIVATE -Wsign-conversion -Wconversion -Wall -Wextra -pedantic)
+endif()
 
 if(TOOLCHAIN_CAN_COMPILE_VEC128 AND HACL_VEC128_O)
     add_dependencies(hacl hacl_vec128)

include/Hacl_RSAPSS.h

@@ -43,9 +43,9 @@ extern "C" {
 Sign a message `msg` and write the signature to `sgnt`.
 
 @param a Hash algorithm to use. Allowed values for `a` are ...
-  * Spec_Hash_Definitions_SHA2_256,
-  * Spec_Hash_Definitions_SHA2_384, and
-  * Spec_Hash_Definitions_SHA2_512.
+  - Spec_Hash_Definitions_SHA2_256,
+  - Spec_Hash_Definitions_SHA2_384, and
+  - Spec_Hash_Definitions_SHA2_512.
 @param modBits Count of bits in the modulus (`n`).
 @param eBits Count of bits in `e` value.
 @param dBits Count of bits in `d` value.
@@ -75,7 +75,10 @@ Hacl_RSAPSS_rsapss_sign(
 /**
 Verify the signature `sgnt` of a message `msg`.
 
-@param a Hash algorithm to use.
+@param a Hash algorithm to use. Allowed values for `a` are ...
+  - Spec_Hash_Definitions_SHA2_256,
+  - Spec_Hash_Definitions_SHA2_384, and
+  - Spec_Hash_Definitions_SHA2_512.
 @param modBits Count of bits in the modulus (`n`).
 @param eBits Count of bits in `e` value.
 @param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`.
@@ -105,10 +108,10 @@ Load a public key from key parts.
 
 @param modBits Count of bits in modulus (`n`).
 @param eBits Count of bits in `e` value.
-@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
-@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
+@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
+@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
 
-@return Returns an allocated public key. Note: caller must take care to `free()` the created key.
+@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key.
 */
 uint64_t
 *Hacl_RSAPSS_new_rsapss_load_pkey(uint32_t modBits, uint32_t eBits, uint8_t *nb, uint8_t *eb);
@@ -119,11 +122,11 @@ Load a secret key from key parts.
 @param modBits Count of bits in modulus (`n`).
 @param eBits Count of bits in `e` value.
 @param dBits Count of bits in `d` value.
-@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
-@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
-@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from.
+@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
+@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
+@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.
 
-@return Returns an allocated secret key. Note: caller must take care to `free()` the created key.
+@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key.
 */
 uint64_t
 *Hacl_RSAPSS_new_rsapss_load_skey(
@@ -138,13 +141,16 @@ uint64_t
 /**
 Sign a message `msg` and write the signature to `sgnt`.
 
-@param a Hash algorithm to use.
+@param a Hash algorithm to use. Allowed values for `a` are ...
+  - Spec_Hash_Definitions_SHA2_256,
+  - Spec_Hash_Definitions_SHA2_384, and
+  - Spec_Hash_Definitions_SHA2_512.
 @param modBits Count of bits in the modulus (`n`).
 @param eBits Count of bits in `e` value.
 @param dBits Count of bits in `d` value.
-@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
-@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
-@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from.
+@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
+@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
+@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.
 @param saltLen Length of salt.
 @param salt Pointer to `saltLen` bytes where the salt is read from.
 @param msgLen Length of message.
@@ -172,11 +178,14 @@ Hacl_RSAPSS_rsapss_skey_sign(
 /**
 Verify the signature `sgnt` of a message `msg`.
 
-@param a Hash algorithm to use.
+@param a Hash algorithm to use. Allowed values for `a` are ...
+  - Spec_Hash_Definitions_SHA2_256,
+  - Spec_Hash_Definitions_SHA2_384, and
+  - Spec_Hash_Definitions_SHA2_512.
 @param modBits Count of bits in the modulus (`n`).
 @param eBits Count of bits in `e` value.
-@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
-@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
+@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
+@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
 @param saltLen Length of salt.
 @param sgntLen Length of signature.
 @param sgnt Pointer to `sgntLen` bytes where the signature is read from.

include/internal/Hacl_Bignum25519_51.h

@@ -84,6 +84,7 @@ Hacl_Impl_Curve25519_Field51_fmul(
   FStar_UInt128_uint128 *uu___
 )
 {
+  KRML_HOST_IGNORE(uu___);
   uint64_t f10 = f1[0U];
   uint64_t f11 = f1[1U];
   uint64_t f12 = f1[2U];
@@ -167,6 +168,7 @@ Hacl_Impl_Curve25519_Field51_fmul2(
   FStar_UInt128_uint128 *uu___
 )
 {
+  KRML_HOST_IGNORE(uu___);
   uint64_t f10 = f1[0U];
   uint64_t f11 = f1[1U];
   uint64_t f12 = f1[2U];
@@ -371,6 +373,7 @@ static inline void Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f
 static inline void
 Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
 {
+  KRML_HOST_IGNORE(uu___);
   uint64_t f0 = f[0U];
   uint64_t f1 = f[1U];
   uint64_t f2 = f[2U];
@@ -446,6 +449,7 @@ Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint
 static inline void
 Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
 {
+  KRML_HOST_IGNORE(uu___);
   uint64_t f10 = f[0U];
   uint64_t f11 = f[1U];
   uint64_t f12 = f[2U];

include/msvc/Hacl_RSAPSS.h

@@ -43,9 +43,9 @@ extern "C" {
 Sign a message `msg` and write the signature to `sgnt`.
 
 @param a Hash algorithm to use. Allowed values for `a` are ...
-  * Spec_Hash_Definitions_SHA2_256,
-  * Spec_Hash_Definitions_SHA2_384, and
-  * Spec_Hash_Definitions_SHA2_512.
+  - Spec_Hash_Definitions_SHA2_256,
+  - Spec_Hash_Definitions_SHA2_384, and
+  - Spec_Hash_Definitions_SHA2_512.
 @param modBits Count of bits in the modulus (`n`).
 @param eBits Count of bits in `e` value.
 @param dBits Count of bits in `d` value.
@@ -75,7 +75,10 @@ Hacl_RSAPSS_rsapss_sign(
 /**
 Verify the signature `sgnt` of a message `msg`.
 
-@param a Hash algorithm to use.
+@param a Hash algorithm to use. Allowed values for `a` are ...
+  - Spec_Hash_Definitions_SHA2_256,
+  - Spec_Hash_Definitions_SHA2_384, and
+  - Spec_Hash_Definitions_SHA2_512.
 @param modBits Count of bits in the modulus (`n`).
 @param eBits Count of bits in `e` value.
 @param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`.
@@ -105,10 +108,10 @@ Load a public key from key parts.
 
 @param modBits Count of bits in modulus (`n`).
 @param eBits Count of bits in `e` value.
-@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
-@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
+@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
+@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
 
-@return Returns an allocated public key. Note: caller must take care to `free()` the created key.
+@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key.
 */
 uint64_t
 *Hacl_RSAPSS_new_rsapss_load_pkey(uint32_t modBits, uint32_t eBits, uint8_t *nb, uint8_t *eb);
@@ -119,11 +122,11 @@ Load a secret key from key parts.
 @param modBits Count of bits in modulus (`n`).
 @param eBits Count of bits in `e` value.
 @param dBits Count of bits in `d` value.
-@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
-@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
-@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from.
+@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
+@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
+@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.
 
-@return Returns an allocated secret key. Note: caller must take care to `free()` the created key.
+@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key.
 */
 uint64_t
 *Hacl_RSAPSS_new_rsapss_load_skey(
@@ -138,13 +141,16 @@ uint64_t
 /**
 Sign a message `msg` and write the signature to `sgnt`.
 
-@param a Hash algorithm to use.
+@param a Hash algorithm to use. Allowed values for `a` are ...
+  - Spec_Hash_Definitions_SHA2_256,
+  - Spec_Hash_Definitions_SHA2_384, and
+  - Spec_Hash_Definitions_SHA2_512.
 @param modBits Count of bits in the modulus (`n`).
 @param eBits Count of bits in `e` value.
 @param dBits Count of bits in `d` value.
-@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
-@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
-@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value is read from.
+@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
+@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
+@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.
 @param saltLen Length of salt.
 @param salt Pointer to `saltLen` bytes where the salt is read from.
 @param msgLen Length of message.
@@ -172,11 +178,14 @@ Hacl_RSAPSS_rsapss_skey_sign(
 /**
 Verify the signature `sgnt` of a message `msg`.
 
-@param a Hash algorithm to use.
+@param a Hash algorithm to use. Allowed values for `a` are ...
+  - Spec_Hash_Definitions_SHA2_256,
+  - Spec_Hash_Definitions_SHA2_384, and
+  - Spec_Hash_Definitions_SHA2_512.
 @param modBits Count of bits in the modulus (`n`).
 @param eBits Count of bits in `e` value.
-@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`) is read from.
-@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value is read from.
+@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.
+@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.
 @param saltLen Length of salt.
 @param sgntLen Length of signature.
 @param sgnt Pointer to `sgntLen` bytes where the signature is read from.

include/msvc/internal/Hacl_Bignum25519_51.h

@@ -84,6 +84,7 @@ Hacl_Impl_Curve25519_Field51_fmul(
   FStar_UInt128_uint128 *uu___
 )
 {
+  KRML_HOST_IGNORE(uu___);
   uint64_t f10 = f1[0U];
   uint64_t f11 = f1[1U];
   uint64_t f12 = f1[2U];
@@ -167,6 +168,7 @@ Hacl_Impl_Curve25519_Field51_fmul2(
   FStar_UInt128_uint128 *uu___
 )
 {
+  KRML_HOST_IGNORE(uu___);
   uint64_t f10 = f1[0U];
   uint64_t f11 = f1[1U];
   uint64_t f12 = f1[2U];
@@ -371,6 +373,7 @@ static inline void Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f
 static inline void
 Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
 {
+  KRML_HOST_IGNORE(uu___);
   uint64_t f0 = f[0U];
   uint64_t f1 = f[1U];
   uint64_t f2 = f[2U];
@@ -446,6 +449,7 @@ Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint
 static inline void
 Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
 {
+  KRML_HOST_IGNORE(uu___);
   uint64_t f10 = f[0U];
   uint64_t f11 = f[1U];
   uint64_t f12 = f[2U];

info.txt

@@ -1,5 +1,5 @@
 The code was generated with the following toolchain.
-F* version: 155853a14336aa0713dba7db5408f4c8ab512a06
-KaRaMeL version: db63c1de17565be0ec4989f58532717a04e3ff40
-HACL* version: ad60c9d98c9ce8f6a4fa13090511fa4b3a2c137b
+F* version: bc622701c668f6b4092760879372968265d4a4e1
+KaRaMeL version: 7cffd27cfefbd220e986e561e8d350f043609f76
+HACL* version: 1b30697fc2b0d8d5e2f541eccfd3fb52b45b905c
 Vale version: 0.3.19

karamel/include/krml/internal/target.h

@@ -57,6 +57,14 @@
 #  define KRML_HOST_IGNORE(x) (void)(x)
 #endif
 
+#ifndef KRML_MAYBE_UNUSED
+#  if defined(__GNUC__)
+#    define KRML_MAYBE_UNUSED __attribute__((unused))
+#  else
+#    define KRML_MAYBE_UNUSED
+#  endif
+#endif
+
 #ifndef KRML_NOINLINE
 #  if defined(_MSC_VER)
 #    define KRML_NOINLINE __declspec(noinline)

karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h

@@ -110,15 +110,15 @@ inline static uint128_t FStar_UInt128_mul_wide(uint64_t x, uint64_t y) {
 inline static uint128_t FStar_UInt128_eq_mask(uint128_t x, uint128_t y) {
   uint64_t mask =
       FStar_UInt64_eq_mask((uint64_t)(x >> 64), (uint64_t)(y >> 64)) &
-      FStar_UInt64_eq_mask(x, y);
+      FStar_UInt64_eq_mask((uint64_t)x, (uint64_t)y);
   return ((uint128_t)mask) << 64 | mask;
 }
 
 inline static uint128_t FStar_UInt128_gte_mask(uint128_t x, uint128_t y) {
   uint64_t mask =
       (FStar_UInt64_gte_mask(x >> 64, y >> 64) &
        ~(FStar_UInt64_eq_mask(x >> 64, y >> 64))) |
-      (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask(x, y));
+      (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask((uint64_t)x, (uint64_t)y));
   return ((uint128_t)mask) << 64 | mask;
 }