From 160321e5304b962a162eb023472aa2bc8307ae15 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 24 May 2023 13:30:11 -0700 Subject: [PATCH] gh-99108: Refresh HACL* (#104808) Refresh HACL* from upstream to improve SHA2 performance and fix a 32-bit issue in SHA3. --- Makefile.pre.in | 14 +- ...3-05-24-09-29-08.gh-issue-99108.hwS2cr.rst | 2 + Modules/Setup | 2 +- Modules/Setup.stdlib.in | 2 +- Modules/_hacl/Hacl_Hash_MD5.c | 6 +- Modules/_hacl/Hacl_Hash_MD5.h | 2 +- Modules/_hacl/Hacl_Hash_SHA1.c | 6 +- Modules/_hacl/Hacl_Hash_SHA1.h | 2 +- ...Hacl_Streaming_SHA2.c => Hacl_Hash_SHA2.c} | 191 ++++++++++-------- ...Hacl_Streaming_SHA2.h => Hacl_Hash_SHA2.h} | 22 +- Modules/_hacl/Hacl_Hash_SHA3.c | 28 ++- Modules/_hacl/Hacl_Hash_SHA3.h | 12 +- Modules/_hacl/Hacl_Streaming_Types.h | 7 + .../{Hacl_SHA2_Generic.h => Hacl_Hash_SHA2.h} | 58 +++++- Modules/_hacl/refresh.sh | 16 +- Modules/sha2module.c | 2 +- PCbuild/pythoncore.vcxproj | 2 +- PCbuild/pythoncore.vcxproj.filters | 2 +- 18 files changed, 226 insertions(+), 150 deletions(-) create mode 100644 Misc/NEWS.d/next/Security/2023-05-24-09-29-08.gh-issue-99108.hwS2cr.rst rename Modules/_hacl/{Hacl_Streaming_SHA2.c => Hacl_Hash_SHA2.c} (87%) rename Modules/_hacl/{Hacl_Streaming_SHA2.h => Hacl_Hash_SHA2.h} (91%) rename Modules/_hacl/internal/{Hacl_SHA2_Generic.h => Hacl_Hash_SHA2.h} (83%) diff --git a/Makefile.pre.in b/Makefile.pre.in index 033fdf98f1f..c24e8aa8583 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 00000000000..312ba89454b --- /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 7d536f87018..e7c64f78473 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 81cf4d44d90..3e3d8c6a213 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 2c613066d9f..222ac824f01 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 015e3668751..13c19fd40f4 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 e155e338271..5ecb3c0b3a5 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 5e2ae8e7132..dc50aa6f6d3 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 69c3be8cdf7..08e3f7edbf4 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_SHA2_Generic.h" +#include "internal/Hacl_Hash_SHA2.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 b58df4c4d12..a0e731094df 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 58eb436881d..b3febdfeb2b 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 2a5cf4b1844..681b6af4a80 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 8a60b707bc4..15ef16ba607 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 6ac47f3cf7e..851f7dc60c9 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 d2ba05f30d8..c1b3e37f3af 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 \n!#include \n#include "python_hacl_namespaces.h"\n!' Hacl_Streaming_SHA2.h +$sed -i -z 's!#include \n!#include \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 6c7c3917198..db3774c81e2 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 48cd4418f90..43716487f91 100644 --- a/PCbuild/pythoncore.vcxproj +++ b/PCbuild/pythoncore.vcxproj @@ -378,7 +378,7 @@ - + diff --git a/PCbuild/pythoncore.vcxproj.filters b/PCbuild/pythoncore.vcxproj.filters index 5c8c1444e81..22eb70a0f2d 100644 --- a/PCbuild/pythoncore.vcxproj.filters +++ b/PCbuild/pythoncore.vcxproj.filters @@ -782,7 +782,7 @@ Modules - + Modules