diff --git a/include/EverCrypt_AEAD.h b/include/EverCrypt_AEAD.h
index 4797df68..5d52493b 100644
--- a/include/EverCrypt_AEAD.h
+++ b/include/EverCrypt_AEAD.h
@@ -42,6 +42,10 @@ extern "C" {
 
 typedef struct EverCrypt_AEAD_state_s_s EverCrypt_AEAD_state_s;
 
+/**
+Both encryption and decryption require a state that holds the key.
+The state may be reused as many times as desired.
+*/
 bool EverCrypt_AEAD_uu___is_Ek(Spec_Agile_AEAD_alg a, EverCrypt_AEAD_state_s projectee);
 
 /**
diff --git a/include/EverCrypt_DRBG.h b/include/EverCrypt_DRBG.h
index aee4e800..b3161bfe 100644
--- a/include/EverCrypt_DRBG.h
+++ b/include/EverCrypt_DRBG.h
@@ -36,7 +36,6 @@ extern "C" {
 #include "krml/internal/target.h"
 
 #include "Lib_RandomBuffer_System.h"
-#include "Lib_Memzero0.h"
 #include "Hacl_Streaming_Types.h"
 #include "Hacl_HMAC_DRBG.h"
 
diff --git a/include/Hacl_Frodo1344.h b/include/Hacl_Frodo1344.h
index 85d29c9f..9fca4c82 100644
--- a/include/Hacl_Frodo1344.h
+++ b/include/Hacl_Frodo1344.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo1344_crypto_bytes;
diff --git a/include/Hacl_Frodo64.h b/include/Hacl_Frodo64.h
index eb17defe..05aecb59 100644
--- a/include/Hacl_Frodo64.h
+++ b/include/Hacl_Frodo64.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 /*
diff --git a/include/Hacl_Frodo640.h b/include/Hacl_Frodo640.h
index c4bf30d7..10c9bd47 100644
--- a/include/Hacl_Frodo640.h
+++ b/include/Hacl_Frodo640.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo640_crypto_bytes;
diff --git a/include/Hacl_Frodo976.h b/include/Hacl_Frodo976.h
index 458ebd2f..c2d5f84f 100644
--- a/include/Hacl_Frodo976.h
+++ b/include/Hacl_Frodo976.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Hash_SHA3.h"
 
 extern uint32_t Hacl_Frodo976_crypto_bytes;
diff --git a/include/Hacl_Hash_Blake2.h b/include/Hacl_Hash_Blake2.h
index aff1c7a9..3ee29015 100644
--- a/include/Hacl_Hash_Blake2.h
+++ b/include/Hacl_Hash_Blake2.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Krmllib.h"
 
 void Hacl_Blake2b_32_blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn);
diff --git a/include/Hacl_Hash_Blake2b_256.h b/include/Hacl_Hash_Blake2b_256.h
index 88bf9ab2..2379fd75 100644
--- a/include/Hacl_Hash_Blake2b_256.h
+++ b/include/Hacl_Hash_Blake2b_256.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "Hacl_Krmllib.h"
 #include "libintvector.h"
 
diff --git a/include/Hacl_Hash_Blake2s_128.h b/include/Hacl_Hash_Blake2s_128.h
index 0e424152..2af827cd 100644
--- a/include/Hacl_Hash_Blake2s_128.h
+++ b/include/Hacl_Hash_Blake2s_128.h
@@ -35,7 +35,6 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
-#include "Lib_Memzero0.h"
 #include "libintvector.h"
 
 void
diff --git a/include/Lib_Memzero0.h b/include/Lib_Memzero0.h
deleted file mode 100644
index 9a7c7ac5..00000000
--- a/include/Lib_Memzero0.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/* MIT License
- *
- * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
- * Copyright (c) 2022-2023 HACL* Contributors
- *
- * Permission is hereby granted, free of charge, to any person obtaining a copy
- * of this software and associated documentation files (the "Software"), to deal
- * in the Software without restriction, including without limitation the rights
- * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
- * copies of the Software, and to permit persons to whom the Software is
- * furnished to do so, subject to the following conditions:
- *
- * The above copyright notice and this permission notice shall be included in all
- * copies or substantial portions of the Software.
- *
- * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
- * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
- * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
- * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
- * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
- * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
- * SOFTWARE.
- */
-
-
-#ifndef __Lib_Memzero0_H
-#define __Lib_Memzero0_H
-
-#if defined(__cplusplus)
-extern "C" {
-#endif
-
-#include <string.h>
-#include "krml/internal/types.h"
-#include "krml/lowstar_endianness.h"
-#include "krml/internal/target.h"
-
-extern void Lib_Memzero0_memzero(void *x0, uint64_t x1);
-
-#if defined(__cplusplus)
-}
-#endif
-
-#define __Lib_Memzero0_H_DEFINED
-#endif
diff --git a/include/TestLib.h b/include/TestLib.h
index 3928a462..62399c0c 100644
--- a/include/TestLib.h
+++ b/include/TestLib.h
@@ -55,7 +55,8 @@ extern void TestLib_checku32(uint32_t uu___, uint32_t uu___1);
 
 extern void TestLib_checku64(uint64_t uu___, uint64_t uu___1);
 
-extern void TestLib_compare_and_print(C_String_t uu___, uint8_t *b1, uint8_t *b2, uint32_t l);
+extern void
+TestLib_compare_and_print(Prims_string uu___, uint8_t *b1, uint8_t *b2, uint32_t l);
 
 extern uint8_t *TestLib_unsafe_malloc(uint32_t l);
 
diff --git a/include/libmemzero0.h b/include/libmemzero0.h
new file mode 100644
index 00000000..506dd50f
--- /dev/null
+++ b/include/libmemzero0.h
@@ -0,0 +1,5 @@
+#include <inttypes.h>
+
+void Lib_Memzero0_memzero0(void *dst, uint64_t len);
+
+#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t))
diff --git a/include/msvc/libmemzero0.h b/include/msvc/libmemzero0.h
new file mode 100644
index 00000000..506dd50f
--- /dev/null
+++ b/include/msvc/libmemzero0.h
@@ -0,0 +1,5 @@
+#include <inttypes.h>
+
+void Lib_Memzero0_memzero0(void *dst, uint64_t len);
+
+#define Lib_Memzero0_memzero(dst, len, t) Lib_Memzero0_memzero0(dst, len * sizeof(t))
diff --git a/src/EverCrypt_AEAD.c b/src/EverCrypt_AEAD.c
index a4b306b7..fe9ea01a 100644
--- a/src/EverCrypt_AEAD.c
+++ b/src/EverCrypt_AEAD.c
@@ -40,6 +40,10 @@ typedef struct EverCrypt_AEAD_state_s_s
 }
 EverCrypt_AEAD_state_s;
 
+/**
+Both encryption and decryption require a state that holds the key.
+The state may be reused as many times as desired.
+*/
 bool EverCrypt_AEAD_uu___is_Ek(Spec_Agile_AEAD_alg a, EverCrypt_AEAD_state_s projectee)
 {
   return true;
diff --git a/src/EverCrypt_DRBG.c b/src/EverCrypt_DRBG.c
index ac521460..6aea91ed 100644
--- a/src/EverCrypt_DRBG.c
+++ b/src/EverCrypt_DRBG.c
@@ -26,6 +26,7 @@
 #include "EverCrypt_DRBG.h"
 
 #include "internal/EverCrypt_HMAC.h"
+#include "libmemzero0.h"
 
 uint32_t EverCrypt_DRBG_reseed_interval = (uint32_t)1024U;
 
@@ -618,20 +619,18 @@ reseed_sha1(
   memcpy(seed_material + entropy_input_len,
     additional_input,
     additional_input_len * sizeof (uint8_t));
-  Hacl_HMAC_DRBG_state uu____0;
+  Hacl_HMAC_DRBG_state scrut;
   if (st_s.tag == SHA1_s)
   {
-    uu____0 = st_s.case_SHA1_s;
+    scrut = st_s.case_SHA1_s;
   }
   else
   {
-    uu____0 =
-      KRML_EABORT(Hacl_HMAC_DRBG_state,
-        "unreachable (pattern matches are exhaustive in F*)");
+    scrut = KRML_EABORT(Hacl_HMAC_DRBG_state, "unreachable (pattern matches are exhaustive in F*)");
   }
-  uint8_t *k = uu____0.k;
-  uint8_t *v = uu____0.v;
-  uint32_t *ctr = uu____0.reseed_counter;
+  uint8_t *k = scrut.k;
+  uint8_t *v = scrut.v;
+  uint32_t *ctr = scrut.reseed_counter;
   uint32_t input_len = (uint32_t)21U + entropy_input_len + additional_input_len;
   KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
   uint8_t input0[input_len];
@@ -699,20 +698,18 @@ reseed_sha2_256(
   memcpy(seed_material + entropy_input_len,
     additional_input,
     additional_input_len * sizeof (uint8_t));
-  Hacl_HMAC_DRBG_state uu____0;
+  Hacl_HMAC_DRBG_state scrut;
   if (st_s.tag == SHA2_256_s)
   {
-    uu____0 = st_s.case_SHA2_256_s;
+    scrut = st_s.case_SHA2_256_s;
   }
   else
   {
-    uu____0 =
-      KRML_EABORT(Hacl_HMAC_DRBG_state,
-        "unreachable (pattern matches are exhaustive in F*)");
+    scrut = KRML_EABORT(Hacl_HMAC_DRBG_state, "unreachable (pattern matches are exhaustive in F*)");
   }
-  uint8_t *k = uu____0.k;
-  uint8_t *v = uu____0.v;
-  uint32_t *ctr = uu____0.reseed_counter;
+  uint8_t *k = scrut.k;
+  uint8_t *v = scrut.v;
+  uint32_t *ctr = scrut.reseed_counter;
   uint32_t input_len = (uint32_t)33U + entropy_input_len + additional_input_len;
   KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
   uint8_t input0[input_len];
@@ -780,20 +777,18 @@ reseed_sha2_384(
   memcpy(seed_material + entropy_input_len,
     additional_input,
     additional_input_len * sizeof (uint8_t));
-  Hacl_HMAC_DRBG_state uu____0;
+  Hacl_HMAC_DRBG_state scrut;
   if (st_s.tag == SHA2_384_s)
   {
-    uu____0 = st_s.case_SHA2_384_s;
+    scrut = st_s.case_SHA2_384_s;
   }
   else
   {
-    uu____0 =
-      KRML_EABORT(Hacl_HMAC_DRBG_state,
-        "unreachable (pattern matches are exhaustive in F*)");
+    scrut = KRML_EABORT(Hacl_HMAC_DRBG_state, "unreachable (pattern matches are exhaustive in F*)");
   }
-  uint8_t *k = uu____0.k;
-  uint8_t *v = uu____0.v;
-  uint32_t *ctr = uu____0.reseed_counter;
+  uint8_t *k = scrut.k;
+  uint8_t *v = scrut.v;
+  uint32_t *ctr = scrut.reseed_counter;
   uint32_t input_len = (uint32_t)49U + entropy_input_len + additional_input_len;
   KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
   uint8_t input0[input_len];
@@ -861,20 +856,18 @@ reseed_sha2_512(
   memcpy(seed_material + entropy_input_len,
     additional_input,
     additional_input_len * sizeof (uint8_t));
-  Hacl_HMAC_DRBG_state uu____0;
+  Hacl_HMAC_DRBG_state scrut;
   if (st_s.tag == SHA2_512_s)
   {
-    uu____0 = st_s.case_SHA2_512_s;
+    scrut = st_s.case_SHA2_512_s;
   }
   else
   {
-    uu____0 =
-      KRML_EABORT(Hacl_HMAC_DRBG_state,
-        "unreachable (pattern matches are exhaustive in F*)");
+    scrut = KRML_EABORT(Hacl_HMAC_DRBG_state, "unreachable (pattern matches are exhaustive in F*)");
   }
-  uint8_t *k = uu____0.k;
-  uint8_t *v = uu____0.v;
-  uint32_t *ctr = uu____0.reseed_counter;
+  uint8_t *k = scrut.k;
+  uint8_t *v = scrut.v;
+  uint32_t *ctr = scrut.reseed_counter;
   uint32_t input_len = (uint32_t)65U + entropy_input_len + additional_input_len;
   KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
   uint8_t input0[input_len];
@@ -960,20 +953,20 @@ generate_sha1(
       memcpy(seed_material + entropy_input_len1,
         additional_input,
         additional_input_len * sizeof (uint8_t));
-      Hacl_HMAC_DRBG_state uu____0;
+      Hacl_HMAC_DRBG_state scrut;
       if (st_s.tag == SHA1_s)
       {
-        uu____0 = st_s.case_SHA1_s;
+        scrut = st_s.case_SHA1_s;
       }
       else
       {
-        uu____0 =
+        scrut =
           KRML_EABORT(Hacl_HMAC_DRBG_state,
             "unreachable (pattern matches are exhaustive in F*)");
       }
-      uint8_t *k = uu____0.k;
-      uint8_t *v = uu____0.v;
-      uint32_t *ctr = uu____0.reseed_counter;
+      uint8_t *k = scrut.k;
+      uint8_t *v = scrut.v;
+      uint32_t *ctr = scrut.reseed_counter;
       uint32_t input_len = (uint32_t)21U + entropy_input_len1 + additional_input_len;
       KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
       uint8_t input0[input_len];
@@ -1181,20 +1174,20 @@ generate_sha2_256(
       memcpy(seed_material + entropy_input_len1,
         additional_input,
         additional_input_len * sizeof (uint8_t));
-      Hacl_HMAC_DRBG_state uu____0;
+      Hacl_HMAC_DRBG_state scrut;
       if (st_s.tag == SHA2_256_s)
       {
-        uu____0 = st_s.case_SHA2_256_s;
+        scrut = st_s.case_SHA2_256_s;
       }
       else
       {
-        uu____0 =
+        scrut =
           KRML_EABORT(Hacl_HMAC_DRBG_state,
             "unreachable (pattern matches are exhaustive in F*)");
       }
-      uint8_t *k = uu____0.k;
-      uint8_t *v = uu____0.v;
-      uint32_t *ctr = uu____0.reseed_counter;
+      uint8_t *k = scrut.k;
+      uint8_t *v = scrut.v;
+      uint32_t *ctr = scrut.reseed_counter;
       uint32_t input_len = (uint32_t)33U + entropy_input_len1 + additional_input_len;
       KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
       uint8_t input0[input_len];
@@ -1402,20 +1395,20 @@ generate_sha2_384(
       memcpy(seed_material + entropy_input_len1,
         additional_input,
         additional_input_len * sizeof (uint8_t));
-      Hacl_HMAC_DRBG_state uu____0;
+      Hacl_HMAC_DRBG_state scrut;
       if (st_s.tag == SHA2_384_s)
       {
-        uu____0 = st_s.case_SHA2_384_s;
+        scrut = st_s.case_SHA2_384_s;
       }
       else
       {
-        uu____0 =
+        scrut =
           KRML_EABORT(Hacl_HMAC_DRBG_state,
             "unreachable (pattern matches are exhaustive in F*)");
       }
-      uint8_t *k = uu____0.k;
-      uint8_t *v = uu____0.v;
-      uint32_t *ctr = uu____0.reseed_counter;
+      uint8_t *k = scrut.k;
+      uint8_t *v = scrut.v;
+      uint32_t *ctr = scrut.reseed_counter;
       uint32_t input_len = (uint32_t)49U + entropy_input_len1 + additional_input_len;
       KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
       uint8_t input0[input_len];
@@ -1623,20 +1616,20 @@ generate_sha2_512(
       memcpy(seed_material + entropy_input_len1,
         additional_input,
         additional_input_len * sizeof (uint8_t));
-      Hacl_HMAC_DRBG_state uu____0;
+      Hacl_HMAC_DRBG_state scrut;
       if (st_s.tag == SHA2_512_s)
       {
-        uu____0 = st_s.case_SHA2_512_s;
+        scrut = st_s.case_SHA2_512_s;
       }
       else
       {
-        uu____0 =
+        scrut =
           KRML_EABORT(Hacl_HMAC_DRBG_state,
             "unreachable (pattern matches are exhaustive in F*)");
       }
-      uint8_t *k = uu____0.k;
-      uint8_t *v = uu____0.v;
-      uint32_t *ctr = uu____0.reseed_counter;
+      uint8_t *k = scrut.k;
+      uint8_t *v = scrut.v;
+      uint32_t *ctr = scrut.reseed_counter;
       uint32_t input_len = (uint32_t)65U + entropy_input_len1 + additional_input_len;
       KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
       uint8_t input0[input_len];
@@ -1813,8 +1806,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, (uint32_t)20U * sizeof (k[0U]));
-  Lib_Memzero0_memzero(v, (uint32_t)20U * sizeof (v[0U]));
+  Lib_Memzero0_memzero(k, (uint32_t)20U, uint8_t);
+  Lib_Memzero0_memzero(v, (uint32_t)20U, uint8_t);
   ctr[0U] = (uint32_t)0U;
   KRML_HOST_FREE(k);
   KRML_HOST_FREE(v);
@@ -1837,8 +1830,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, (uint32_t)32U * sizeof (k[0U]));
-  Lib_Memzero0_memzero(v, (uint32_t)32U * sizeof (v[0U]));
+  Lib_Memzero0_memzero(k, (uint32_t)32U, uint8_t);
+  Lib_Memzero0_memzero(v, (uint32_t)32U, uint8_t);
   ctr[0U] = (uint32_t)0U;
   KRML_HOST_FREE(k);
   KRML_HOST_FREE(v);
@@ -1861,8 +1854,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, (uint32_t)48U * sizeof (k[0U]));
-  Lib_Memzero0_memzero(v, (uint32_t)48U * sizeof (v[0U]));
+  Lib_Memzero0_memzero(k, (uint32_t)48U, uint8_t);
+  Lib_Memzero0_memzero(v, (uint32_t)48U, uint8_t);
   ctr[0U] = (uint32_t)0U;
   KRML_HOST_FREE(k);
   KRML_HOST_FREE(v);
@@ -1885,8 +1878,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, (uint32_t)64U * sizeof (k[0U]));
-  Lib_Memzero0_memzero(v, (uint32_t)64U * sizeof (v[0U]));
+  Lib_Memzero0_memzero(k, (uint32_t)64U, uint8_t);
+  Lib_Memzero0_memzero(v, (uint32_t)64U, uint8_t);
   ctr[0U] = (uint32_t)0U;
   KRML_HOST_FREE(k);
   KRML_HOST_FREE(v);
diff --git a/src/Hacl_Frodo1344.c b/src/Hacl_Frodo1344.c
index 81bddfd9..e37510d4 100644
--- a/src/Hacl_Frodo1344.c
+++ b/src/Hacl_Frodo1344.c
@@ -27,6 +27,7 @@
 
 #include "internal/Hacl_Spec.h"
 #include "internal/Hacl_Frodo_KEM.h"
+#include "libmemzero0.h"
 
 uint32_t Hacl_Frodo1344_crypto_bytes = (uint32_t)32U;
 
@@ -54,7 +55,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = (uint8_t)0x5fU;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)32U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl((uint32_t)33U, shake_input_seed_se, (uint32_t)43008U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)33U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)33U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344((uint32_t)1344U, (uint32_t)8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344((uint32_t)1344U,
     (uint32_t)8U,
@@ -80,14 +81,14 @@ uint32_t Hacl_Frodo1344_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
     b_matrix,
     b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes((uint32_t)1344U, (uint32_t)8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, (uint32_t)10752U * sizeof (s_matrix[0U]));
-  Lib_Memzero0_memzero(e_matrix, (uint32_t)10752U * sizeof (e_matrix[0U]));
+  Lib_Memzero0_memzero(s_matrix, (uint32_t)10752U, uint16_t);
+  Lib_Memzero0_memzero(e_matrix, (uint32_t)10752U, uint16_t);
   uint32_t slen1 = (uint32_t)43056U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, (uint32_t)32U * sizeof (uint8_t));
   memcpy(sk_p + (uint32_t)32U, pk, (uint32_t)21520U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl((uint32_t)21520U, pk, (uint32_t)32U, sk + slen1);
-  Lib_Memzero0_memzero(coins, (uint32_t)80U * sizeof (coins[0U]));
+  Lib_Memzero0_memzero(coins, (uint32_t)80U, uint8_t);
   return (uint32_t)0U;
 }
 
@@ -112,7 +113,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   shake_input_seed_se[0U] = (uint8_t)0x96U;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)32U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl((uint32_t)33U, shake_input_seed_se, (uint32_t)43136U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)33U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)33U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344((uint32_t)8U, (uint32_t)1344U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344((uint32_t)8U,
     (uint32_t)1344U,
@@ -156,12 +157,12 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
     coins,
     mu_encode);
   Hacl_Impl_Matrix_matrix_add((uint32_t)8U, (uint32_t)8U, v_matrix, mu_encode);
-  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U * sizeof (mu_encode[0U]));
+  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U, uint16_t);
   Hacl_Impl_Frodo_Pack_frodo_pack((uint32_t)8U, (uint32_t)8U, (uint32_t)16U, v_matrix, c2);
-  Lib_Memzero0_memzero(v_matrix, (uint32_t)64U * sizeof (v_matrix[0U]));
-  Lib_Memzero0_memzero(sp_matrix, (uint32_t)10752U * sizeof (sp_matrix[0U]));
-  Lib_Memzero0_memzero(ep_matrix, (uint32_t)10752U * sizeof (ep_matrix[0U]));
-  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U * sizeof (epp_matrix[0U]));
+  Lib_Memzero0_memzero(v_matrix, (uint32_t)64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, (uint32_t)10752U, uint16_t);
+  Lib_Memzero0_memzero(ep_matrix, (uint32_t)10752U, uint16_t);
+  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U, uint16_t);
   uint32_t ss_init_len = (uint32_t)21664U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t shake_input_ss[ss_init_len];
@@ -169,9 +170,9 @@ uint32_t Hacl_Frodo1344_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, (uint32_t)21632U * sizeof (uint8_t));
   memcpy(shake_input_ss + (uint32_t)21632U, k, (uint32_t)32U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl(ss_init_len, shake_input_ss, (uint32_t)32U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len * sizeof (shake_input_ss[0U]));
-  Lib_Memzero0_memzero(seed_se_k, (uint32_t)64U * sizeof (seed_se_k[0U]));
-  Lib_Memzero0_memzero(coins, (uint32_t)32U * sizeof (coins[0U]));
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
+  Lib_Memzero0_memzero(seed_se_k, (uint32_t)64U, uint8_t);
+  Lib_Memzero0_memzero(coins, (uint32_t)32U, uint8_t);
   return (uint32_t)0U;
 }
 
@@ -200,8 +201,8 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
     (uint32_t)8U,
     m_matrix,
     mu_decode);
-  Lib_Memzero0_memzero(s_matrix, (uint32_t)10752U * sizeof (s_matrix[0U]));
-  Lib_Memzero0_memzero(m_matrix, (uint32_t)64U * sizeof (m_matrix[0U]));
+  Lib_Memzero0_memzero(s_matrix, (uint32_t)10752U, uint16_t);
+  Lib_Memzero0_memzero(m_matrix, (uint32_t)64U, uint16_t);
   uint8_t seed_se_k[64U] = { 0U };
   uint32_t pkh_mu_decode_len = (uint32_t)64U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -224,7 +225,7 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   shake_input_seed_se[0U] = (uint8_t)0x96U;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)32U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl((uint32_t)33U, shake_input_seed_se, (uint32_t)43136U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)33U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)33U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344((uint32_t)8U, (uint32_t)1344U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix1344((uint32_t)8U,
     (uint32_t)1344U,
@@ -266,12 +267,12 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
     mu_decode,
     mu_encode);
   Hacl_Impl_Matrix_matrix_add((uint32_t)8U, (uint32_t)8U, cp_matrix, mu_encode);
-  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U * sizeof (mu_encode[0U]));
+  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U, uint16_t);
   Hacl_Impl_Matrix_mod_pow2((uint32_t)8U, (uint32_t)1344U, (uint32_t)16U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2((uint32_t)8U, (uint32_t)8U, (uint32_t)16U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, (uint32_t)10752U * sizeof (sp_matrix[0U]));
-  Lib_Memzero0_memzero(ep_matrix, (uint32_t)10752U * sizeof (ep_matrix[0U]));
-  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U * sizeof (epp_matrix[0U]));
+  Lib_Memzero0_memzero(sp_matrix, (uint32_t)10752U, uint16_t);
+  Lib_Memzero0_memzero(ep_matrix, (uint32_t)10752U, uint16_t);
+  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U, uint16_t);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq((uint32_t)8U, (uint32_t)1344U, bp_matrix, bpp_matrix);
   uint16_t b2 = Hacl_Impl_Matrix_matrix_eq((uint32_t)8U, (uint32_t)8U, c_matrix, cp_matrix);
   uint16_t mask = b1 & b2;
@@ -291,10 +292,10 @@ uint32_t Hacl_Frodo1344_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, (uint32_t)21632U * sizeof (uint8_t));
   memcpy(ss_init + (uint32_t)21632U, kp_s, (uint32_t)32U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl(ss_init_len, ss_init, (uint32_t)32U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len * sizeof (ss_init[0U]));
-  Lib_Memzero0_memzero(kp_s, (uint32_t)32U * sizeof (kp_s[0U]));
-  Lib_Memzero0_memzero(seed_se_k, (uint32_t)64U * sizeof (seed_se_k[0U]));
-  Lib_Memzero0_memzero(mu_decode, (uint32_t)32U * sizeof (mu_decode[0U]));
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
+  Lib_Memzero0_memzero(kp_s, (uint32_t)32U, uint8_t);
+  Lib_Memzero0_memzero(seed_se_k, (uint32_t)64U, uint8_t);
+  Lib_Memzero0_memzero(mu_decode, (uint32_t)32U, uint8_t);
   return (uint32_t)0U;
 }
 
diff --git a/src/Hacl_Frodo64.c b/src/Hacl_Frodo64.c
index 6c652c9b..be74e766 100644
--- a/src/Hacl_Frodo64.c
+++ b/src/Hacl_Frodo64.c
@@ -27,6 +27,7 @@
 
 #include "internal/Hacl_Spec.h"
 #include "internal/Hacl_Frodo_KEM.h"
+#include "libmemzero0.h"
 
 /*
  this variant is used only for testing purposes!
@@ -59,7 +60,7 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = (uint8_t)0x5fU;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl((uint32_t)17U, shake_input_seed_se, (uint32_t)2048U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64((uint32_t)64U, (uint32_t)8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64((uint32_t)64U,
     (uint32_t)8U,
@@ -80,14 +81,14 @@ uint32_t Hacl_Frodo64_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   Hacl_Impl_Matrix_matrix_add((uint32_t)64U, (uint32_t)8U, b_matrix, e_matrix);
   Hacl_Impl_Frodo_Pack_frodo_pack((uint32_t)64U, (uint32_t)8U, (uint32_t)15U, b_matrix, b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes((uint32_t)64U, (uint32_t)8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, (uint32_t)512U * sizeof (s_matrix[0U]));
-  Lib_Memzero0_memzero(e_matrix, (uint32_t)512U * sizeof (e_matrix[0U]));
+  Lib_Memzero0_memzero(s_matrix, (uint32_t)512U, uint16_t);
+  Lib_Memzero0_memzero(e_matrix, (uint32_t)512U, uint16_t);
   uint32_t slen1 = (uint32_t)2016U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, (uint32_t)16U * sizeof (uint8_t));
   memcpy(sk_p + (uint32_t)16U, pk, (uint32_t)976U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl((uint32_t)976U, pk, (uint32_t)16U, sk + slen1);
-  Lib_Memzero0_memzero(coins, (uint32_t)48U * sizeof (coins[0U]));
+  Lib_Memzero0_memzero(coins, (uint32_t)48U, uint8_t);
   return (uint32_t)0U;
 }
 
@@ -112,7 +113,7 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   shake_input_seed_se[0U] = (uint8_t)0x96U;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl((uint32_t)17U, shake_input_seed_se, (uint32_t)2176U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64((uint32_t)8U, (uint32_t)64U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64((uint32_t)8U,
     (uint32_t)64U,
@@ -155,12 +156,12 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
     coins,
     mu_encode);
   Hacl_Impl_Matrix_matrix_add((uint32_t)8U, (uint32_t)8U, v_matrix, mu_encode);
-  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U * sizeof (mu_encode[0U]));
+  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U, uint16_t);
   Hacl_Impl_Frodo_Pack_frodo_pack((uint32_t)8U, (uint32_t)8U, (uint32_t)15U, v_matrix, c2);
-  Lib_Memzero0_memzero(v_matrix, (uint32_t)64U * sizeof (v_matrix[0U]));
-  Lib_Memzero0_memzero(sp_matrix, (uint32_t)512U * sizeof (sp_matrix[0U]));
-  Lib_Memzero0_memzero(ep_matrix, (uint32_t)512U * sizeof (ep_matrix[0U]));
-  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U * sizeof (epp_matrix[0U]));
+  Lib_Memzero0_memzero(v_matrix, (uint32_t)64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, (uint32_t)512U, uint16_t);
+  Lib_Memzero0_memzero(ep_matrix, (uint32_t)512U, uint16_t);
+  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U, uint16_t);
   uint32_t ss_init_len = (uint32_t)1096U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t shake_input_ss[ss_init_len];
@@ -168,9 +169,9 @@ uint32_t Hacl_Frodo64_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, (uint32_t)1080U * sizeof (uint8_t));
   memcpy(shake_input_ss + (uint32_t)1080U, k, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl(ss_init_len, shake_input_ss, (uint32_t)16U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len * sizeof (shake_input_ss[0U]));
-  Lib_Memzero0_memzero(seed_se_k, (uint32_t)32U * sizeof (seed_se_k[0U]));
-  Lib_Memzero0_memzero(coins, (uint32_t)16U * sizeof (coins[0U]));
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
+  Lib_Memzero0_memzero(seed_se_k, (uint32_t)32U, uint8_t);
+  Lib_Memzero0_memzero(coins, (uint32_t)16U, uint8_t);
   return (uint32_t)0U;
 }
 
@@ -199,8 +200,8 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
     (uint32_t)8U,
     m_matrix,
     mu_decode);
-  Lib_Memzero0_memzero(s_matrix, (uint32_t)512U * sizeof (s_matrix[0U]));
-  Lib_Memzero0_memzero(m_matrix, (uint32_t)64U * sizeof (m_matrix[0U]));
+  Lib_Memzero0_memzero(s_matrix, (uint32_t)512U, uint16_t);
+  Lib_Memzero0_memzero(m_matrix, (uint32_t)64U, uint16_t);
   uint8_t seed_se_k[32U] = { 0U };
   uint32_t pkh_mu_decode_len = (uint32_t)32U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -223,7 +224,7 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   shake_input_seed_se[0U] = (uint8_t)0x96U;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl((uint32_t)17U, shake_input_seed_se, (uint32_t)2176U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64((uint32_t)8U, (uint32_t)64U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix64((uint32_t)8U,
     (uint32_t)64U,
@@ -264,12 +265,12 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
     mu_decode,
     mu_encode);
   Hacl_Impl_Matrix_matrix_add((uint32_t)8U, (uint32_t)8U, cp_matrix, mu_encode);
-  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U * sizeof (mu_encode[0U]));
+  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U, uint16_t);
   Hacl_Impl_Matrix_mod_pow2((uint32_t)8U, (uint32_t)64U, (uint32_t)15U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2((uint32_t)8U, (uint32_t)8U, (uint32_t)15U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, (uint32_t)512U * sizeof (sp_matrix[0U]));
-  Lib_Memzero0_memzero(ep_matrix, (uint32_t)512U * sizeof (ep_matrix[0U]));
-  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U * sizeof (epp_matrix[0U]));
+  Lib_Memzero0_memzero(sp_matrix, (uint32_t)512U, uint16_t);
+  Lib_Memzero0_memzero(ep_matrix, (uint32_t)512U, uint16_t);
+  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U, uint16_t);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq((uint32_t)8U, (uint32_t)64U, bp_matrix, bpp_matrix);
   uint16_t b2 = Hacl_Impl_Matrix_matrix_eq((uint32_t)8U, (uint32_t)8U, c_matrix, cp_matrix);
   uint16_t mask = b1 & b2;
@@ -290,10 +291,10 @@ uint32_t Hacl_Frodo64_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, (uint32_t)1080U * sizeof (uint8_t));
   memcpy(ss_init + (uint32_t)1080U, kp_s, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl(ss_init_len, ss_init, (uint32_t)16U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len * sizeof (ss_init[0U]));
-  Lib_Memzero0_memzero(kp_s, (uint32_t)16U * sizeof (kp_s[0U]));
-  Lib_Memzero0_memzero(seed_se_k, (uint32_t)32U * sizeof (seed_se_k[0U]));
-  Lib_Memzero0_memzero(mu_decode, (uint32_t)16U * sizeof (mu_decode[0U]));
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
+  Lib_Memzero0_memzero(kp_s, (uint32_t)16U, uint8_t);
+  Lib_Memzero0_memzero(seed_se_k, (uint32_t)32U, uint8_t);
+  Lib_Memzero0_memzero(mu_decode, (uint32_t)16U, uint8_t);
   return (uint32_t)0U;
 }
 
diff --git a/src/Hacl_Frodo640.c b/src/Hacl_Frodo640.c
index 904865c2..5b81d06d 100644
--- a/src/Hacl_Frodo640.c
+++ b/src/Hacl_Frodo640.c
@@ -27,6 +27,7 @@
 
 #include "internal/Hacl_Spec.h"
 #include "internal/Hacl_Frodo_KEM.h"
+#include "libmemzero0.h"
 
 uint32_t Hacl_Frodo640_crypto_bytes = (uint32_t)16U;
 
@@ -54,7 +55,7 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = (uint8_t)0x5fU;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl((uint32_t)17U, shake_input_seed_se, (uint32_t)20480U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640((uint32_t)640U, (uint32_t)8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640((uint32_t)640U,
     (uint32_t)8U,
@@ -80,14 +81,14 @@ uint32_t Hacl_Frodo640_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
     b_matrix,
     b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes((uint32_t)640U, (uint32_t)8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, (uint32_t)5120U * sizeof (s_matrix[0U]));
-  Lib_Memzero0_memzero(e_matrix, (uint32_t)5120U * sizeof (e_matrix[0U]));
+  Lib_Memzero0_memzero(s_matrix, (uint32_t)5120U, uint16_t);
+  Lib_Memzero0_memzero(e_matrix, (uint32_t)5120U, uint16_t);
   uint32_t slen1 = (uint32_t)19872U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, (uint32_t)16U * sizeof (uint8_t));
   memcpy(sk_p + (uint32_t)16U, pk, (uint32_t)9616U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl((uint32_t)9616U, pk, (uint32_t)16U, sk + slen1);
-  Lib_Memzero0_memzero(coins, (uint32_t)48U * sizeof (coins[0U]));
+  Lib_Memzero0_memzero(coins, (uint32_t)48U, uint8_t);
   return (uint32_t)0U;
 }
 
@@ -112,7 +113,7 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   shake_input_seed_se[0U] = (uint8_t)0x96U;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl((uint32_t)17U, shake_input_seed_se, (uint32_t)20608U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640((uint32_t)8U, (uint32_t)640U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640((uint32_t)8U,
     (uint32_t)640U,
@@ -156,12 +157,12 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
     coins,
     mu_encode);
   Hacl_Impl_Matrix_matrix_add((uint32_t)8U, (uint32_t)8U, v_matrix, mu_encode);
-  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U * sizeof (mu_encode[0U]));
+  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U, uint16_t);
   Hacl_Impl_Frodo_Pack_frodo_pack((uint32_t)8U, (uint32_t)8U, (uint32_t)15U, v_matrix, c2);
-  Lib_Memzero0_memzero(v_matrix, (uint32_t)64U * sizeof (v_matrix[0U]));
-  Lib_Memzero0_memzero(sp_matrix, (uint32_t)5120U * sizeof (sp_matrix[0U]));
-  Lib_Memzero0_memzero(ep_matrix, (uint32_t)5120U * sizeof (ep_matrix[0U]));
-  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U * sizeof (epp_matrix[0U]));
+  Lib_Memzero0_memzero(v_matrix, (uint32_t)64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, (uint32_t)5120U, uint16_t);
+  Lib_Memzero0_memzero(ep_matrix, (uint32_t)5120U, uint16_t);
+  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U, uint16_t);
   uint32_t ss_init_len = (uint32_t)9736U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t shake_input_ss[ss_init_len];
@@ -169,9 +170,9 @@ uint32_t Hacl_Frodo640_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, (uint32_t)9720U * sizeof (uint8_t));
   memcpy(shake_input_ss + (uint32_t)9720U, k, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl(ss_init_len, shake_input_ss, (uint32_t)16U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len * sizeof (shake_input_ss[0U]));
-  Lib_Memzero0_memzero(seed_se_k, (uint32_t)32U * sizeof (seed_se_k[0U]));
-  Lib_Memzero0_memzero(coins, (uint32_t)16U * sizeof (coins[0U]));
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
+  Lib_Memzero0_memzero(seed_se_k, (uint32_t)32U, uint8_t);
+  Lib_Memzero0_memzero(coins, (uint32_t)16U, uint8_t);
   return (uint32_t)0U;
 }
 
@@ -200,8 +201,8 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
     (uint32_t)8U,
     m_matrix,
     mu_decode);
-  Lib_Memzero0_memzero(s_matrix, (uint32_t)5120U * sizeof (s_matrix[0U]));
-  Lib_Memzero0_memzero(m_matrix, (uint32_t)64U * sizeof (m_matrix[0U]));
+  Lib_Memzero0_memzero(s_matrix, (uint32_t)5120U, uint16_t);
+  Lib_Memzero0_memzero(m_matrix, (uint32_t)64U, uint16_t);
   uint8_t seed_se_k[32U] = { 0U };
   uint32_t pkh_mu_decode_len = (uint32_t)32U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -224,7 +225,7 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   shake_input_seed_se[0U] = (uint8_t)0x96U;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl((uint32_t)17U, shake_input_seed_se, (uint32_t)20608U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)17U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640((uint32_t)8U, (uint32_t)640U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix640((uint32_t)8U,
     (uint32_t)640U,
@@ -266,12 +267,12 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
     mu_decode,
     mu_encode);
   Hacl_Impl_Matrix_matrix_add((uint32_t)8U, (uint32_t)8U, cp_matrix, mu_encode);
-  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U * sizeof (mu_encode[0U]));
+  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U, uint16_t);
   Hacl_Impl_Matrix_mod_pow2((uint32_t)8U, (uint32_t)640U, (uint32_t)15U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2((uint32_t)8U, (uint32_t)8U, (uint32_t)15U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, (uint32_t)5120U * sizeof (sp_matrix[0U]));
-  Lib_Memzero0_memzero(ep_matrix, (uint32_t)5120U * sizeof (ep_matrix[0U]));
-  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U * sizeof (epp_matrix[0U]));
+  Lib_Memzero0_memzero(sp_matrix, (uint32_t)5120U, uint16_t);
+  Lib_Memzero0_memzero(ep_matrix, (uint32_t)5120U, uint16_t);
+  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U, uint16_t);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq((uint32_t)8U, (uint32_t)640U, bp_matrix, bpp_matrix);
   uint16_t b2 = Hacl_Impl_Matrix_matrix_eq((uint32_t)8U, (uint32_t)8U, c_matrix, cp_matrix);
   uint16_t mask = b1 & b2;
@@ -292,10 +293,10 @@ uint32_t Hacl_Frodo640_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, (uint32_t)9720U * sizeof (uint8_t));
   memcpy(ss_init + (uint32_t)9720U, kp_s, (uint32_t)16U * sizeof (uint8_t));
   Hacl_SHA3_shake128_hacl(ss_init_len, ss_init, (uint32_t)16U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len * sizeof (ss_init[0U]));
-  Lib_Memzero0_memzero(kp_s, (uint32_t)16U * sizeof (kp_s[0U]));
-  Lib_Memzero0_memzero(seed_se_k, (uint32_t)32U * sizeof (seed_se_k[0U]));
-  Lib_Memzero0_memzero(mu_decode, (uint32_t)16U * sizeof (mu_decode[0U]));
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
+  Lib_Memzero0_memzero(kp_s, (uint32_t)16U, uint8_t);
+  Lib_Memzero0_memzero(seed_se_k, (uint32_t)32U, uint8_t);
+  Lib_Memzero0_memzero(mu_decode, (uint32_t)16U, uint8_t);
   return (uint32_t)0U;
 }
 
diff --git a/src/Hacl_Frodo976.c b/src/Hacl_Frodo976.c
index 2f796b32..b9d2c9de 100644
--- a/src/Hacl_Frodo976.c
+++ b/src/Hacl_Frodo976.c
@@ -27,6 +27,7 @@
 
 #include "internal/Hacl_Spec.h"
 #include "internal/Hacl_Frodo_KEM.h"
+#include "libmemzero0.h"
 
 uint32_t Hacl_Frodo976_crypto_bytes = (uint32_t)24U;
 
@@ -54,7 +55,7 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
   shake_input_seed_se[0U] = (uint8_t)0x5fU;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)24U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl((uint32_t)25U, shake_input_seed_se, (uint32_t)31232U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)25U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)25U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976((uint32_t)976U, (uint32_t)8U, r, s_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976((uint32_t)976U,
     (uint32_t)8U,
@@ -80,14 +81,14 @@ uint32_t Hacl_Frodo976_crypto_kem_keypair(uint8_t *pk, uint8_t *sk)
     b_matrix,
     b_bytes);
   Hacl_Impl_Matrix_matrix_to_lbytes((uint32_t)976U, (uint32_t)8U, s_matrix, s_bytes);
-  Lib_Memzero0_memzero(s_matrix, (uint32_t)7808U * sizeof (s_matrix[0U]));
-  Lib_Memzero0_memzero(e_matrix, (uint32_t)7808U * sizeof (e_matrix[0U]));
+  Lib_Memzero0_memzero(s_matrix, (uint32_t)7808U, uint16_t);
+  Lib_Memzero0_memzero(e_matrix, (uint32_t)7808U, uint16_t);
   uint32_t slen1 = (uint32_t)31272U;
   uint8_t *sk_p = sk;
   memcpy(sk_p, s, (uint32_t)24U * sizeof (uint8_t));
   memcpy(sk_p + (uint32_t)24U, pk, (uint32_t)15632U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl((uint32_t)15632U, pk, (uint32_t)24U, sk + slen1);
-  Lib_Memzero0_memzero(coins, (uint32_t)64U * sizeof (coins[0U]));
+  Lib_Memzero0_memzero(coins, (uint32_t)64U, uint8_t);
   return (uint32_t)0U;
 }
 
@@ -112,7 +113,7 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   shake_input_seed_se[0U] = (uint8_t)0x96U;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)24U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl((uint32_t)25U, shake_input_seed_se, (uint32_t)31360U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)25U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)25U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976((uint32_t)8U, (uint32_t)976U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976((uint32_t)8U,
     (uint32_t)976U,
@@ -156,12 +157,12 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
     coins,
     mu_encode);
   Hacl_Impl_Matrix_matrix_add((uint32_t)8U, (uint32_t)8U, v_matrix, mu_encode);
-  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U * sizeof (mu_encode[0U]));
+  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U, uint16_t);
   Hacl_Impl_Frodo_Pack_frodo_pack((uint32_t)8U, (uint32_t)8U, (uint32_t)16U, v_matrix, c2);
-  Lib_Memzero0_memzero(v_matrix, (uint32_t)64U * sizeof (v_matrix[0U]));
-  Lib_Memzero0_memzero(sp_matrix, (uint32_t)7808U * sizeof (sp_matrix[0U]));
-  Lib_Memzero0_memzero(ep_matrix, (uint32_t)7808U * sizeof (ep_matrix[0U]));
-  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U * sizeof (epp_matrix[0U]));
+  Lib_Memzero0_memzero(v_matrix, (uint32_t)64U, uint16_t);
+  Lib_Memzero0_memzero(sp_matrix, (uint32_t)7808U, uint16_t);
+  Lib_Memzero0_memzero(ep_matrix, (uint32_t)7808U, uint16_t);
+  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U, uint16_t);
   uint32_t ss_init_len = (uint32_t)15768U;
   KRML_CHECK_SIZE(sizeof (uint8_t), ss_init_len);
   uint8_t shake_input_ss[ss_init_len];
@@ -169,9 +170,9 @@ uint32_t Hacl_Frodo976_crypto_kem_enc(uint8_t *ct, uint8_t *ss, uint8_t *pk)
   memcpy(shake_input_ss, ct, (uint32_t)15744U * sizeof (uint8_t));
   memcpy(shake_input_ss + (uint32_t)15744U, k, (uint32_t)24U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl(ss_init_len, shake_input_ss, (uint32_t)24U, ss);
-  Lib_Memzero0_memzero(shake_input_ss, ss_init_len * sizeof (shake_input_ss[0U]));
-  Lib_Memzero0_memzero(seed_se_k, (uint32_t)48U * sizeof (seed_se_k[0U]));
-  Lib_Memzero0_memzero(coins, (uint32_t)24U * sizeof (coins[0U]));
+  Lib_Memzero0_memzero(shake_input_ss, ss_init_len, uint8_t);
+  Lib_Memzero0_memzero(seed_se_k, (uint32_t)48U, uint8_t);
+  Lib_Memzero0_memzero(coins, (uint32_t)24U, uint8_t);
   return (uint32_t)0U;
 }
 
@@ -200,8 +201,8 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
     (uint32_t)8U,
     m_matrix,
     mu_decode);
-  Lib_Memzero0_memzero(s_matrix, (uint32_t)7808U * sizeof (s_matrix[0U]));
-  Lib_Memzero0_memzero(m_matrix, (uint32_t)64U * sizeof (m_matrix[0U]));
+  Lib_Memzero0_memzero(s_matrix, (uint32_t)7808U, uint16_t);
+  Lib_Memzero0_memzero(m_matrix, (uint32_t)64U, uint16_t);
   uint8_t seed_se_k[48U] = { 0U };
   uint32_t pkh_mu_decode_len = (uint32_t)48U;
   KRML_CHECK_SIZE(sizeof (uint8_t), pkh_mu_decode_len);
@@ -224,7 +225,7 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   shake_input_seed_se[0U] = (uint8_t)0x96U;
   memcpy(shake_input_seed_se + (uint32_t)1U, seed_se, (uint32_t)24U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl((uint32_t)25U, shake_input_seed_se, (uint32_t)31360U, r);
-  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)25U * sizeof (shake_input_seed_se[0U]));
+  Lib_Memzero0_memzero(shake_input_seed_se, (uint32_t)25U, uint8_t);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976((uint32_t)8U, (uint32_t)976U, r, sp_matrix);
   Hacl_Impl_Frodo_Sample_frodo_sample_matrix976((uint32_t)8U,
     (uint32_t)976U,
@@ -266,12 +267,12 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
     mu_decode,
     mu_encode);
   Hacl_Impl_Matrix_matrix_add((uint32_t)8U, (uint32_t)8U, cp_matrix, mu_encode);
-  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U * sizeof (mu_encode[0U]));
+  Lib_Memzero0_memzero(mu_encode, (uint32_t)64U, uint16_t);
   Hacl_Impl_Matrix_mod_pow2((uint32_t)8U, (uint32_t)976U, (uint32_t)16U, bpp_matrix);
   Hacl_Impl_Matrix_mod_pow2((uint32_t)8U, (uint32_t)8U, (uint32_t)16U, cp_matrix);
-  Lib_Memzero0_memzero(sp_matrix, (uint32_t)7808U * sizeof (sp_matrix[0U]));
-  Lib_Memzero0_memzero(ep_matrix, (uint32_t)7808U * sizeof (ep_matrix[0U]));
-  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U * sizeof (epp_matrix[0U]));
+  Lib_Memzero0_memzero(sp_matrix, (uint32_t)7808U, uint16_t);
+  Lib_Memzero0_memzero(ep_matrix, (uint32_t)7808U, uint16_t);
+  Lib_Memzero0_memzero(epp_matrix, (uint32_t)64U, uint16_t);
   uint16_t b1 = Hacl_Impl_Matrix_matrix_eq((uint32_t)8U, (uint32_t)976U, bp_matrix, bpp_matrix);
   uint16_t b2 = Hacl_Impl_Matrix_matrix_eq((uint32_t)8U, (uint32_t)8U, c_matrix, cp_matrix);
   uint16_t mask = b1 & b2;
@@ -291,10 +292,10 @@ uint32_t Hacl_Frodo976_crypto_kem_dec(uint8_t *ss, uint8_t *ct, uint8_t *sk)
   memcpy(ss_init, ct, (uint32_t)15744U * sizeof (uint8_t));
   memcpy(ss_init + (uint32_t)15744U, kp_s, (uint32_t)24U * sizeof (uint8_t));
   Hacl_SHA3_shake256_hacl(ss_init_len, ss_init, (uint32_t)24U, ss);
-  Lib_Memzero0_memzero(ss_init, ss_init_len * sizeof (ss_init[0U]));
-  Lib_Memzero0_memzero(kp_s, (uint32_t)24U * sizeof (kp_s[0U]));
-  Lib_Memzero0_memzero(seed_se_k, (uint32_t)48U * sizeof (seed_se_k[0U]));
-  Lib_Memzero0_memzero(mu_decode, (uint32_t)24U * sizeof (mu_decode[0U]));
+  Lib_Memzero0_memzero(ss_init, ss_init_len, uint8_t);
+  Lib_Memzero0_memzero(kp_s, (uint32_t)24U, uint8_t);
+  Lib_Memzero0_memzero(seed_se_k, (uint32_t)48U, uint8_t);
+  Lib_Memzero0_memzero(mu_decode, (uint32_t)24U, uint8_t);
   return (uint32_t)0U;
 }
 
diff --git a/src/Hacl_HMAC_DRBG.c b/src/Hacl_HMAC_DRBG.c
index f0e01bd8..181a8ef4 100644
--- a/src/Hacl_HMAC_DRBG.c
+++ b/src/Hacl_HMAC_DRBG.c
@@ -455,10 +455,9 @@ Hacl_HMAC_DRBG_reseed(
         memcpy(seed_material + entropy_input_len,
           additional_input_input,
           additional_input_input_len * sizeof (uint8_t));
-        Hacl_HMAC_DRBG_state uu____0 = st;
-        uint8_t *k = uu____0.k;
-        uint8_t *v = uu____0.v;
-        uint32_t *ctr = uu____0.reseed_counter;
+        uint8_t *k = st.k;
+        uint8_t *v = st.v;
+        uint32_t *ctr = st.reseed_counter;
         uint32_t input_len = (uint32_t)21U + entropy_input_len + additional_input_input_len;
         KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
         uint8_t input0[input_len];
@@ -508,10 +507,9 @@ Hacl_HMAC_DRBG_reseed(
         memcpy(seed_material + entropy_input_len,
           additional_input_input,
           additional_input_input_len * sizeof (uint8_t));
-        Hacl_HMAC_DRBG_state uu____1 = st;
-        uint8_t *k = uu____1.k;
-        uint8_t *v = uu____1.v;
-        uint32_t *ctr = uu____1.reseed_counter;
+        uint8_t *k = st.k;
+        uint8_t *v = st.v;
+        uint32_t *ctr = st.reseed_counter;
         uint32_t input_len = (uint32_t)33U + entropy_input_len + additional_input_input_len;
         KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
         uint8_t input0[input_len];
@@ -561,10 +559,9 @@ Hacl_HMAC_DRBG_reseed(
         memcpy(seed_material + entropy_input_len,
           additional_input_input,
           additional_input_input_len * sizeof (uint8_t));
-        Hacl_HMAC_DRBG_state uu____2 = st;
-        uint8_t *k = uu____2.k;
-        uint8_t *v = uu____2.v;
-        uint32_t *ctr = uu____2.reseed_counter;
+        uint8_t *k = st.k;
+        uint8_t *v = st.v;
+        uint32_t *ctr = st.reseed_counter;
         uint32_t input_len = (uint32_t)49U + entropy_input_len + additional_input_input_len;
         KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
         uint8_t input0[input_len];
@@ -614,10 +611,9 @@ Hacl_HMAC_DRBG_reseed(
         memcpy(seed_material + entropy_input_len,
           additional_input_input,
           additional_input_input_len * sizeof (uint8_t));
-        Hacl_HMAC_DRBG_state uu____3 = st;
-        uint8_t *k = uu____3.k;
-        uint8_t *v = uu____3.v;
-        uint32_t *ctr = uu____3.reseed_counter;
+        uint8_t *k = st.k;
+        uint8_t *v = st.v;
+        uint32_t *ctr = st.reseed_counter;
         uint32_t input_len = (uint32_t)65U + entropy_input_len + additional_input_input_len;
         KRML_CHECK_SIZE(sizeof (uint8_t), input_len);
         uint8_t input0[input_len];
diff --git a/src/Hacl_Hash_Blake2.c b/src/Hacl_Hash_Blake2.c
index 6080585c..5190a421 100644
--- a/src/Hacl_Hash_Blake2.c
+++ b/src/Hacl_Hash_Blake2.c
@@ -26,6 +26,7 @@
 #include "internal/Hacl_Hash_Blake2.h"
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
+#include "libmemzero0.h"
 
 static void
 blake2b_update_block(
@@ -531,7 +532,7 @@ Hacl_Blake2b_32_blake2b_update_key(
   {
     blake2b_update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, (uint32_t)128U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)128U, uint8_t);
 }
 
 void
@@ -571,7 +572,7 @@ Hacl_Blake2b_32_blake2b_update_last(
   FStar_UInt128_uint128
   totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len));
   blake2b_update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, (uint32_t)128U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)128U, uint8_t);
 }
 
 static void
@@ -642,7 +643,7 @@ void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, uint64_t *hash
     store64_le(second + i * (uint32_t)8U, row1[i]););
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t);
 }
 
 /**
@@ -670,8 +671,8 @@ Hacl_Blake2b_32_blake2b(
   Hacl_Blake2b_32_blake2b_init(b, kk, nn);
   blake2b_update(b1, b, kk, k, ll, d);
   Hacl_Blake2b_32_blake2b_finish(nn, output, b);
-  Lib_Memzero0_memzero(b1, (uint32_t)16U * sizeof (b1[0U]));
-  Lib_Memzero0_memzero(b, (uint32_t)16U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b1, (uint32_t)16U, uint64_t);
+  Lib_Memzero0_memzero(b, (uint32_t)16U, uint64_t);
 }
 
 uint64_t *Hacl_Blake2b_32_blake2b_malloc(void)
@@ -1178,7 +1179,7 @@ Hacl_Blake2s_32_blake2s_update_key(
   {
     blake2s_update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t);
 }
 
 void
@@ -1214,7 +1215,7 @@ Hacl_Blake2s_32_blake2s_update_last(
   memcpy(b, last, rem * sizeof (uint8_t));
   uint64_t totlen = prev + (uint64_t)len;
   blake2s_update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t);
 }
 
 static void
@@ -1281,7 +1282,7 @@ void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, uint32_t *hash
     store32_le(second + i * (uint32_t)4U, row1[i]););
   uint8_t *final = b;
   memcpy(output, final, nn * sizeof (uint8_t));
-  Lib_Memzero0_memzero(b, (uint32_t)32U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)32U, uint8_t);
 }
 
 /**
@@ -1309,8 +1310,8 @@ Hacl_Blake2s_32_blake2s(
   Hacl_Blake2s_32_blake2s_init(b, kk, nn);
   blake2s_update(b1, b, kk, k, ll, d);
   Hacl_Blake2s_32_blake2s_finish(nn, output, b);
-  Lib_Memzero0_memzero(b1, (uint32_t)16U * sizeof (b1[0U]));
-  Lib_Memzero0_memzero(b, (uint32_t)16U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b1, (uint32_t)16U, uint32_t);
+  Lib_Memzero0_memzero(b, (uint32_t)16U, uint32_t);
 }
 
 uint32_t *Hacl_Blake2s_32_blake2s_malloc(void)
diff --git a/src/Hacl_Hash_Blake2b_256.c b/src/Hacl_Hash_Blake2b_256.c
index 2761aeb1..07d4f4d6 100644
--- a/src/Hacl_Hash_Blake2b_256.c
+++ b/src/Hacl_Hash_Blake2b_256.c
@@ -27,6 +27,7 @@
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
 #include "internal/Hacl_Hash_Blake2.h"
+#include "libmemzero0.h"
 
 static inline void
 blake2b_update_block(
@@ -254,7 +255,7 @@ Hacl_Blake2b_256_blake2b_update_key(
   {
     blake2b_update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, (uint32_t)128U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)128U, uint8_t);
 }
 
 void
@@ -294,7 +295,7 @@ Hacl_Blake2b_256_blake2b_update_last(
   FStar_UInt128_uint128
   totlen = FStar_UInt128_add_mod(prev, FStar_UInt128_uint64_to_uint128((uint64_t)len));
   blake2b_update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, (uint32_t)128U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)128U, uint8_t);
 }
 
 static inline void
@@ -369,7 +370,7 @@ Hacl_Blake2b_256_blake2b_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, (uint32_t)64U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t);
 }
 
 /**
@@ -397,8 +398,8 @@ Hacl_Blake2b_256_blake2b(
   Hacl_Blake2b_256_blake2b_init(b, kk, nn);
   blake2b_update(b1, b, kk, k, ll, d);
   Hacl_Blake2b_256_blake2b_finish(nn, output, b);
-  Lib_Memzero0_memzero(b1, (uint32_t)4U * sizeof (b1[0U]));
-  Lib_Memzero0_memzero(b, (uint32_t)4U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b1, (uint32_t)4U, Lib_IntVector_Intrinsics_vec256);
+  Lib_Memzero0_memzero(b, (uint32_t)4U, Lib_IntVector_Intrinsics_vec256);
 }
 
 void
diff --git a/src/Hacl_Hash_Blake2s_128.c b/src/Hacl_Hash_Blake2s_128.c
index ce5252cc..26c15742 100644
--- a/src/Hacl_Hash_Blake2s_128.c
+++ b/src/Hacl_Hash_Blake2s_128.c
@@ -27,6 +27,7 @@
 
 #include "internal/Hacl_Impl_Blake2_Constants.h"
 #include "internal/Hacl_Hash_Blake2.h"
+#include "libmemzero0.h"
 
 static inline void
 blake2s_update_block(
@@ -254,7 +255,7 @@ Hacl_Blake2s_128_blake2s_update_key(
   {
     blake2s_update_block(wv, hash, false, lb, b);
   }
-  Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t);
 }
 
 void
@@ -290,7 +291,7 @@ Hacl_Blake2s_128_blake2s_update_last(
   memcpy(b, last, rem * sizeof (uint8_t));
   uint64_t totlen = prev + (uint64_t)len;
   blake2s_update_block(wv, hash, true, totlen, b);
-  Lib_Memzero0_memzero(b, (uint32_t)64U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t);
 }
 
 static inline void
@@ -361,7 +362,7 @@ Hacl_Blake2s_128_blake2s_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, (uint32_t)32U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b, (uint32_t)32U, uint8_t);
 }
 
 /**
@@ -389,8 +390,8 @@ Hacl_Blake2s_128_blake2s(
   Hacl_Blake2s_128_blake2s_init(b, kk, nn);
   blake2s_update(b1, b, kk, k, ll, d);
   Hacl_Blake2s_128_blake2s_finish(nn, output, b);
-  Lib_Memzero0_memzero(b1, (uint32_t)4U * sizeof (b1[0U]));
-  Lib_Memzero0_memzero(b, (uint32_t)4U * sizeof (b[0U]));
+  Lib_Memzero0_memzero(b1, (uint32_t)4U, Lib_IntVector_Intrinsics_vec128);
+  Lib_Memzero0_memzero(b, (uint32_t)4U, Lib_IntVector_Intrinsics_vec128);
 }
 
 void
diff --git a/src/Lib_Memzero0.c b/src/Lib_Memzero0.c
index 8e225318..45a04efe 100644
--- a/src/Lib_Memzero0.c
+++ b/src/Lib_Memzero0.c
@@ -22,13 +22,13 @@
 #include <limits.h>
 #include <inttypes.h>
 
-#include "Lib_Memzero0.h"
+#include "libmemzero0.h"
 #include "krml/internal/target.h"
 
 /* The F* formalization talks about the number of elements in the array. The C
    implementation wants a number of bytes in the array. KaRaMeL is aware of this
    and inserts a sizeof multiplication. */
-void Lib_Memzero0_memzero(void *dst, uint64_t len) {
+void Lib_Memzero0_memzero0(void *dst, uint64_t len) {
   /* This is safe: karamel checks at run-time (if needed) that all object sizes
      fit within a size_t, so the size we receive has been checked at
      allocation-time, possibly via KRML_CHECK_SIZE, to fit in a size_t. */
diff --git a/src/wasm/Hacl_Lib.wasm b/src/wasm/Hacl_Lib.wasm
new file mode 100644
index 00000000..f29473f2
Binary files /dev/null and b/src/wasm/Hacl_Lib.wasm differ
diff --git a/src/wasm/INFO.txt b/src/wasm/INFO.txt
index 0288bd71..c90ea6d6 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: e617752a1b014a16892f7d8772d62e5c234f06c1
-Karamel version: 2cf2974007f4103dba5619e4eb9e3eaeefad533b
+F* version: c880c737ab338f110fa7747f50f4ef2e37e21e5d
+Karamel version: fabda97b2a90bbd244b015d637199bef5b02c374
 Vale version: 0.3.19