diff --git a/include/Hacl_Ed25519.h b/include/Hacl_Ed25519.h
index b2654704..f0dc31e2 100644
--- a/include/Hacl_Ed25519.h
+++ b/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);
diff --git a/include/internal/Hacl_Hash_Blake2b.h b/include/internal/Hacl_Hash_Blake2b.h
index 21689d60..e2437d97 100644
--- a/include/internal/Hacl_Hash_Blake2b.h
+++ b/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
diff --git a/include/internal/Hacl_Hash_Blake2b_Simd256.h b/include/internal/Hacl_Hash_Blake2b_Simd256.h
index 4cc07869..4dd986b2 100644
--- a/include/internal/Hacl_Hash_Blake2b_Simd256.h
+++ b/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"
 
diff --git a/include/internal/Hacl_Hash_Blake2s.h b/include/internal/Hacl_Hash_Blake2s.h
index f814aa95..eccd92de 100644
--- a/include/internal/Hacl_Hash_Blake2s.h
+++ b/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);
diff --git a/include/internal/Hacl_Hash_Blake2s_Simd128.h b/include/internal/Hacl_Hash_Blake2s_Simd128.h
index 0589aec5..2c422949 100644
--- a/include/internal/Hacl_Hash_Blake2s_Simd128.h
+++ b/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"
 
diff --git a/include/lib_memzero0.h b/include/lib_memzero0.h
index 506dd50f..fea3e41c 100644
--- a/include/lib_memzero0.h
+++ b/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))
diff --git a/include/msvc/Hacl_Ed25519.h b/include/msvc/Hacl_Ed25519.h
index b2654704..f0dc31e2 100644
--- a/include/msvc/Hacl_Ed25519.h
+++ b/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);
diff --git a/include/msvc/internal/Hacl_Hash_Blake2b.h b/include/msvc/internal/Hacl_Hash_Blake2b.h
index 21689d60..e2437d97 100644
--- a/include/msvc/internal/Hacl_Hash_Blake2b.h
+++ b/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
diff --git a/include/msvc/internal/Hacl_Hash_Blake2b_Simd256.h b/include/msvc/internal/Hacl_Hash_Blake2b_Simd256.h
index 4cc07869..4dd986b2 100644
--- a/include/msvc/internal/Hacl_Hash_Blake2b_Simd256.h
+++ b/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"
 
diff --git a/include/msvc/internal/Hacl_Hash_Blake2s.h b/include/msvc/internal/Hacl_Hash_Blake2s.h
index f814aa95..eccd92de 100644
--- a/include/msvc/internal/Hacl_Hash_Blake2s.h
+++ b/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);
diff --git a/include/msvc/internal/Hacl_Hash_Blake2s_Simd128.h b/include/msvc/internal/Hacl_Hash_Blake2s_Simd128.h
index 0589aec5..2c422949 100644
--- a/include/msvc/internal/Hacl_Hash_Blake2s_Simd128.h
+++ b/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"
 
diff --git a/include/msvc/lib_memzero0.h b/include/msvc/lib_memzero0.h
index 506dd50f..fea3e41c 100644
--- a/include/msvc/lib_memzero0.h
+++ b/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))
diff --git a/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml b/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml
index 75c75e90..b594e2ef 100644
--- a/ocaml/lib/Hacl_Hash_Blake2b_bindings.ml
+++ b/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))))
diff --git a/src/EverCrypt_DRBG.c b/src/EverCrypt_DRBG.c
index 301fe528..a831a5b5 100644
--- a/src/EverCrypt_DRBG.c
+++ b/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);
diff --git a/src/Hacl_Ed25519.c b/src/Hacl_Ed25519.c
index 05d96cd0..d1f8edf2 100644
--- a/src/Hacl_Ed25519.c
+++ b/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)
diff --git a/src/Hacl_Frodo1344.c b/src/Hacl_Frodo1344.c
index a565a85b..741a593b 100644
--- a/src/Hacl_Frodo1344.c
+++ b/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,12 +119,12 @@ 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];
@@ -132,9 +132,9 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   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;
 }
 
diff --git a/src/Hacl_Frodo64.c b/src/Hacl_Frodo64.c
index 91434038..b54a7c62 100644
--- a/src/Hacl_Frodo64.c
+++ b/src/Hacl_Frodo64.c
@@ -60,7 +60,7 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = 0x5fU;
   memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2048U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(64U, 8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(64U, 8U, r + 1024U, e_matrix);
   uint16_t b_matrix[512U] = { 0U };
@@ -70,14 +70,14 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_add(64U, 8U, b_matrix, e_matrix);
   Hacl_Impl_Frodo_Pack_frodo_pack(64U, 8U, 15U, b_matrix, b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes(64U, 8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(e_matrix, 512U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(e_matrix, 512U, uint16_t, void *);
   uint32_t slen1 = 2016U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, 16U * sizeof (uint8_t));
   memcpy(sk_p + 16U, pk, 976U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(976U, pk, 16U, sk + slen1);
-  Lib_Memzero0_memzero(coins, 48U, uint8_t);
+  Lib_Memzero0_memzero(coins, 48U, uint8_t, void *);
   return 0U;
 }
 
@@ -102,7 +102,7 @@ uint32_t Hacl_Frodo64_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, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2176U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r + 1024U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 8U, r + 2048U, epp_matrix);
@@ -122,12 +122,12 @@ uint32_t Hacl_Frodo64_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(15U, 2U, 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, 15U, v_matrix, c2);
-  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t);
-  Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *);
+  Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint32_t ss_init_len = 1096U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t shake_input_ss[ss_init_len];
@@ -135,9 +135,9 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, 1080U * sizeof (uint8_t));
   memcpy(shake_input_ss + 1080U, k, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(ss_init_len, shake_input_ss, 16U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t);
-  Lib_Memzero0_memzero(coins, 16U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *);
+  Lib_Memzero0_memzero(coins, 16U, uint8_t, void *);
   return 0U;
 }
 
@@ -157,8 +157,8 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_mul_s(8U, 64U, 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(15U, 2U, 8U, m_matrix, mu_decode);
-  Lib_Memzero0_memzero(s_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *);
   uint8_t seed_se_k[32U] = { 0U };
   uint32_t pkh_mu_decode_len = 32U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -181,7 +181,7 @@ uint32_t Hacl_Frodo64_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, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2176U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r + 1024U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 8U, r + 2048U, epp_matrix);
@@ -199,12 +199,12 @@ uint32_t Hacl_Frodo64_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(15U, 2U, 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, 64U, 15U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2(8U, 8U, 15U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 64U, 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;
@@ -226,10 +226,10 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, 1080U * sizeof (uint8_t));
   memcpy(ss_init + 1080U, kp_s, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(ss_init_len, ss_init, 16U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(kp_s, 16U, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t);
-  Lib_Memzero0_memzero(mu_decode, 16U, uint8_t);
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(kp_s, 16U, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *);
+  Lib_Memzero0_memzero(mu_decode, 16U, uint8_t, void *);
   return 0U;
 }
 
diff --git a/src/Hacl_Frodo640.c b/src/Hacl_Frodo640.c
index 8baaee46..86f3ed23 100644
--- a/src/Hacl_Frodo640.c
+++ b/src/Hacl_Frodo640.c
@@ -55,7 +55,7 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = 0x5fU;
   memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20480U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(640U, 8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(640U, 8U, r + 10240U, e_matrix);
   uint16_t b_matrix[5120U] = { 0U };
@@ -66,14 +66,14 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_add(640U, 8U, b_matrix, e_matrix);
   Hacl_Impl_Frodo_Pack_frodo_pack(640U, 8U, 15U, b_matrix, b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes(640U, 8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(e_matrix, 5120U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(e_matrix, 5120U, uint16_t, void *);
   uint32_t slen1 = 19872U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, 16U * sizeof (uint8_t));
   memcpy(sk_p + 16U, pk, 9616U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(9616U, pk, 16U, sk + slen1);
-  Lib_Memzero0_memzero(coins, 48U, uint8_t);
+  Lib_Memzero0_memzero(coins, 48U, uint8_t, void *);
   return 0U;
 }
 
@@ -98,7 +98,7 @@ uint32_t Hacl_Frodo640_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, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20608U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r + 10240U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 8U, r + 20480U, epp_matrix);
@@ -119,12 +119,12 @@ uint32_t Hacl_Frodo640_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(15U, 2U, 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, 15U, v_matrix, c2);
-  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t);
-  Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *);
+  Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint32_t ss_init_len = 9736U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t shake_input_ss[ss_init_len];
@@ -132,9 +132,9 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, 9720U * sizeof (uint8_t));
   memcpy(shake_input_ss + 9720U, k, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(ss_init_len, shake_input_ss, 16U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t);
-  Lib_Memzero0_memzero(coins, 16U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *);
+  Lib_Memzero0_memzero(coins, 16U, uint8_t, void *);
   return 0U;
 }
 
@@ -154,8 +154,8 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_mul_s(8U, 640U, 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(15U, 2U, 8U, m_matrix, mu_decode);
-  Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *);
   uint8_t seed_se_k[32U] = { 0U };
   uint32_t pkh_mu_decode_len = 32U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -178,7 +178,7 @@ uint32_t Hacl_Frodo640_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, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20608U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r + 10240U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 8U, r + 20480U, epp_matrix);
@@ -197,12 +197,12 @@ uint32_t Hacl_Frodo640_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(15U, 2U, 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, 640U, 15U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2(8U, 8U, 15U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 640U, 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;
@@ -224,10 +224,10 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, 9720U * sizeof (uint8_t));
   memcpy(ss_init + 9720U, kp_s, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(ss_init_len, ss_init, 16U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(kp_s, 16U, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t);
-  Lib_Memzero0_memzero(mu_decode, 16U, uint8_t);
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(kp_s, 16U, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *);
+  Lib_Memzero0_memzero(mu_decode, 16U, uint8_t, void *);
   return 0U;
 }
 
diff --git a/src/Hacl_Frodo976.c b/src/Hacl_Frodo976.c
index 76d78a30..3e3dca8e 100644
--- a/src/Hacl_Frodo976.c
+++ b/src/Hacl_Frodo976.c
@@ -55,7 +55,7 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = 0x5fU;
   memcpy(shake_input_seed_se + 1U, seed_se, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31232U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(976U, 8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(976U, 8U, r + 15616U, e_matrix);
   uint16_t b_matrix[7808U] = { 0U };
@@ -66,14 +66,14 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_add(976U, 8U, b_matrix, e_matrix);
   Hacl_Impl_Frodo_Pack_frodo_pack(976U, 8U, 16U, b_matrix, b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes(976U, 8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(e_matrix, 7808U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(e_matrix, 7808U, uint16_t, void *);
   uint32_t slen1 = 31272U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, 24U * sizeof (uint8_t));
   memcpy(sk_p + 24U, pk, 15632U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(15632U, pk, 24U, sk + slen1);
-  Lib_Memzero0_memzero(coins, 64U, uint8_t);
+  Lib_Memzero0_memzero(coins, 64U, uint8_t, void *);
   return 0U;
 }
 
@@ -98,7 +98,7 @@ uint32_t Hacl_Frodo976_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, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31360U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r + 15616U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 8U, r + 31232U, epp_matrix);
@@ -119,12 +119,12 @@ uint32_t Hacl_Frodo976_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, 3U, 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, 7808U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *);
+  Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint32_t ss_init_len = 15768U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t shake_input_ss[ss_init_len];
@@ -132,9 +132,9 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, 15744U * sizeof (uint8_t));
   memcpy(shake_input_ss + 15744U, k, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(ss_init_len, shake_input_ss, 24U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t);
-  Lib_Memzero0_memzero(coins, 24U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t, void *);
+  Lib_Memzero0_memzero(coins, 24U, uint8_t, void *);
   return 0U;
 }
 
@@ -154,8 +154,8 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_mul_s(8U, 976U, 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, 3U, 8U, m_matrix, mu_decode);
-  Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *);
   uint8_t seed_se_k[48U] = { 0U };
   uint32_t pkh_mu_decode_len = 48U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -178,7 +178,7 @@ uint32_t Hacl_Frodo976_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, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31360U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r + 15616U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 8U, r + 31232U, epp_matrix);
@@ -197,12 +197,12 @@ uint32_t Hacl_Frodo976_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, 3U, 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, 976U, 16U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2(8U, 8U, 16U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 976U, 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_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, 15744U * sizeof (uint8_t));
   memcpy(ss_init + 15744U, kp_s, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(ss_init_len, ss_init, 24U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(kp_s, 24U, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t);
-  Lib_Memzero0_memzero(mu_decode, 24U, uint8_t);
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(kp_s, 24U, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t, void *);
+  Lib_Memzero0_memzero(mu_decode, 24U, uint8_t, void *);
   return 0U;
 }
 
diff --git a/src/Hacl_Hash_Blake2b.c b/src/Hacl_Hash_Blake2b.c
index 2dceaf4b..68de8340 100644
--- a/src/Hacl_Hash_Blake2b.c
+++ b/src/Hacl_Hash_Blake2b.c
@@ -474,6 +474,7 @@ update_block(uint64_t *wv, uint64_t *hash, bool flag, FStar_UInt128_uint128 totl
 
 void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn)
 {
+  uint64_t tmp[8U] = { 0U };
   uint64_t *r0 = hash;
   uint64_t *r1 = hash + 4U;
   uint64_t *r2 = hash + 8U;
@@ -494,16 +495,67 @@ void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn)
   r3[1U] = iv5;
   r3[2U] = iv6;
   r3[3U] = iv7;
-  uint64_t kk_shift_8 = (uint64_t)kk << 8U;
-  uint64_t iv0_ = iv0 ^ (0x01010000ULL ^ (kk_shift_8 ^ (uint64_t)nn));
+  uint8_t salt[16U] = { 0U };
+  uint8_t personal[16U] = { 0U };
+  Hacl_Hash_Blake2s_blake2_params
+  p =
+    {
+      .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U,
+      .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 4U;
+    uint8_t *bj = p.salt + i * 8U;
+    uint64_t u = load64_le(bj);
+    uint64_t r = u;
+    uint64_t x = r;
+    os[i] = x;);
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 6U;
+    uint8_t *bj = p.personal + i * 8U;
+    uint64_t u = load64_le(bj);
+    uint64_t r = u;
+    uint64_t x = r;
+    os[i] = x;);
+  tmp[0U] =
+    (uint64_t)nn
+    ^
+      ((uint64_t)kk
+      << 8U
+      ^ ((uint64_t)p.fanout << 16U ^ ((uint64_t)p.depth << 24U ^ (uint64_t)p.leaf_length << 32U)));
+  tmp[1U] = p.node_offset;
+  tmp[2U] = (uint64_t)p.node_depth ^ (uint64_t)p.inner_length << 8U;
+  tmp[3U] = 0ULL;
+  uint64_t tmp0 = tmp[0U];
+  uint64_t tmp1 = tmp[1U];
+  uint64_t tmp2 = tmp[2U];
+  uint64_t tmp3 = tmp[3U];
+  uint64_t tmp4 = tmp[4U];
+  uint64_t tmp5 = tmp[5U];
+  uint64_t tmp6 = tmp[6U];
+  uint64_t tmp7 = tmp[7U];
+  uint64_t iv0_ = iv0 ^ tmp0;
+  uint64_t iv1_ = iv1 ^ tmp1;
+  uint64_t iv2_ = iv2 ^ tmp2;
+  uint64_t iv3_ = iv3 ^ tmp3;
+  uint64_t iv4_ = iv4 ^ tmp4;
+  uint64_t iv5_ = iv5 ^ tmp5;
+  uint64_t iv6_ = iv6 ^ tmp6;
+  uint64_t iv7_ = iv7 ^ tmp7;
   r0[0U] = iv0_;
-  r0[1U] = iv1;
-  r0[2U] = iv2;
-  r0[3U] = iv3;
-  r1[0U] = iv4;
-  r1[1U] = iv5;
-  r1[2U] = iv6;
-  r1[3U] = iv7;
+  r0[1U] = iv1_;
+  r0[2U] = iv2_;
+  r0[3U] = iv3_;
+  r1[0U] = iv4_;
+  r1[1U] = iv5_;
+  r1[2U] = iv6_;
+  r1[3U] = iv7_;
 }
 
 static void update_key(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, uint32_t ll)
@@ -519,7 +571,7 @@ static void update_key(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, ui
   {
     update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, 128U, uint8_t);
+  Lib_Memzero0_memzero(b, 128U, uint8_t, void *);
 }
 
 void
@@ -560,7 +612,7 @@ Hacl_Hash_Blake2b_update_last(
   FStar_UInt128_uint128
   totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len));
   update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, 128U, uint8_t);
+  Lib_Memzero0_memzero(b, 128U, uint8_t, void *);
 }
 
 static void
@@ -624,7 +676,7 @@ void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash)
   KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store64_le(second + i * 8U, row1[i]););
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 /**
@@ -965,7 +1017,7 @@ Hacl_Hash_Blake2b_hash_with_key(
   Hacl_Hash_Blake2b_init(b, key_len, output_len);
   update(b1, b, key_len, key, input_len, input);
   Hacl_Hash_Blake2b_finish(output_len, output, b);
-  Lib_Memzero0_memzero(b1, 16U, uint64_t);
-  Lib_Memzero0_memzero(b, 16U, uint64_t);
+  Lib_Memzero0_memzero(b1, 16U, uint64_t, void *);
+  Lib_Memzero0_memzero(b, 16U, uint64_t, void *);
 }
 
diff --git a/src/Hacl_Hash_Blake2b_Simd256.c b/src/Hacl_Hash_Blake2b_Simd256.c
index 1a5e8cf2..7aea4d42 100644
--- a/src/Hacl_Hash_Blake2b_Simd256.c
+++ b/src/Hacl_Hash_Blake2b_Simd256.c
@@ -26,6 +26,7 @@
 #include "internal/Hacl_Hash_Blake2b_Simd256.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "lib_memzero0.h"
 
 static inline void
@@ -214,6 +215,7 @@ update_block(
 void
 Hacl_Hash_Blake2b_Simd256_init(Lib_IntVector_Intrinsics_vec256 *hash, uint32_t kk, uint32_t nn)
 {
+  uint64_t tmp[8U] = { 0U };
   Lib_IntVector_Intrinsics_vec256 *r0 = hash;
   Lib_IntVector_Intrinsics_vec256 *r1 = hash + 1U;
   Lib_IntVector_Intrinsics_vec256 *r2 = hash + 2U;
@@ -228,10 +230,61 @@ Hacl_Hash_Blake2b_Simd256_init(Lib_IntVector_Intrinsics_vec256 *hash, uint32_t k
   uint64_t iv7 = Hacl_Hash_Blake2s_ivTable_B[7U];
   r2[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0, iv1, iv2, iv3);
   r3[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7);
-  uint64_t kk_shift_8 = (uint64_t)kk << 8U;
-  uint64_t iv0_ = iv0 ^ (0x01010000ULL ^ (kk_shift_8 ^ (uint64_t)nn));
-  r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1, iv2, iv3);
-  r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7);
+  uint8_t salt[16U] = { 0U };
+  uint8_t personal[16U] = { 0U };
+  Hacl_Hash_Blake2s_blake2_params
+  p =
+    {
+      .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U,
+      .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 4U;
+    uint8_t *bj = p.salt + i * 8U;
+    uint64_t u = load64_le(bj);
+    uint64_t r = u;
+    uint64_t x = r;
+    os[i] = x;);
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 6U;
+    uint8_t *bj = p.personal + i * 8U;
+    uint64_t u = load64_le(bj);
+    uint64_t r = u;
+    uint64_t x = r;
+    os[i] = x;);
+  tmp[0U] =
+    (uint64_t)nn
+    ^
+      ((uint64_t)kk
+      << 8U
+      ^ ((uint64_t)p.fanout << 16U ^ ((uint64_t)p.depth << 24U ^ (uint64_t)p.leaf_length << 32U)));
+  tmp[1U] = p.node_offset;
+  tmp[2U] = (uint64_t)p.node_depth ^ (uint64_t)p.inner_length << 8U;
+  tmp[3U] = 0ULL;
+  uint64_t tmp0 = tmp[0U];
+  uint64_t tmp1 = tmp[1U];
+  uint64_t tmp2 = tmp[2U];
+  uint64_t tmp3 = tmp[3U];
+  uint64_t tmp4 = tmp[4U];
+  uint64_t tmp5 = tmp[5U];
+  uint64_t tmp6 = tmp[6U];
+  uint64_t tmp7 = tmp[7U];
+  uint64_t iv0_ = iv0 ^ tmp0;
+  uint64_t iv1_ = iv1 ^ tmp1;
+  uint64_t iv2_ = iv2 ^ tmp2;
+  uint64_t iv3_ = iv3 ^ tmp3;
+  uint64_t iv4_ = iv4 ^ tmp4;
+  uint64_t iv5_ = iv5 ^ tmp5;
+  uint64_t iv6_ = iv6 ^ tmp6;
+  uint64_t iv7_ = iv7 ^ tmp7;
+  r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1_, iv2_, iv3_);
+  r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4_, iv5_, iv6_, iv7_);
 }
 
 static void
@@ -254,7 +307,7 @@ update_key(
   {
     update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, 128U, uint8_t);
+  Lib_Memzero0_memzero(b, 128U, uint8_t, void *);
 }
 
 void
@@ -295,7 +348,7 @@ Hacl_Hash_Blake2b_Simd256_update_last(
   FStar_UInt128_uint128
   totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len));
   update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, 128U, uint8_t);
+  Lib_Memzero0_memzero(b, 128U, uint8_t, void *);
 }
 
 static inline void
@@ -371,7 +424,7 @@ Hacl_Hash_Blake2b_Simd256_finish(
   Lib_IntVector_Intrinsics_vec256_store64_le(second, row1[0U]);
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 void
@@ -822,7 +875,7 @@ Hacl_Hash_Blake2b_Simd256_hash_with_key(
   Hacl_Hash_Blake2b_Simd256_init(b, key_len, output_len);
   update(b1, b, key_len, key, input_len, input);
   Hacl_Hash_Blake2b_Simd256_finish(output_len, output, b);
-  Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec256);
-  Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec256);
+  Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec256, void *);
+  Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec256, void *);
 }
 
diff --git a/src/Hacl_Hash_Blake2s.c b/src/Hacl_Hash_Blake2s.c
index 652c3f33..37fabb67 100644
--- a/src/Hacl_Hash_Blake2s.c
+++ b/src/Hacl_Hash_Blake2s.c
@@ -26,6 +26,7 @@
 #include "internal/Hacl_Hash_Blake2s.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "lib_memzero0.h"
 
 static inline void
@@ -474,6 +475,7 @@ update_block(uint32_t *wv, uint32_t *hash, bool flag, uint64_t totlen, uint8_t *
 
 void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn)
 {
+  uint32_t tmp[8U] = { 0U };
   uint32_t *r0 = hash;
   uint32_t *r1 = hash + 4U;
   uint32_t *r2 = hash + 8U;
@@ -494,16 +496,64 @@ void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn)
   r3[1U] = iv5;
   r3[2U] = iv6;
   r3[3U] = iv7;
-  uint32_t kk_shift_8 = kk << 8U;
-  uint32_t iv0_ = iv0 ^ (0x01010000U ^ (kk_shift_8 ^ nn));
+  uint8_t salt[8U] = { 0U };
+  uint8_t personal[8U] = { 0U };
+  Hacl_Hash_Blake2s_blake2_params
+  p =
+    {
+      .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U,
+      .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint32_t *os = tmp + 4U;
+    uint8_t *bj = p.salt + i * 4U;
+    uint32_t u = load32_le(bj);
+    uint32_t r = u;
+    uint32_t x = r;
+    os[i] = x;);
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint32_t *os = tmp + 6U;
+    uint8_t *bj = p.personal + i * 4U;
+    uint32_t u = load32_le(bj);
+    uint32_t r = u;
+    uint32_t x = r;
+    os[i] = x;);
+  tmp[0U] = nn ^ (kk << 8U ^ ((uint32_t)p.fanout << 16U ^ (uint32_t)p.depth << 24U));
+  tmp[1U] = p.leaf_length;
+  tmp[2U] = (uint32_t)p.node_offset;
+  tmp[3U] =
+    (uint32_t)(p.node_offset >> 32U)
+    ^ ((uint32_t)p.node_depth << 16U ^ (uint32_t)p.inner_length << 24U);
+  uint32_t tmp0 = tmp[0U];
+  uint32_t tmp1 = tmp[1U];
+  uint32_t tmp2 = tmp[2U];
+  uint32_t tmp3 = tmp[3U];
+  uint32_t tmp4 = tmp[4U];
+  uint32_t tmp5 = tmp[5U];
+  uint32_t tmp6 = tmp[6U];
+  uint32_t tmp7 = tmp[7U];
+  uint32_t iv0_ = iv0 ^ tmp0;
+  uint32_t iv1_ = iv1 ^ tmp1;
+  uint32_t iv2_ = iv2 ^ tmp2;
+  uint32_t iv3_ = iv3 ^ tmp3;
+  uint32_t iv4_ = iv4 ^ tmp4;
+  uint32_t iv5_ = iv5 ^ tmp5;
+  uint32_t iv6_ = iv6 ^ tmp6;
+  uint32_t iv7_ = iv7 ^ tmp7;
   r0[0U] = iv0_;
-  r0[1U] = iv1;
-  r0[2U] = iv2;
-  r0[3U] = iv3;
-  r1[0U] = iv4;
-  r1[1U] = iv5;
-  r1[2U] = iv6;
-  r1[3U] = iv7;
+  r0[1U] = iv1_;
+  r0[2U] = iv2_;
+  r0[3U] = iv3_;
+  r1[0U] = iv4_;
+  r1[1U] = iv5_;
+  r1[2U] = iv6_;
+  r1[3U] = iv7_;
 }
 
 static void update_key(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, uint32_t ll)
@@ -519,7 +569,7 @@ static void update_key(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, ui
   {
     update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 void
@@ -556,7 +606,7 @@ Hacl_Hash_Blake2s_update_last(
   memcpy(b, last, rem * sizeof (uint8_t));
   uint64_t totlen = prev + (uint64_t)len;
   update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 static void
@@ -614,7 +664,7 @@ void Hacl_Hash_Blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash)
   KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store32_le(second + i * 4U, row1[i]););
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, 32U, uint8_t);
+  Lib_Memzero0_memzero(b, 32U, uint8_t, void *);
 }
 
 /**
@@ -925,7 +975,7 @@ Hacl_Hash_Blake2s_hash_with_key(
   Hacl_Hash_Blake2s_init(b, key_len, output_len);
   update(b1, b, key_len, key, input_len, input);
   Hacl_Hash_Blake2s_finish(output_len, output, b);
-  Lib_Memzero0_memzero(b1, 16U, uint32_t);
-  Lib_Memzero0_memzero(b, 16U, uint32_t);
+  Lib_Memzero0_memzero(b1, 16U, uint32_t, void *);
+  Lib_Memzero0_memzero(b, 16U, uint32_t, void *);
 }
 
diff --git a/src/Hacl_Hash_Blake2s_Simd128.c b/src/Hacl_Hash_Blake2s_Simd128.c
index 73f0cccb..ed86be43 100644
--- a/src/Hacl_Hash_Blake2s_Simd128.c
+++ b/src/Hacl_Hash_Blake2s_Simd128.c
@@ -26,6 +26,7 @@
 #include "internal/Hacl_Hash_Blake2s_Simd128.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "lib_memzero0.h"
 
 static inline void
@@ -214,6 +215,7 @@ update_block(
 void
 Hacl_Hash_Blake2s_Simd128_init(Lib_IntVector_Intrinsics_vec128 *hash, uint32_t kk, uint32_t nn)
 {
+  uint32_t tmp[8U] = { 0U };
   Lib_IntVector_Intrinsics_vec128 *r0 = hash;
   Lib_IntVector_Intrinsics_vec128 *r1 = hash + 1U;
   Lib_IntVector_Intrinsics_vec128 *r2 = hash + 2U;
@@ -228,10 +230,58 @@ Hacl_Hash_Blake2s_Simd128_init(Lib_IntVector_Intrinsics_vec128 *hash, uint32_t k
   uint32_t iv7 = Hacl_Hash_Blake2s_ivTable_S[7U];
   r2[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0, iv1, iv2, iv3);
   r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7);
-  uint32_t kk_shift_8 = kk << 8U;
-  uint32_t iv0_ = iv0 ^ (0x01010000U ^ (kk_shift_8 ^ nn));
-  r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1, iv2, iv3);
-  r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7);
+  uint8_t salt[8U] = { 0U };
+  uint8_t personal[8U] = { 0U };
+  Hacl_Hash_Blake2s_blake2_params
+  p =
+    {
+      .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U,
+      .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint32_t *os = tmp + 4U;
+    uint8_t *bj = p.salt + i * 4U;
+    uint32_t u = load32_le(bj);
+    uint32_t r = u;
+    uint32_t x = r;
+    os[i] = x;);
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint32_t *os = tmp + 6U;
+    uint8_t *bj = p.personal + i * 4U;
+    uint32_t u = load32_le(bj);
+    uint32_t r = u;
+    uint32_t x = r;
+    os[i] = x;);
+  tmp[0U] = nn ^ (kk << 8U ^ ((uint32_t)p.fanout << 16U ^ (uint32_t)p.depth << 24U));
+  tmp[1U] = p.leaf_length;
+  tmp[2U] = (uint32_t)p.node_offset;
+  tmp[3U] =
+    (uint32_t)(p.node_offset >> 32U)
+    ^ ((uint32_t)p.node_depth << 16U ^ (uint32_t)p.inner_length << 24U);
+  uint32_t tmp0 = tmp[0U];
+  uint32_t tmp1 = tmp[1U];
+  uint32_t tmp2 = tmp[2U];
+  uint32_t tmp3 = tmp[3U];
+  uint32_t tmp4 = tmp[4U];
+  uint32_t tmp5 = tmp[5U];
+  uint32_t tmp6 = tmp[6U];
+  uint32_t tmp7 = tmp[7U];
+  uint32_t iv0_ = iv0 ^ tmp0;
+  uint32_t iv1_ = iv1 ^ tmp1;
+  uint32_t iv2_ = iv2 ^ tmp2;
+  uint32_t iv3_ = iv3 ^ tmp3;
+  uint32_t iv4_ = iv4 ^ tmp4;
+  uint32_t iv5_ = iv5 ^ tmp5;
+  uint32_t iv6_ = iv6 ^ tmp6;
+  uint32_t iv7_ = iv7 ^ tmp7;
+  r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1_, iv2_, iv3_);
+  r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4_, iv5_, iv6_, iv7_);
 }
 
 static void
@@ -254,7 +304,7 @@ update_key(
   {
     update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 void
@@ -291,7 +341,7 @@ Hacl_Hash_Blake2s_Simd128_update_last(
   memcpy(b, last, rem * sizeof (uint8_t));
   uint64_t totlen = prev + (uint64_t)len;
   update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 static inline void
@@ -367,7 +417,7 @@ Hacl_Hash_Blake2s_Simd128_finish(
   Lib_IntVector_Intrinsics_vec128_store32_le(second, row1[0U]);
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, 32U, uint8_t);
+  Lib_Memzero0_memzero(b, 32U, uint8_t, void *);
 }
 
 void
@@ -788,7 +838,7 @@ Hacl_Hash_Blake2s_Simd128_hash_with_key(
   Hacl_Hash_Blake2s_Simd128_init(b, key_len, output_len);
   update(b1, b, key_len, key, input_len, input);
   Hacl_Hash_Blake2s_Simd128_finish(output_len, output, b);
-  Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec128);
-  Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec128);
+  Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec128, void *);
+  Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec128, void *);
 }
 
diff --git a/src/Lib_RandomBuffer_System.c b/src/Lib_RandomBuffer_System.c
index 0d7924b4..de6ef337 100644
--- a/src/Lib_RandomBuffer_System.c
+++ b/src/Lib_RandomBuffer_System.c
@@ -31,6 +31,7 @@ bool read_random_bytes(uint32_t len, uint8_t *buf) {
 #include <stdlib.h>
 #include <sys/stat.h>
 #include <sys/types.h>
+#include <sys/syscall.h>
 #include <unistd.h>
 
 bool read_random_bytes(uint32_t len, uint8_t *buf) {
diff --git a/src/msvc/EverCrypt_DRBG.c b/src/msvc/EverCrypt_DRBG.c
index 1395f59f..c76a69cd 100644
--- a/src/msvc/EverCrypt_DRBG.c
+++ b/src/msvc/EverCrypt_DRBG.c
@@ -1798,8 +1798,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);
@@ -1822,8 +1822,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);
@@ -1846,8 +1846,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);
@@ -1870,8 +1870,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);
diff --git a/src/msvc/Hacl_Ed25519.c b/src/msvc/Hacl_Ed25519.c
index 05d96cd0..d1f8edf2 100644
--- a/src/msvc/Hacl_Ed25519.c
+++ b/src/msvc/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)
diff --git a/src/msvc/Hacl_Frodo1344.c b/src/msvc/Hacl_Frodo1344.c
index 61262a4c..f4c19de3 100644
--- a/src/msvc/Hacl_Frodo1344.c
+++ b/src/msvc/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,12 +119,12 @@ 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 = (uint8_t *)alloca(ss_init_len * sizeof (uint8_t));
@@ -132,9 +132,9 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   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;
 }
 
diff --git a/src/msvc/Hacl_Frodo64.c b/src/msvc/Hacl_Frodo64.c
index 392d87f9..e9a19d93 100644
--- a/src/msvc/Hacl_Frodo64.c
+++ b/src/msvc/Hacl_Frodo64.c
@@ -60,7 +60,7 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = 0x5fU;
   memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2048U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(64U, 8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(64U, 8U, r + 1024U, e_matrix);
   uint16_t b_matrix[512U] = { 0U };
@@ -70,14 +70,14 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_add(64U, 8U, b_matrix, e_matrix);
   Hacl_Impl_Frodo_Pack_frodo_pack(64U, 8U, 15U, b_matrix, b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes(64U, 8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(e_matrix, 512U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(e_matrix, 512U, uint16_t, void *);
   uint32_t slen1 = 2016U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, 16U * sizeof (uint8_t));
   memcpy(sk_p + 16U, pk, 976U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(976U, pk, 16U, sk + slen1);
-  Lib_Memzero0_memzero(coins, 48U, uint8_t);
+  Lib_Memzero0_memzero(coins, 48U, uint8_t, void *);
   return 0U;
 }
 
@@ -102,7 +102,7 @@ uint32_t Hacl_Frodo64_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, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2176U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r + 1024U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 8U, r + 2048U, epp_matrix);
@@ -122,12 +122,12 @@ uint32_t Hacl_Frodo64_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(15U, 2U, 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, 15U, v_matrix, c2);
-  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t);
-  Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *);
+  Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint32_t ss_init_len = 1096U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t *shake_input_ss = (uint8_t *)alloca(ss_init_len * sizeof (uint8_t));
@@ -135,9 +135,9 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, 1080U * sizeof (uint8_t));
   memcpy(shake_input_ss + 1080U, k, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(ss_init_len, shake_input_ss, 16U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t);
-  Lib_Memzero0_memzero(coins, 16U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *);
+  Lib_Memzero0_memzero(coins, 16U, uint8_t, void *);
   return 0U;
 }
 
@@ -157,8 +157,8 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_mul_s(8U, 64U, 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(15U, 2U, 8U, m_matrix, mu_decode);
-  Lib_Memzero0_memzero(s_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *);
   uint8_t seed_se_k[32U] = { 0U };
   uint32_t pkh_mu_decode_len = 32U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -181,7 +181,7 @@ uint32_t Hacl_Frodo64_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, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 2176U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 64U, r + 1024U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64(8U, 8U, r + 2048U, epp_matrix);
@@ -199,12 +199,12 @@ uint32_t Hacl_Frodo64_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(15U, 2U, 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, 64U, 15U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2(8U, 8U, 15U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 512U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 64U, 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;
@@ -226,10 +226,10 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, 1080U * sizeof (uint8_t));
   memcpy(ss_init + 1080U, kp_s, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(ss_init_len, ss_init, 16U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(kp_s, 16U, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t);
-  Lib_Memzero0_memzero(mu_decode, 16U, uint8_t);
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(kp_s, 16U, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *);
+  Lib_Memzero0_memzero(mu_decode, 16U, uint8_t, void *);
   return 0U;
 }
 
diff --git a/src/msvc/Hacl_Frodo640.c b/src/msvc/Hacl_Frodo640.c
index 5de5871f..3a117991 100644
--- a/src/msvc/Hacl_Frodo640.c
+++ b/src/msvc/Hacl_Frodo640.c
@@ -55,7 +55,7 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = 0x5fU;
   memcpy(shake_input_seed_se + 1U, seed_se, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20480U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(640U, 8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(640U, 8U, r + 10240U, e_matrix);
   uint16_t b_matrix[5120U] = { 0U };
@@ -66,14 +66,14 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_add(640U, 8U, b_matrix, e_matrix);
   Hacl_Impl_Frodo_Pack_frodo_pack(640U, 8U, 15U, b_matrix, b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes(640U, 8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(e_matrix, 5120U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(e_matrix, 5120U, uint16_t, void *);
   uint32_t slen1 = 19872U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, 16U * sizeof (uint8_t));
   memcpy(sk_p + 16U, pk, 9616U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(9616U, pk, 16U, sk + slen1);
-  Lib_Memzero0_memzero(coins, 48U, uint8_t);
+  Lib_Memzero0_memzero(coins, 48U, uint8_t, void *);
   return 0U;
 }
 
@@ -98,7 +98,7 @@ uint32_t Hacl_Frodo640_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, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20608U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r + 10240U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 8U, r + 20480U, epp_matrix);
@@ -119,12 +119,12 @@ uint32_t Hacl_Frodo640_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(15U, 2U, 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, 15U, v_matrix, c2);
-  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t);
-  Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *);
+  Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint32_t ss_init_len = 9736U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t *shake_input_ss = (uint8_t *)alloca(ss_init_len * sizeof (uint8_t));
@@ -132,9 +132,9 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, 9720U * sizeof (uint8_t));
   memcpy(shake_input_ss + 9720U, k, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(ss_init_len, shake_input_ss, 16U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t);
-  Lib_Memzero0_memzero(coins, 16U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *);
+  Lib_Memzero0_memzero(coins, 16U, uint8_t, void *);
   return 0U;
 }
 
@@ -154,8 +154,8 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_mul_s(8U, 640U, 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(15U, 2U, 8U, m_matrix, mu_decode);
-  Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *);
   uint8_t seed_se_k[32U] = { 0U };
   uint32_t pkh_mu_decode_len = 32U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -178,7 +178,7 @@ uint32_t Hacl_Frodo640_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, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(17U, shake_input_seed_se, 20608U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 17U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 640U, r + 10240U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640(8U, 8U, r + 20480U, epp_matrix);
@@ -197,12 +197,12 @@ uint32_t Hacl_Frodo640_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(15U, 2U, 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, 640U, 15U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2(8U, 8U, 15U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 5120U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 640U, 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;
@@ -224,10 +224,10 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, 9720U * sizeof (uint8_t));
   memcpy(ss_init + 9720U, kp_s, 16U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake128_hacl(ss_init_len, ss_init, 16U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(kp_s, 16U, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t);
-  Lib_Memzero0_memzero(mu_decode, 16U, uint8_t);
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(kp_s, 16U, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 32U, uint8_t, void *);
+  Lib_Memzero0_memzero(mu_decode, 16U, uint8_t, void *);
   return 0U;
 }
 
diff --git a/src/msvc/Hacl_Frodo976.c b/src/msvc/Hacl_Frodo976.c
index 61454ceb..b358a5e2 100644
--- a/src/msvc/Hacl_Frodo976.c
+++ b/src/msvc/Hacl_Frodo976.c
@@ -55,7 +55,7 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = 0x5fU;
   memcpy(shake_input_seed_se + 1U, seed_se, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31232U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(976U, 8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(976U, 8U, r + 15616U, e_matrix);
   uint16_t b_matrix[7808U] = { 0U };
@@ -66,14 +66,14 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_add(976U, 8U, b_matrix, e_matrix);
   Hacl_Impl_Frodo_Pack_frodo_pack(976U, 8U, 16U, b_matrix, b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes(976U, 8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(e_matrix, 7808U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(e_matrix, 7808U, uint16_t, void *);
   uint32_t slen1 = 31272U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, 24U * sizeof (uint8_t));
   memcpy(sk_p + 24U, pk, 15632U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(15632U, pk, 24U, sk + slen1);
-  Lib_Memzero0_memzero(coins, 64U, uint8_t);
+  Lib_Memzero0_memzero(coins, 64U, uint8_t, void *);
   return 0U;
 }
 
@@ -98,7 +98,7 @@ uint32_t Hacl_Frodo976_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, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31360U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r + 15616U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 8U, r + 31232U, epp_matrix);
@@ -119,12 +119,12 @@ uint32_t Hacl_Frodo976_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, 3U, 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, 7808U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(v_matrix, 64U, uint16_t, void *);
+  Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint32_t ss_init_len = 15768U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t *shake_input_ss = (uint8_t *)alloca(ss_init_len * sizeof (uint8_t));
@@ -132,9 +132,9 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, 15744U * sizeof (uint8_t));
   memcpy(shake_input_ss + 15744U, k, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(ss_init_len, shake_input_ss, 24U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t);
-  Lib_Memzero0_memzero(coins, 24U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t, void *);
+  Lib_Memzero0_memzero(coins, 24U, uint8_t, void *);
   return 0U;
 }
 
@@ -154,8 +154,8 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_mul_s(8U, 976U, 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, 3U, 8U, m_matrix, mu_decode);
-  Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(s_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(m_matrix, 64U, uint16_t, void *);
   uint8_t seed_se_k[48U] = { 0U };
   uint32_t pkh_mu_decode_len = 48U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -178,7 +178,7 @@ uint32_t Hacl_Frodo976_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, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(25U, shake_input_seed_se, 31360U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t);
+  Lib_Memzero0_memzero(shake_input_seed_se, 25U, uint8_t, void *);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 976U, r + 15616U, ep_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976(8U, 8U, r + 31232U, epp_matrix);
@@ -197,12 +197,12 @@ uint32_t Hacl_Frodo976_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, 3U, 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, 976U, 16U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2(8U, 8U, 16U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t);
-  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(ep_matrix, 7808U, uint16_t, void *);
+  Lib_Memzero0_memzero(epp_matrix, 64U, uint16_t, void *);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq(8U, 976U, 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_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, 15744U * sizeof (uint8_t));
   memcpy(ss_init + 15744U, kp_s, 24U * sizeof (uint8_t));
   Hacl_Hash_SHA3_shake256_hacl(ss_init_len, ss_init, 24U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
-  Lib_Memzero0_memzero(kp_s, 24U, uint8_t);
-  Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t);
-  Lib_Memzero0_memzero(mu_decode, 24U, uint8_t);
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t, void *);
+  Lib_Memzero0_memzero(kp_s, 24U, uint8_t, void *);
+  Lib_Memzero0_memzero(seed_se_k, 48U, uint8_t, void *);
+  Lib_Memzero0_memzero(mu_decode, 24U, uint8_t, void *);
   return 0U;
 }
 
diff --git a/src/msvc/Hacl_Hash_Blake2b.c b/src/msvc/Hacl_Hash_Blake2b.c
index 2dceaf4b..68de8340 100644
--- a/src/msvc/Hacl_Hash_Blake2b.c
+++ b/src/msvc/Hacl_Hash_Blake2b.c
@@ -474,6 +474,7 @@ update_block(uint64_t *wv, uint64_t *hash, bool flag, FStar_UInt128_uint128 totl
 
 void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn)
 {
+  uint64_t tmp[8U] = { 0U };
   uint64_t *r0 = hash;
   uint64_t *r1 = hash + 4U;
   uint64_t *r2 = hash + 8U;
@@ -494,16 +495,67 @@ void Hacl_Hash_Blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn)
   r3[1U] = iv5;
   r3[2U] = iv6;
   r3[3U] = iv7;
-  uint64_t kk_shift_8 = (uint64_t)kk << 8U;
-  uint64_t iv0_ = iv0 ^ (0x01010000ULL ^ (kk_shift_8 ^ (uint64_t)nn));
+  uint8_t salt[16U] = { 0U };
+  uint8_t personal[16U] = { 0U };
+  Hacl_Hash_Blake2s_blake2_params
+  p =
+    {
+      .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U,
+      .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 4U;
+    uint8_t *bj = p.salt + i * 8U;
+    uint64_t u = load64_le(bj);
+    uint64_t r = u;
+    uint64_t x = r;
+    os[i] = x;);
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 6U;
+    uint8_t *bj = p.personal + i * 8U;
+    uint64_t u = load64_le(bj);
+    uint64_t r = u;
+    uint64_t x = r;
+    os[i] = x;);
+  tmp[0U] =
+    (uint64_t)nn
+    ^
+      ((uint64_t)kk
+      << 8U
+      ^ ((uint64_t)p.fanout << 16U ^ ((uint64_t)p.depth << 24U ^ (uint64_t)p.leaf_length << 32U)));
+  tmp[1U] = p.node_offset;
+  tmp[2U] = (uint64_t)p.node_depth ^ (uint64_t)p.inner_length << 8U;
+  tmp[3U] = 0ULL;
+  uint64_t tmp0 = tmp[0U];
+  uint64_t tmp1 = tmp[1U];
+  uint64_t tmp2 = tmp[2U];
+  uint64_t tmp3 = tmp[3U];
+  uint64_t tmp4 = tmp[4U];
+  uint64_t tmp5 = tmp[5U];
+  uint64_t tmp6 = tmp[6U];
+  uint64_t tmp7 = tmp[7U];
+  uint64_t iv0_ = iv0 ^ tmp0;
+  uint64_t iv1_ = iv1 ^ tmp1;
+  uint64_t iv2_ = iv2 ^ tmp2;
+  uint64_t iv3_ = iv3 ^ tmp3;
+  uint64_t iv4_ = iv4 ^ tmp4;
+  uint64_t iv5_ = iv5 ^ tmp5;
+  uint64_t iv6_ = iv6 ^ tmp6;
+  uint64_t iv7_ = iv7 ^ tmp7;
   r0[0U] = iv0_;
-  r0[1U] = iv1;
-  r0[2U] = iv2;
-  r0[3U] = iv3;
-  r1[0U] = iv4;
-  r1[1U] = iv5;
-  r1[2U] = iv6;
-  r1[3U] = iv7;
+  r0[1U] = iv1_;
+  r0[2U] = iv2_;
+  r0[3U] = iv3_;
+  r1[0U] = iv4_;
+  r1[1U] = iv5_;
+  r1[2U] = iv6_;
+  r1[3U] = iv7_;
 }
 
 static void update_key(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, uint32_t ll)
@@ -519,7 +571,7 @@ static void update_key(uint64_t *wv, uint64_t *hash, uint32_t kk, uint8_t *k, ui
   {
     update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, 128U, uint8_t);
+  Lib_Memzero0_memzero(b, 128U, uint8_t, void *);
 }
 
 void
@@ -560,7 +612,7 @@ Hacl_Hash_Blake2b_update_last(
   FStar_UInt128_uint128
   totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len));
   update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, 128U, uint8_t);
+  Lib_Memzero0_memzero(b, 128U, uint8_t, void *);
 }
 
 static void
@@ -624,7 +676,7 @@ void Hacl_Hash_Blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash)
   KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store64_le(second + i * 8U, row1[i]););
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 /**
@@ -965,7 +1017,7 @@ Hacl_Hash_Blake2b_hash_with_key(
   Hacl_Hash_Blake2b_init(b, key_len, output_len);
   update(b1, b, key_len, key, input_len, input);
   Hacl_Hash_Blake2b_finish(output_len, output, b);
-  Lib_Memzero0_memzero(b1, 16U, uint64_t);
-  Lib_Memzero0_memzero(b, 16U, uint64_t);
+  Lib_Memzero0_memzero(b1, 16U, uint64_t, void *);
+  Lib_Memzero0_memzero(b, 16U, uint64_t, void *);
 }
 
diff --git a/src/msvc/Hacl_Hash_Blake2b_Simd256.c b/src/msvc/Hacl_Hash_Blake2b_Simd256.c
index 1a5e8cf2..7aea4d42 100644
--- a/src/msvc/Hacl_Hash_Blake2b_Simd256.c
+++ b/src/msvc/Hacl_Hash_Blake2b_Simd256.c
@@ -26,6 +26,7 @@
 #include "internal/Hacl_Hash_Blake2b_Simd256.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "lib_memzero0.h"
 
 static inline void
@@ -214,6 +215,7 @@ update_block(
 void
 Hacl_Hash_Blake2b_Simd256_init(Lib_IntVector_Intrinsics_vec256 *hash, uint32_t kk, uint32_t nn)
 {
+  uint64_t tmp[8U] = { 0U };
   Lib_IntVector_Intrinsics_vec256 *r0 = hash;
   Lib_IntVector_Intrinsics_vec256 *r1 = hash + 1U;
   Lib_IntVector_Intrinsics_vec256 *r2 = hash + 2U;
@@ -228,10 +230,61 @@ Hacl_Hash_Blake2b_Simd256_init(Lib_IntVector_Intrinsics_vec256 *hash, uint32_t k
   uint64_t iv7 = Hacl_Hash_Blake2s_ivTable_B[7U];
   r2[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0, iv1, iv2, iv3);
   r3[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7);
-  uint64_t kk_shift_8 = (uint64_t)kk << 8U;
-  uint64_t iv0_ = iv0 ^ (0x01010000ULL ^ (kk_shift_8 ^ (uint64_t)nn));
-  r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1, iv2, iv3);
-  r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4, iv5, iv6, iv7);
+  uint8_t salt[16U] = { 0U };
+  uint8_t personal[16U] = { 0U };
+  Hacl_Hash_Blake2s_blake2_params
+  p =
+    {
+      .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U,
+      .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 4U;
+    uint8_t *bj = p.salt + i * 8U;
+    uint64_t u = load64_le(bj);
+    uint64_t r = u;
+    uint64_t x = r;
+    os[i] = x;);
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint64_t *os = tmp + 6U;
+    uint8_t *bj = p.personal + i * 8U;
+    uint64_t u = load64_le(bj);
+    uint64_t r = u;
+    uint64_t x = r;
+    os[i] = x;);
+  tmp[0U] =
+    (uint64_t)nn
+    ^
+      ((uint64_t)kk
+      << 8U
+      ^ ((uint64_t)p.fanout << 16U ^ ((uint64_t)p.depth << 24U ^ (uint64_t)p.leaf_length << 32U)));
+  tmp[1U] = p.node_offset;
+  tmp[2U] = (uint64_t)p.node_depth ^ (uint64_t)p.inner_length << 8U;
+  tmp[3U] = 0ULL;
+  uint64_t tmp0 = tmp[0U];
+  uint64_t tmp1 = tmp[1U];
+  uint64_t tmp2 = tmp[2U];
+  uint64_t tmp3 = tmp[3U];
+  uint64_t tmp4 = tmp[4U];
+  uint64_t tmp5 = tmp[5U];
+  uint64_t tmp6 = tmp[6U];
+  uint64_t tmp7 = tmp[7U];
+  uint64_t iv0_ = iv0 ^ tmp0;
+  uint64_t iv1_ = iv1 ^ tmp1;
+  uint64_t iv2_ = iv2 ^ tmp2;
+  uint64_t iv3_ = iv3 ^ tmp3;
+  uint64_t iv4_ = iv4 ^ tmp4;
+  uint64_t iv5_ = iv5 ^ tmp5;
+  uint64_t iv6_ = iv6 ^ tmp6;
+  uint64_t iv7_ = iv7 ^ tmp7;
+  r0[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv0_, iv1_, iv2_, iv3_);
+  r1[0U] = Lib_IntVector_Intrinsics_vec256_load64s(iv4_, iv5_, iv6_, iv7_);
 }
 
 static void
@@ -254,7 +307,7 @@ update_key(
   {
     update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, 128U, uint8_t);
+  Lib_Memzero0_memzero(b, 128U, uint8_t, void *);
 }
 
 void
@@ -295,7 +348,7 @@ Hacl_Hash_Blake2b_Simd256_update_last(
   FStar_UInt128_uint128
   totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len));
   update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, 128U, uint8_t);
+  Lib_Memzero0_memzero(b, 128U, uint8_t, void *);
 }
 
 static inline void
@@ -371,7 +424,7 @@ Hacl_Hash_Blake2b_Simd256_finish(
   Lib_IntVector_Intrinsics_vec256_store64_le(second, row1[0U]);
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 void
@@ -822,7 +875,7 @@ Hacl_Hash_Blake2b_Simd256_hash_with_key(
   Hacl_Hash_Blake2b_Simd256_init(b, key_len, output_len);
   update(b1, b, key_len, key, input_len, input);
   Hacl_Hash_Blake2b_Simd256_finish(output_len, output, b);
-  Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec256);
-  Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec256);
+  Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec256, void *);
+  Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec256, void *);
 }
 
diff --git a/src/msvc/Hacl_Hash_Blake2s.c b/src/msvc/Hacl_Hash_Blake2s.c
index 652c3f33..37fabb67 100644
--- a/src/msvc/Hacl_Hash_Blake2s.c
+++ b/src/msvc/Hacl_Hash_Blake2s.c
@@ -26,6 +26,7 @@
 #include "internal/Hacl_Hash_Blake2s.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "lib_memzero0.h"
 
 static inline void
@@ -474,6 +475,7 @@ update_block(uint32_t *wv, uint32_t *hash, bool flag, uint64_t totlen, uint8_t *
 
 void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn)
 {
+  uint32_t tmp[8U] = { 0U };
   uint32_t *r0 = hash;
   uint32_t *r1 = hash + 4U;
   uint32_t *r2 = hash + 8U;
@@ -494,16 +496,64 @@ void Hacl_Hash_Blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn)
   r3[1U] = iv5;
   r3[2U] = iv6;
   r3[3U] = iv7;
-  uint32_t kk_shift_8 = kk << 8U;
-  uint32_t iv0_ = iv0 ^ (0x01010000U ^ (kk_shift_8 ^ nn));
+  uint8_t salt[8U] = { 0U };
+  uint8_t personal[8U] = { 0U };
+  Hacl_Hash_Blake2s_blake2_params
+  p =
+    {
+      .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U,
+      .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint32_t *os = tmp + 4U;
+    uint8_t *bj = p.salt + i * 4U;
+    uint32_t u = load32_le(bj);
+    uint32_t r = u;
+    uint32_t x = r;
+    os[i] = x;);
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint32_t *os = tmp + 6U;
+    uint8_t *bj = p.personal + i * 4U;
+    uint32_t u = load32_le(bj);
+    uint32_t r = u;
+    uint32_t x = r;
+    os[i] = x;);
+  tmp[0U] = nn ^ (kk << 8U ^ ((uint32_t)p.fanout << 16U ^ (uint32_t)p.depth << 24U));
+  tmp[1U] = p.leaf_length;
+  tmp[2U] = (uint32_t)p.node_offset;
+  tmp[3U] =
+    (uint32_t)(p.node_offset >> 32U)
+    ^ ((uint32_t)p.node_depth << 16U ^ (uint32_t)p.inner_length << 24U);
+  uint32_t tmp0 = tmp[0U];
+  uint32_t tmp1 = tmp[1U];
+  uint32_t tmp2 = tmp[2U];
+  uint32_t tmp3 = tmp[3U];
+  uint32_t tmp4 = tmp[4U];
+  uint32_t tmp5 = tmp[5U];
+  uint32_t tmp6 = tmp[6U];
+  uint32_t tmp7 = tmp[7U];
+  uint32_t iv0_ = iv0 ^ tmp0;
+  uint32_t iv1_ = iv1 ^ tmp1;
+  uint32_t iv2_ = iv2 ^ tmp2;
+  uint32_t iv3_ = iv3 ^ tmp3;
+  uint32_t iv4_ = iv4 ^ tmp4;
+  uint32_t iv5_ = iv5 ^ tmp5;
+  uint32_t iv6_ = iv6 ^ tmp6;
+  uint32_t iv7_ = iv7 ^ tmp7;
   r0[0U] = iv0_;
-  r0[1U] = iv1;
-  r0[2U] = iv2;
-  r0[3U] = iv3;
-  r1[0U] = iv4;
-  r1[1U] = iv5;
-  r1[2U] = iv6;
-  r1[3U] = iv7;
+  r0[1U] = iv1_;
+  r0[2U] = iv2_;
+  r0[3U] = iv3_;
+  r1[0U] = iv4_;
+  r1[1U] = iv5_;
+  r1[2U] = iv6_;
+  r1[3U] = iv7_;
 }
 
 static void update_key(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, uint32_t ll)
@@ -519,7 +569,7 @@ static void update_key(uint32_t *wv, uint32_t *hash, uint32_t kk, uint8_t *k, ui
   {
     update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 void
@@ -556,7 +606,7 @@ Hacl_Hash_Blake2s_update_last(
   memcpy(b, last, rem * sizeof (uint8_t));
   uint64_t totlen = prev + (uint64_t)len;
   update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 static void
@@ -614,7 +664,7 @@ void Hacl_Hash_Blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash)
   KRML_MAYBE_FOR4(i, 0U, 4U, 1U, store32_le(second + i * 4U, row1[i]););
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, 32U, uint8_t);
+  Lib_Memzero0_memzero(b, 32U, uint8_t, void *);
 }
 
 /**
@@ -925,7 +975,7 @@ Hacl_Hash_Blake2s_hash_with_key(
   Hacl_Hash_Blake2s_init(b, key_len, output_len);
   update(b1, b, key_len, key, input_len, input);
   Hacl_Hash_Blake2s_finish(output_len, output, b);
-  Lib_Memzero0_memzero(b1, 16U, uint32_t);
-  Lib_Memzero0_memzero(b, 16U, uint32_t);
+  Lib_Memzero0_memzero(b1, 16U, uint32_t, void *);
+  Lib_Memzero0_memzero(b, 16U, uint32_t, void *);
 }
 
diff --git a/src/msvc/Hacl_Hash_Blake2s_Simd128.c b/src/msvc/Hacl_Hash_Blake2s_Simd128.c
index 73f0cccb..ed86be43 100644
--- a/src/msvc/Hacl_Hash_Blake2s_Simd128.c
+++ b/src/msvc/Hacl_Hash_Blake2s_Simd128.c
@@ -26,6 +26,7 @@
 #include "internal/Hacl_Hash_Blake2s_Simd128.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "internal/Hacl_Hash_Blake2b.h"
 #include "lib_memzero0.h"
 
 static inline void
@@ -214,6 +215,7 @@ update_block(
 void
 Hacl_Hash_Blake2s_Simd128_init(Lib_IntVector_Intrinsics_vec128 *hash, uint32_t kk, uint32_t nn)
 {
+  uint32_t tmp[8U] = { 0U };
   Lib_IntVector_Intrinsics_vec128 *r0 = hash;
   Lib_IntVector_Intrinsics_vec128 *r1 = hash + 1U;
   Lib_IntVector_Intrinsics_vec128 *r2 = hash + 2U;
@@ -228,10 +230,58 @@ Hacl_Hash_Blake2s_Simd128_init(Lib_IntVector_Intrinsics_vec128 *hash, uint32_t k
   uint32_t iv7 = Hacl_Hash_Blake2s_ivTable_S[7U];
   r2[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0, iv1, iv2, iv3);
   r3[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7);
-  uint32_t kk_shift_8 = kk << 8U;
-  uint32_t iv0_ = iv0 ^ (0x01010000U ^ (kk_shift_8 ^ nn));
-  r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1, iv2, iv3);
-  r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4, iv5, iv6, iv7);
+  uint8_t salt[8U] = { 0U };
+  uint8_t personal[8U] = { 0U };
+  Hacl_Hash_Blake2s_blake2_params
+  p =
+    {
+      .digest_length = 32U, .key_length = 0U, .fanout = 1U, .depth = 1U, .leaf_length = 0U,
+      .node_offset = 0ULL, .node_depth = 0U, .inner_length = 0U, .salt = salt, .personal = personal
+    };
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint32_t *os = tmp + 4U;
+    uint8_t *bj = p.salt + i * 4U;
+    uint32_t u = load32_le(bj);
+    uint32_t r = u;
+    uint32_t x = r;
+    os[i] = x;);
+  KRML_MAYBE_FOR2(i,
+    0U,
+    2U,
+    1U,
+    uint32_t *os = tmp + 6U;
+    uint8_t *bj = p.personal + i * 4U;
+    uint32_t u = load32_le(bj);
+    uint32_t r = u;
+    uint32_t x = r;
+    os[i] = x;);
+  tmp[0U] = nn ^ (kk << 8U ^ ((uint32_t)p.fanout << 16U ^ (uint32_t)p.depth << 24U));
+  tmp[1U] = p.leaf_length;
+  tmp[2U] = (uint32_t)p.node_offset;
+  tmp[3U] =
+    (uint32_t)(p.node_offset >> 32U)
+    ^ ((uint32_t)p.node_depth << 16U ^ (uint32_t)p.inner_length << 24U);
+  uint32_t tmp0 = tmp[0U];
+  uint32_t tmp1 = tmp[1U];
+  uint32_t tmp2 = tmp[2U];
+  uint32_t tmp3 = tmp[3U];
+  uint32_t tmp4 = tmp[4U];
+  uint32_t tmp5 = tmp[5U];
+  uint32_t tmp6 = tmp[6U];
+  uint32_t tmp7 = tmp[7U];
+  uint32_t iv0_ = iv0 ^ tmp0;
+  uint32_t iv1_ = iv1 ^ tmp1;
+  uint32_t iv2_ = iv2 ^ tmp2;
+  uint32_t iv3_ = iv3 ^ tmp3;
+  uint32_t iv4_ = iv4 ^ tmp4;
+  uint32_t iv5_ = iv5 ^ tmp5;
+  uint32_t iv6_ = iv6 ^ tmp6;
+  uint32_t iv7_ = iv7 ^ tmp7;
+  r0[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv0_, iv1_, iv2_, iv3_);
+  r1[0U] = Lib_IntVector_Intrinsics_vec128_load32s(iv4_, iv5_, iv6_, iv7_);
 }
 
 static void
@@ -254,7 +304,7 @@ update_key(
   {
     update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 void
@@ -291,7 +341,7 @@ Hacl_Hash_Blake2s_Simd128_update_last(
   memcpy(b, last, rem * sizeof (uint8_t));
   uint64_t totlen = prev + (uint64_t)len;
   update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, 64U, uint8_t);
+  Lib_Memzero0_memzero(b, 64U, uint8_t, void *);
 }
 
 static inline void
@@ -367,7 +417,7 @@ Hacl_Hash_Blake2s_Simd128_finish(
   Lib_IntVector_Intrinsics_vec128_store32_le(second, row1[0U]);
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, 32U, uint8_t);
+  Lib_Memzero0_memzero(b, 32U, uint8_t, void *);
 }
 
 void
@@ -788,7 +838,7 @@ Hacl_Hash_Blake2s_Simd128_hash_with_key(
   Hacl_Hash_Blake2s_Simd128_init(b, key_len, output_len);
   update(b1, b, key_len, key, input_len, input);
   Hacl_Hash_Blake2s_Simd128_finish(output_len, output, b);
-  Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec128);
-  Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec128);
+  Lib_Memzero0_memzero(b1, 4U, Lib_IntVector_Intrinsics_vec128, void *);
+  Lib_Memzero0_memzero(b, 4U, Lib_IntVector_Intrinsics_vec128, void *);
 }
 
diff --git a/src/msvc/Lib_RandomBuffer_System.c b/src/msvc/Lib_RandomBuffer_System.c
index 0d7924b4..de6ef337 100644
--- a/src/msvc/Lib_RandomBuffer_System.c
+++ b/src/msvc/Lib_RandomBuffer_System.c
@@ -31,6 +31,7 @@ bool read_random_bytes(uint32_t len, uint8_t *buf) {
 #include <stdlib.h>
 #include <sys/stat.h>
 #include <sys/types.h>
+#include <sys/syscall.h>
 #include <unistd.h>
 
 bool read_random_bytes(uint32_t len, uint8_t *buf) {
diff --git a/src/wasm/EverCrypt_Hash.wasm b/src/wasm/EverCrypt_Hash.wasm
index 101c3f68..a5f05d9d 100644
Binary files a/src/wasm/EverCrypt_Hash.wasm and b/src/wasm/EverCrypt_Hash.wasm differ
diff --git a/src/wasm/Hacl_AEAD_Chacha20Poly1305_Simd256.wasm b/src/wasm/Hacl_AEAD_Chacha20Poly1305_Simd256.wasm
index 804858db..1f8a5cdc 100644
Binary files a/src/wasm/Hacl_AEAD_Chacha20Poly1305_Simd256.wasm and b/src/wasm/Hacl_AEAD_Chacha20Poly1305_Simd256.wasm differ
diff --git a/src/wasm/Hacl_Ed25519_PrecompTable.wasm b/src/wasm/Hacl_Ed25519_PrecompTable.wasm
index 46a7380d..c94538f0 100644
Binary files a/src/wasm/Hacl_Ed25519_PrecompTable.wasm and b/src/wasm/Hacl_Ed25519_PrecompTable.wasm differ
diff --git a/src/wasm/Hacl_HMAC.wasm b/src/wasm/Hacl_HMAC.wasm
index c2e51b85..4837783c 100644
Binary files a/src/wasm/Hacl_HMAC.wasm and b/src/wasm/Hacl_HMAC.wasm differ
diff --git a/src/wasm/Hacl_HMAC_DRBG.wasm b/src/wasm/Hacl_HMAC_DRBG.wasm
index c1cb2fd3..f536237d 100644
Binary files a/src/wasm/Hacl_HMAC_DRBG.wasm and b/src/wasm/Hacl_HMAC_DRBG.wasm differ
diff --git a/src/wasm/Hacl_Hash_Blake2b.wasm b/src/wasm/Hacl_Hash_Blake2b.wasm
index 8882f5e8..0727bd3b 100644
Binary files a/src/wasm/Hacl_Hash_Blake2b.wasm and b/src/wasm/Hacl_Hash_Blake2b.wasm differ
diff --git a/src/wasm/Hacl_Hash_Blake2b_Simd256.wasm b/src/wasm/Hacl_Hash_Blake2b_Simd256.wasm
index 27244515..d144e065 100644
Binary files a/src/wasm/Hacl_Hash_Blake2b_Simd256.wasm and b/src/wasm/Hacl_Hash_Blake2b_Simd256.wasm differ
diff --git a/src/wasm/Hacl_Hash_Blake2s.wasm b/src/wasm/Hacl_Hash_Blake2s.wasm
index 0dcaff92..755a6306 100644
Binary files a/src/wasm/Hacl_Hash_Blake2s.wasm and b/src/wasm/Hacl_Hash_Blake2s.wasm differ
diff --git a/src/wasm/Hacl_Hash_Blake2s_Simd128.wasm b/src/wasm/Hacl_Hash_Blake2s_Simd128.wasm
index 6d5cdb78..fd3c1b86 100644
Binary files a/src/wasm/Hacl_Hash_Blake2s_Simd128.wasm and b/src/wasm/Hacl_Hash_Blake2s_Simd128.wasm differ
diff --git a/src/wasm/Hacl_SHA2_Vec128.wasm b/src/wasm/Hacl_SHA2_Vec128.wasm
index cef1c90d..549c8a5f 100644
Binary files a/src/wasm/Hacl_SHA2_Vec128.wasm and b/src/wasm/Hacl_SHA2_Vec128.wasm differ
diff --git a/src/wasm/INFO.txt b/src/wasm/INFO.txt
index d2f1192f..197a9c67 100644
--- a/src/wasm/INFO.txt
+++ b/src/wasm/INFO.txt
@@ -1,4 +1,4 @@
 This code was generated with the following toolchain.
-F* version: 6e23042e74555544267731295b7d382c86edc574
-Karamel version: a7be2a7c43eca637ceb57fe8f3ffd16fc6627ebd
+F* version: 7c8968bb0e417da75144912dcffd714364525eb2
+Karamel version: d9186a778bd8a730cc8ddcd84eac542fa7226a59
 Vale version: 0.3.19
diff --git a/src/wasm/layouts.json b/src/wasm/layouts.json
index 81273a66..6d56245a 100644
--- a/src/wasm/layouts.json
+++ b/src/wasm/layouts.json
@@ -1 +1 @@
-{"Spec_Hash_Definitions_hash_alg":["LEnum"],"Prims_string":["LBuiltin",["I32"],["A32"]],"Prims_int":["LBuiltin",["I32"],["A32"]],"K___uint32_t_uint32_t":["LFlat",{"size":8,"fields":[["fst",[0,["Int",["A32"]]]],["snd",[4,["Int",["A32"]]]]]}],"__bool_bool_bool_bool":["LFlat",{"size":4,"fields":[["fst",[0,["Int",["A8"]]]],["snd",[1,["Int",["A8"]]]],["thd",[2,["Int",["A8"]]]],["f3",[3,["Int",["A8"]]]]]}],"__bool_bool":["LFlat",{"size":2,"fields":[["fst",[0,["Int",["A8"]]]],["snd",[1,["Int",["A8"]]]]]}],"Hacl_Streaming_Types_error_code":["LEnum"],"Hacl_MAC_Poly1305_state_t":["LFlat",{"size":20,"fields":[["block_state",[0,["Pointer",["Int",["A64"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]],["p_key",[16,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Streaming_MD_state_64":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Int",["A64"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"Hacl_Streaming_MD_state_32":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Int",["A32"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"Hacl_Hash_SHA3_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_SHA3_hash_buf"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"hash_buf2":["LFlat",{"size":16,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA3_hash_buf"]]],["snd",[8,["Layout","Hacl_Hash_SHA3_hash_buf"]]]]}],"Hacl_Hash_SHA3_hash_buf":["LFlat",{"size":8,"fields":[["fst",[0,["Int",["A32"]]]],["snd",[4,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Hash_Blake2s_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2s_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2s_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A32"]]]]],["snd",[4,["Pointer",["Int",["A32"]]]]]]}],"Hacl_Hash_Blake2s_Simd128_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2s_Simd128_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2s_Simd128_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Unknown"]]]],["snd",[4,["Pointer",["Unknown"]]]]]}],"Hacl_Hash_Blake2b_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2b_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2b_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A64"]]]]],["snd",[4,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Hash_Blake2b_Simd256_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2b_Simd256_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2b_Simd256_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Unknown"]]]],["snd",[4,["Pointer",["Unknown"]]]]]}],"Hacl_Hash_SHA2_uint8_8p":["LFlat",{"size":56,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_7p"]]]]}],"Hacl_Hash_SHA2_uint8_7p":["LFlat",{"size":48,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_6p"]]]]}],"Hacl_Hash_SHA2_uint8_6p":["LFlat",{"size":40,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_5p"]]]]}],"Hacl_Hash_SHA2_uint8_5p":["LFlat",{"size":32,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_4p"]]]]}],"Hacl_Hash_SHA2_uint8_4p":["LFlat",{"size":24,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_3p"]]]]}],"Hacl_Hash_SHA2_uint8_3p":["LFlat",{"size":16,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_2p"]]]]}],"Hacl_Hash_SHA2_uint8_2x8p":["LFlat",{"size":112,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA2_uint8_8p"]]],["snd",[56,["Layout","Hacl_Hash_SHA2_uint8_8p"]]]]}],"Hacl_Hash_SHA2_uint8_2x4p":["LFlat",{"size":48,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA2_uint8_4p"]]],["snd",[24,["Layout","Hacl_Hash_SHA2_uint8_4p"]]]]}],"Hacl_Hash_SHA2_uint8_2p":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[4,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Impl_HPKE_context_s":["LFlat",{"size":16,"fields":[["ctx_key",[0,["Pointer",["Int",["A8"]]]]],["ctx_nonce",[4,["Pointer",["Int",["A8"]]]]],["ctx_seq",[8,["Pointer",["Int",["A64"]]]]],["ctx_exporter",[12,["Pointer",["Int",["A8"]]]]]]}],"Hacl_HMAC_DRBG_state":["LFlat",{"size":12,"fields":[["k",[0,["Pointer",["Int",["A8"]]]]],["v",[4,["Pointer",["Int",["A8"]]]]],["reseed_counter",[8,["Pointer",["Int",["A32"]]]]]]}],"Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64":["LFlat",{"size":20,"fields":[["len",[0,["Int",["A32"]]]],["n",[4,["Pointer",["Int",["A64"]]]]],["mu",[8,["Int",["A64"]]]],["r2",[16,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32":["LFlat",{"size":16,"fields":[["len",[0,["Int",["A32"]]]],["n",[4,["Pointer",["Int",["A32"]]]]],["mu",[8,["Int",["A32"]]]],["r2",[12,["Pointer",["Int",["A32"]]]]]]}],"FStar_UInt128_uint128":["LFlat",{"size":16,"fields":[["low",[0,["Int",["A64"]]]],["high",[8,["Int",["A64"]]]]]}],"EverCrypt_Hash_Incremental_state_t":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Layout","EverCrypt_Hash_state_s"]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"state_s_tags":["LEnum"],"EverCrypt_Hash_state_s":["LFlat",{"size":12,"fields":[["tag",[0,["Int",["A32"]]]],["val",[8,["Union",[["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A32"]]],["Pointer",["Unknown"]],["Pointer",["Int",["A64"]]],["Pointer",["Unknown"]]]]]]]}],"EverCrypt_Error_error_code":["LEnum"],"C_String_t_":["LBuiltin",["I32"],["A32"]],"C_String_t":["LBuiltin",["I32"],["A32"]],"C_Compat_String_t_":["LBuiltin",["I32"],["A32"]],"C_Compat_String_t":["LBuiltin",["I32"],["A32"]],"exit_code":["LBuiltin",["I32"],["A32"]],"clock_t":["LBuiltin",["I32"],["A32"]]}
\ No newline at end of file
+{"Spec_Hash_Definitions_hash_alg":["LEnum"],"Prims_string":["LBuiltin",["I32"],["A32"]],"Prims_int":["LBuiltin",["I32"],["A32"]],"K___uint32_t_uint32_t":["LFlat",{"size":8,"fields":[["fst",[0,["Int",["A32"]]]],["snd",[4,["Int",["A32"]]]]]}],"__bool_bool_bool_bool":["LFlat",{"size":4,"fields":[["fst",[0,["Int",["A8"]]]],["snd",[1,["Int",["A8"]]]],["thd",[2,["Int",["A8"]]]],["f3",[3,["Int",["A8"]]]]]}],"__bool_bool":["LFlat",{"size":2,"fields":[["fst",[0,["Int",["A8"]]]],["snd",[1,["Int",["A8"]]]]]}],"Hacl_Streaming_Types_error_code":["LEnum"],"Hacl_MAC_Poly1305_state_t":["LFlat",{"size":20,"fields":[["block_state",[0,["Pointer",["Int",["A64"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]],["p_key",[16,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Streaming_MD_state_64":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Int",["A64"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"Hacl_Streaming_MD_state_32":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Int",["A32"]]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"Hacl_Hash_SHA3_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_SHA3_hash_buf"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"hash_buf2":["LFlat",{"size":16,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA3_hash_buf"]]],["snd",[8,["Layout","Hacl_Hash_SHA3_hash_buf"]]]]}],"Hacl_Hash_SHA3_hash_buf":["LFlat",{"size":8,"fields":[["fst",[0,["Int",["A32"]]]],["snd",[4,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Hash_Blake2s_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2s_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2s_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A32"]]]]],["snd",[4,["Pointer",["Int",["A32"]]]]]]}],"Hacl_Hash_Blake2s_Simd128_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2s_Simd128_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2s_Simd128_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Unknown"]]]],["snd",[4,["Pointer",["Unknown"]]]]]}],"Hacl_Hash_Blake2b_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2b_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2b_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A64"]]]]],["snd",[4,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Hash_Blake2b_Simd256_state_t":["LFlat",{"size":24,"fields":[["block_state",[0,["Layout","Hacl_Hash_Blake2b_Simd256_block_state_t"]]],["buf",[8,["Pointer",["Int",["A8"]]]]],["total_len",[16,["Int",["A64"]]]]]}],"Hacl_Hash_Blake2b_Simd256_block_state_t":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Unknown"]]]],["snd",[4,["Pointer",["Unknown"]]]]]}],"Hacl_Hash_SHA2_uint8_8p":["LFlat",{"size":56,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_7p"]]]]}],"Hacl_Hash_SHA2_uint8_7p":["LFlat",{"size":48,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_6p"]]]]}],"Hacl_Hash_SHA2_uint8_6p":["LFlat",{"size":40,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_5p"]]]]}],"Hacl_Hash_SHA2_uint8_5p":["LFlat",{"size":32,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_4p"]]]]}],"Hacl_Hash_SHA2_uint8_4p":["LFlat",{"size":24,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_3p"]]]]}],"Hacl_Hash_SHA2_uint8_3p":["LFlat",{"size":16,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[8,["Layout","Hacl_Hash_SHA2_uint8_2p"]]]]}],"Hacl_Hash_SHA2_uint8_2x8p":["LFlat",{"size":112,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA2_uint8_8p"]]],["snd",[56,["Layout","Hacl_Hash_SHA2_uint8_8p"]]]]}],"Hacl_Hash_SHA2_uint8_2x4p":["LFlat",{"size":48,"fields":[["fst",[0,["Layout","Hacl_Hash_SHA2_uint8_4p"]]],["snd",[24,["Layout","Hacl_Hash_SHA2_uint8_4p"]]]]}],"Hacl_Hash_SHA2_uint8_2p":["LFlat",{"size":8,"fields":[["fst",[0,["Pointer",["Int",["A8"]]]]],["snd",[4,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Impl_HPKE_context_s":["LFlat",{"size":16,"fields":[["ctx_key",[0,["Pointer",["Int",["A8"]]]]],["ctx_nonce",[4,["Pointer",["Int",["A8"]]]]],["ctx_seq",[8,["Pointer",["Int",["A64"]]]]],["ctx_exporter",[12,["Pointer",["Int",["A8"]]]]]]}],"Hacl_Hash_Blake2s_blake2_params":["LFlat",{"size":28,"fields":[["digest_length",[0,["Int",["A8"]]]],["key_length",[1,["Int",["A8"]]]],["fanout",[2,["Int",["A8"]]]],["depth",[3,["Int",["A8"]]]],["leaf_length",[4,["Int",["A32"]]]],["node_offset",[8,["Int",["A64"]]]],["node_depth",[16,["Int",["A8"]]]],["inner_length",[17,["Int",["A8"]]]],["salt",[20,["Pointer",["Int",["A8"]]]]],["personal",[24,["Pointer",["Int",["A8"]]]]]]}],"Hacl_HMAC_DRBG_state":["LFlat",{"size":12,"fields":[["k",[0,["Pointer",["Int",["A8"]]]]],["v",[4,["Pointer",["Int",["A8"]]]]],["reseed_counter",[8,["Pointer",["Int",["A32"]]]]]]}],"Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64":["LFlat",{"size":20,"fields":[["len",[0,["Int",["A32"]]]],["n",[4,["Pointer",["Int",["A64"]]]]],["mu",[8,["Int",["A64"]]]],["r2",[16,["Pointer",["Int",["A64"]]]]]]}],"Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32":["LFlat",{"size":16,"fields":[["len",[0,["Int",["A32"]]]],["n",[4,["Pointer",["Int",["A32"]]]]],["mu",[8,["Int",["A32"]]]],["r2",[12,["Pointer",["Int",["A32"]]]]]]}],"FStar_UInt128_uint128":["LFlat",{"size":16,"fields":[["low",[0,["Int",["A64"]]]],["high",[8,["Int",["A64"]]]]]}],"EverCrypt_Hash_Incremental_state_t":["LFlat",{"size":16,"fields":[["block_state",[0,["Pointer",["Layout","EverCrypt_Hash_state_s"]]]],["buf",[4,["Pointer",["Int",["A8"]]]]],["total_len",[8,["Int",["A64"]]]]]}],"state_s_tags":["LEnum"],"EverCrypt_Hash_state_s":["LFlat",{"size":12,"fields":[["tag",[0,["Int",["A32"]]]],["val",[8,["Union",[["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A32"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A64"]]],["Pointer",["Int",["A32"]]],["Pointer",["Unknown"]],["Pointer",["Int",["A64"]]],["Pointer",["Unknown"]]]]]]]}],"EverCrypt_Error_error_code":["LEnum"],"C_String_t_":["LBuiltin",["I32"],["A32"]],"C_String_t":["LBuiltin",["I32"],["A32"]],"C_Compat_String_t_":["LBuiltin",["I32"],["A32"]],"C_Compat_String_t":["LBuiltin",["I32"],["A32"]],"exit_code":["LBuiltin",["I32"],["A32"]],"clock_t":["LBuiltin",["I32"],["A32"]]}
\ No newline at end of file