diff --git a/Makefile.pre.in b/Makefile.pre.in
index eb79c9c4ca1801..2482b637739a79 100644
--- a/Makefile.pre.in
+++ b/Makefile.pre.in
@@ -208,7 +208,7 @@ ENSUREPIP=      @ENSUREPIP@
 # Internal static libraries
 LIBMPDEC_A= Modules/_decimal/libmpdec/libmpdec.a
 LIBEXPAT_A= Modules/expat/libexpat.a
-LIBHACL_SHA2_A= Modules/_hacl/libHacl_Streaming_SHA2.a
+LIBHACL_SHA2_A= Modules/_hacl/libHacl_Hash_SHA2.a
 
 # Module state, compiler flags and linker flags
 # Empty CFLAGS and LDFLAGS are omitted.
@@ -583,7 +583,7 @@ LIBEXPAT_HEADERS= \
 # hashlib's HACL* library
 
 LIBHACL_SHA2_OBJS= \
-                Modules/_hacl/Hacl_Streaming_SHA2.o
+                Modules/_hacl/Hacl_Hash_SHA2.o
 
 LIBHACL_HEADERS= \
                 Modules/_hacl/include/krml/FStar_UInt128_Verified.h \
@@ -596,8 +596,8 @@ LIBHACL_HEADERS= \
                 Modules/_hacl/python_hacl_namespaces.h
 
 LIBHACL_SHA2_HEADERS= \
-                Modules/_hacl/Hacl_Streaming_SHA2.h \
-                Modules/_hacl/internal/Hacl_SHA2_Generic.h \
+                Modules/_hacl/Hacl_Hash_SHA2.h \
+                Modules/_hacl/internal/Hacl_Hash_SHA2.h \
 		$(LIBHACL_HEADERS)
 
 #########################################################################
@@ -964,11 +964,11 @@ $(LIBEXPAT_A): $(LIBEXPAT_OBJS)
 	$(AR) $(ARFLAGS) $@ $(LIBEXPAT_OBJS)
 
 ##########################################################################
-# Build HACL* static libraries for hashlib: libHacl_Streaming_SHA2.a
+# Build HACL* static libraries for hashlib: libHacl_Hash_SHA2.a
 LIBHACL_CFLAGS=-I$(srcdir)/Modules/_hacl/include -D_BSD_SOURCE -D_DEFAULT_SOURCE $(PY_STDMODULE_CFLAGS) $(CCSHARED)
 
-Modules/_hacl/Hacl_Streaming_SHA2.o: $(srcdir)/Modules/_hacl/Hacl_Streaming_SHA2.c $(LIBHACL_SHA2_HEADERS)
-	$(CC) -c $(LIBHACL_CFLAGS) -o $@ $(srcdir)/Modules/_hacl/Hacl_Streaming_SHA2.c
+Modules/_hacl/Hacl_Hash_SHA2.o: $(srcdir)/Modules/_hacl/Hacl_Hash_SHA2.c $(LIBHACL_SHA2_HEADERS)
+	$(CC) -c $(LIBHACL_CFLAGS) -o $@ $(srcdir)/Modules/_hacl/Hacl_Hash_SHA2.c
 
 $(LIBHACL_SHA2_A): $(LIBHACL_SHA2_OBJS)
 	-rm -f $@
diff --git a/Misc/NEWS.d/next/Security/2023-05-24-09-29-08.gh-issue-99108.hwS2cr.rst b/Misc/NEWS.d/next/Security/2023-05-24-09-29-08.gh-issue-99108.hwS2cr.rst
new file mode 100644
index 00000000000000..312ba89454b5b8
--- /dev/null
+++ b/Misc/NEWS.d/next/Security/2023-05-24-09-29-08.gh-issue-99108.hwS2cr.rst
@@ -0,0 +1,2 @@
+Refresh our new HACL* built-in :mod:`hashlib` code from upstream. Built-in
+SHA2 should be faster and an issue with SHA3 on 32-bit platforms is fixed.
diff --git a/Modules/Setup b/Modules/Setup
index 312e99fea530dc..a8faa1d1028da5 100644
--- a/Modules/Setup
+++ b/Modules/Setup
@@ -165,7 +165,7 @@ PYTHONPATH=$(COREPYTHONPATH)
 #_blake2 _blake2/blake2module.c _blake2/blake2b_impl.c _blake2/blake2s_impl.c
 #_md5 md5module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_MD5.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
 #_sha1 sha1module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_SHA1.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
-#_sha2 sha2module.c -I$(srcdir)/Modules/_hacl/include Modules/_hacl/libHacl_Streaming_SHA2.a
+#_sha2 sha2module.c -I$(srcdir)/Modules/_hacl/include Modules/_hacl/libHacl_Hash_SHA2.a
 #_sha3 sha3module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_SHA3.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
 
 # text encodings and unicode
diff --git a/Modules/Setup.stdlib.in b/Modules/Setup.stdlib.in
index 6db567d713090d..0fc7955cd9b7c2 100644
--- a/Modules/Setup.stdlib.in
+++ b/Modules/Setup.stdlib.in
@@ -78,7 +78,7 @@
 # hashing builtins, can be disabled with --without-builtin-hashlib-hashes
 @MODULE__MD5_TRUE@_md5 md5module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_MD5.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
 @MODULE__SHA1_TRUE@_sha1 sha1module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_SHA1.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
-@MODULE__SHA2_TRUE@_sha2 sha2module.c -I$(srcdir)/Modules/_hacl/include Modules/_hacl/libHacl_Streaming_SHA2.a
+@MODULE__SHA2_TRUE@_sha2 sha2module.c -I$(srcdir)/Modules/_hacl/include Modules/_hacl/libHacl_Hash_SHA2.a
 @MODULE__SHA3_TRUE@_sha3 sha3module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_SHA3.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
 @MODULE__BLAKE2_TRUE@_blake2 _blake2/blake2module.c _blake2/blake2b_impl.c _blake2/blake2s_impl.c
 
diff --git a/Modules/_hacl/Hacl_Hash_MD5.c b/Modules/_hacl/Hacl_Hash_MD5.c
index 2c613066d9f682..222ac824f01961 100644
--- a/Modules/_hacl/Hacl_Hash_MD5.c
+++ b/Modules/_hacl/Hacl_Hash_MD5.c
@@ -1227,14 +1227,14 @@ void Hacl_Streaming_MD5_legacy_init(Hacl_Streaming_MD_state_32 *s)
 /**
 0 = success, 1 = max length exceeded
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_MD5_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_MD_state_32 s = *p;
   uint64_t total_len = s.total_len;
   if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -1399,7 +1399,7 @@ Hacl_Streaming_MD5_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data, u
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 void Hacl_Streaming_MD5_legacy_finish(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)
diff --git a/Modules/_hacl/Hacl_Hash_MD5.h b/Modules/_hacl/Hacl_Hash_MD5.h
index 015e3668751b75..13c19fd40f4d12 100644
--- a/Modules/_hacl/Hacl_Hash_MD5.h
+++ b/Modules/_hacl/Hacl_Hash_MD5.h
@@ -46,7 +46,7 @@ void Hacl_Streaming_MD5_legacy_init(Hacl_Streaming_MD_state_32 *s);
 /**
 0 = success, 1 = max length exceeded
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_MD5_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len);
 
 void Hacl_Streaming_MD5_legacy_finish(Hacl_Streaming_MD_state_32 *p, uint8_t *dst);
diff --git a/Modules/_hacl/Hacl_Hash_SHA1.c b/Modules/_hacl/Hacl_Hash_SHA1.c
index e155e338271c56..5ecb3c0b3a56e0 100644
--- a/Modules/_hacl/Hacl_Hash_SHA1.c
+++ b/Modules/_hacl/Hacl_Hash_SHA1.c
@@ -263,14 +263,14 @@ void Hacl_Streaming_SHA1_legacy_init(Hacl_Streaming_MD_state_32 *s)
 /**
 0 = success, 1 = max length exceeded
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA1_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_MD_state_32 s = *p;
   uint64_t total_len = s.total_len;
   if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -435,7 +435,7 @@ Hacl_Streaming_SHA1_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data,
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 void Hacl_Streaming_SHA1_legacy_finish(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)
diff --git a/Modules/_hacl/Hacl_Hash_SHA1.h b/Modules/_hacl/Hacl_Hash_SHA1.h
index 5e2ae8e713292d..dc50aa6f6d3902 100644
--- a/Modules/_hacl/Hacl_Hash_SHA1.h
+++ b/Modules/_hacl/Hacl_Hash_SHA1.h
@@ -46,7 +46,7 @@ void Hacl_Streaming_SHA1_legacy_init(Hacl_Streaming_MD_state_32 *s);
 /**
 0 = success, 1 = max length exceeded
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA1_legacy_update(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len);
 
 void Hacl_Streaming_SHA1_legacy_finish(Hacl_Streaming_MD_state_32 *p, uint8_t *dst);
diff --git a/Modules/_hacl/Hacl_Streaming_SHA2.c b/Modules/_hacl/Hacl_Hash_SHA2.c
similarity index 87%
rename from Modules/_hacl/Hacl_Streaming_SHA2.c
rename to Modules/_hacl/Hacl_Hash_SHA2.c
index 69c3be8cdf7fd1..08e3f7edbf4ede 100644
--- a/Modules/_hacl/Hacl_Streaming_SHA2.c
+++ b/Modules/_hacl/Hacl_Hash_SHA2.c
@@ -23,12 +23,11 @@
  */
 
 
-#include "Hacl_Streaming_SHA2.h"
+#include "internal/Hacl_Hash_SHA2.h"
 
-#include "internal/Hacl_SHA2_Generic.h"
 
 
-static inline void sha256_init(uint32_t *hash)
+void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash)
 {
   KRML_MAYBE_FOR8(i,
     (uint32_t)0U,
@@ -39,7 +38,7 @@ static inline void sha256_init(uint32_t *hash)
     os[i] = x;);
 }
 
-static inline void sha256_update0(uint8_t *b, uint32_t *hash)
+static inline void sha256_update(uint8_t *b, uint32_t *hash)
 {
   uint32_t hash_old[8U] = { 0U };
   uint32_t ws[16U] = { 0U };
@@ -159,19 +158,24 @@ static inline void sha256_update0(uint8_t *b, uint32_t *hash)
     os[i] = x;);
 }
 
-static inline void sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st)
+void Hacl_SHA2_Scalar32_sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st)
 {
   uint32_t blocks = len / (uint32_t)64U;
   for (uint32_t i = (uint32_t)0U; i < blocks; i++)
   {
     uint8_t *b0 = b;
     uint8_t *mb = b0 + i * (uint32_t)64U;
-    sha256_update0(mb, st);
+    sha256_update(mb, st);
   }
 }
 
-static inline void
-sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *hash)
+void
+Hacl_SHA2_Scalar32_sha256_update_last(
+  uint64_t totlen,
+  uint32_t len,
+  uint8_t *b,
+  uint32_t *hash
+)
 {
   uint32_t blocks;
   if (len + (uint32_t)8U + (uint32_t)1U <= (uint32_t)64U)
@@ -199,15 +203,15 @@ sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *hash)
   uint8_t *lb1 = l1;
   uint8_t *last0 = lb0;
   uint8_t *last1 = lb1;
-  sha256_update0(last0, hash);
+  sha256_update(last0, hash);
   if (blocks > (uint32_t)1U)
   {
-    sha256_update0(last1, hash);
+    sha256_update(last1, hash);
     return;
   }
 }
 
-static inline void sha256_finish(uint32_t *st, uint8_t *h)
+void Hacl_SHA2_Scalar32_sha256_finish(uint32_t *st, uint8_t *h)
 {
   uint8_t hbuf[32U] = { 0U };
   KRML_MAYBE_FOR8(i,
@@ -218,7 +222,7 @@ static inline void sha256_finish(uint32_t *st, uint8_t *h)
   memcpy(h, hbuf, (uint32_t)32U * sizeof (uint8_t));
 }
 
-static inline void sha224_init(uint32_t *hash)
+void Hacl_SHA2_Scalar32_sha224_init(uint32_t *hash)
 {
   KRML_MAYBE_FOR8(i,
     (uint32_t)0U,
@@ -231,15 +235,16 @@ static inline void sha224_init(uint32_t *hash)
 
 static inline void sha224_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st)
 {
-  sha256_update_nblocks(len, b, st);
+  Hacl_SHA2_Scalar32_sha256_update_nblocks(len, b, st);
 }
 
-static void sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st)
+void
+Hacl_SHA2_Scalar32_sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st)
 {
-  sha256_update_last(totlen, len, b, st);
+  Hacl_SHA2_Scalar32_sha256_update_last(totlen, len, b, st);
 }
 
-static inline void sha224_finish(uint32_t *st, uint8_t *h)
+void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h)
 {
   uint8_t hbuf[32U] = { 0U };
   KRML_MAYBE_FOR8(i,
@@ -381,7 +386,7 @@ static inline void sha512_update(uint8_t *b, uint64_t *hash)
     os[i] = x;);
 }
 
-static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
+void Hacl_SHA2_Scalar32_sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
 {
   uint32_t blocks = len / (uint32_t)128U;
   for (uint32_t i = (uint32_t)0U; i < blocks; i++)
@@ -392,8 +397,13 @@ static inline void sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
   }
 }
 
-static inline void
-sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *hash)
+void
+Hacl_SHA2_Scalar32_sha512_update_last(
+  FStar_UInt128_uint128 totlen,
+  uint32_t len,
+  uint8_t *b,
+  uint64_t *hash
+)
 {
   uint32_t blocks;
   if (len + (uint32_t)16U + (uint32_t)1U <= (uint32_t)128U)
@@ -429,7 +439,7 @@ sha512_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint6
   }
 }
 
-static inline void sha512_finish(uint64_t *st, uint8_t *h)
+void Hacl_SHA2_Scalar32_sha512_finish(uint64_t *st, uint8_t *h)
 {
   uint8_t hbuf[64U] = { 0U };
   KRML_MAYBE_FOR8(i,
@@ -440,7 +450,7 @@ static inline void sha512_finish(uint64_t *st, uint8_t *h)
   memcpy(h, hbuf, (uint32_t)64U * sizeof (uint8_t));
 }
 
-static inline void sha384_init(uint64_t *hash)
+void Hacl_SHA2_Scalar32_sha384_init(uint64_t *hash)
 {
   KRML_MAYBE_FOR8(i,
     (uint32_t)0U,
@@ -451,18 +461,23 @@ static inline void sha384_init(uint64_t *hash)
     os[i] = x;);
 }
 
-static inline void sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
+void Hacl_SHA2_Scalar32_sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st)
 {
-  sha512_update_nblocks(len, b, st);
+  Hacl_SHA2_Scalar32_sha512_update_nblocks(len, b, st);
 }
 
-static void
-sha384_update_last(FStar_UInt128_uint128 totlen, uint32_t len, uint8_t *b, uint64_t *st)
+void
+Hacl_SHA2_Scalar32_sha384_update_last(
+  FStar_UInt128_uint128 totlen,
+  uint32_t len,
+  uint8_t *b,
+  uint64_t *st
+)
 {
-  sha512_update_last(totlen, len, b, st);
+  Hacl_SHA2_Scalar32_sha512_update_last(totlen, len, b, st);
 }
 
-static inline void sha384_finish(uint64_t *st, uint8_t *h)
+void Hacl_SHA2_Scalar32_sha384_finish(uint64_t *st, uint8_t *h)
 {
   uint8_t hbuf[64U] = { 0U };
   KRML_MAYBE_FOR8(i,
@@ -486,7 +501,7 @@ Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void)
   Hacl_Streaming_MD_state_32
   *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
   p[0U] = s;
-  sha256_init(block_state);
+  Hacl_SHA2_Scalar32_sha256_init(block_state);
   return p;
 }
 
@@ -522,20 +537,20 @@ void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s)
   Hacl_Streaming_MD_state_32 scrut = *s;
   uint8_t *buf = scrut.buf;
   uint32_t *block_state = scrut.block_state;
-  sha256_init(block_state);
+  Hacl_SHA2_Scalar32_sha256_init(block_state);
   Hacl_Streaming_MD_state_32
   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
   s[0U] = tmp;
 }
 
-static inline uint32_t
+static inline Hacl_Streaming_Types_error_code
 update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_MD_state_32 s = *p;
   uint64_t total_len = s.total_len;
   if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -591,7 +606,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
     }
     if (!(sz1 == (uint32_t)0U))
     {
-      sha256_update_nblocks((uint32_t)64U, buf, block_state1);
+      Hacl_SHA2_Scalar32_sha256_update_nblocks((uint32_t)64U, buf, block_state1);
     }
     uint32_t ite;
     if ((uint64_t)len % (uint64_t)(uint32_t)64U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U)
@@ -607,7 +622,9 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
     uint32_t data2_len = len - data1_len;
     uint8_t *data1 = data;
     uint8_t *data2 = data + data1_len;
-    sha256_update_nblocks(data1_len, data1, block_state1);
+    Hacl_SHA2_Scalar32_sha256_update_nblocks(data1_len / (uint32_t)64U * (uint32_t)64U,
+      data1,
+      block_state1);
     uint8_t *dst = buf;
     memcpy(dst, data2, data2_len * sizeof (uint8_t));
     *p
@@ -665,7 +682,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
     }
     if (!(sz1 == (uint32_t)0U))
     {
-      sha256_update_nblocks((uint32_t)64U, buf, block_state1);
+      Hacl_SHA2_Scalar32_sha256_update_nblocks((uint32_t)64U, buf, block_state1);
     }
     uint32_t ite;
     if
@@ -687,7 +704,9 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
     uint32_t data2_len = len - diff - data1_len;
     uint8_t *data11 = data2;
     uint8_t *data21 = data2 + data1_len;
-    sha256_update_nblocks(data1_len, data11, block_state1);
+    Hacl_SHA2_Scalar32_sha256_update_nblocks(data1_len / (uint32_t)64U * (uint32_t)64U,
+      data11,
+      block_state1);
     uint8_t *dst = buf;
     memcpy(dst, data21, data2_len * sizeof (uint8_t));
     *p
@@ -700,7 +719,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len)
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 /**
@@ -710,7 +729,7 @@ success, or 1 if the combined length of all of the data passed to `update_256`
 
 This function is identical to the update function for SHA2_224.
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_256(
   Hacl_Streaming_MD_state_32 *p,
   uint8_t *input,
@@ -755,10 +774,13 @@ void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)
   }
   uint8_t *buf_last = buf_1 + r - ite;
   uint8_t *buf_multi = buf_1;
-  sha256_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
+  Hacl_SHA2_Scalar32_sha256_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
   uint64_t prev_len_last = total_len - (uint64_t)r;
-  sha256_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state);
-  sha256_finish(tmp_block_state, dst);
+  Hacl_SHA2_Scalar32_sha256_update_last(prev_len_last + (uint64_t)r,
+    r,
+    buf_last,
+    tmp_block_state);
+  Hacl_SHA2_Scalar32_sha256_finish(tmp_block_state, dst);
 }
 
 /**
@@ -779,20 +801,20 @@ void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s)
 /**
 Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes.
 */
-void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst)
+void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst)
 {
   uint8_t *ib = input;
   uint8_t *rb = dst;
   uint32_t st[8U] = { 0U };
-  sha256_init(st);
+  Hacl_SHA2_Scalar32_sha256_init(st);
   uint32_t rem = input_len % (uint32_t)64U;
   uint64_t len_ = (uint64_t)input_len;
-  sha256_update_nblocks(input_len, ib, st);
+  Hacl_SHA2_Scalar32_sha256_update_nblocks(input_len, ib, st);
   uint32_t rem1 = input_len % (uint32_t)64U;
   uint8_t *b0 = ib;
   uint8_t *lb = b0 + input_len - rem1;
-  sha256_update_last(len_, rem, lb, st);
-  sha256_finish(st, rb);
+  Hacl_SHA2_Scalar32_sha256_update_last(len_, rem, lb, st);
+  Hacl_SHA2_Scalar32_sha256_finish(st, rb);
 }
 
 Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void)
@@ -804,7 +826,7 @@ Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void)
   Hacl_Streaming_MD_state_32
   *p = (Hacl_Streaming_MD_state_32 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_32));
   p[0U] = s;
-  sha224_init(block_state);
+  Hacl_SHA2_Scalar32_sha224_init(block_state);
   return p;
 }
 
@@ -813,13 +835,13 @@ void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s)
   Hacl_Streaming_MD_state_32 scrut = *s;
   uint8_t *buf = scrut.buf;
   uint32_t *block_state = scrut.block_state;
-  sha224_init(block_state);
+  Hacl_SHA2_Scalar32_sha224_init(block_state);
   Hacl_Streaming_MD_state_32
   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
   s[0U] = tmp;
 }
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_224(
   Hacl_Streaming_MD_state_32 *p,
   uint8_t *input,
@@ -865,8 +887,11 @@ void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst)
   uint8_t *buf_multi = buf_1;
   sha224_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
   uint64_t prev_len_last = total_len - (uint64_t)r;
-  sha224_update_last(prev_len_last + (uint64_t)r, r, buf_last, tmp_block_state);
-  sha224_finish(tmp_block_state, dst);
+  Hacl_SHA2_Scalar32_sha224_update_last(prev_len_last + (uint64_t)r,
+    r,
+    buf_last,
+    tmp_block_state);
+  Hacl_SHA2_Scalar32_sha224_finish(tmp_block_state, dst);
 }
 
 void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p)
@@ -877,20 +902,20 @@ void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p)
 /**
 Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes.
 */
-void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst)
+void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst)
 {
   uint8_t *ib = input;
   uint8_t *rb = dst;
   uint32_t st[8U] = { 0U };
-  sha224_init(st);
+  Hacl_SHA2_Scalar32_sha224_init(st);
   uint32_t rem = input_len % (uint32_t)64U;
   uint64_t len_ = (uint64_t)input_len;
   sha224_update_nblocks(input_len, ib, st);
   uint32_t rem1 = input_len % (uint32_t)64U;
   uint8_t *b0 = ib;
   uint8_t *lb = b0 + input_len - rem1;
-  sha224_update_last(len_, rem, lb, st);
-  sha224_finish(st, rb);
+  Hacl_SHA2_Scalar32_sha224_update_last(len_, rem, lb, st);
+  Hacl_SHA2_Scalar32_sha224_finish(st, rb);
 }
 
 Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void)
@@ -941,14 +966,14 @@ void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s)
   s[0U] = tmp;
 }
 
-static inline uint32_t
+static inline Hacl_Streaming_Types_error_code
 update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_MD_state_64 s = *p;
   uint64_t total_len = s.total_len;
   if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -1004,7 +1029,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
     }
     if (!(sz1 == (uint32_t)0U))
     {
-      sha512_update_nblocks((uint32_t)128U, buf, block_state1);
+      Hacl_SHA2_Scalar32_sha512_update_nblocks((uint32_t)128U, buf, block_state1);
     }
     uint32_t ite;
     if ((uint64_t)len % (uint64_t)(uint32_t)128U == (uint64_t)0U && (uint64_t)len > (uint64_t)0U)
@@ -1020,7 +1045,9 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
     uint32_t data2_len = len - data1_len;
     uint8_t *data1 = data;
     uint8_t *data2 = data + data1_len;
-    sha512_update_nblocks(data1_len, data1, block_state1);
+    Hacl_SHA2_Scalar32_sha512_update_nblocks(data1_len / (uint32_t)128U * (uint32_t)128U,
+      data1,
+      block_state1);
     uint8_t *dst = buf;
     memcpy(dst, data2, data2_len * sizeof (uint8_t));
     *p
@@ -1078,7 +1105,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
     }
     if (!(sz1 == (uint32_t)0U))
     {
-      sha512_update_nblocks((uint32_t)128U, buf, block_state1);
+      Hacl_SHA2_Scalar32_sha512_update_nblocks((uint32_t)128U, buf, block_state1);
     }
     uint32_t ite;
     if
@@ -1100,7 +1127,9 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
     uint32_t data2_len = len - diff - data1_len;
     uint8_t *data11 = data2;
     uint8_t *data21 = data2 + data1_len;
-    sha512_update_nblocks(data1_len, data11, block_state1);
+    Hacl_SHA2_Scalar32_sha512_update_nblocks(data1_len / (uint32_t)128U * (uint32_t)128U,
+      data11,
+      block_state1);
     uint8_t *dst = buf;
     memcpy(dst, data21, data2_len * sizeof (uint8_t));
     *p
@@ -1113,7 +1142,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len)
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 /**
@@ -1123,7 +1152,7 @@ success, or 1 if the combined length of all of the data passed to `update_512`
 
 This function is identical to the update function for SHA2_384.
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_512(
   Hacl_Streaming_MD_state_64 *p,
   uint8_t *input,
@@ -1168,14 +1197,14 @@ void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst)
   }
   uint8_t *buf_last = buf_1 + r - ite;
   uint8_t *buf_multi = buf_1;
-  sha512_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
+  Hacl_SHA2_Scalar32_sha512_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
   uint64_t prev_len_last = total_len - (uint64_t)r;
-  sha512_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last),
+  Hacl_SHA2_Scalar32_sha512_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last),
       FStar_UInt128_uint64_to_uint128((uint64_t)r)),
     r,
     buf_last,
     tmp_block_state);
-  sha512_finish(tmp_block_state, dst);
+  Hacl_SHA2_Scalar32_sha512_finish(tmp_block_state, dst);
 }
 
 /**
@@ -1196,7 +1225,7 @@ void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s)
 /**
 Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes.
 */
-void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst)
+void Hacl_Streaming_SHA2_hash_512(uint8_t *input, uint32_t input_len, uint8_t *dst)
 {
   uint8_t *ib = input;
   uint8_t *rb = dst;
@@ -1204,12 +1233,12 @@ void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst
   Hacl_SHA2_Scalar32_sha512_init(st);
   uint32_t rem = input_len % (uint32_t)128U;
   FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len);
-  sha512_update_nblocks(input_len, ib, st);
+  Hacl_SHA2_Scalar32_sha512_update_nblocks(input_len, ib, st);
   uint32_t rem1 = input_len % (uint32_t)128U;
   uint8_t *b0 = ib;
   uint8_t *lb = b0 + input_len - rem1;
-  sha512_update_last(len_, rem, lb, st);
-  sha512_finish(st, rb);
+  Hacl_SHA2_Scalar32_sha512_update_last(len_, rem, lb, st);
+  Hacl_SHA2_Scalar32_sha512_finish(st, rb);
 }
 
 Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void)
@@ -1221,7 +1250,7 @@ Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void)
   Hacl_Streaming_MD_state_64
   *p = (Hacl_Streaming_MD_state_64 *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_MD_state_64));
   p[0U] = s;
-  sha384_init(block_state);
+  Hacl_SHA2_Scalar32_sha384_init(block_state);
   return p;
 }
 
@@ -1230,13 +1259,13 @@ void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s)
   Hacl_Streaming_MD_state_64 scrut = *s;
   uint8_t *buf = scrut.buf;
   uint64_t *block_state = scrut.block_state;
-  sha384_init(block_state);
+  Hacl_SHA2_Scalar32_sha384_init(block_state);
   Hacl_Streaming_MD_state_64
   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
   s[0U] = tmp;
 }
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_384(
   Hacl_Streaming_MD_state_64 *p,
   uint8_t *input,
@@ -1280,14 +1309,14 @@ void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst)
   }
   uint8_t *buf_last = buf_1 + r - ite;
   uint8_t *buf_multi = buf_1;
-  sha384_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
+  Hacl_SHA2_Scalar32_sha384_update_nblocks((uint32_t)0U, buf_multi, tmp_block_state);
   uint64_t prev_len_last = total_len - (uint64_t)r;
-  sha384_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last),
+  Hacl_SHA2_Scalar32_sha384_update_last(FStar_UInt128_add(FStar_UInt128_uint64_to_uint128(prev_len_last),
       FStar_UInt128_uint64_to_uint128((uint64_t)r)),
     r,
     buf_last,
     tmp_block_state);
-  sha384_finish(tmp_block_state, dst);
+  Hacl_SHA2_Scalar32_sha384_finish(tmp_block_state, dst);
 }
 
 void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p)
@@ -1298,19 +1327,19 @@ void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p)
 /**
 Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes.
 */
-void Hacl_Streaming_SHA2_sha384(uint8_t *input, uint32_t input_len, uint8_t *dst)
+void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst)
 {
   uint8_t *ib = input;
   uint8_t *rb = dst;
   uint64_t st[8U] = { 0U };
-  sha384_init(st);
+  Hacl_SHA2_Scalar32_sha384_init(st);
   uint32_t rem = input_len % (uint32_t)128U;
   FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len);
-  sha384_update_nblocks(input_len, ib, st);
+  Hacl_SHA2_Scalar32_sha384_update_nblocks(input_len, ib, st);
   uint32_t rem1 = input_len % (uint32_t)128U;
   uint8_t *b0 = ib;
   uint8_t *lb = b0 + input_len - rem1;
-  sha384_update_last(len_, rem, lb, st);
-  sha384_finish(st, rb);
+  Hacl_SHA2_Scalar32_sha384_update_last(len_, rem, lb, st);
+  Hacl_SHA2_Scalar32_sha384_finish(st, rb);
 }
 
diff --git a/Modules/_hacl/Hacl_Streaming_SHA2.h b/Modules/_hacl/Hacl_Hash_SHA2.h
similarity index 91%
rename from Modules/_hacl/Hacl_Streaming_SHA2.h
rename to Modules/_hacl/Hacl_Hash_SHA2.h
index b58df4c4d121c9..a0e731094dfaa5 100644
--- a/Modules/_hacl/Hacl_Streaming_SHA2.h
+++ b/Modules/_hacl/Hacl_Hash_SHA2.h
@@ -23,8 +23,8 @@
  */
 
 
-#ifndef __Hacl_Streaming_SHA2_H
-#define __Hacl_Streaming_SHA2_H
+#ifndef __Hacl_Hash_SHA2_H
+#define __Hacl_Hash_SHA2_H
 
 #if defined(__cplusplus)
 extern "C" {
@@ -73,7 +73,7 @@ success, or 1 if the combined length of all of the data passed to `update_256`
 
 This function is identical to the update function for SHA2_224.
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_256(
   Hacl_Streaming_MD_state_32 *p,
   uint8_t *input,
@@ -98,13 +98,13 @@ void Hacl_Streaming_SHA2_free_256(Hacl_Streaming_MD_state_32 *s);
 /**
 Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes.
 */
-void Hacl_Streaming_SHA2_sha256(uint8_t *input, uint32_t input_len, uint8_t *dst);
+void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst);
 
 Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_224(void);
 
 void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s);
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_224(
   Hacl_Streaming_MD_state_32 *p,
   uint8_t *input,
@@ -123,7 +123,7 @@ void Hacl_Streaming_SHA2_free_224(Hacl_Streaming_MD_state_32 *p);
 /**
 Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes.
 */
-void Hacl_Streaming_SHA2_sha224(uint8_t *input, uint32_t input_len, uint8_t *dst);
+void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst);
 
 Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void);
 
@@ -144,7 +144,7 @@ success, or 1 if the combined length of all of the data passed to `update_512`
 
 This function is identical to the update function for SHA2_384.
 */
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_512(
   Hacl_Streaming_MD_state_64 *p,
   uint8_t *input,
@@ -169,13 +169,13 @@ void Hacl_Streaming_SHA2_free_512(Hacl_Streaming_MD_state_64 *s);
 /**
 Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes.
 */
-void Hacl_Streaming_SHA2_sha512(uint8_t *input, uint32_t input_len, uint8_t *dst);
+void Hacl_Streaming_SHA2_hash_512(uint8_t *input, uint32_t input_len, uint8_t *dst);
 
 Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_384(void);
 
 void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s);
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_SHA2_update_384(
   Hacl_Streaming_MD_state_64 *p,
   uint8_t *input,
@@ -194,11 +194,11 @@ void Hacl_Streaming_SHA2_free_384(Hacl_Streaming_MD_state_64 *p);
 /**
 Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes.
 */
-void Hacl_Streaming_SHA2_sha384(uint8_t *input, uint32_t input_len, uint8_t *dst);
+void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst);
 
 #if defined(__cplusplus)
 }
 #endif
 
-#define __Hacl_Streaming_SHA2_H_DEFINED
+#define __Hacl_Hash_SHA2_H_DEFINED
 #endif
diff --git a/Modules/_hacl/Hacl_Hash_SHA3.c b/Modules/_hacl/Hacl_Hash_SHA3.c
index 58eb436881d45c..b3febdfeb2b221 100644
--- a/Modules/_hacl/Hacl_Hash_SHA3.c
+++ b/Modules/_hacl/Hacl_Hash_SHA3.c
@@ -184,8 +184,7 @@ Hacl_Streaming_Keccak_state *Hacl_Streaming_Keccak_malloc(Spec_Hash_Definitions_
   *p = (Hacl_Streaming_Keccak_state *)KRML_HOST_MALLOC(sizeof (Hacl_Streaming_Keccak_state));
   p[0U] = s;
   uint64_t *s1 = block_state.snd;
-  for (uint32_t _i = 0U; _i < (uint32_t)25U; ++_i)
-    ((void **)s1)[_i] = (void *)(uint64_t)0U;
+  memset(s1, 0U, (uint32_t)25U * sizeof (uint64_t));
   return p;
 }
 
@@ -230,23 +229,22 @@ void Hacl_Streaming_Keccak_reset(Hacl_Streaming_Keccak_state *s)
   uint8_t *buf = scrut.buf;
   Hacl_Streaming_Keccak_hash_buf block_state = scrut.block_state;
   uint64_t *s1 = block_state.snd;
-  for (uint32_t _i = 0U; _i < (uint32_t)25U; ++_i)
-    ((void **)s1)[_i] = (void *)(uint64_t)0U;
+  memset(s1, 0U, (uint32_t)25U * sizeof (uint64_t));
   Hacl_Streaming_Keccak_state
   tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U };
   s[0U] = tmp;
 }
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_update(Hacl_Streaming_Keccak_state *p, uint8_t *data, uint32_t len)
 {
   Hacl_Streaming_Keccak_state s = *p;
   Hacl_Streaming_Keccak_hash_buf block_state = s.block_state;
   uint64_t total_len = s.total_len;
   Spec_Hash_Definitions_hash_alg i = block_state.fst;
-  if ((uint64_t)len > (uint64_t)0xffffffffffffffffU - total_len)
+  if ((uint64_t)len > (uint64_t)0xFFFFFFFFFFFFFFFFU - total_len)
   {
-    return (uint32_t)1U;
+    return Hacl_Streaming_Types_MaximumLengthExceeded;
   }
   uint32_t sz;
   if (total_len % (uint64_t)block_len(i) == (uint64_t)0U && total_len > (uint64_t)0U)
@@ -419,7 +417,7 @@ Hacl_Streaming_Keccak_update(Hacl_Streaming_Keccak_state *p, uint8_t *data, uint
         }
       );
   }
-  return (uint32_t)0U;
+  return Hacl_Streaming_Types_Success;
 }
 
 static void
@@ -486,32 +484,32 @@ finish_(
   Hacl_Impl_SHA3_squeeze(s, block_len(a11), hash_len(a11), dst);
 }
 
-Hacl_Streaming_Keccak_error_code
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_finish(Hacl_Streaming_Keccak_state *s, uint8_t *dst)
 {
   Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s);
   if (a1 == Spec_Hash_Definitions_Shake128 || a1 == Spec_Hash_Definitions_Shake256)
   {
-    return Hacl_Streaming_Keccak_InvalidAlgorithm;
+    return Hacl_Streaming_Types_InvalidAlgorithm;
   }
   finish_(a1, s, dst, hash_len(a1));
-  return Hacl_Streaming_Keccak_Success;
+  return Hacl_Streaming_Types_Success;
 }
 
-Hacl_Streaming_Keccak_error_code
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_squeeze(Hacl_Streaming_Keccak_state *s, uint8_t *dst, uint32_t l)
 {
   Spec_Hash_Definitions_hash_alg a1 = Hacl_Streaming_Keccak_get_alg(s);
   if (!(a1 == Spec_Hash_Definitions_Shake128 || a1 == Spec_Hash_Definitions_Shake256))
   {
-    return Hacl_Streaming_Keccak_InvalidAlgorithm;
+    return Hacl_Streaming_Types_InvalidAlgorithm;
   }
   if (l == (uint32_t)0U)
   {
-    return Hacl_Streaming_Keccak_InvalidLength;
+    return Hacl_Streaming_Types_InvalidLength;
   }
   finish_(a1, s, dst, l);
-  return Hacl_Streaming_Keccak_Success;
+  return Hacl_Streaming_Types_Success;
 }
 
 uint32_t Hacl_Streaming_Keccak_block_len(Hacl_Streaming_Keccak_state *s)
diff --git a/Modules/_hacl/Hacl_Hash_SHA3.h b/Modules/_hacl/Hacl_Hash_SHA3.h
index 2a5cf4b1844b9d..681b6af4a80e77 100644
--- a/Modules/_hacl/Hacl_Hash_SHA3.h
+++ b/Modules/_hacl/Hacl_Hash_SHA3.h
@@ -62,19 +62,13 @@ Hacl_Streaming_Keccak_state *Hacl_Streaming_Keccak_copy(Hacl_Streaming_Keccak_st
 
 void Hacl_Streaming_Keccak_reset(Hacl_Streaming_Keccak_state *s);
 
-uint32_t
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_update(Hacl_Streaming_Keccak_state *p, uint8_t *data, uint32_t len);
 
-#define Hacl_Streaming_Keccak_Success 0
-#define Hacl_Streaming_Keccak_InvalidAlgorithm 1
-#define Hacl_Streaming_Keccak_InvalidLength 2
-
-typedef uint8_t Hacl_Streaming_Keccak_error_code;
-
-Hacl_Streaming_Keccak_error_code
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_finish(Hacl_Streaming_Keccak_state *s, uint8_t *dst);
 
-Hacl_Streaming_Keccak_error_code
+Hacl_Streaming_Types_error_code
 Hacl_Streaming_Keccak_squeeze(Hacl_Streaming_Keccak_state *s, uint8_t *dst, uint32_t l);
 
 uint32_t Hacl_Streaming_Keccak_block_len(Hacl_Streaming_Keccak_state *s);
diff --git a/Modules/_hacl/Hacl_Streaming_Types.h b/Modules/_hacl/Hacl_Streaming_Types.h
index 8a60b707bc4958..15ef16ba6075a9 100644
--- a/Modules/_hacl/Hacl_Streaming_Types.h
+++ b/Modules/_hacl/Hacl_Streaming_Types.h
@@ -52,6 +52,13 @@ extern "C" {
 
 typedef uint8_t Spec_Hash_Definitions_hash_alg;
 
+#define Hacl_Streaming_Types_Success 0
+#define Hacl_Streaming_Types_InvalidAlgorithm 1
+#define Hacl_Streaming_Types_InvalidLength 2
+#define Hacl_Streaming_Types_MaximumLengthExceeded 3
+
+typedef uint8_t Hacl_Streaming_Types_error_code;
+
 typedef struct Hacl_Streaming_MD_state_32_s
 {
   uint32_t *block_state;
diff --git a/Modules/_hacl/internal/Hacl_SHA2_Generic.h b/Modules/_hacl/internal/Hacl_Hash_SHA2.h
similarity index 83%
rename from Modules/_hacl/internal/Hacl_SHA2_Generic.h
rename to Modules/_hacl/internal/Hacl_Hash_SHA2.h
index 6ac47f3cf7ed36..851f7dc60c94c2 100644
--- a/Modules/_hacl/internal/Hacl_SHA2_Generic.h
+++ b/Modules/_hacl/internal/Hacl_Hash_SHA2.h
@@ -23,8 +23,8 @@
  */
 
 
-#ifndef __internal_Hacl_SHA2_Generic_H
-#define __internal_Hacl_SHA2_Generic_H
+#ifndef __internal_Hacl_Hash_SHA2_H
+#define __internal_Hacl_Hash_SHA2_H
 
 #if defined(__cplusplus)
 extern "C" {
@@ -35,6 +35,9 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/target.h"
 
+
+#include "../Hacl_Hash_SHA2.h"
+
 static const
 uint32_t
 Hacl_Impl_SHA2_Generic_h224[8U] =
@@ -124,9 +127,58 @@ Hacl_Impl_SHA2_Generic_k384_512[80U] =
     (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U
   };
 
+void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash);
+
+void Hacl_SHA2_Scalar32_sha256_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st);
+
+void
+Hacl_SHA2_Scalar32_sha256_update_last(
+  uint64_t totlen,
+  uint32_t len,
+  uint8_t *b,
+  uint32_t *hash
+);
+
+void Hacl_SHA2_Scalar32_sha256_finish(uint32_t *st, uint8_t *h);
+
+void Hacl_SHA2_Scalar32_sha224_init(uint32_t *hash);
+
+void
+Hacl_SHA2_Scalar32_sha224_update_last(uint64_t totlen, uint32_t len, uint8_t *b, uint32_t *st);
+
+void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h);
+
+void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash);
+
+void Hacl_SHA2_Scalar32_sha512_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st);
+
+void
+Hacl_SHA2_Scalar32_sha512_update_last(
+  FStar_UInt128_uint128 totlen,
+  uint32_t len,
+  uint8_t *b,
+  uint64_t *hash
+);
+
+void Hacl_SHA2_Scalar32_sha512_finish(uint64_t *st, uint8_t *h);
+
+void Hacl_SHA2_Scalar32_sha384_init(uint64_t *hash);
+
+void Hacl_SHA2_Scalar32_sha384_update_nblocks(uint32_t len, uint8_t *b, uint64_t *st);
+
+void
+Hacl_SHA2_Scalar32_sha384_update_last(
+  FStar_UInt128_uint128 totlen,
+  uint32_t len,
+  uint8_t *b,
+  uint64_t *st
+);
+
+void Hacl_SHA2_Scalar32_sha384_finish(uint64_t *st, uint8_t *h);
+
 #if defined(__cplusplus)
 }
 #endif
 
-#define __internal_Hacl_SHA2_Generic_H_DEFINED
+#define __internal_Hacl_Hash_SHA2_H_DEFINED
 #endif
diff --git a/Modules/_hacl/refresh.sh b/Modules/_hacl/refresh.sh
index d2ba05f30d860f..c1b3e37f3afb9d 100755
--- a/Modules/_hacl/refresh.sh
+++ b/Modules/_hacl/refresh.sh
@@ -22,7 +22,7 @@ fi
 
 # Update this when updating to a new version after verifying that the changes
 # the update brings in are good.
-expected_hacl_star_rev=b6903a3e6458000730c3d83174d4b08d6d3e2ece
+expected_hacl_star_rev=521af282fdf6d60227335120f18ae9309a4b8e8c
 
 hacl_dir="$(realpath "$1")"
 cd "$(dirname "$0")"
@@ -40,7 +40,7 @@ fi
 
 declare -a dist_files
 dist_files=(
-  Hacl_Streaming_SHA2.h
+  Hacl_Hash_SHA2.h
   Hacl_Streaming_Types.h
   Hacl_Hash_SHA1.h
   internal/Hacl_Hash_SHA1.h
@@ -48,8 +48,8 @@ dist_files=(
   Hacl_Hash_SHA3.h
   internal/Hacl_Hash_MD5.h
   internal/Hacl_Hash_SHA3.h
-  internal/Hacl_SHA2_Generic.h
-  Hacl_Streaming_SHA2.c
+  Hacl_Hash_SHA2.c
+  internal/Hacl_Hash_SHA2.h
   Hacl_Hash_SHA1.c
   Hacl_Hash_MD5.c
   Hacl_Hash_SHA3.c
@@ -126,14 +126,8 @@ $sed -i -z 's!\(extern\|typedef\)[^;]*;\n\n!!g' include/krml/FStar_UInt_8_16_32_
 # compilation, but this is not necessary.
 $sed -i 's!#include.*Hacl_Krmllib.h"!!g' "${all_files[@]}"
 
-# This header is useful for *other* algorithms that refer to SHA2, e.g. Ed25519
-# which needs to compute a digest of a message before signing it. Here, since no
-# other algorithm builds upon SHA2, this internal header is useless (and is not
-# included in $dist_files).
-$sed -i 's!#include.*internal/Hacl_Streaming_SHA2.h"!#include "Hacl_Streaming_SHA2.h"!g' "${all_files[@]}"
-
 # Use globally unique names for the Hacl_ C APIs to avoid linkage conflicts.
-$sed -i -z 's!#include <string.h>\n!#include <string.h>\n#include "python_hacl_namespaces.h"\n!' Hacl_Streaming_SHA2.h
+$sed -i -z 's!#include <string.h>\n!#include <string.h>\n#include "python_hacl_namespaces.h"\n!' Hacl_Hash_SHA2.h
 
 # Finally, we remove a bunch of ifdefs from target.h that are, again, useful in
 # the general case, but not exercised by the subset of HACL* that we vendor.
diff --git a/Modules/sha2module.c b/Modules/sha2module.c
index 6c7c3917198d18..db3774c81e2d92 100644
--- a/Modules/sha2module.c
+++ b/Modules/sha2module.c
@@ -45,7 +45,7 @@ class SHA512Type "SHA512object *" "&PyType_Type"
 
 /* Our SHA2 implementations defer to the HACL* verified library. */
 
-#include "_hacl/Hacl_Streaming_SHA2.h"
+#include "_hacl/Hacl_Hash_SHA2.h"
 
 // TODO: Get rid of int digestsize in favor of Hacl state info?
 
diff --git a/PCbuild/pythoncore.vcxproj b/PCbuild/pythoncore.vcxproj
index 48cd4418f90fee..43716487f91bd5 100644
--- a/PCbuild/pythoncore.vcxproj
+++ b/PCbuild/pythoncore.vcxproj
@@ -378,7 +378,7 @@
     <ClCompile Include="..\Modules\_functoolsmodule.c" />
     <ClCompile Include="..\Modules\_hacl\Hacl_Hash_MD5.c" />
     <ClCompile Include="..\Modules\_hacl\Hacl_Hash_SHA1.c" />
-    <ClCompile Include="..\Modules\_hacl\Hacl_Streaming_SHA2.c" />
+    <ClCompile Include="..\Modules\_hacl\Hacl_Hash_SHA2.c" />
     <ClCompile Include="..\Modules\_hacl\Hacl_Hash_SHA3.c" />
     <ClCompile Include="..\Modules\_heapqmodule.c" />
     <ClCompile Include="..\Modules\_json.c" />
diff --git a/PCbuild/pythoncore.vcxproj.filters b/PCbuild/pythoncore.vcxproj.filters
index 5c8c1444e8100e..22eb70a0f2dde4 100644
--- a/PCbuild/pythoncore.vcxproj.filters
+++ b/PCbuild/pythoncore.vcxproj.filters
@@ -782,7 +782,7 @@
     <ClCompile Include="..\Modules\_hacl\Hacl_Hash_SHA1.c">
       <Filter>Modules</Filter>
     </ClCompile>
-    <ClCompile Include="..\Modules\_hacl\Hacl_Streaming_SHA2.c">
+    <ClCompile Include="..\Modules\_hacl\Hacl_Hash_SHA2.c">
       <Filter>Modules</Filter>
     </ClCompile>
     <ClCompile Include="..\Modules\_hacl\Hacl_Hash_SHA3.c">