update to hacl 1a20576fc736d51e1ab3c317b46ba81560b75786

sys/hacl/build.rs

@@ -169,12 +169,16 @@ fn compile_files(
         .files(
             files
                 .iter()
-                .map(|fname| src_prefix.join(fname))
+                .map(|fname| {
+                    if fname == "hacl.c" {
+                        home_path.join("c").join("config").join(fname)
+                    } else {
+                        src_prefix.join(fname)
+                    }
+                })
                 .chain(vale_files.iter().map(|fname| vale_prefix.join(fname))),
         )
-        .file(home_path.join("c").join("config").join("hacl.c"))
-        // XXX: There are too many warnings for now
-        .warnings(false);
+        .warnings_into_errors(true);
 
     for include in includes(platform, home_path, "") {
         build.include(include);
@@ -193,6 +197,7 @@ fn compile_files(
 
 fn build(platform: &Platform, home_path: &Path) {
     let files = svec![
+        "hacl.c",
         "Hacl_NaCl.c",
         "Hacl_Salsa20.c",
         "Hacl_Poly1305_32.c",

sys/hacl/c/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);
 
 /**

sys/hacl/c/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"
 

sys/hacl/c/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;

sys/hacl/c/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"
 
 /*

sys/hacl/c/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;

sys/hacl/c/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;

sys/hacl/c/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);

sys/hacl/c/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"
 

sys/hacl/c/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

sys/hacl/c/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);

sys/hacl/c/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.

sys/hacl/c/include/Lib_Memzero0.h

@@ -1,45 +1,5 @@
-/* MIT License
- *
- * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
- * Copyright (c) 2022-2023 HACL* Contributors
- *
- * Permission is hereby granted, free of charge, to any person obtaining a copy
- * of this software and associated documentation files (the "Software"), to deal
- * in the Software without restriction, including without limitation the rights
- * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
- * copies of the Software, and to permit persons to whom the Software is
- * furnished to do so, subject to the following conditions:
- *
- * The above copyright notice and this permission notice shall be included in all
- * copies or substantial portions of the Software.
- *
- * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
- * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
- * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
- * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
- * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
- * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
- * SOFTWARE.
- */
+#include <inttypes.h>
 
+void Lib_Memzero0_memzero0(void *dst, uint64_t len);
 
-#ifndef __Lib_Memzero0_H
-#define __Lib_Memzero0_H
-
-#if defined(__cplusplus)
-extern "C" {
-#endif
-
-#include <string.h>
-#include "krml/internal/types.h"
-#include "krml/lowstar_endianness.h"
-#include "krml/internal/target.h"
-
-extern void Lib_Memzero0_memzero(void *x0, uint64_t x1);
-
-#if defined(__cplusplus)
-}
-#endif
-
-#define __Lib_Memzero0_H_DEFINED
-#endif
+#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t))

sys/hacl/c/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);
 

sys/hacl/c/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];

sys/hacl/c/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)

sys/hacl/c/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);