[CI] update code

include/internal/Hacl_Hash_Blake2b.h

@@ -38,6 +38,38 @@ extern "C" {
 #include "internal/Hacl_Impl_Blake2_Constants.h"
 #include "../Hacl_Hash_Blake2b.h"
 
+typedef struct Hacl_Hash_Blake2s_blake2s_params_s
+{
+ uint8_t digest_length;
+ uint8_t key_length;
+ uint8_t fanout;
+ uint8_t depth;
+ uint32_t leaf_length;
+ uint32_t node_offset;
+ uint16_t xof_length;
+ uint8_t node_depth;
+ uint8_t inner_length;
+ uint8_t *salt;
+ uint8_t *personal;
+}
+Hacl_Hash_Blake2s_blake2s_params;
+
+typedef struct Hacl_Hash_Blake2s_blake2b_params_s
+{
+ uint8_t digest_length1;
+ uint8_t key_length1;
+ uint8_t fanout1;
+ uint8_t depth1;
+ uint32_t leaf_length1;
+ uint32_t node_offset1;
+ uint32_t xof_length1;
+ uint8_t node_depth1;
+ uint8_t inner_length1;
+ uint8_t *salt1;
+ uint8_t *personal1;
+}
+Hacl_Hash_Blake2s_blake2b_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/internal/Hacl_Hash_Blake2b.h

@@ -38,6 +38,38 @@ extern "C" {
 #include "internal/Hacl_Impl_Blake2_Constants.h"
 #include "../Hacl_Hash_Blake2b.h"
 
+typedef struct Hacl_Hash_Blake2s_blake2s_params_s
+{
+ uint8_t digest_length;
+ uint8_t key_length;
+ uint8_t fanout;
+ uint8_t depth;
+ uint32_t leaf_length;
+ uint32_t node_offset;
+ uint16_t xof_length;
+ uint8_t node_depth;
+ uint8_t inner_length;
+ uint8_t *salt;
+ uint8_t *personal;
+}
+Hacl_Hash_Blake2s_blake2s_params;
+
+typedef struct Hacl_Hash_Blake2s_blake2b_params_s
+{
+ uint8_t digest_length1;
+ uint8_t key_length1;
+ uint8_t fanout1;
+ uint8_t depth1;
+ uint32_t leaf_length1;
+ uint32_t node_offset1;
+ uint32_t xof_length1;
+ uint8_t node_depth1;
+ uint8_t inner_length1;
+ uint8_t *salt1;
+ uint8_t *personal1;
+}
+Hacl_Hash_Blake2s_blake2b_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,62 @@ 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_blake2s_params =
+ [ `hacl_Hash_Blake2s_blake2s_params ] structure
+ let (hacl_Hash_Blake2s_blake2s_params :
+ [ `hacl_Hash_Blake2s_blake2s_params ] structure typ) =
+ structure "Hacl_Hash_Blake2s_blake2s_params_s"
+ let hacl_Hash_Blake2s_blake2s_params_digest_length =
+ field hacl_Hash_Blake2s_blake2s_params "digest_length" uint8_t
+ let hacl_Hash_Blake2s_blake2s_params_key_length =
+ field hacl_Hash_Blake2s_blake2s_params "key_length" uint8_t
+ let hacl_Hash_Blake2s_blake2s_params_fanout =
+ field hacl_Hash_Blake2s_blake2s_params "fanout" uint8_t
+ let hacl_Hash_Blake2s_blake2s_params_depth =
+ field hacl_Hash_Blake2s_blake2s_params "depth" uint8_t
+ let hacl_Hash_Blake2s_blake2s_params_leaf_length =
+ field hacl_Hash_Blake2s_blake2s_params "leaf_length" uint32_t
+ let hacl_Hash_Blake2s_blake2s_params_node_offset =
+ field hacl_Hash_Blake2s_blake2s_params "node_offset" uint32_t
+ let hacl_Hash_Blake2s_blake2s_params_xof_length =
+ field hacl_Hash_Blake2s_blake2s_params "xof_length" uint16_t
+ let hacl_Hash_Blake2s_blake2s_params_node_depth =
+ field hacl_Hash_Blake2s_blake2s_params "node_depth" uint8_t
+ let hacl_Hash_Blake2s_blake2s_params_inner_length =
+ field hacl_Hash_Blake2s_blake2s_params "inner_length" uint8_t
+ let hacl_Hash_Blake2s_blake2s_params_salt =
+ field hacl_Hash_Blake2s_blake2s_params "salt" (ptr uint8_t)
+ let hacl_Hash_Blake2s_blake2s_params_personal =
+ field hacl_Hash_Blake2s_blake2s_params "personal" (ptr uint8_t)
+ let _ = seal hacl_Hash_Blake2s_blake2s_params
+ type hacl_Hash_Blake2s_blake2b_params =
+ [ `hacl_Hash_Blake2s_blake2b_params ] structure
+ let (hacl_Hash_Blake2s_blake2b_params :
+ [ `hacl_Hash_Blake2s_blake2b_params ] structure typ) =
+ structure "Hacl_Hash_Blake2s_blake2b_params_s"
+ let hacl_Hash_Blake2s_blake2b_params_digest_length1 =
+ field hacl_Hash_Blake2s_blake2b_params "digest_length1" uint8_t
+ let hacl_Hash_Blake2s_blake2b_params_key_length1 =
+ field hacl_Hash_Blake2s_blake2b_params "key_length1" uint8_t
+ let hacl_Hash_Blake2s_blake2b_params_fanout1 =
+ field hacl_Hash_Blake2s_blake2b_params "fanout1" uint8_t
+ let hacl_Hash_Blake2s_blake2b_params_depth1 =
+ field hacl_Hash_Blake2s_blake2b_params "depth1" uint8_t
+ let hacl_Hash_Blake2s_blake2b_params_leaf_length1 =
+ field hacl_Hash_Blake2s_blake2b_params "leaf_length1" uint32_t
+ let hacl_Hash_Blake2s_blake2b_params_node_offset1 =
+ field hacl_Hash_Blake2s_blake2b_params "node_offset1" uint32_t
+ let hacl_Hash_Blake2s_blake2b_params_xof_length1 =
+ field hacl_Hash_Blake2s_blake2b_params "xof_length1" uint32_t
+ let hacl_Hash_Blake2s_blake2b_params_node_depth1 =
+ field hacl_Hash_Blake2s_blake2b_params "node_depth1" uint8_t
+ let hacl_Hash_Blake2s_blake2b_params_inner_length1 =
+ field hacl_Hash_Blake2s_blake2b_params "inner_length1" uint8_t
+ let hacl_Hash_Blake2s_blake2b_params_salt1 =
+ field hacl_Hash_Blake2s_blake2b_params "salt1" (ptr uint8_t)
+ let hacl_Hash_Blake2s_blake2b_params_personal1 =
+ field hacl_Hash_Blake2s_blake2b_params "personal1" (ptr uint8_t)
+ let _ = seal hacl_Hash_Blake2s_blake2b_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_Frodo1344.c

@@ -55,7 +55,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
  shake_input_seed_se[0U] = 0x5fU;
  memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t));
  Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43008U, r);
- Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t);
+ Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *);
  Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(1344U, 8U, r, s_matrix);
  Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(1344U, 8U, r + 21504U, e_matrix);
  uint16_t b_matrix[10752U] = { 0U };
@@ -66,14 +66,14 @@ uint32_t Hacl_Frodo1344_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
  Hacl_Impl_Matrix_matrix_add(1344U, 8U, b_matrix, e_matrix);
  Hacl_Impl_Frodo_Pack_frodo_pack(1344U, 8U, 16U, b_matrix, b_bytes);
  Hacl_Impl_Matrix_matrix_to_lbytes(1344U, 8U, s_matrix, s_bytes);
- Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t);
- Lib_Memzero0_memzero(e_matrix, 10752U, uint16_t);
+ Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t, void *);
+ Lib_Memzero0_memzero(e_matrix, 10752U, uint16_t, void *);
  uint32_t slen1 = 43056U;
  uint8_t *sk_p = sk;
  memcpy(sk_p, s, 32U * sizeof (uint8_t));
  memcpy(sk_p + 32U, pk, 21520U * sizeof (uint8_t));
  Hacl_Hash_SHA3_shake256_hacl(21520U, pk, 32U, sk + slen1);
- Lib_Memzero0_memzero(coins, 80U, uint8_t);
+ Lib_Memzero0_memzero(coins, 80U, uint8_t, void *);
  return 0U;
 }
 
@@ -98,7 +98,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
  shake_input_seed_se[0U] = 0x96U;
  memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t));
  Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43136U, r);
- Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t);
+ Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *);
  Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r, sp_matrix);
  Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r + 21504U, ep_matrix);
  Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 8U, r + 43008U, epp_matrix);
@@ -119,22 +119,22 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
  uint16_t mu_encode[64U] = { 0U };
  Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 4U, 8U, coins, mu_encode);
  Hacl_Impl_Matrix_matrix_add(8U, 8U, v_matrix, mu_encode);
- Lib_Memzero0_memzero(mu_encode, 64U, uint16_t);
+ Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *);
  Hacl_Impl_Frodo_Pack_frodo_pack(8U, 8U, 16U, v_matrix, c2);
- Lib_Memzero0_memzero(v_matrix, 64U, uint16_t);
- Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t);
- Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t);
- Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+ Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *);
+ Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t, void *);
+ Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t, void *);
+ Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
  uint32_t ss_init_len = 21664U;
  KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
  uint8_t shake_input_ss[ss_init_len];
  memset(shake_input_ss, 0U, ss_init_len * sizeof (uint8_t));
  memcpy(shake_input_ss, ct, 21632U * sizeof (uint8_t));
  memcpy(shake_input_ss + 21632U, k, 32U * sizeof (uint8_t));
  Hacl_Hash_SHA3_shake256_hacl(ss_init_len, shake_input_ss, 32U, ss);
- Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
- Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t);
- Lib_Memzero0_memzero(coins, 32U, uint8_t);
+ Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *);
+ Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t, void *);
+ Lib_Memzero0_memzero(coins, 32U, uint8_t, void *);
  return 0U;
 }
 
@@ -154,8 +154,8 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
  Hacl_Impl_Matrix_matrix_mul_s(8U, 1344U, 8U, bp_matrix, s_matrix, m_matrix);
  Hacl_Impl_Matrix_matrix_sub(8U, 8U, c_matrix, m_matrix);
  Hacl_Impl_Frodo_Encode_frodo_key_decode(16U, 4U, 8U, m_matrix, mu_decode);
- Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t);
- Lib_Memzero0_memzero(m_matrix, 64U, uint16_t);
+ Lib_Memzero0_memzero(s_matrix, 10752U, uint16_t, void *);
+ Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *);
  uint8_t seed_se_k[64U] = { 0U };
  uint32_t pkh_mu_decode_len = 64U;
  KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -178,7 +178,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
  shake_input_seed_se[0U] = 0x96U;
  memcpy(shake_input_seed_se + 1U, seed_se, 32U * sizeof (uint8_t));
  Hacl_Hash_SHA3_shake256_hacl(33U, shake_input_seed_se, 43136U, r);
- Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t);
+ Lib_Memzero0_memzero(shake_input_seed_se, 33U, uint8_t, void *);
  Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r, sp_matrix);
  Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 1344U, r + 21504U, ep_matrix);
  Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344(8U, 8U, r + 43008U, epp_matrix);
@@ -197,12 +197,12 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
  uint16_t mu_encode[64U] = { 0U };
  Hacl_Impl_Frodo_Encode_frodo_key_encode(16U, 4U, 8U, mu_decode, mu_encode);
  Hacl_Impl_Matrix_matrix_add(8U, 8U, cp_matrix, mu_encode);
- Lib_Memzero0_memzero(mu_encode, 64U, uint16_t);
+ Lib_Memzero0_memzero(mu_encode, 64U, uint16_t, void *);
  Hacl_Impl_Matrix_mod_pow2(8U, 1344U, 16U, bpp_matrix);
  Hacl_Impl_Matrix_mod_pow2(8U, 8U, 16U, cp_matrix);
- Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t);
- Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t);
- Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+ Lib_Memzero0_memzero(sp_matrix, 10752U, uint16_t, void *);
+ Lib_Memzero0_memzero(ep_matrix, 10752U, uint16_t, void *);
+ Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
  uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 1344U, bp_matrix, bpp_matrix);
  uint16_t b2 = Hacl_Impl_Matrix_matrix_eq(8U, 8U, c_matrix, cp_matrix);
  uint16_t mask = (uint32_t)b1 & (uint32_t)b2;
@@ -223,10 +223,10 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
  memcpy(ss_init, ct, 21632U * sizeof (uint8_t));
  memcpy(ss_init + 21632U, kp_s, 32U * sizeof (uint8_t));
  Hacl_Hash_SHA3_shake256_hacl(ss_init_len, ss_init, 32U, ss);
- Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
- Lib_Memzero0_memzero(kp_s, 32U, uint8_t);
- Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t);
- Lib_Memzero0_memzero(mu_decode, 32U, uint8_t);
+ Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *);
+ Lib_Memzero0_memzero(kp_s, 32U, uint8_t, void *);
+ Lib_Memzero0_memzero(seed_se_k, 64U, uint8_t, void *);
+ Lib_Memzero0_memzero(mu_decode, 32U, uint8_t, void *);
  return 0U;
 }