[CI] update code

include/Hacl_Ed25519.h

@@ -47,16 +47,16 @@ extern "C" {
 /**
 Compute the public key from the private key.
 
- The outparam `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ @param[out] public_key Points to 32 bytes of valid memory, i.e., `uint8_t[32]`. Must not overlap the memory location of `private_key`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 */
 void Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key);
 
 /**
 Compute the expanded keys for an Ed25519 signature.
 
- The outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ @param[out] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`. Must not overlap the memory location of `private_key`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 
  If one needs to sign several messages under the same private key, it is more efficient
  to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -66,11 +66,10 @@ void Hacl_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key);
 /**
 Create an Ed25519 signature with the (precomputed) expanded keys.
 
- The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
- The argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
-
- The argument `expanded_keys` is obtained through `expand_keys`.
+ @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `expanded_keys` nor `msg`.
+ @param[in] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`, containing the expanded keys obtained by invoking `expand_keys`.
+ @param[in] msg_len Length of `msg`.
+ @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
  If one needs to sign several messages under the same private key, it is more efficient
  to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -86,9 +85,10 @@ Hacl_Ed25519_sign_expanded(
 /**
 Create an Ed25519 signature.
 
- The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+ @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `private_key` nor `msg`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
+ @param[in] msg_len Length of `msg`.
+ @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
  The function first calls `expand_keys` and then invokes `sign_expanded`.
 
@@ -101,11 +101,12 @@ Hacl_Ed25519_sign(uint8_t *signature, uint8_t *private_key, uint32_t msg_len, ui
 /**
 Verify an Ed25519 signature.
 
- The function returns `true` if the signature is valid and `false` otherwise.
+ @param public_key Points to 32 bytes of valid memory containing the public key, i.e., `uint8_t[32]`.
+ @param msg_len Length of `msg`.
+ @param msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
+ @param signature Points to 64 bytes of valid memory containing the signature, i.e., `uint8_t[64]`.
 
- The argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
- The argument `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
+ @return Returns `true` if the signature is valid and `false` otherwise.
 */
 bool
 Hacl_Ed25519_verify(uint8_t *public_key, uint32_t msg_len, uint8_t *msg, uint8_t *signature);

include/internal/Hacl_Hash_Blake2b.h

@@ -38,6 +38,21 @@ extern "C" {
 #include "internal/Hacl_Impl_Blake2_Constants.h"
 #include "../Hacl_Hash_Blake2b.h"
 
+typedef struct Hacl_Hash_Blake2s_blake2_params_s
+{
+ uint8_t digest_length;
+ uint8_t key_length;
+ uint8_t fanout;
+ uint8_t depth;
+ uint32_t leaf_length;
+ uint64_t node_offset;
+ uint8_t node_depth;
+ uint8_t inner_length;
+ uint8_t *salt;
+ uint8_t *personal;
+}
+Hacl_Hash_Blake2s_blake2_params;
+
 void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn);
 
 void

include/internal/Hacl_Hash_Blake2b_Simd256.h

@@ -36,6 +36,7 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "../Hacl_Hash_Blake2b_Simd256.h"
 #include "libintvector.h"
 

include/internal/Hacl_Hash_Blake2s.h

@@ -36,6 +36,7 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "../Hacl_Hash_Blake2s.h"
 
 void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn);

include/internal/Hacl_Hash_Blake2s_Simd128.h

@@ -36,6 +36,7 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "../Hacl_Hash_Blake2s_Simd128.h"
 #include "libintvector.h"
 

include/lib_memzero0.h

@@ -2,4 +2,4 @@
 
 void Lib_Memzero0_memzero0(void *dst, uint64_t len);
 
-#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t))
+#define Lib_Memzero0_memzero(dst, len, t, _ret_t) Lib_Memzero0_memzero0(dst, len * sizeof(t))

include/msvc/Hacl_Ed25519.h

@@ -47,16 +47,16 @@ extern "C" {
 /**
 Compute the public key from the private key.
 
- The outparam `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ @param[out] public_key Points to 32 bytes of valid memory, i.e., `uint8_t[32]`. Must not overlap the memory location of `private_key`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 */
 void Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key);
 
 /**
 Compute the expanded keys for an Ed25519 signature.
 
- The outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ @param[out] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`. Must not overlap the memory location of `private_key`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 
  If one needs to sign several messages under the same private key, it is more efficient
  to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -66,11 +66,10 @@ void Hacl_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key);
 /**
 Create an Ed25519 signature with the (precomputed) expanded keys.
 
- The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
- The argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
-
- The argument `expanded_keys` is obtained through `expand_keys`.
+ @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `expanded_keys` nor `msg`.
+ @param[in] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`, containing the expanded keys obtained by invoking `expand_keys`.
+ @param[in] msg_len Length of `msg`.
+ @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
  If one needs to sign several messages under the same private key, it is more efficient
  to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -86,9 +85,10 @@ Hacl_Ed25519_sign_expanded(
 /**
 Create an Ed25519 signature.
 
- The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+ @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `private_key` nor `msg`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
+ @param[in] msg_len Length of `msg`.
+ @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
  The function first calls `expand_keys` and then invokes `sign_expanded`.
 
@@ -101,11 +101,12 @@ Hacl_Ed25519_sign(uint8_t *signature, uint8_t *private_key, uint32_t msg_len, ui
 /**
 Verify an Ed25519 signature.
 
- The function returns `true` if the signature is valid and `false` otherwise.
+ @param public_key Points to 32 bytes of valid memory containing the public key, i.e., `uint8_t[32]`.
+ @param msg_len Length of `msg`.
+ @param msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
+ @param signature Points to 64 bytes of valid memory containing the signature, i.e., `uint8_t[64]`.
 
- The argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
- The argument `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
+ @return Returns `true` if the signature is valid and `false` otherwise.
 */
 bool
 Hacl_Ed25519_verify(uint8_t *public_key, uint32_t msg_len, uint8_t *msg, uint8_t *signature);

include/msvc/internal/Hacl_Hash_Blake2b.h

@@ -38,6 +38,21 @@ extern "C" {
 #include "internal/Hacl_Impl_Blake2_Constants.h"
 #include "../Hacl_Hash_Blake2b.h"
 
+typedef struct Hacl_Hash_Blake2s_blake2_params_s
+{
+ uint8_t digest_length;
+ uint8_t key_length;
+ uint8_t fanout;
+ uint8_t depth;
+ uint32_t leaf_length;
+ uint64_t node_offset;
+ uint8_t node_depth;
+ uint8_t inner_length;
+ uint8_t *salt;
+ uint8_t *personal;
+}
+Hacl_Hash_Blake2s_blake2_params;
+
 void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn);
 
 void

include/msvc/internal/Hacl_Hash_Blake2b_Simd256.h

@@ -36,6 +36,7 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "../Hacl_Hash_Blake2b_Simd256.h"
 #include "libintvector.h"
 

include/msvc/internal/Hacl_Hash_Blake2s.h

@@ -36,6 +36,7 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "../Hacl_Hash_Blake2s.h"
 
 void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn);

include/msvc/internal/Hacl_Hash_Blake2s_Simd128.h

@@ -36,6 +36,7 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "../Hacl_Hash_Blake2s_Simd128.h"
 #include "libintvector.h"
 

include/msvc/lib_memzero0.h

@@ -2,4 +2,4 @@
 
 void Lib_Memzero0_memzero0(void *dst, uint64_t len);
 
-#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t))
+#define Lib_Memzero0_memzero(dst, len, t, _ret_t) Lib_Memzero0_memzero0(dst, len * sizeof(t))

ocaml/lib/Hacl_Hash_Blake2b_bindings.ml

@@ -5,6 +5,32 @@ module Bindings(F:Cstubs.FOREIGN) =
  module Hacl_Streaming_Types_applied =
  (Hacl_Streaming_Types_bindings.Bindings)(Hacl_Streaming_Types_stubs)
  open Hacl_Streaming_Types_applied
+ type hacl_Hash_Blake2s_blake2_params =
+ [ `hacl_Hash_Blake2s_blake2_params ] structure
+ let (hacl_Hash_Blake2s_blake2_params :
+ [ `hacl_Hash_Blake2s_blake2_params ] structure typ) =
+ structure "Hacl_Hash_Blake2s_blake2_params_s"
+ let hacl_Hash_Blake2s_blake2_params_digest_length =
+ field hacl_Hash_Blake2s_blake2_params "digest_length" uint8_t
+ let hacl_Hash_Blake2s_blake2_params_key_length =
+ field hacl_Hash_Blake2s_blake2_params "key_length" uint8_t
+ let hacl_Hash_Blake2s_blake2_params_fanout =
+ field hacl_Hash_Blake2s_blake2_params "fanout" uint8_t
+ let hacl_Hash_Blake2s_blake2_params_depth =
+ field hacl_Hash_Blake2s_blake2_params "depth" uint8_t
+ let hacl_Hash_Blake2s_blake2_params_leaf_length =
+ field hacl_Hash_Blake2s_blake2_params "leaf_length" uint32_t
+ let hacl_Hash_Blake2s_blake2_params_node_offset =
+ field hacl_Hash_Blake2s_blake2_params "node_offset" uint64_t
+ let hacl_Hash_Blake2s_blake2_params_node_depth =
+ field hacl_Hash_Blake2s_blake2_params "node_depth" uint8_t
+ let hacl_Hash_Blake2s_blake2_params_inner_length =
+ field hacl_Hash_Blake2s_blake2_params "inner_length" uint8_t
+ let hacl_Hash_Blake2s_blake2_params_salt =
+ field hacl_Hash_Blake2s_blake2_params "salt" (ptr uint8_t)
+ let hacl_Hash_Blake2s_blake2_params_personal =
+ field hacl_Hash_Blake2s_blake2_params "personal" (ptr uint8_t)
+ let _ = seal hacl_Hash_Blake2s_blake2_params
  let hacl_Hash_Blake2b_init =
  foreign "Hacl_Hash_Blake2b_init"
  ((ptr uint64_t) @-> (uint32_t @-> (uint32_t @-> (returning void))))

src/EverCrypt_DRBG.c

@@ -1770,8 +1770,8 @@ static void uninstantiate_sha1(EverCrypt_DRBG_state_s *st)
  uint8_t *k = s.k;
  uint8_t *v = s.v;
  uint32_t *ctr = s.reseed_counter;
- Lib_Memzero0_memzero(k, 20U, uint8_t);
- Lib_Memzero0_memzero(v, 20U, uint8_t);
+ Lib_Memzero0_memzero(k, 20U, uint8_t, void *);
+ Lib_Memzero0_memzero(v, 20U, uint8_t, void *);
  ctr[0U] = 0U;
  KRML_HOST_FREE(k);
  KRML_HOST_FREE(v);
@@ -1794,8 +1794,8 @@ static void uninstantiate_sha2_256(EverCrypt_DRBG_state_s *st)
  uint8_t *k = s.k;
  uint8_t *v = s.v;
  uint32_t *ctr = s.reseed_counter;
- Lib_Memzero0_memzero(k, 32U, uint8_t);
- Lib_Memzero0_memzero(v, 32U, uint8_t);
+ Lib_Memzero0_memzero(k, 32U, uint8_t, void *);
+ Lib_Memzero0_memzero(v, 32U, uint8_t, void *);
  ctr[0U] = 0U;
  KRML_HOST_FREE(k);
  KRML_HOST_FREE(v);
@@ -1818,8 +1818,8 @@ static void uninstantiate_sha2_384(EverCrypt_DRBG_state_s *st)
  uint8_t *k = s.k;
  uint8_t *v = s.v;
  uint32_t *ctr = s.reseed_counter;
- Lib_Memzero0_memzero(k, 48U, uint8_t);
- Lib_Memzero0_memzero(v, 48U, uint8_t);
+ Lib_Memzero0_memzero(k, 48U, uint8_t, void *);
+ Lib_Memzero0_memzero(v, 48U, uint8_t, void *);
  ctr[0U] = 0U;
  KRML_HOST_FREE(k);
  KRML_HOST_FREE(v);
@@ -1842,8 +1842,8 @@ static void uninstantiate_sha2_512(EverCrypt_DRBG_state_s *st)
  uint8_t *k = s.k;
  uint8_t *v = s.v;
  uint32_t *ctr = s.reseed_counter;
- Lib_Memzero0_memzero(k, 64U, uint8_t);
- Lib_Memzero0_memzero(v, 64U, uint8_t);
+ Lib_Memzero0_memzero(k, 64U, uint8_t, void *);
+ Lib_Memzero0_memzero(v, 64U, uint8_t, void *);
  ctr[0U] = 0U;
  KRML_HOST_FREE(k);
  KRML_HOST_FREE(v);

src/Hacl_Ed25519.c

@@ -1712,8 +1712,8 @@ static inline void secret_expand(uint8_t *expanded, uint8_t *secret)
 /**
 Compute the public key from the private key.
 
- The outparam `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ @param[out] public_key Points to 32 bytes of valid memory, i.e., `uint8_t[32]`. Must not overlap the memory location of `private_key`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 */
 void Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key)
 {
@@ -1726,8 +1726,8 @@ void Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key)
 /**
 Compute the expanded keys for an Ed25519 signature.
 
- The outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ @param[out] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`. Must not overlap the memory location of `private_key`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
 
  If one needs to sign several messages under the same private key, it is more efficient
  to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -1744,11 +1744,10 @@ void Hacl_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key)
 /**
 Create an Ed25519 signature with the (precomputed) expanded keys.
 
- The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
- The argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
-
- The argument `expanded_keys` is obtained through `expand_keys`.
+ @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `expanded_keys` nor `msg`.
+ @param[in] expanded_keys Points to 96 bytes of valid memory, i.e., `uint8_t[96]`, containing the expanded keys obtained by invoking `expand_keys`.
+ @param[in] msg_len Length of `msg`.
+ @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
  If one needs to sign several messages under the same private key, it is more efficient
  to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
@@ -1783,9 +1782,10 @@ Hacl_Ed25519_sign_expanded(
 /**
 Create an Ed25519 signature.
 
- The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
- The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+ @param[out] signature Points to 64 bytes of valid memory, i.e., `uint8_t[64]`. Must not overlap the memory locations of `private_key` nor `msg`.
+ @param[in] private_key Points to 32 bytes of valid memory containing the private key, i.e., `uint8_t[32]`.
+ @param[in] msg_len Length of `msg`.
+ @param[in] msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
 
  The function first calls `expand_keys` and then invokes `sign_expanded`.
 
@@ -1803,11 +1803,12 @@ Hacl_Ed25519_sign(uint8_t *signature, uint8_t *private_key, uint32_t msg_len, ui
 /**
 Verify an Ed25519 signature.
 
- The function returns `true` if the signature is valid and `false` otherwise.
+ @param public_key Points to 32 bytes of valid memory containing the public key, i.e., `uint8_t[32]`.
+ @param msg_len Length of `msg`.
+ @param msg Points to `msg_len` bytes of valid memory containing the message, i.e., `uint8_t[msg_len]`.
+ @param signature Points to 64 bytes of valid memory containing the signature, i.e., `uint8_t[64]`.
 
- The argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
- The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
- The argument `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
+ @return Returns `true` if the signature is valid and `false` otherwise.
 */
 bool
 Hacl_Ed25519_verify(uint8_t *public_key, uint32_t msg_len, uint8_t *msg, uint8_t *signature)