[Python-checkins] gh-99108: Refresh HACL* (#104808)
gpshead
webhook-mailer at python.org
Wed May 24 16:30:27 EDT 2023
https://github.com/python/cpython/commit/160321e5304b962a162eb023472aa2bc8307ae15
commit: 160321e5304b962a162eb023472aa2bc8307ae15
branch: main
author: Jonathan Protzenko <protz at microsoft.com>
committer: gpshead <greg at krypto.org>
date: 2023-05-24T13:30:11-07:00
summary:
gh-99108: Refresh HACL* (#104808)
Refresh HACL* from upstream to improve SHA2 performance and fix a 32-bit issue in SHA3.
files:
A Misc/NEWS.d/next/Security/2023-05-24-09-29-08.gh-issue-99108.hwS2cr.rst
A Modules/_hacl/Hacl_Hash_SHA2.c
A Modules/_hacl/Hacl_Hash_SHA2.h
A Modules/_hacl/internal/Hacl_Hash_SHA2.h
D Modules/_hacl/Hacl_Streaming_SHA2.c
D Modules/_hacl/Hacl_Streaming_SHA2.h
D Modules/_hacl/internal/Hacl_SHA2_Generic.h
M Makefile.pre.in
M Modules/Setup
M Modules/Setup.stdlib.in
M Modules/_hacl/Hacl_Hash_MD5.c
M Modules/_hacl/Hacl_Hash_MD5.h
M Modules/_hacl/Hacl_Hash_SHA1.c
M Modules/_hacl/Hacl_Hash_SHA1.h
M Modules/_hacl/Hacl_Hash_SHA3.c
M Modules/_hacl/Hacl_Hash_SHA3.h
M Modules/_hacl/Hacl_Streaming_Types.h
M Modules/_hacl/refresh.sh
M Modules/sha2module.c
M PCbuild/pythoncore.vcxproj
M PCbuild/pythoncore.vcxproj.filters
diff --git a/Makefile.pre.in b/Makefile.pre.in
index 033fdf98f1f7..c24e8aa85831 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 000000000000..312ba89454b5
--- /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 7d536f87018a..e7c64f784739 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 81cf4d44d902..3e3d8c6a2130 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 at _md5 md5module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_MD5.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
@MODULE__SHA1_TRUE at _sha1 sha1module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_SHA1.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
- at MODULE__SHA2_TRUE@_sha2 sha2module.c -I$(srcdir)/Modules/_hacl/include Modules/_hacl/libHacl_Streaming_SHA2.a
+ at MODULE__SHA2_TRUE@_sha2 sha2module.c -I$(srcdir)/Modules/_hacl/include Modules/_hacl/libHacl_Hash_SHA2.a
@MODULE__SHA3_TRUE at _sha3 sha3module.c -I$(srcdir)/Modules/_hacl/include _hacl/Hacl_Hash_SHA3.c -D_BSD_SOURCE -D_DEFAULT_SOURCE
@MODULE__BLAKE2_TRUE at _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 2c613066d9f6..222ac824f019 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 015e3668751b..13c19fd40f4d 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 e155e338271c..5ecb3c0b3a56 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 5e2ae8e71329..dc50aa6f6d39 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 69c3be8cdf7f..08e3f7edbf4e 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 b58df4c4d121..a0e731094dfa 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 58eb436881d4..b3febdfeb2b2 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 2a5cf4b1844b..681b6af4a80e 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 8a60b707bc49..15ef16ba6075 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 6ac47f3cf7ed..851f7dc60c94 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 d2ba05f30d86..c1b3e37f3afb 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 6c7c3917198d..db3774c81e2d 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 48cd4418f90f..43716487f91b 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 5c8c1444e810..22eb70a0f2dd 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">
More information about the Python-checkins
mailing list