From 418466250b0a2f608045627aef5470d9a8def640 Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 16 Oct 2023 16:41:23 -0700 Subject: [PATCH 01/18] zeta: updating format rule and removing linter rule. --- zeta/.clang-format | 2 +- zeta/Makefile | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/zeta/.clang-format b/zeta/.clang-format index 8c826f32067e9..72d680c57861b 100644 --- a/zeta/.clang-format +++ b/zeta/.clang-format @@ -675,7 +675,7 @@ SpaceBeforeInheritanceColon: true SpaceBeforeParens: ControlStatementsExceptForEachMacros SpaceBeforeRangeBasedForLoopColon: true SpaceInEmptyParentheses: false -SpacesBeforeTrailingComments: 1 +SpacesBeforeTrailingComments: 2 SpacesInAngles: false SpacesInContainerLiterals: false SpacesInCStyleCastParentheses: false diff --git a/zeta/Makefile b/zeta/Makefile index c16b40572124c..4e0d502ee7806 100644 --- a/zeta/Makefile +++ b/zeta/Makefile @@ -28,4 +28,4 @@ format: check-env lint: check-env # Tested with cpplint v1.5.5 - cpplint --filter=-whitespace/braces,-readability/casting ${ALL_FILES} + cpplint --filter=-whitespace/braces,-readability/casting,-build/include_subdir ${ALL_FILES} From 7ac92cec892e95ef3d2cd9325ce856946915fdbc Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Thu, 5 Oct 2023 14:54:13 +0200 Subject: [PATCH 02/18] HACL SHA2 code --- crypto/hacl_hash.h | 392 +++++++++++++++ crypto/hacl_lib.h | 231 +++++++++ crypto/sha2-hacl-generated.c | 939 +++++++++++++++++++++++++++++++++++ crypto/sha2-hacl.c | 187 +++++++ 4 files changed, 1749 insertions(+) create mode 100644 crypto/hacl_hash.h create mode 100644 crypto/hacl_lib.h create mode 100644 crypto/sha2-hacl-generated.c create mode 100644 crypto/sha2-hacl.c diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h new file mode 100644 index 0000000000000..38901e36dbe8c --- /dev/null +++ b/crypto/hacl_hash.h @@ -0,0 +1,392 @@ +/* + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * Copyright (c) 2023 Cryspen + */ + +#ifndef CRYPTO_HACL_HASH_H_ +#define CRYPTO_HACL_HASH_H_ + +#include "./hacl_lib.h" + +#define Spec_Hash_Definitions_SHA2_224 0 +#define Spec_Hash_Definitions_SHA2_256 1 +#define Spec_Hash_Definitions_SHA2_384 2 +#define Spec_Hash_Definitions_SHA2_512 3 +#define Spec_Hash_Definitions_SHA1 4 +#define Spec_Hash_Definitions_MD5 5 +#define Spec_Hash_Definitions_Blake2S 6 +#define Spec_Hash_Definitions_Blake2B 7 +#define Spec_Hash_Definitions_SHA3_256 8 +#define Spec_Hash_Definitions_SHA3_224 9 +#define Spec_Hash_Definitions_SHA3_384 10 +#define Spec_Hash_Definitions_SHA3_512 11 +#define Spec_Hash_Definitions_Shake128 12 +#define Spec_Hash_Definitions_Shake256 13 + +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 + +uint32_t Hacl_Hash_Definitions_word_len(Spec_Hash_Definitions_hash_alg a); + +uint32_t Hacl_Hash_Definitions_block_len(Spec_Hash_Definitions_hash_alg a); + +uint32_t Hacl_Hash_Definitions_hash_word_len(Spec_Hash_Definitions_hash_alg a); + +uint32_t Hacl_Hash_Definitions_hash_len(Spec_Hash_Definitions_hash_alg a); + +typedef uint8_t *Hacl_Hash_Definitions_hash_t; + +typedef uint8_t Hacl_Streaming_Types_error_code; + +typedef struct Hacl_Streaming_MD_state_32_s { + uint32_t *block_state; + uint8_t *buf; + uint64_t total_len; +} Hacl_Streaming_MD_state_32; + +typedef struct Hacl_Streaming_MD_state_64_s { + uint64_t *block_state; + uint8_t *buf; + uint64_t total_len; +} Hacl_Streaming_MD_state_64; + +static const uint32_t Hacl_Impl_SHA2_Generic_h224[8U] = { + (uint32_t)0xc1059ed8U, (uint32_t)0x367cd507U, (uint32_t)0x3070dd17U, + (uint32_t)0xf70e5939U, (uint32_t)0xffc00b31U, (uint32_t)0x68581511U, + (uint32_t)0x64f98fa7U, (uint32_t)0xbefa4fa4U +}; + +static const uint32_t Hacl_Impl_SHA2_Generic_h256[8U] = { + (uint32_t)0x6a09e667U, (uint32_t)0xbb67ae85U, (uint32_t)0x3c6ef372U, + (uint32_t)0xa54ff53aU, (uint32_t)0x510e527fU, (uint32_t)0x9b05688cU, + (uint32_t)0x1f83d9abU, (uint32_t)0x5be0cd19U +}; + +static const uint64_t Hacl_Impl_SHA2_Generic_h384[8U] = { + (uint64_t)0xcbbb9d5dc1059ed8U, (uint64_t)0x629a292a367cd507U, + (uint64_t)0x9159015a3070dd17U, (uint64_t)0x152fecd8f70e5939U, + (uint64_t)0x67332667ffc00b31U, (uint64_t)0x8eb44a8768581511U, + (uint64_t)0xdb0c2e0d64f98fa7U, (uint64_t)0x47b5481dbefa4fa4U +}; + +static const uint64_t Hacl_Impl_SHA2_Generic_h512[8U] = { + (uint64_t)0x6a09e667f3bcc908U, (uint64_t)0xbb67ae8584caa73bU, + (uint64_t)0x3c6ef372fe94f82bU, (uint64_t)0xa54ff53a5f1d36f1U, + (uint64_t)0x510e527fade682d1U, (uint64_t)0x9b05688c2b3e6c1fU, + (uint64_t)0x1f83d9abfb41bd6bU, (uint64_t)0x5be0cd19137e2179U +}; + +static const uint32_t Hacl_Impl_SHA2_Generic_k224_256[64U] = { + (uint32_t)0x428a2f98U, (uint32_t)0x71374491U, (uint32_t)0xb5c0fbcfU, + (uint32_t)0xe9b5dba5U, (uint32_t)0x3956c25bU, (uint32_t)0x59f111f1U, + (uint32_t)0x923f82a4U, (uint32_t)0xab1c5ed5U, (uint32_t)0xd807aa98U, + (uint32_t)0x12835b01U, (uint32_t)0x243185beU, (uint32_t)0x550c7dc3U, + (uint32_t)0x72be5d74U, (uint32_t)0x80deb1feU, (uint32_t)0x9bdc06a7U, + (uint32_t)0xc19bf174U, (uint32_t)0xe49b69c1U, (uint32_t)0xefbe4786U, + (uint32_t)0x0fc19dc6U, (uint32_t)0x240ca1ccU, (uint32_t)0x2de92c6fU, + (uint32_t)0x4a7484aaU, (uint32_t)0x5cb0a9dcU, (uint32_t)0x76f988daU, + (uint32_t)0x983e5152U, (uint32_t)0xa831c66dU, (uint32_t)0xb00327c8U, + (uint32_t)0xbf597fc7U, (uint32_t)0xc6e00bf3U, (uint32_t)0xd5a79147U, + (uint32_t)0x06ca6351U, (uint32_t)0x14292967U, (uint32_t)0x27b70a85U, + (uint32_t)0x2e1b2138U, (uint32_t)0x4d2c6dfcU, (uint32_t)0x53380d13U, + (uint32_t)0x650a7354U, (uint32_t)0x766a0abbU, (uint32_t)0x81c2c92eU, + (uint32_t)0x92722c85U, (uint32_t)0xa2bfe8a1U, (uint32_t)0xa81a664bU, + (uint32_t)0xc24b8b70U, (uint32_t)0xc76c51a3U, (uint32_t)0xd192e819U, + (uint32_t)0xd6990624U, (uint32_t)0xf40e3585U, (uint32_t)0x106aa070U, + (uint32_t)0x19a4c116U, (uint32_t)0x1e376c08U, (uint32_t)0x2748774cU, + (uint32_t)0x34b0bcb5U, (uint32_t)0x391c0cb3U, (uint32_t)0x4ed8aa4aU, + (uint32_t)0x5b9cca4fU, (uint32_t)0x682e6ff3U, (uint32_t)0x748f82eeU, + (uint32_t)0x78a5636fU, (uint32_t)0x84c87814U, (uint32_t)0x8cc70208U, + (uint32_t)0x90befffaU, (uint32_t)0xa4506cebU, (uint32_t)0xbef9a3f7U, + (uint32_t)0xc67178f2U +}; + +static const uint64_t Hacl_Impl_SHA2_Generic_k384_512[80U] = { + (uint64_t)0x428a2f98d728ae22U, (uint64_t)0x7137449123ef65cdU, + (uint64_t)0xb5c0fbcfec4d3b2fU, (uint64_t)0xe9b5dba58189dbbcU, + (uint64_t)0x3956c25bf348b538U, (uint64_t)0x59f111f1b605d019U, + (uint64_t)0x923f82a4af194f9bU, (uint64_t)0xab1c5ed5da6d8118U, + (uint64_t)0xd807aa98a3030242U, (uint64_t)0x12835b0145706fbeU, + (uint64_t)0x243185be4ee4b28cU, (uint64_t)0x550c7dc3d5ffb4e2U, + (uint64_t)0x72be5d74f27b896fU, (uint64_t)0x80deb1fe3b1696b1U, + (uint64_t)0x9bdc06a725c71235U, (uint64_t)0xc19bf174cf692694U, + (uint64_t)0xe49b69c19ef14ad2U, (uint64_t)0xefbe4786384f25e3U, + (uint64_t)0x0fc19dc68b8cd5b5U, (uint64_t)0x240ca1cc77ac9c65U, + (uint64_t)0x2de92c6f592b0275U, (uint64_t)0x4a7484aa6ea6e483U, + (uint64_t)0x5cb0a9dcbd41fbd4U, (uint64_t)0x76f988da831153b5U, + (uint64_t)0x983e5152ee66dfabU, (uint64_t)0xa831c66d2db43210U, + (uint64_t)0xb00327c898fb213fU, (uint64_t)0xbf597fc7beef0ee4U, + (uint64_t)0xc6e00bf33da88fc2U, (uint64_t)0xd5a79147930aa725U, + (uint64_t)0x06ca6351e003826fU, (uint64_t)0x142929670a0e6e70U, + (uint64_t)0x27b70a8546d22ffcU, (uint64_t)0x2e1b21385c26c926U, + (uint64_t)0x4d2c6dfc5ac42aedU, (uint64_t)0x53380d139d95b3dfU, + (uint64_t)0x650a73548baf63deU, (uint64_t)0x766a0abb3c77b2a8U, + (uint64_t)0x81c2c92e47edaee6U, (uint64_t)0x92722c851482353bU, + (uint64_t)0xa2bfe8a14cf10364U, (uint64_t)0xa81a664bbc423001U, + (uint64_t)0xc24b8b70d0f89791U, (uint64_t)0xc76c51a30654be30U, + (uint64_t)0xd192e819d6ef5218U, (uint64_t)0xd69906245565a910U, + (uint64_t)0xf40e35855771202aU, (uint64_t)0x106aa07032bbd1b8U, + (uint64_t)0x19a4c116b8d2d0c8U, (uint64_t)0x1e376c085141ab53U, + (uint64_t)0x2748774cdf8eeb99U, (uint64_t)0x34b0bcb5e19b48a8U, + (uint64_t)0x391c0cb3c5c95a63U, (uint64_t)0x4ed8aa4ae3418acbU, + (uint64_t)0x5b9cca4f7763e373U, (uint64_t)0x682e6ff3d6b2b8a3U, + (uint64_t)0x748f82ee5defb2fcU, (uint64_t)0x78a5636f43172f60U, + (uint64_t)0x84c87814a1f0ab72U, (uint64_t)0x8cc702081a6439ecU, + (uint64_t)0x90befffa23631e28U, (uint64_t)0xa4506cebde82bde9U, + (uint64_t)0xbef9a3f7b2c67915U, (uint64_t)0xc67178f2e372532bU, + (uint64_t)0xca273eceea26619cU, (uint64_t)0xd186b8c721c0c207U, + (uint64_t)0xeada7dd6cde0eb1eU, (uint64_t)0xf57d4f7fee6ed178U, + (uint64_t)0x06f067aa72176fbaU, (uint64_t)0x0a637dc5a2c898a6U, + (uint64_t)0x113f9804bef90daeU, (uint64_t)0x1b710b35131c471bU, + (uint64_t)0x28db77f523047d84U, (uint64_t)0x32caab7b40c72493U, + (uint64_t)0x3c9ebe0a15c9bebcU, (uint64_t)0x431d67c49c100d4cU, + (uint64_t)0x4cc5d4becb3e42b6U, (uint64_t)0x597f299cfc657e2aU, + (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); + +typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_224; + +typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_256; + +typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_384; + +typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_512; + +/** +Allocate initial state for the SHA2_256 hash. The state is to be freed by +calling `free_256`. +*/ +Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void); + +/** +Copies the state passed as argument into a newly allocated state (deep copy). +The state is to be freed by calling `free_256`. Cloning the state this way is +useful, for instance, if your control-flow diverges and you need to feed +more (different) data into the hash in each branch. +*/ +Hacl_Streaming_MD_state_32 * +Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0); + +/** +Reset an existing state to the initial hash state with empty data. +*/ +void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s); + +/** +Feed an arbitrary amount of data into the hash. This function returns 0 for +success, or 1 if the combined length of all of the data passed to `update_256` +(since the last call to `init_256`) exceeds 2^61-1 bytes. + +This function is identical to the update function for SHA2_224. +*/ +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_256(Hacl_Streaming_MD_state_32 *p, uint8_t *input, + uint32_t input_len); + +/** +Write the resulting hash into `dst`, an array of 32 bytes. The state remains +valid after a call to `finish_256`, meaning the user may feed more data into +the hash via `update_256`. (The finish_256 function operates on an internal copy +of the state and therefore does not invalidate the client-held state `p`.) +*/ +void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, + uint8_t *dst); + +/** +Free a state allocated with `create_in_256`. + +This function is identical to the free function for SHA2_224. +*/ +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_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); + +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_224(Hacl_Streaming_MD_state_32 *p, uint8_t *input, + uint32_t input_len); + +/** +Write the resulting hash into `dst`, an array of 28 bytes. The state remains +valid after a call to `finish_224`, meaning the user may feed more data into +the hash via `update_224`. +*/ +void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, + uint8_t *dst); + +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_hash_224(uint8_t *input, uint32_t input_len, + uint8_t *dst); + +Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void); + +/** +Copies the state passed as argument into a newly allocated state (deep copy). +The state is to be freed by calling `free_512`. Cloning the state this way is +useful, for instance, if your control-flow diverges and you need to feed +more (different) data into the hash in each branch. +*/ +Hacl_Streaming_MD_state_64 * +Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0); + +void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s); + +/** +Feed an arbitrary amount of data into the hash. This function returns 0 for +success, or 1 if the combined length of all of the data passed to `update_512` +(since the last call to `init_512`) exceeds 2^125-1 bytes. + +This function is identical to the update function for SHA2_384. +*/ +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_512(Hacl_Streaming_MD_state_64 *p, uint8_t *input, + uint32_t input_len); + +/** +Write the resulting hash into `dst`, an array of 64 bytes. The state remains +valid after a call to `finish_512`, meaning the user may feed more data into +the hash via `update_512`. (The finish_512 function operates on an internal copy +of the state and therefore does not invalidate the client-held state `p`.) +*/ +void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, + uint8_t *dst); + +/** +Free a state allocated with `create_in_512`. + +This function is identical to the free function for SHA2_384. +*/ +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_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); + +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_384(Hacl_Streaming_MD_state_64 *p, uint8_t *input, + uint32_t input_len); + +/** +Write the resulting hash into `dst`, an array of 48 bytes. The state remains +valid after a call to `finish_384`, meaning the user may feed more data into +the hash via `update_384`. +*/ +void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, + uint8_t *dst); + +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_hash_384(uint8_t *input, uint32_t input_len, + uint8_t *dst); + +typedef struct Hacl_Impl_SHA2_Types_uint8_2p_s { + uint8_t *fst; + uint8_t *snd; +} Hacl_Impl_SHA2_Types_uint8_2p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_3p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_2p snd; +} Hacl_Impl_SHA2_Types_uint8_3p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_4p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_3p snd; +} Hacl_Impl_SHA2_Types_uint8_4p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_5p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_4p snd; +} Hacl_Impl_SHA2_Types_uint8_5p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_6p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_5p snd; +} Hacl_Impl_SHA2_Types_uint8_6p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_7p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_6p snd; +} Hacl_Impl_SHA2_Types_uint8_7p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_8p_s { + uint8_t *fst; + Hacl_Impl_SHA2_Types_uint8_7p snd; +} Hacl_Impl_SHA2_Types_uint8_8p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_2x4p_s { + Hacl_Impl_SHA2_Types_uint8_4p fst; + Hacl_Impl_SHA2_Types_uint8_4p snd; +} Hacl_Impl_SHA2_Types_uint8_2x4p; + +typedef struct Hacl_Impl_SHA2_Types_uint8_2x8p_s { + Hacl_Impl_SHA2_Types_uint8_8p fst; + Hacl_Impl_SHA2_Types_uint8_8p snd; +} Hacl_Impl_SHA2_Types_uint8_2x8p; + +#define __Hacl_Hash_H_DEFINED +#endif // CRYPTO_HACL_HASH_H_ diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h new file mode 100644 index 0000000000000..44c8038ed124d --- /dev/null +++ b/crypto/hacl_lib.h @@ -0,0 +1,231 @@ +/* + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * Copyright (c) 2023 Cryspen + */ + +#ifndef CRYPTO_HACL_LIB_H_ +#define CRYPTO_HACL_LIB_H_ + +#include +#include +#include +#include +#include + +typedef u128 FStar_UInt128_uint128; + +static inline u128 FStar_UInt128_shift_left(u128 x, u32 y) +{ + return (x << y); +} + +static inline u128 FStar_UInt128_add(u128 x, u128 y) +{ + return (x + y); +} + +static inline u128 FStar_UInt128_uint64_to_uint128(u64 x) +{ + return ((u128)x); +} + +/* Loads and stores. These avoid undefined behavior due to unaligned memory + * accesses, via memcpy. */ + +#define load32_be(b) (get_unaligned_be32(b)) +#define store32_be(b, i) put_unaligned_be32(i, b); +#define load64_be(b) (get_unaligned_be64(b)) +#define store64_be(b, i) put_unaligned_be64(i, b); + +static inline void store128_be(u8 *buf, u128 x) +{ + store64_be(buf, (u64)(x >> 64)); + store64_be(buf + 8, (u64)(x)); +} + +/* Macros for prettier unrolling of loops */ +#define KRML_LOOP1(i, n, x) \ + { \ + x i += n; \ + } + +#define KRML_LOOP2(i, n, x) \ + KRML_LOOP1(i, n, x) \ + KRML_LOOP1(i, n, x) + +#define KRML_LOOP3(i, n, x) \ + KRML_LOOP2(i, n, x) \ + KRML_LOOP1(i, n, x) + +#define KRML_LOOP4(i, n, x) \ + KRML_LOOP2(i, n, x) \ + KRML_LOOP2(i, n, x) + +#define KRML_LOOP5(i, n, x) \ + KRML_LOOP4(i, n, x) \ + KRML_LOOP1(i, n, x) + +#define KRML_LOOP6(i, n, x) \ + KRML_LOOP4(i, n, x) \ + KRML_LOOP2(i, n, x) + +#define KRML_LOOP7(i, n, x) \ + KRML_LOOP4(i, n, x) \ + KRML_LOOP3(i, n, x) + +#define KRML_LOOP8(i, n, x) \ + KRML_LOOP4(i, n, x) \ + KRML_LOOP4(i, n, x) + +#define KRML_LOOP9(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP1(i, n, x) + +#define KRML_LOOP10(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP2(i, n, x) + +#define KRML_LOOP11(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP3(i, n, x) + +#define KRML_LOOP12(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP4(i, n, x) + +#define KRML_LOOP13(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP5(i, n, x) + +#define KRML_LOOP14(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP6(i, n, x) + +#define KRML_LOOP15(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP7(i, n, x) + +#define KRML_LOOP16(i, n, x) \ + KRML_LOOP8(i, n, x) \ + KRML_LOOP8(i, n, x) + +#define KRML_UNROLL_FOR(i, z, n, k, x) \ + do { \ + uint32_t i = z; \ + KRML_LOOP##n(i, k, x) \ + } while (0) + +#define KRML_ACTUAL_FOR(i, z, n, k, x) \ + do { \ + for (uint32_t i = z; i < n; i += k) { \ + x \ + } \ + } while (0) + +#define KRML_UNROLL_MAX 16 + +/* 1 is the number of loop iterations, i.e. (n - z)/k as evaluated by krml */ +#if 0 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR0(i, z, n, k, x) +#else +#define KRML_MAYBE_FOR0(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 1 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 1, k, x) +#else +#define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 2 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 2, k, x) +#else +#define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 3 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 3, k, x) +#else +#define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 4 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 4, k, x) +#else +#define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 5 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 5, k, x) +#else +#define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 6 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 6, k, x) +#else +#define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 7 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 7, k, x) +#else +#define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 8 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 8, k, x) +#else +#define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 9 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 9, k, x) +#else +#define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 10 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 10, k, x) +#else +#define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 11 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 11, k, x) +#else +#define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 12 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 12, k, x) +#else +#define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 13 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 13, k, x) +#else +#define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 14 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 14, k, x) +#else +#define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 15 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 15, k, x) +#else +#define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#if 16 <= KRML_UNROLL_MAX +#define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 16, k, x) +#else +#define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) +#endif + +#endif // CRYPTO_HACL_LIB_H_" diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c new file mode 100644 index 0000000000000..9a5e081915b74 --- /dev/null +++ b/crypto/sha2-hacl-generated.c @@ -0,0 +1,939 @@ +/* GPLv2 or MIT License + * + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * + */ + +#include "./hacl_hash.h" +#include "./hacl_lib.h" + +void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash) +{ + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint32_t *os = hash; + uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; + os[i] = x;); +} + +static inline void sha256_update_(uint8_t *b, uint32_t *hash) +{ + uint32_t hash_old[8U] = { 0U }; + uint32_t ws[16U] = { 0U }; + memcpy(hash_old, hash, (uint32_t)8U * sizeof(uint32_t)); + uint8_t *b10 = b; + uint32_t u = load32_be(b10); + ws[0U] = u; + uint32_t u0 = load32_be(b10 + (uint32_t)4U); + ws[1U] = u0; + uint32_t u1 = load32_be(b10 + (uint32_t)8U); + ws[2U] = u1; + uint32_t u2 = load32_be(b10 + (uint32_t)12U); + ws[3U] = u2; + uint32_t u3 = load32_be(b10 + (uint32_t)16U); + ws[4U] = u3; + uint32_t u4 = load32_be(b10 + (uint32_t)20U); + ws[5U] = u4; + uint32_t u5 = load32_be(b10 + (uint32_t)24U); + ws[6U] = u5; + uint32_t u6 = load32_be(b10 + (uint32_t)28U); + ws[7U] = u6; + uint32_t u7 = load32_be(b10 + (uint32_t)32U); + ws[8U] = u7; + uint32_t u8 = load32_be(b10 + (uint32_t)36U); + ws[9U] = u8; + uint32_t u9 = load32_be(b10 + (uint32_t)40U); + ws[10U] = u9; + uint32_t u10 = load32_be(b10 + (uint32_t)44U); + ws[11U] = u10; + uint32_t u11 = load32_be(b10 + (uint32_t)48U); + ws[12U] = u11; + uint32_t u12 = load32_be(b10 + (uint32_t)52U); + ws[13U] = u12; + uint32_t u13 = load32_be(b10 + (uint32_t)56U); + ws[14U] = u13; + uint32_t u14 = load32_be(b10 + (uint32_t)60U); + ws[15U] = u14; + KRML_MAYBE_FOR4( + i0, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + KRML_MAYBE_FOR16( + i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint32_t k_t = Hacl_Impl_SHA2_Generic_k224_256 + [(uint32_t)16U * i0 + i]; + uint32_t ws_t = ws[i]; uint32_t a0 = hash[0U]; + uint32_t b0 = hash[1U]; uint32_t c0 = hash[2U]; + uint32_t d0 = hash[3U]; uint32_t e0 = hash[4U]; + uint32_t f0 = hash[5U]; uint32_t g0 = hash[6U]; + uint32_t h02 = hash[7U]; uint32_t k_e_t = k_t; + uint32_t t1 = + h02 + + ((e0 << (uint32_t)26U | e0 >> (uint32_t)6U) ^ + ((e0 << (uint32_t)21U | e0 >> (uint32_t)11U) ^ + (e0 << (uint32_t)7U | e0 >> (uint32_t)25U))) + + ((e0 & f0) ^ (~e0 & g0)) + k_e_t + ws_t; + uint32_t t2 = + ((a0 << (uint32_t)30U | a0 >> (uint32_t)2U) ^ + ((a0 << (uint32_t)19U | a0 >> (uint32_t)13U) ^ + (a0 << (uint32_t)10U | a0 >> (uint32_t)22U))) + + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); + uint32_t a1 = t1 + t2; uint32_t b1 = a0; + uint32_t c1 = b0; uint32_t d1 = c0; + uint32_t e1 = d0 + t1; uint32_t f1 = e0; + uint32_t g1 = f0; uint32_t h12 = g0; hash[0U] = a1; + hash[1U] = b1; hash[2U] = c1; hash[3U] = d1; + hash[4U] = e1; hash[5U] = f1; hash[6U] = g1; + hash[7U] = h12;); + if (i0 < (uint32_t)3U) { + KRML_MAYBE_FOR16( + i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint32_t t16 = ws[i]; + uint32_t t15 = + ws[(i + (uint32_t)1U) % (uint32_t)16U]; + uint32_t t7 = + ws[(i + (uint32_t)9U) % (uint32_t)16U]; + uint32_t t2 = + ws[(i + (uint32_t)14U) % (uint32_t)16U]; + uint32_t s1 = (t2 << (uint32_t)15U | + t2 >> (uint32_t)17U) ^ + ((t2 << (uint32_t)13U | + t2 >> (uint32_t)19U) ^ + t2 >> (uint32_t)10U); + uint32_t s0 = (t15 << (uint32_t)25U | + t15 >> (uint32_t)7U) ^ + ((t15 << (uint32_t)14U | + t15 >> (uint32_t)18U) ^ + t15 >> (uint32_t)3U); + ws[i] = s1 + t7 + s0 + t16;); + }); + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint32_t *os = hash; + uint32_t x = hash[i] + hash_old[i]; os[i] = x;); +} + +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_update_(mb, st); + } +} + +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) { + blocks = (uint32_t)1U; + } else { + blocks = (uint32_t)2U; + } + uint32_t fin = blocks * (uint32_t)64U; + uint8_t last[128U] = { 0U }; + uint8_t totlen_buf[8U] = { 0U }; + uint64_t total_len_bits = totlen << (uint32_t)3U; + store64_be(totlen_buf, total_len_bits); + uint8_t *b0 = b; + memcpy(last, b0, len * sizeof(uint8_t)); + last[len] = (uint8_t)0x80U; + memcpy(last + fin - (uint32_t)8U, totlen_buf, + (uint32_t)8U * sizeof(uint8_t)); + uint8_t *last00 = last; + uint8_t *last10 = last + (uint32_t)64U; + uint8_t *l0 = last00; + uint8_t *l1 = last10; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + uint8_t *last0 = lb0; + uint8_t *last1 = lb1; + sha256_update_(last0, hash); + if (blocks > (uint32_t)1U) { + sha256_update_(last1, hash); + return; + } +} + +void Hacl_SHA2_Scalar32_sha256_finish(uint32_t *st, uint8_t *h) +{ + uint8_t hbuf[32U] = { 0U }; + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + store32_be(hbuf + i * (uint32_t)4U, st[i]);); + memcpy(h, hbuf, (uint32_t)32U * sizeof(uint8_t)); +} + +void Hacl_SHA2_Scalar32_sha224_init(uint32_t *hash) +{ + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint32_t *os = hash; + uint32_t x = Hacl_Impl_SHA2_Generic_h224[i]; + os[i] = x;); +} + +static inline void sha224_update_nblocks(uint32_t len, uint8_t *b, uint32_t *st) +{ + Hacl_SHA2_Scalar32_sha256_update_nblocks(len, b, st); +} + +void Hacl_SHA2_Scalar32_sha224_update_last(uint64_t totlen, uint32_t len, + uint8_t *b, uint32_t *st) +{ + Hacl_SHA2_Scalar32_sha256_update_last(totlen, len, b, st); +} + +void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h) +{ + uint8_t hbuf[32U] = { 0U }; + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + store32_be(hbuf + i * (uint32_t)4U, st[i]);); + memcpy(h, hbuf, (uint32_t)28U * sizeof(uint8_t)); +} + +/** +Reset an existing state to the initial hash state with empty data. +*/ +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; + 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 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 Hacl_Streaming_Types_MaximumLengthExceeded; + } + uint32_t sz; + if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len > (uint64_t)0U) { + sz = (uint32_t)64U; + } else { + sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); + } + if (len <= (uint32_t)64U - sz) { + Hacl_Streaming_MD_state_32 s1 = *p; + uint32_t *block_state1 = s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + uint8_t *buf2 = buf + sz1; + memcpy(buf2, data, len * sizeof(uint8_t)); + uint64_t total_len2 = total_len1 + (uint64_t)len; + *p = ((Hacl_Streaming_MD_state_32){ .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); + } else if (sz == (uint32_t)0U) { + Hacl_Streaming_MD_state_32 s1 = *p; + uint32_t *block_state1 = s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + if (!(sz1 == (uint32_t)0U)) { + 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) { + ite = (uint32_t)64U; + } else { + ite = (uint32_t)((uint64_t)len % + (uint64_t)(uint32_t)64U); + } + uint32_t n_blocks = (len - ite) / (uint32_t)64U; + uint32_t data1_len = n_blocks * (uint32_t)64U; + uint32_t data2_len = len - data1_len; + uint8_t *data1 = data; + uint8_t *data2 = data + data1_len; + 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 = ((Hacl_Streaming_MD_state_32){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)len }); + } else { + uint32_t diff = (uint32_t)64U - sz; + uint8_t *data1 = data; + uint8_t *data2 = data + diff; + Hacl_Streaming_MD_state_32 s1 = *p; + uint32_t *block_state10 = s1.block_state; + uint8_t *buf0 = s1.buf; + uint64_t total_len10 = s1.total_len; + uint32_t sz10; + if (total_len10 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len10 > (uint64_t)0U) { + sz10 = (uint32_t)64U; + } else { + sz10 = (uint32_t)(total_len10 % + (uint64_t)(uint32_t)64U); + } + uint8_t *buf2 = buf0 + sz10; + memcpy(buf2, data1, diff * sizeof(uint8_t)); + uint64_t total_len2 = total_len10 + (uint64_t)diff; + *p = ((Hacl_Streaming_MD_state_32){ .block_state = + block_state10, + .buf = buf0, + .total_len = total_len2 }); + Hacl_Streaming_MD_state_32 s10 = *p; + uint32_t *block_state1 = s10.block_state; + uint8_t *buf = s10.buf; + uint64_t total_len1 = s10.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + if (!(sz1 == (uint32_t)0U)) { + Hacl_SHA2_Scalar32_sha256_update_nblocks( + (uint32_t)64U, buf, block_state1); + } + uint32_t ite; + if ((uint64_t)(len - diff) % (uint64_t)(uint32_t)64U == + (uint64_t)0U && + (uint64_t)(len - diff) > (uint64_t)0U) { + ite = (uint32_t)64U; + } else { + ite = (uint32_t)((uint64_t)(len - diff) % + (uint64_t)(uint32_t)64U); + } + uint32_t n_blocks = (len - diff - ite) / (uint32_t)64U; + uint32_t data1_len = n_blocks * (uint32_t)64U; + uint32_t data2_len = len - diff - data1_len; + uint8_t *data11 = data2; + uint8_t *data21 = data2 + data1_len; + 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 = ((Hacl_Streaming_MD_state_32){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)(len - diff) }); + } + return Hacl_Streaming_Types_Success; +} + +/** +Feed an arbitrary amount of data into the hash. This function returns 0 for +success, or 1 if the combined length of all of the data passed to `update_256` +(since the last call to `init_256`) exceeds 2^61-1 bytes. + +This function is identical to the update function for SHA2_224. +*/ +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_256(Hacl_Streaming_MD_state_32 *p, uint8_t *input, + uint32_t input_len) +{ + return update_224_256(p, input, input_len); +} + +/** +Write the resulting hash into `dst`, an array of 32 bytes. The state remains +valid after a call to `finish_256`, meaning the user may feed more data into +the hash via `update_256`. (The finish_256 function operates on an internal copy +of the state and therefore does not invalidate the client-held state `p`.) +*/ +void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) +{ + Hacl_Streaming_MD_state_32 scrut = *p; + uint32_t *block_state = scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)64U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); + } + uint8_t *buf_1 = buf_; + uint32_t tmp_block_state[8U] = { 0U }; + memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof(uint32_t)); + uint32_t ite; + if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)64U; + } else { + ite = r % (uint32_t)64U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + Hacl_SHA2_Scalar32_sha256_update_nblocks((uint32_t)0U, buf_multi, + tmp_block_state); + uint64_t prev_len_last = total_len - (uint64_t)r; + 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); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. +*/ +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 }; + Hacl_SHA2_Scalar32_sha256_init(st); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + 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; + Hacl_SHA2_Scalar32_sha256_update_last(len_, rem, lb, st); + Hacl_SHA2_Scalar32_sha256_finish(st, rb); +} + +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; + 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; +} + +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_224(Hacl_Streaming_MD_state_32 *p, uint8_t *input, + uint32_t input_len) +{ + return update_224_256(p, input, input_len); +} + +/** +Write the resulting hash into `dst`, an array of 28 bytes. The state remains +valid after a call to `finish_224`, meaning the user may feed more data into +the hash via `update_224`. +*/ +void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) +{ + Hacl_Streaming_MD_state_32 scrut = *p; + uint32_t *block_state = scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)64U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); + } + uint8_t *buf_1 = buf_; + uint32_t tmp_block_state[8U] = { 0U }; + memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof(uint32_t)); + uint32_t ite; + if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)64U; + } else { + ite = r % (uint32_t)64U; + } + uint8_t *buf_last = buf_1 + r - ite; + 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; + 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); +} + +/** +Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. +*/ +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 }; + 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; + Hacl_SHA2_Scalar32_sha224_update_last(len_, rem, lb, st); + Hacl_SHA2_Scalar32_sha224_finish(st, rb); +} + +void Hacl_SHA2_Scalar32_sha512_init(uint64_t *hash) +{ + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint64_t *os = hash; + uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; + os[i] = x;); +} + +static inline void sha512_update(uint8_t *b, uint64_t *hash) +{ + uint64_t hash_old[8U] = { 0U }; + uint64_t ws[16U] = { 0U }; + memcpy(hash_old, hash, (uint32_t)8U * sizeof(uint64_t)); + uint8_t *b10 = b; + uint64_t u = load64_be(b10); + ws[0U] = u; + uint64_t u0 = load64_be(b10 + (uint32_t)8U); + ws[1U] = u0; + uint64_t u1 = load64_be(b10 + (uint32_t)16U); + ws[2U] = u1; + uint64_t u2 = load64_be(b10 + (uint32_t)24U); + ws[3U] = u2; + uint64_t u3 = load64_be(b10 + (uint32_t)32U); + ws[4U] = u3; + uint64_t u4 = load64_be(b10 + (uint32_t)40U); + ws[5U] = u4; + uint64_t u5 = load64_be(b10 + (uint32_t)48U); + ws[6U] = u5; + uint64_t u6 = load64_be(b10 + (uint32_t)56U); + ws[7U] = u6; + uint64_t u7 = load64_be(b10 + (uint32_t)64U); + ws[8U] = u7; + uint64_t u8 = load64_be(b10 + (uint32_t)72U); + ws[9U] = u8; + uint64_t u9 = load64_be(b10 + (uint32_t)80U); + ws[10U] = u9; + uint64_t u10 = load64_be(b10 + (uint32_t)88U); + ws[11U] = u10; + uint64_t u11 = load64_be(b10 + (uint32_t)96U); + ws[12U] = u11; + uint64_t u12 = load64_be(b10 + (uint32_t)104U); + ws[13U] = u12; + uint64_t u13 = load64_be(b10 + (uint32_t)112U); + ws[14U] = u13; + uint64_t u14 = load64_be(b10 + (uint32_t)120U); + ws[15U] = u14; + KRML_MAYBE_FOR5( + i0, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, + KRML_MAYBE_FOR16( + i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint64_t k_t = Hacl_Impl_SHA2_Generic_k384_512 + [(uint32_t)16U * i0 + i]; + uint64_t ws_t = ws[i]; uint64_t a0 = hash[0U]; + uint64_t b0 = hash[1U]; uint64_t c0 = hash[2U]; + uint64_t d0 = hash[3U]; uint64_t e0 = hash[4U]; + uint64_t f0 = hash[5U]; uint64_t g0 = hash[6U]; + uint64_t h02 = hash[7U]; uint64_t k_e_t = k_t; + uint64_t t1 = + h02 + + ((e0 << (uint32_t)50U | e0 >> (uint32_t)14U) ^ + ((e0 << (uint32_t)46U | e0 >> (uint32_t)18U) ^ + (e0 << (uint32_t)23U | e0 >> (uint32_t)41U))) + + ((e0 & f0) ^ (~e0 & g0)) + k_e_t + ws_t; + uint64_t t2 = + ((a0 << (uint32_t)36U | a0 >> (uint32_t)28U) ^ + ((a0 << (uint32_t)30U | a0 >> (uint32_t)34U) ^ + (a0 << (uint32_t)25U | a0 >> (uint32_t)39U))) + + ((a0 & b0) ^ ((a0 & c0) ^ (b0 & c0))); + uint64_t a1 = t1 + t2; uint64_t b1 = a0; + uint64_t c1 = b0; uint64_t d1 = c0; + uint64_t e1 = d0 + t1; uint64_t f1 = e0; + uint64_t g1 = f0; uint64_t h12 = g0; hash[0U] = a1; + hash[1U] = b1; hash[2U] = c1; hash[3U] = d1; + hash[4U] = e1; hash[5U] = f1; hash[6U] = g1; + hash[7U] = h12;); + if (i0 < (uint32_t)4U) { + KRML_MAYBE_FOR16( + i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint64_t t16 = ws[i]; + uint64_t t15 = + ws[(i + (uint32_t)1U) % (uint32_t)16U]; + uint64_t t7 = + ws[(i + (uint32_t)9U) % (uint32_t)16U]; + uint64_t t2 = + ws[(i + (uint32_t)14U) % (uint32_t)16U]; + uint64_t s1 = (t2 << (uint32_t)45U | + t2 >> (uint32_t)19U) ^ + ((t2 << (uint32_t)3U | + t2 >> (uint32_t)61U) ^ + t2 >> (uint32_t)6U); + uint64_t s0 = (t15 << (uint32_t)63U | + t15 >> (uint32_t)1U) ^ + ((t15 << (uint32_t)56U | + t15 >> (uint32_t)8U) ^ + t15 >> (uint32_t)7U); + ws[i] = s1 + t7 + s0 + t16;); + }); + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint64_t *os = hash; + uint64_t x = hash[i] + hash_old[i]; os[i] = x;); +} + +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++) { + uint8_t *b0 = b; + uint8_t *mb = b0 + i * (uint32_t)128U; + sha512_update(mb, st); + } +} + +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) { + blocks = (uint32_t)1U; + } else { + blocks = (uint32_t)2U; + } + uint32_t fin = blocks * (uint32_t)128U; + uint8_t last[256U] = { 0U }; + uint8_t totlen_buf[16U] = { 0U }; + FStar_UInt128_uint128 total_len_bits = + FStar_UInt128_shift_left(totlen, (uint32_t)3U); + store128_be(totlen_buf, total_len_bits); + uint8_t *b0 = b; + memcpy(last, b0, len * sizeof(uint8_t)); + last[len] = (uint8_t)0x80U; + memcpy(last + fin - (uint32_t)16U, totlen_buf, + (uint32_t)16U * sizeof(uint8_t)); + uint8_t *last00 = last; + uint8_t *last10 = last + (uint32_t)128U; + uint8_t *l0 = last00; + uint8_t *l1 = last10; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + uint8_t *last0 = lb0; + uint8_t *last1 = lb1; + sha512_update(last0, hash); + if (blocks > (uint32_t)1U) { + sha512_update(last1, hash); + return; + } +} + +void Hacl_SHA2_Scalar32_sha512_finish(uint64_t *st, uint8_t *h) +{ + uint8_t hbuf[64U] = { 0U }; + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + store64_be(hbuf + i * (uint32_t)8U, st[i]);); + memcpy(h, hbuf, (uint32_t)64U * sizeof(uint8_t)); +} + +void Hacl_SHA2_Scalar32_sha384_init(uint64_t *hash) +{ + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + uint64_t *os = hash; + uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; + os[i] = x;); +} + +void Hacl_SHA2_Scalar32_sha384_update_nblocks(uint32_t len, uint8_t *b, + uint64_t *st) +{ + Hacl_SHA2_Scalar32_sha512_update_nblocks(len, b, st); +} + +void Hacl_SHA2_Scalar32_sha384_update_last(FStar_UInt128_uint128 totlen, + uint32_t len, uint8_t *b, + uint64_t *st) +{ + Hacl_SHA2_Scalar32_sha512_update_last(totlen, len, b, st); +} + +void Hacl_SHA2_Scalar32_sha384_finish(uint64_t *st, uint8_t *h) +{ + uint8_t hbuf[64U] = { 0U }; + KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, + store64_be(hbuf + i * (uint32_t)8U, st[i]);); + memcpy(h, hbuf, (uint32_t)48U * sizeof(uint8_t)); +} + +void Hacl_Streaming_SHA2_init_512(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; + Hacl_SHA2_Scalar32_sha512_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; +} + +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 Hacl_Streaming_Types_MaximumLengthExceeded; + } + uint32_t sz; + if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len > (uint64_t)0U) { + sz = (uint32_t)128U; + } else { + sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); + } + if (len <= (uint32_t)128U - sz) { + Hacl_Streaming_MD_state_64 s1 = *p; + uint64_t *block_state1 = s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + uint8_t *buf2 = buf + sz1; + memcpy(buf2, data, len * sizeof(uint8_t)); + uint64_t total_len2 = total_len1 + (uint64_t)len; + *p = ((Hacl_Streaming_MD_state_64){ .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); + } else if (sz == (uint32_t)0U) { + Hacl_Streaming_MD_state_64 s1 = *p; + uint64_t *block_state1 = s1.block_state; + uint8_t *buf = s1.buf; + uint64_t total_len1 = s1.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + if (!(sz1 == (uint32_t)0U)) { + 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) { + ite = (uint32_t)128U; + } else { + ite = (uint32_t)((uint64_t)len % + (uint64_t)(uint32_t)128U); + } + uint32_t n_blocks = (len - ite) / (uint32_t)128U; + uint32_t data1_len = n_blocks * (uint32_t)128U; + uint32_t data2_len = len - data1_len; + uint8_t *data1 = data; + uint8_t *data2 = data + data1_len; + 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 = ((Hacl_Streaming_MD_state_64){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)len }); + } else { + uint32_t diff = (uint32_t)128U - sz; + uint8_t *data1 = data; + uint8_t *data2 = data + diff; + Hacl_Streaming_MD_state_64 s1 = *p; + uint64_t *block_state10 = s1.block_state; + uint8_t *buf0 = s1.buf; + uint64_t total_len10 = s1.total_len; + uint32_t sz10; + if (total_len10 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len10 > (uint64_t)0U) { + sz10 = (uint32_t)128U; + } else { + sz10 = (uint32_t)(total_len10 % + (uint64_t)(uint32_t)128U); + } + uint8_t *buf2 = buf0 + sz10; + memcpy(buf2, data1, diff * sizeof(uint8_t)); + uint64_t total_len2 = total_len10 + (uint64_t)diff; + *p = ((Hacl_Streaming_MD_state_64){ .block_state = + block_state10, + .buf = buf0, + .total_len = total_len2 }); + Hacl_Streaming_MD_state_64 s10 = *p; + uint64_t *block_state1 = s10.block_state; + uint8_t *buf = s10.buf; + uint64_t total_len1 = s10.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + if (!(sz1 == (uint32_t)0U)) { + Hacl_SHA2_Scalar32_sha512_update_nblocks( + (uint32_t)128U, buf, block_state1); + } + uint32_t ite; + if ((uint64_t)(len - diff) % (uint64_t)(uint32_t)128U == + (uint64_t)0U && + (uint64_t)(len - diff) > (uint64_t)0U) { + ite = (uint32_t)128U; + } else { + ite = (uint32_t)((uint64_t)(len - diff) % + (uint64_t)(uint32_t)128U); + } + uint32_t n_blocks = (len - diff - ite) / (uint32_t)128U; + uint32_t data1_len = n_blocks * (uint32_t)128U; + uint32_t data2_len = len - diff - data1_len; + uint8_t *data11 = data2; + uint8_t *data21 = data2 + data1_len; + 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 = ((Hacl_Streaming_MD_state_64){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)(len - diff) }); + } + return Hacl_Streaming_Types_Success; +} + +/** +Feed an arbitrary amount of data into the hash. This function returns 0 for +success, or 1 if the combined length of all of the data passed to `update_512` +(since the last call to `init_512`) exceeds 2^125-1 bytes. + +This function is identical to the update function for SHA2_384. +*/ +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_512(Hacl_Streaming_MD_state_64 *p, uint8_t *input, + uint32_t input_len) +{ + return update_384_512(p, input, input_len); +} + +/** +Write the resulting hash into `dst`, an array of 64 bytes. The state remains +valid after a call to `finish_512`, meaning the user may feed more data into +the hash via `update_512`. (The finish_512 function operates on an internal copy +of the state and therefore does not invalidate the client-held state `p`.) +*/ +void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) +{ + Hacl_Streaming_MD_state_64 scrut = *p; + uint64_t *block_state = scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)128U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); + } + uint8_t *buf_1 = buf_; + uint64_t tmp_block_state[8U] = { 0U }; + memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof(uint64_t)); + uint32_t ite; + if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)128U; + } else { + ite = r % (uint32_t)128U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + Hacl_SHA2_Scalar32_sha512_update_nblocks((uint32_t)0U, buf_multi, + tmp_block_state); + uint64_t prev_len_last = total_len - (uint64_t)r; + 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); + Hacl_SHA2_Scalar32_sha512_finish(tmp_block_state, dst); +} + +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; + 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; +} + +Hacl_Streaming_Types_error_code +Hacl_Streaming_SHA2_update_384(Hacl_Streaming_MD_state_64 *p, uint8_t *input, + uint32_t input_len) +{ + return update_384_512(p, input, input_len); +} + +/** +Write the resulting hash into `dst`, an array of 48 bytes. The state remains +valid after a call to `finish_384`, meaning the user may feed more data into +the hash via `update_384`. +*/ +void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) +{ + Hacl_Streaming_MD_state_64 scrut = *p; + uint64_t *block_state = scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)128U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); + } + uint8_t *buf_1 = buf_; + uint64_t tmp_block_state[8U] = { 0U }; + memcpy(tmp_block_state, block_state, (uint32_t)8U * sizeof(uint64_t)); + uint32_t ite; + if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)128U; + } else { + ite = r % (uint32_t)128U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + Hacl_SHA2_Scalar32_sha384_update_nblocks((uint32_t)0U, buf_multi, + tmp_block_state); + uint64_t prev_len_last = total_len - (uint64_t)r; + 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); + Hacl_SHA2_Scalar32_sha384_finish(tmp_block_state, dst); +} diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c new file mode 100644 index 0000000000000..51565911b167e --- /dev/null +++ b/crypto/sha2-hacl.c @@ -0,0 +1,187 @@ +/* + * GPLv2 or MIT License + * + * Copyright (c) 2023 Cryspen + * + */ + +#include +#include + +#include "./hacl_hash.h" +#include "./hacl_lib.h" + +int hacl_sha256_update(struct shash_desc *desc, const u8 *data, + unsigned int len) +{ + struct sha256_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_32 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count; + Hacl_Streaming_SHA2_update_256(&st, (u8 *)data, len); + sctx->count = st.total_len; + return 0; +} +EXPORT_SYMBOL(hacl_sha256_update); + +static int hacl_sha256_final(struct shash_desc *desc, u8 *out) +{ + struct sha256_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_32 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count; + if (crypto_shash_digestsize(desc->tfm) == SHA224_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_224(&st, out); + else + Hacl_Streaming_SHA2_finish_256(&st, out); + return 0; +} + +int hacl_sha256_finup(struct shash_desc *desc, const u8 *data, unsigned int len, + u8 *hash) +{ + struct sha256_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_32 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count; + Hacl_Streaming_SHA2_update_256(&st, (u8 *)data, len); + if (crypto_shash_digestsize(desc->tfm) == SHA224_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_224(&st, hash); + else + Hacl_Streaming_SHA2_finish_256(&st, hash); + return 0; +} +EXPORT_SYMBOL(hacl_sha256_finup); + +int hacl_sha512_update(struct shash_desc *desc, const u8 *data, + unsigned int len) +{ + struct sha512_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_64 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count[0]; + Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); + sctx->count[0] = st.total_len; + return 0; +} +EXPORT_SYMBOL(hacl_sha512_update); + +static int hacl_sha512_final(struct shash_desc *desc, u8 *hash) +{ + struct sha512_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_64 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count[0]; + if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_384(&st, hash); + else + Hacl_Streaming_SHA2_finish_512(&st, hash); + return 0; +} + +int hacl_sha512_finup(struct shash_desc *desc, const u8 *data, unsigned int len, + u8 *hash) +{ + struct sha512_state *sctx = shash_desc_ctx(desc); + Hacl_Streaming_MD_state_64 st; + st.block_state = sctx->state; + st.buf = sctx->buf; + st.total_len = sctx->count[0]; + Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); + if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_384(&st, hash); + else + Hacl_Streaming_SHA2_finish_512(&st, hash); + return 0; +} +EXPORT_SYMBOL(hacl_sha512_finup); + +static struct shash_alg sha2_hacl_algs[4] = { { + .digestsize = SHA256_DIGEST_SIZE, + .init = sha256_base_init, + .update = hacl_sha256_update, + .final = hacl_sha256_final, + .finup = hacl_sha256_finup, + .descsize = sizeof(struct sha256_state), + .base = { + .cra_name = "sha256", + .cra_driver_name = "sha256-hacl", + .cra_priority = 100, + .cra_blocksize = SHA256_BLOCK_SIZE, + .cra_module = THIS_MODULE, + } + }, { + .digestsize = SHA224_DIGEST_SIZE, + .init = sha224_base_init, + .update = hacl_sha256_update, + .final = hacl_sha256_final, + .finup = hacl_sha256_finup, + .descsize = sizeof(struct sha256_state), + .base = { + .cra_name = "sha224", + .cra_driver_name = "sha224-hacl", + .cra_priority = 100, + .cra_blocksize = SHA224_BLOCK_SIZE, + .cra_module = THIS_MODULE, + } + }, { + .digestsize = SHA384_DIGEST_SIZE, + .init = sha384_base_init, + .update = hacl_sha512_update, + .final = hacl_sha512_final, + .finup = hacl_sha512_finup, + .descsize = sizeof(struct sha512_state), + .base = { + .cra_name = "sha384", + .cra_driver_name = "sha384-hacl", + .cra_priority = 100, + .cra_blocksize = SHA384_BLOCK_SIZE, + .cra_module = THIS_MODULE, + } + }, { + .digestsize = SHA512_DIGEST_SIZE, + .init = sha512_base_init, + .update = hacl_sha512_update, + .final = hacl_sha512_final, + .finup = hacl_sha512_finup, + .descsize = sizeof(struct sha512_state), + .base = { + .cra_name = "sha512", + .cra_driver_name = "sha512-hacl", + .cra_priority = 100, + .cra_blocksize = SHA512_BLOCK_SIZE, + .cra_module = THIS_MODULE, + } + } +}; + +static int __init sha2_hacl_mod_init(void) +{ + return crypto_register_shashes(sha2_hacl_algs, + ARRAY_SIZE(sha2_hacl_algs)); +} + +static void __exit sha2_hacl_mod_fini(void) +{ + crypto_unregister_shashes(sha2_hacl_algs, ARRAY_SIZE(sha2_hacl_algs)); +} + +subsys_initcall(sha2_hacl_mod_init); +module_exit(sha2_hacl_mod_fini); + +MODULE_LICENSE("GPLv2 or MIT"); +MODULE_DESCRIPTION("Formally Verified SHA-2 Secure Hash Algorithm from HACL*"); + +MODULE_ALIAS_CRYPTO("sha224"); +MODULE_ALIAS_CRYPTO("sha224-hacl"); +MODULE_ALIAS_CRYPTO("sha256"); +MODULE_ALIAS_CRYPTO("sha256-hacl"); +MODULE_ALIAS_CRYPTO("sha384"); +MODULE_ALIAS_CRYPTO("sha384-hacl"); +MODULE_ALIAS_CRYPTO("sha512"); +MODULE_ALIAS_CRYPTO("sha512-hacl"); From eda684b7aa7b7af286eb9108640d287398bc3947 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Thu, 5 Oct 2023 14:55:16 +0200 Subject: [PATCH 03/18] Add HACL SHA2 to Makefile and config --- crypto/Kconfig | 6 ++++++ crypto/Makefile | 1 + 2 files changed, 7 insertions(+) diff --git a/crypto/Kconfig b/crypto/Kconfig index 650b1b3620d81..e35350102a433 100644 --- a/crypto/Kconfig +++ b/crypto/Kconfig @@ -1026,6 +1026,12 @@ config CRYPTO_SHA256 This is required for IPsec AH (XFRM_AH) and IPsec ESP (XFRM_ESP). Used by the btrfs filesystem, Ceph, NFS, and SMB. +config CRYPTO_SHA2_HACL + tristate "SHA-224 and SHA-256 and SHA-384 and SHA-512" + select CRYPTO_HASH + help + SHA-2 secure hash algorithms (FIPS 180, ISO/IEC 10118-3) from HACL* + config CRYPTO_SHA512 tristate "SHA-384 and SHA-512" select CRYPTO_HASH diff --git a/crypto/Makefile b/crypto/Makefile index 953a7e105e58c..2c88f3c8ce4db 100644 --- a/crypto/Makefile +++ b/crypto/Makefile @@ -77,6 +77,7 @@ obj-$(CONFIG_CRYPTO_MD5) += md5.o obj-$(CONFIG_CRYPTO_RMD160) += rmd160.o obj-$(CONFIG_CRYPTO_SHA1) += sha1_generic.o obj-$(CONFIG_CRYPTO_SHA256) += sha256_generic.o +obj-$(CONFIG_CRYPTO_SHA2_HACL) += sha2-hacl-generated.o sha2-hacl.o obj-$(CONFIG_CRYPTO_SHA512) += sha512_generic.o obj-$(CONFIG_CRYPTO_SHA3) += sha3_generic.o obj-$(CONFIG_CRYPTO_SM3) += sm3.o From ad8e84e3c62a72aa99063d85e7b1f1b6db67c03a Mon Sep 17 00:00:00 2001 From: Karthik Bhargavan Date: Fri, 13 Oct 2023 11:25:56 +0200 Subject: [PATCH 04/18] addressed review comments --- crypto/hacl_hash.h | 201 +++-------------------------------- crypto/sha2-hacl-generated.c | 100 ++++++++--------- crypto/sha2-hacl.c | 12 +-- 3 files changed, 73 insertions(+), 240 deletions(-) diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index 38901e36dbe8c..32c4f33d7a809 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -9,51 +9,24 @@ #include "./hacl_lib.h" -#define Spec_Hash_Definitions_SHA2_224 0 -#define Spec_Hash_Definitions_SHA2_256 1 -#define Spec_Hash_Definitions_SHA2_384 2 -#define Spec_Hash_Definitions_SHA2_512 3 -#define Spec_Hash_Definitions_SHA1 4 -#define Spec_Hash_Definitions_MD5 5 -#define Spec_Hash_Definitions_Blake2S 6 -#define Spec_Hash_Definitions_Blake2B 7 -#define Spec_Hash_Definitions_SHA3_256 8 -#define Spec_Hash_Definitions_SHA3_224 9 -#define Spec_Hash_Definitions_SHA3_384 10 -#define Spec_Hash_Definitions_SHA3_512 11 -#define Spec_Hash_Definitions_Shake128 12 -#define Spec_Hash_Definitions_Shake256 13 - -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 -uint32_t Hacl_Hash_Definitions_word_len(Spec_Hash_Definitions_hash_alg a); - -uint32_t Hacl_Hash_Definitions_block_len(Spec_Hash_Definitions_hash_alg a); - -uint32_t Hacl_Hash_Definitions_hash_word_len(Spec_Hash_Definitions_hash_alg a); - -uint32_t Hacl_Hash_Definitions_hash_len(Spec_Hash_Definitions_hash_alg a); - -typedef uint8_t *Hacl_Hash_Definitions_hash_t; - typedef uint8_t Hacl_Streaming_Types_error_code; -typedef struct Hacl_Streaming_MD_state_32_s { +struct Hacl_Streaming_MD_state_32_s { uint32_t *block_state; uint8_t *buf; uint64_t total_len; -} Hacl_Streaming_MD_state_32; +}; -typedef struct Hacl_Streaming_MD_state_64_s { +struct Hacl_Streaming_MD_state_64_s { uint64_t *block_state; uint8_t *buf; uint64_t total_len; -} Hacl_Streaming_MD_state_64; +}; static const uint32_t Hacl_Impl_SHA2_Generic_h224[8U] = { (uint32_t)0xc1059ed8U, (uint32_t)0x367cd507U, (uint32_t)0x3070dd17U, @@ -149,72 +122,10 @@ static const uint64_t 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); - -typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_224; - -typedef Hacl_Streaming_MD_state_32 Hacl_Streaming_SHA2_state_sha2_256; - -typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_384; - -typedef Hacl_Streaming_MD_state_64 Hacl_Streaming_SHA2_state_sha2_512; - -/** -Allocate initial state for the SHA2_256 hash. The state is to be freed by -calling `free_256`. -*/ -Hacl_Streaming_MD_state_32 *Hacl_Streaming_SHA2_create_in_256(void); - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_256`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_32 * -Hacl_Streaming_SHA2_copy_256(Hacl_Streaming_MD_state_32 *s0); - /** Reset an existing state to the initial hash state with empty data. */ -void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s); +void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s); /** Feed an arbitrary amount of data into the hash. This function returns 0 for @@ -224,7 +135,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. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_256(Hacl_Streaming_MD_state_32 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len); /** @@ -233,28 +144,19 @@ valid after a call to `finish_256`, meaning the user may feed more data into the hash via `update_256`. (The finish_256 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, +void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst); -/** -Free a state allocated with `create_in_256`. - -This function is identical to the free function for SHA2_224. -*/ -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_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); +void Hacl_Streaming_SHA2_init_224(struct Hacl_Streaming_MD_state_32_s *s); Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_224(Hacl_Streaming_MD_state_32 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len); /** @@ -262,29 +164,16 @@ Write the resulting hash into `dst`, an array of 28 bytes. The state remains valid after a call to `finish_224`, meaning the user may feed more data into the hash via `update_224`. */ -void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, +void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst); -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_hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst); -Hacl_Streaming_MD_state_64 *Hacl_Streaming_SHA2_create_in_512(void); - -/** -Copies the state passed as argument into a newly allocated state (deep copy). -The state is to be freed by calling `free_512`. Cloning the state this way is -useful, for instance, if your control-flow diverges and you need to feed -more (different) data into the hash in each branch. -*/ -Hacl_Streaming_MD_state_64 * -Hacl_Streaming_SHA2_copy_512(Hacl_Streaming_MD_state_64 *s0); - -void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s); +void Hacl_Streaming_SHA2_init_512(struct Hacl_Streaming_MD_state_64_s *s); /** Feed an arbitrary amount of data into the hash. This function returns 0 for @@ -294,7 +183,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. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_512(Hacl_Streaming_MD_state_64 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len); /** @@ -303,28 +192,19 @@ valid after a call to `finish_512`, meaning the user may feed more data into the hash via `update_512`. (The finish_512 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, +void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst); -/** -Free a state allocated with `create_in_512`. - -This function is identical to the free function for SHA2_384. -*/ -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_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); +void Hacl_Streaming_SHA2_init_384(struct Hacl_Streaming_MD_state_64_s *s); Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_384(Hacl_Streaming_MD_state_64 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len); /** @@ -332,61 +212,12 @@ Write the resulting hash into `dst`, an array of 48 bytes. The state remains valid after a call to `finish_384`, meaning the user may feed more data into the hash via `update_384`. */ -void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, +void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst); - -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_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst); -typedef struct Hacl_Impl_SHA2_Types_uint8_2p_s { - uint8_t *fst; - uint8_t *snd; -} Hacl_Impl_SHA2_Types_uint8_2p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_3p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_2p snd; -} Hacl_Impl_SHA2_Types_uint8_3p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_4p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_3p snd; -} Hacl_Impl_SHA2_Types_uint8_4p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_5p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_4p snd; -} Hacl_Impl_SHA2_Types_uint8_5p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_6p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_5p snd; -} Hacl_Impl_SHA2_Types_uint8_6p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_7p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_6p snd; -} Hacl_Impl_SHA2_Types_uint8_7p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_8p_s { - uint8_t *fst; - Hacl_Impl_SHA2_Types_uint8_7p snd; -} Hacl_Impl_SHA2_Types_uint8_8p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_2x4p_s { - Hacl_Impl_SHA2_Types_uint8_4p fst; - Hacl_Impl_SHA2_Types_uint8_4p snd; -} Hacl_Impl_SHA2_Types_uint8_2x4p; - -typedef struct Hacl_Impl_SHA2_Types_uint8_2x8p_s { - Hacl_Impl_SHA2_Types_uint8_8p fst; - Hacl_Impl_SHA2_Types_uint8_8p snd; -} Hacl_Impl_SHA2_Types_uint8_2x8p; - -#define __Hacl_Hash_H_DEFINED #endif // CRYPTO_HACL_HASH_H_ diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index 9a5e081915b74..ca0b6de5736fc 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -1,4 +1,5 @@ -/* GPLv2 or MIT License +/* + * GPLv2 or MIT License * * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors @@ -16,7 +17,7 @@ void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash) os[i] = x;); } -static inline void sha256_update_(uint8_t *b, uint32_t *hash) +static inline void hacl_sha256_update(uint8_t *b, uint32_t *hash) { uint32_t hash_old[8U] = { 0U }; uint32_t ws[16U] = { 0U }; @@ -117,7 +118,7 @@ void Hacl_SHA2_Scalar32_sha256_update_nblocks(uint32_t len, uint8_t *b, for (uint32_t i = (uint32_t)0U; i < blocks; i++) { uint8_t *b0 = b; uint8_t *mb = b0 + i * (uint32_t)64U; - sha256_update_(mb, st); + hacl_sha256_update(mb, st); } } @@ -148,9 +149,9 @@ void Hacl_SHA2_Scalar32_sha256_update_last(uint64_t totlen, uint32_t len, uint8_t *lb1 = l1; uint8_t *last0 = lb0; uint8_t *last1 = lb1; - sha256_update_(last0, hash); + hacl_sha256_update(last0, hash); if (blocks > (uint32_t)1U) { - sha256_update_(last1, hash); + hacl_sha256_update(last1, hash); return; } } @@ -193,13 +194,14 @@ void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h) /** Reset an existing state to the initial hash state with empty data. */ -void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) + +void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s) { - Hacl_Streaming_MD_state_32 scrut = *s; + struct Hacl_Streaming_MD_state_32_s scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha256_init(block_state); - Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, + struct Hacl_Streaming_MD_state_32_s tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -207,9 +209,9 @@ void Hacl_Streaming_SHA2_init_256(Hacl_Streaming_MD_state_32 *s) } static inline Hacl_Streaming_Types_error_code -update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) +update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, uint32_t len) { - Hacl_Streaming_MD_state_32 s = *p; + struct Hacl_Streaming_MD_state_32_s s = *p; uint64_t total_len = s.total_len; if ((uint64_t)len > (uint64_t)2305843009213693951U - total_len) { return Hacl_Streaming_Types_MaximumLengthExceeded; @@ -222,7 +224,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); } if (len <= (uint32_t)64U - sz) { - Hacl_Streaming_MD_state_32 s1 = *p; + struct Hacl_Streaming_MD_state_32_s s1 = *p; uint32_t *block_state1 = s1.block_state; uint8_t *buf = s1.buf; uint64_t total_len1 = s1.total_len; @@ -236,11 +238,11 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) uint8_t *buf2 = buf + sz1; memcpy(buf2, data, len * sizeof(uint8_t)); uint64_t total_len2 = total_len1 + (uint64_t)len; - *p = ((Hacl_Streaming_MD_state_32){ .block_state = block_state1, + *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state1, .buf = buf, .total_len = total_len2 }); } else if (sz == (uint32_t)0U) { - Hacl_Streaming_MD_state_32 s1 = *p; + struct Hacl_Streaming_MD_state_32_s s1 = *p; uint32_t *block_state1 = s1.block_state; uint8_t *buf = s1.buf; uint64_t total_len1 = s1.total_len; @@ -273,7 +275,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) block_state1); uint8_t *dst = buf; memcpy(dst, data2, data2_len * sizeof(uint8_t)); - *p = ((Hacl_Streaming_MD_state_32){ + *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state1, .buf = buf, .total_len = total_len1 + (uint64_t)len }); @@ -281,7 +283,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) uint32_t diff = (uint32_t)64U - sz; uint8_t *data1 = data; uint8_t *data2 = data + diff; - Hacl_Streaming_MD_state_32 s1 = *p; + struct Hacl_Streaming_MD_state_32_s s1 = *p; uint32_t *block_state10 = s1.block_state; uint8_t *buf0 = s1.buf; uint64_t total_len10 = s1.total_len; @@ -296,11 +298,11 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) uint8_t *buf2 = buf0 + sz10; memcpy(buf2, data1, diff * sizeof(uint8_t)); uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p = ((Hacl_Streaming_MD_state_32){ .block_state = + *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state10, .buf = buf0, .total_len = total_len2 }); - Hacl_Streaming_MD_state_32 s10 = *p; + struct Hacl_Streaming_MD_state_32_s s10 = *p; uint32_t *block_state1 = s10.block_state; uint8_t *buf = s10.buf; uint64_t total_len1 = s10.total_len; @@ -334,7 +336,7 @@ update_224_256(Hacl_Streaming_MD_state_32 *p, uint8_t *data, uint32_t len) block_state1); uint8_t *dst = buf; memcpy(dst, data21, data2_len * sizeof(uint8_t)); - *p = ((Hacl_Streaming_MD_state_32){ + *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state1, .buf = buf, .total_len = total_len1 + (uint64_t)(len - diff) }); @@ -350,7 +352,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. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_256(Hacl_Streaming_MD_state_32 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len) { return update_224_256(p, input, input_len); @@ -362,9 +364,9 @@ valid after a call to `finish_256`, meaning the user may feed more data into the hash via `update_256`. (The finish_256 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_256(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) { - Hacl_Streaming_MD_state_32 scrut = *p; + struct Hacl_Streaming_MD_state_32_s scrut = *p; uint32_t *block_state = scrut.block_state; uint8_t *buf_ = scrut.buf; uint64_t total_len = scrut.total_len; @@ -414,13 +416,13 @@ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, Hacl_SHA2_Scalar32_sha256_finish(st, rb); } -void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) +void Hacl_Streaming_SHA2_init_224(struct Hacl_Streaming_MD_state_32_s *s) { - Hacl_Streaming_MD_state_32 scrut = *s; + struct Hacl_Streaming_MD_state_32_s scrut = *s; uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha224_init(block_state); - Hacl_Streaming_MD_state_32 tmp = { .block_state = block_state, + struct Hacl_Streaming_MD_state_32_s tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -428,7 +430,7 @@ void Hacl_Streaming_SHA2_init_224(Hacl_Streaming_MD_state_32 *s) } Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_224(Hacl_Streaming_MD_state_32 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len) { return update_224_256(p, input, input_len); @@ -439,9 +441,9 @@ Write the resulting hash into `dst`, an array of 28 bytes. The state remains valid after a call to `finish_224`, meaning the user may feed more data into the hash via `update_224`. */ -void Hacl_Streaming_SHA2_finish_224(Hacl_Streaming_MD_state_32 *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) { - Hacl_Streaming_MD_state_32 scrut = *p; + struct Hacl_Streaming_MD_state_32_s scrut = *p; uint32_t *block_state = scrut.block_state; uint8_t *buf_ = scrut.buf; uint64_t total_len = scrut.total_len; @@ -676,13 +678,13 @@ void Hacl_SHA2_Scalar32_sha384_finish(uint64_t *st, uint8_t *h) memcpy(h, hbuf, (uint32_t)48U * sizeof(uint8_t)); } -void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) +void Hacl_Streaming_SHA2_init_512(struct Hacl_Streaming_MD_state_64_s *s) { - Hacl_Streaming_MD_state_64 scrut = *s; + struct Hacl_Streaming_MD_state_64_s scrut = *s; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha512_init(block_state); - Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, + struct Hacl_Streaming_MD_state_64_s tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -690,9 +692,9 @@ void Hacl_Streaming_SHA2_init_512(Hacl_Streaming_MD_state_64 *s) } static inline Hacl_Streaming_Types_error_code -update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) +update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, uint32_t len) { - Hacl_Streaming_MD_state_64 s = *p; + struct Hacl_Streaming_MD_state_64_s s = *p; uint64_t total_len = s.total_len; if ((uint64_t)len > (uint64_t)18446744073709551615U - total_len) { return Hacl_Streaming_Types_MaximumLengthExceeded; @@ -705,7 +707,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); } if (len <= (uint32_t)128U - sz) { - Hacl_Streaming_MD_state_64 s1 = *p; + struct Hacl_Streaming_MD_state_64_s s1 = *p; uint64_t *block_state1 = s1.block_state; uint8_t *buf = s1.buf; uint64_t total_len1 = s1.total_len; @@ -719,11 +721,11 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) uint8_t *buf2 = buf + sz1; memcpy(buf2, data, len * sizeof(uint8_t)); uint64_t total_len2 = total_len1 + (uint64_t)len; - *p = ((Hacl_Streaming_MD_state_64){ .block_state = block_state1, + *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state1, .buf = buf, .total_len = total_len2 }); } else if (sz == (uint32_t)0U) { - Hacl_Streaming_MD_state_64 s1 = *p; + struct Hacl_Streaming_MD_state_64_s s1 = *p; uint64_t *block_state1 = s1.block_state; uint8_t *buf = s1.buf; uint64_t total_len1 = s1.total_len; @@ -756,7 +758,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) block_state1); uint8_t *dst = buf; memcpy(dst, data2, data2_len * sizeof(uint8_t)); - *p = ((Hacl_Streaming_MD_state_64){ + *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state1, .buf = buf, .total_len = total_len1 + (uint64_t)len }); @@ -764,7 +766,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) uint32_t diff = (uint32_t)128U - sz; uint8_t *data1 = data; uint8_t *data2 = data + diff; - Hacl_Streaming_MD_state_64 s1 = *p; + struct Hacl_Streaming_MD_state_64_s s1 = *p; uint64_t *block_state10 = s1.block_state; uint8_t *buf0 = s1.buf; uint64_t total_len10 = s1.total_len; @@ -779,11 +781,11 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) uint8_t *buf2 = buf0 + sz10; memcpy(buf2, data1, diff * sizeof(uint8_t)); uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p = ((Hacl_Streaming_MD_state_64){ .block_state = + *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state10, .buf = buf0, .total_len = total_len2 }); - Hacl_Streaming_MD_state_64 s10 = *p; + struct Hacl_Streaming_MD_state_64_s s10 = *p; uint64_t *block_state1 = s10.block_state; uint8_t *buf = s10.buf; uint64_t total_len1 = s10.total_len; @@ -817,7 +819,7 @@ update_384_512(Hacl_Streaming_MD_state_64 *p, uint8_t *data, uint32_t len) block_state1); uint8_t *dst = buf; memcpy(dst, data21, data2_len * sizeof(uint8_t)); - *p = ((Hacl_Streaming_MD_state_64){ + *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state1, .buf = buf, .total_len = total_len1 + (uint64_t)(len - diff) }); @@ -833,7 +835,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. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_512(Hacl_Streaming_MD_state_64 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len) { return update_384_512(p, input, input_len); @@ -845,9 +847,9 @@ valid after a call to `finish_512`, meaning the user may feed more data into the hash via `update_512`. (The finish_512 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) { - Hacl_Streaming_MD_state_64 scrut = *p; + struct Hacl_Streaming_MD_state_64_s scrut = *p; uint64_t *block_state = scrut.block_state; uint8_t *buf_ = scrut.buf; uint64_t total_len = scrut.total_len; @@ -879,13 +881,13 @@ void Hacl_Streaming_SHA2_finish_512(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) Hacl_SHA2_Scalar32_sha512_finish(tmp_block_state, dst); } -void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) +void Hacl_Streaming_SHA2_init_384(struct Hacl_Streaming_MD_state_64_s *s) { - Hacl_Streaming_MD_state_64 scrut = *s; + struct Hacl_Streaming_MD_state_64_s scrut = *s; uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha384_init(block_state); - Hacl_Streaming_MD_state_64 tmp = { .block_state = block_state, + struct Hacl_Streaming_MD_state_64_s tmp = { .block_state = block_state, .buf = buf, .total_len = (uint64_t)(uint32_t)0U }; @@ -893,7 +895,7 @@ void Hacl_Streaming_SHA2_init_384(Hacl_Streaming_MD_state_64 *s) } Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_384(Hacl_Streaming_MD_state_64 *p, uint8_t *input, +Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len) { return update_384_512(p, input, input_len); @@ -904,9 +906,9 @@ Write the resulting hash into `dst`, an array of 48 bytes. The state remains valid after a call to `finish_384`, meaning the user may feed more data into the hash via `update_384`. */ -void Hacl_Streaming_SHA2_finish_384(Hacl_Streaming_MD_state_64 *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) { - Hacl_Streaming_MD_state_64 scrut = *p; + struct Hacl_Streaming_MD_state_64_s scrut = *p; uint64_t *block_state = scrut.block_state; uint8_t *buf_ = scrut.buf; uint64_t total_len = scrut.total_len; diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c index 51565911b167e..89e4ec2e2c457 100644 --- a/crypto/sha2-hacl.c +++ b/crypto/sha2-hacl.c @@ -15,7 +15,7 @@ int hacl_sha256_update(struct shash_desc *desc, const u8 *data, unsigned int len) { struct sha256_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_32 st; + struct Hacl_Streaming_MD_state_32_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count; @@ -28,7 +28,7 @@ EXPORT_SYMBOL(hacl_sha256_update); static int hacl_sha256_final(struct shash_desc *desc, u8 *out) { struct sha256_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_32 st; + struct Hacl_Streaming_MD_state_32_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count; @@ -43,7 +43,7 @@ int hacl_sha256_finup(struct shash_desc *desc, const u8 *data, unsigned int len, u8 *hash) { struct sha256_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_32 st; + struct Hacl_Streaming_MD_state_32_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count; @@ -60,7 +60,7 @@ int hacl_sha512_update(struct shash_desc *desc, const u8 *data, unsigned int len) { struct sha512_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_64 st; + struct Hacl_Streaming_MD_state_64_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; @@ -73,7 +73,7 @@ EXPORT_SYMBOL(hacl_sha512_update); static int hacl_sha512_final(struct shash_desc *desc, u8 *hash) { struct sha512_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_64 st; + struct Hacl_Streaming_MD_state_64_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; @@ -88,7 +88,7 @@ int hacl_sha512_finup(struct shash_desc *desc, const u8 *data, unsigned int len, u8 *hash) { struct sha512_state *sctx = shash_desc_ctx(desc); - Hacl_Streaming_MD_state_64 st; + struct Hacl_Streaming_MD_state_64_s st; st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; From 585ad7d4e280114b5df50bb9e5625a93599d1cf3 Mon Sep 17 00:00:00 2001 From: Karthik Bhargavan Date: Fri, 13 Oct 2023 11:34:21 +0200 Subject: [PATCH 05/18] propagating errors --- crypto/sha2-hacl.c | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c index 89e4ec2e2c457..efc9e09b1f1b9 100644 --- a/crypto/sha2-hacl.c +++ b/crypto/sha2-hacl.c @@ -19,9 +19,9 @@ int hacl_sha256_update(struct shash_desc *desc, const u8 *data, st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count; - Hacl_Streaming_SHA2_update_256(&st, (u8 *)data, len); + uint8_t res = Hacl_Streaming_SHA2_update_256(&st, (u8 *)data, len); sctx->count = st.total_len; - return 0; + return res; } EXPORT_SYMBOL(hacl_sha256_update); @@ -64,9 +64,9 @@ int hacl_sha512_update(struct shash_desc *desc, const u8 *data, st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; - Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); + uint8_t res = Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); sctx->count[0] = st.total_len; - return 0; + return res; } EXPORT_SYMBOL(hacl_sha512_update); @@ -92,12 +92,15 @@ int hacl_sha512_finup(struct shash_desc *desc, const u8 *data, unsigned int len, st.block_state = sctx->state; st.buf = sctx->buf; st.total_len = sctx->count[0]; - Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); - if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) - Hacl_Streaming_SHA2_finish_384(&st, hash); - else - Hacl_Streaming_SHA2_finish_512(&st, hash); - return 0; + uint8_t res = Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); + if (res == 0) { + if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_384(&st, hash); + else + Hacl_Streaming_SHA2_finish_512(&st, hash); + return 0; + } else + return res; } EXPORT_SYMBOL(hacl_sha512_finup); From b0e03392ce0ac298fe22ebe18b9454a7e404d7f4 Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 16 Oct 2023 16:42:06 -0700 Subject: [PATCH 06/18] Formatting files according to clang-format. --- crypto/hacl_hash.h | 20 +++---- crypto/hacl_lib.h | 2 +- crypto/sha2-hacl-generated.c | 106 +++++++++++++++++++---------------- crypto/sha2-hacl.c | 21 +++---- 4 files changed, 81 insertions(+), 68 deletions(-) diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index 32c4f33d7a809..a9524994e9023 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -7,7 +7,7 @@ #ifndef CRYPTO_HACL_HASH_H_ #define CRYPTO_HACL_HASH_H_ -#include "./hacl_lib.h" +#include "hacl_lib.h" #define Hacl_Streaming_Types_Success 0 #define Hacl_Streaming_Types_InvalidAlgorithm 1 @@ -135,8 +135,8 @@ 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. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, - uint32_t input_len); +Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *input, uint32_t input_len); /** Write the resulting hash into `dst`, an array of 32 bytes. The state remains @@ -156,8 +156,8 @@ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, void Hacl_Streaming_SHA2_init_224(struct Hacl_Streaming_MD_state_32_s *s); Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, - uint32_t input_len); +Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *input, uint32_t input_len); /** Write the resulting hash into `dst`, an array of 28 bytes. The state remains @@ -183,8 +183,8 @@ 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. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, - uint32_t input_len); +Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *input, uint32_t input_len); /** Write the resulting hash into `dst`, an array of 64 bytes. The state remains @@ -204,8 +204,8 @@ void Hacl_Streaming_SHA2_hash_512(uint8_t *input, uint32_t input_len, void Hacl_Streaming_SHA2_init_384(struct Hacl_Streaming_MD_state_64_s *s); Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, - uint32_t input_len); +Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *input, uint32_t input_len); /** Write the resulting hash into `dst`, an array of 48 bytes. The state remains @@ -220,4 +220,4 @@ Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst); -#endif // CRYPTO_HACL_HASH_H_ +#endif // CRYPTO_HACL_HASH_H_ diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h index 44c8038ed124d..b6e3e015294d3 100644 --- a/crypto/hacl_lib.h +++ b/crypto/hacl_lib.h @@ -228,4 +228,4 @@ static inline void store128_be(u8 *buf, u128 x) #define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) #endif -#endif // CRYPTO_HACL_LIB_H_" +#endif // CRYPTO_HACL_LIB_H_ diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index ca0b6de5736fc..9f3bfa4824219 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -1,4 +1,4 @@ -/* +/* * GPLv2 or MIT License * * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation @@ -6,8 +6,8 @@ * */ -#include "./hacl_hash.h" -#include "./hacl_lib.h" +#include "hacl_hash.h" +#include "hacl_lib.h" void Hacl_SHA2_Scalar32_sha256_init(uint32_t *hash) { @@ -201,15 +201,17 @@ void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s) uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha256_init(block_state); - struct Hacl_Streaming_MD_state_32_s tmp = { .block_state = block_state, - .buf = buf, - .total_len = - (uint64_t)(uint32_t)0U }; + struct Hacl_Streaming_MD_state_32_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; s[0U] = tmp; } static inline Hacl_Streaming_Types_error_code -update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, uint32_t len) +update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, + uint32_t len) { struct Hacl_Streaming_MD_state_32_s s = *p; uint64_t total_len = s.total_len; @@ -238,9 +240,10 @@ update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, uint32_t l uint8_t *buf2 = buf + sz1; memcpy(buf2, data, len * sizeof(uint8_t)); uint64_t total_len2 = total_len1 + (uint64_t)len; - *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = block_state1, - .buf = buf, - .total_len = total_len2 }); + *p = ((struct Hacl_Streaming_MD_state_32_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); } else if (sz == (uint32_t)0U) { struct Hacl_Streaming_MD_state_32_s s1 = *p; uint32_t *block_state1 = s1.block_state; @@ -298,10 +301,10 @@ update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, uint32_t l uint8_t *buf2 = buf0 + sz10; memcpy(buf2, data1, diff * sizeof(uint8_t)); uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p = ((struct Hacl_Streaming_MD_state_32_s){ .block_state = - block_state10, - .buf = buf0, - .total_len = total_len2 }); + *p = ((struct Hacl_Streaming_MD_state_32_s){ + .block_state = block_state10, + .buf = buf0, + .total_len = total_len2 }); struct Hacl_Streaming_MD_state_32_s s10 = *p; uint32_t *block_state1 = s10.block_state; uint8_t *buf = s10.buf; @@ -352,8 +355,8 @@ 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. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, - uint32_t input_len) +Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *input, uint32_t input_len) { return update_224_256(p, input, input_len); } @@ -364,7 +367,8 @@ valid after a call to `finish_256`, meaning the user may feed more data into the hash via `update_256`. (The finish_256 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *dst) { struct Hacl_Streaming_MD_state_32_s scrut = *p; uint32_t *block_state = scrut.block_state; @@ -422,16 +426,17 @@ void Hacl_Streaming_SHA2_init_224(struct Hacl_Streaming_MD_state_32_s *s) uint8_t *buf = scrut.buf; uint32_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha224_init(block_state); - struct Hacl_Streaming_MD_state_32_s tmp = { .block_state = block_state, - .buf = buf, - .total_len = - (uint64_t)(uint32_t)0U }; + struct Hacl_Streaming_MD_state_32_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; s[0U] = tmp; } Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, - uint32_t input_len) +Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *input, uint32_t input_len) { return update_224_256(p, input, input_len); } @@ -441,7 +446,8 @@ Write the resulting hash into `dst`, an array of 28 bytes. The state remains valid after a call to `finish_224`, meaning the user may feed more data into the hash via `update_224`. */ -void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, + uint8_t *dst) { struct Hacl_Streaming_MD_state_32_s scrut = *p; uint32_t *block_state = scrut.block_state; @@ -684,15 +690,17 @@ void Hacl_Streaming_SHA2_init_512(struct Hacl_Streaming_MD_state_64_s *s) uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha512_init(block_state); - struct Hacl_Streaming_MD_state_64_s tmp = { .block_state = block_state, - .buf = buf, - .total_len = - (uint64_t)(uint32_t)0U }; + struct Hacl_Streaming_MD_state_64_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; s[0U] = tmp; } static inline Hacl_Streaming_Types_error_code -update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, uint32_t len) +update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, + uint32_t len) { struct Hacl_Streaming_MD_state_64_s s = *p; uint64_t total_len = s.total_len; @@ -721,9 +729,10 @@ update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, uint32_t l uint8_t *buf2 = buf + sz1; memcpy(buf2, data, len * sizeof(uint8_t)); uint64_t total_len2 = total_len1 + (uint64_t)len; - *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = block_state1, - .buf = buf, - .total_len = total_len2 }); + *p = ((struct Hacl_Streaming_MD_state_64_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); } else if (sz == (uint32_t)0U) { struct Hacl_Streaming_MD_state_64_s s1 = *p; uint64_t *block_state1 = s1.block_state; @@ -781,10 +790,10 @@ update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, uint32_t l uint8_t *buf2 = buf0 + sz10; memcpy(buf2, data1, diff * sizeof(uint8_t)); uint64_t total_len2 = total_len10 + (uint64_t)diff; - *p = ((struct Hacl_Streaming_MD_state_64_s){ .block_state = - block_state10, - .buf = buf0, - .total_len = total_len2 }); + *p = ((struct Hacl_Streaming_MD_state_64_s){ + .block_state = block_state10, + .buf = buf0, + .total_len = total_len2 }); struct Hacl_Streaming_MD_state_64_s s10 = *p; uint64_t *block_state1 = s10.block_state; uint8_t *buf = s10.buf; @@ -835,8 +844,8 @@ 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. */ Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, - uint32_t input_len) +Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *input, uint32_t input_len) { return update_384_512(p, input, input_len); } @@ -847,7 +856,8 @@ valid after a call to `finish_512`, meaning the user may feed more data into the hash via `update_512`. (The finish_512 function operates on an internal copy of the state and therefore does not invalidate the client-held state `p`.) */ -void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *dst) { struct Hacl_Streaming_MD_state_64_s scrut = *p; uint64_t *block_state = scrut.block_state; @@ -887,16 +897,17 @@ void Hacl_Streaming_SHA2_init_384(struct Hacl_Streaming_MD_state_64_s *s) uint8_t *buf = scrut.buf; uint64_t *block_state = scrut.block_state; Hacl_SHA2_Scalar32_sha384_init(block_state); - struct Hacl_Streaming_MD_state_64_s tmp = { .block_state = block_state, - .buf = buf, - .total_len = - (uint64_t)(uint32_t)0U }; + struct Hacl_Streaming_MD_state_64_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; s[0U] = tmp; } Hacl_Streaming_Types_error_code -Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, - uint32_t input_len) +Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *input, uint32_t input_len) { return update_384_512(p, input, input_len); } @@ -906,7 +917,8 @@ Write the resulting hash into `dst`, an array of 48 bytes. The state remains valid after a call to `finish_384`, meaning the user may feed more data into the hash via `update_384`. */ -void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) +void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, + uint8_t *dst) { struct Hacl_Streaming_MD_state_64_s scrut = *p; uint64_t *block_state = scrut.block_state; diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c index efc9e09b1f1b9..6400fbce0ae0b 100644 --- a/crypto/sha2-hacl.c +++ b/crypto/sha2-hacl.c @@ -8,8 +8,8 @@ #include #include -#include "./hacl_hash.h" -#include "./hacl_lib.h" +#include "hacl_hash.h" +#include "hacl_lib.h" int hacl_sha256_update(struct shash_desc *desc, const u8 *data, unsigned int len) @@ -93,14 +93,15 @@ int hacl_sha512_finup(struct shash_desc *desc, const u8 *data, unsigned int len, st.buf = sctx->buf; st.total_len = sctx->count[0]; uint8_t res = Hacl_Streaming_SHA2_update_512(&st, (u8 *)data, len); - if (res == 0) { - if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) - Hacl_Streaming_SHA2_finish_384(&st, hash); - else - Hacl_Streaming_SHA2_finish_512(&st, hash); - return 0; - } else - return res; + if (res == 0) { + if (crypto_shash_digestsize(desc->tfm) == SHA384_DIGEST_SIZE) + Hacl_Streaming_SHA2_finish_384(&st, hash); + else + Hacl_Streaming_SHA2_finish_512(&st, hash); + return 0; + } else { + return res; + } } EXPORT_SYMBOL(hacl_sha512_finup); From 0a59a731f54310b87f850fe9071ff5081279e6f4 Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 16 Oct 2023 16:47:21 -0700 Subject: [PATCH 07/18] Updating comment style. --- crypto/hacl_hash.h | 104 ++++++++++++++++++----------------- crypto/hacl_lib.h | 6 +- crypto/sha2-hacl-generated.c | 10 ++-- 3 files changed, 62 insertions(+), 58 deletions(-) diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index a9524994e9023..1e10e54dfd6c2 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -122,34 +122,35 @@ static const uint64_t Hacl_Impl_SHA2_Generic_k384_512[80U] = { (uint64_t)0x5fcb6fab3ad6faecU, (uint64_t)0x6c44198c4a475817U }; -/** -Reset an existing state to the initial hash state with empty data. -*/ +/* + * Reset an existing state to the initial hash state with empty data. + */ void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s); -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_256` -(since the last call to `init_256`) exceeds 2^61-1 bytes. - -This function is identical to the update function for SHA2_224. -*/ +/* + * Feed an arbitrary amount of data into the hash. This function returns 0 for + * success, or 1 if the combined length of all of the data passed to + * `update_256` (since the last call to `init_256`) exceeds 2^61-1 bytes. + * + * This function is identical to the update function for SHA2_224. + */ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len); -/** -Write the resulting hash into `dst`, an array of 32 bytes. The state remains -valid after a call to `finish_256`, meaning the user may feed more data into -the hash via `update_256`. (The finish_256 function operates on an internal copy -of the state and therefore does not invalidate the client-held state `p`.) -*/ +/* + * Write the resulting hash into `dst`, an array of 32 bytes. The state remains + * valid after a call to `finish_256`, meaning the user may feed more data into + * the hash via `update_256`. (The finish_256 function operates on an internal + * copy of the state and therefore does not invalidate the client-held state + * `p`.) + */ void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst); -/** -Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. + */ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst); @@ -159,45 +160,46 @@ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len); -/** -Write the resulting hash into `dst`, an array of 28 bytes. The state remains -valid after a call to `finish_224`, meaning the user may feed more data into -the hash via `update_224`. -*/ +/* + * Write the resulting hash into `dst`, an array of 28 bytes. The state remains + * valid after a call to `finish_224`, meaning the user may feed more data into + * the hash via `update_224`. + */ void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst); -/** -Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. + */ void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst); void Hacl_Streaming_SHA2_init_512(struct Hacl_Streaming_MD_state_64_s *s); -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_512` -(since the last call to `init_512`) exceeds 2^125-1 bytes. - -This function is identical to the update function for SHA2_384. -*/ +/* + * Feed an arbitrary amount of data into the hash. This function returns 0 for + * success, or 1 if the combined length of all of the data passed to + * `update_512` (since the last call to `init_512`) exceeds 2^125-1 bytes. + * + * This function is identical to the update function for SHA2_384. + */ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len); -/** -Write the resulting hash into `dst`, an array of 64 bytes. The state remains -valid after a call to `finish_512`, meaning the user may feed more data into -the hash via `update_512`. (The finish_512 function operates on an internal copy -of the state and therefore does not invalidate the client-held state `p`.) -*/ +/* + * Write the resulting hash into `dst`, an array of 64 bytes. The state remains + * valid after a call to `finish_512`, meaning the user may feed more data into + * the hash via `update_512`. (The finish_512 function operates on an internal + * copy of the state and therefore does not invalidate the client-held state + * `p`.) + */ void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst); -/** -Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 64 bytes. + */ void Hacl_Streaming_SHA2_hash_512(uint8_t *input, uint32_t input_len, uint8_t *dst); @@ -207,16 +209,16 @@ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len); -/** -Write the resulting hash into `dst`, an array of 48 bytes. The state remains -valid after a call to `finish_384`, meaning the user may feed more data into -the hash via `update_384`. -*/ +/* + * Write the resulting hash into `dst`, an array of 48 bytes. The state remains + * valid after a call to `finish_384`, meaning the user may feed more data into + * the hash via `update_384`. + */ void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst); -/** -Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 48 bytes. + */ void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst); diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h index b6e3e015294d3..7ecb4db961767 100644 --- a/crypto/hacl_lib.h +++ b/crypto/hacl_lib.h @@ -30,8 +30,10 @@ static inline u128 FStar_UInt128_uint64_to_uint128(u64 x) return ((u128)x); } -/* Loads and stores. These avoid undefined behavior due to unaligned memory - * accesses, via memcpy. */ +/* + * Loads and stores. These avoid undefined behavior due to unaligned memory + * accesses, via memcpy. + */ #define load32_be(b) (get_unaligned_be32(b)) #define store32_be(b, i) put_unaligned_be32(i, b); diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index 9f3bfa4824219..a90e1cdc24a9f 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -912,11 +912,11 @@ Hacl_Streaming_SHA2_update_384(struct Hacl_Streaming_MD_state_64_s *p, return update_384_512(p, input, input_len); } -/** -Write the resulting hash into `dst`, an array of 48 bytes. The state remains -valid after a call to `finish_384`, meaning the user may feed more data into -the hash via `update_384`. -*/ +/* + * Write the resulting hash into `dst`, an array of 48 bytes. The state remains + * valid after a call to `finish_384`, meaning the user may feed more data into + * the hash via `update_384`. + */ void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) { From 0bf813846dce7780365e17ae5bff5b3e84f4307f Mon Sep 17 00:00:00 2001 From: armfazh Date: Mon, 16 Oct 2023 16:47:46 -0700 Subject: [PATCH 08/18] Adding CRYPTO_SHA2_HACL module. --- zeta/test-artifacts/config-um | 6 ++++++ zeta/test-artifacts/test-script.sh | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/zeta/test-artifacts/config-um b/zeta/test-artifacts/config-um index 06d98e23e21b5..b7c9b183457c6 100644 --- a/zeta/test-artifacts/config-um +++ b/zeta/test-artifacts/config-um @@ -1403,6 +1403,12 @@ CONFIG_CRYPTO_AUTHENC=y CONFIG_CRYPTO_TEST=m # end of Crypto core or helper +# +# HACL implementation +# +CONFIG_CRYPTO_SHA2_HACL=y +# end of HACL implementation + # # Public-key cryptography # diff --git a/zeta/test-artifacts/test-script.sh b/zeta/test-artifacts/test-script.sh index 1ff9b2df6fe9d..3a7b53c6db47d 100755 --- a/zeta/test-artifacts/test-script.sh +++ b/zeta/test-artifacts/test-script.sh @@ -1,5 +1,11 @@ #!/bin/busybox sh +echo "tcrypt: starting CRYPTO_SHA2_HACL" +modprobe tcrypt mode=300 alg=sha224-hacl sec=2 +modprobe tcrypt mode=300 alg=sha256-hacl sec=2 +modprobe tcrypt mode=300 alg=sha384-hacl sec=2 +modprobe tcrypt mode=300 alg=sha512-hacl sec=2 + echo "tcrypt: starting SHA2 (256) test" echo "tcrypt: testing sha256 generic implementation" modprobe tcrypt mode=300 alg=sha256-generic sec=2 From c2998c783091322b8787390932af4168844e5187 Mon Sep 17 00:00:00 2001 From: armfazh Date: Fri, 1 Dec 2023 20:21:00 -0800 Subject: [PATCH 09/18] Set correct version identifier. --- crypto/hacl_hash.h | 1 + crypto/hacl_lib.h | 1 + crypto/sha2-hacl-generated.c | 6 ++++-- crypto/sha2-hacl.c | 6 +++--- 4 files changed, 9 insertions(+), 5 deletions(-) diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index 1e10e54dfd6c2..80d8dd4ef2249 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -1,3 +1,4 @@ +/* SPDX-License-Identifier: GPL-2.0 OR MIT */ /* * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h index 7ecb4db961767..12a9a3c2fcac4 100644 --- a/crypto/hacl_lib.h +++ b/crypto/hacl_lib.h @@ -1,3 +1,4 @@ +/* SPDX-License-Identifier: GPL-2.0 OR MIT */ /* * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index a90e1cdc24a9f..2084b2a19dd62 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -1,9 +1,9 @@ +// SPDX-License-Identifier: GPL-2.0 OR MIT /* - * GPLv2 or MIT License - * * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors * + * This is a formally-verified implementation of SHA-2 produced by HACL*. */ #include "hacl_hash.h" @@ -951,3 +951,5 @@ void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, r, buf_last, tmp_block_state); Hacl_SHA2_Scalar32_sha384_finish(tmp_block_state, dst); } + +MODULE_LICENSE("Dual MIT/GPL"); diff --git a/crypto/sha2-hacl.c b/crypto/sha2-hacl.c index 6400fbce0ae0b..d5339c93949e3 100644 --- a/crypto/sha2-hacl.c +++ b/crypto/sha2-hacl.c @@ -1,8 +1,8 @@ +// SPDX-License-Identifier: GPL-2.0 OR MIT /* - * GPLv2 or MIT License - * * Copyright (c) 2023 Cryspen * + * This is a formally-verified implementation of SHA-2 produced by HACL*. */ #include @@ -178,7 +178,7 @@ static void __exit sha2_hacl_mod_fini(void) subsys_initcall(sha2_hacl_mod_init); module_exit(sha2_hacl_mod_fini); -MODULE_LICENSE("GPLv2 or MIT"); +MODULE_LICENSE("Dual MIT/GPL"); MODULE_DESCRIPTION("Formally Verified SHA-2 Secure Hash Algorithm from HACL*"); MODULE_ALIAS_CRYPTO("sha224"); From 37a16ff66085c4023038b6f21f8066d157e8436c Mon Sep 17 00:00:00 2001 From: armfazh Date: Fri, 1 Dec 2023 20:21:21 -0800 Subject: [PATCH 10/18] Compiles single module from multiple files. --- crypto/Kconfig | 11 ++++++++++- crypto/Makefile | 4 +++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/crypto/Kconfig b/crypto/Kconfig index e35350102a433..d4fd42bc33da8 100644 --- a/crypto/Kconfig +++ b/crypto/Kconfig @@ -1027,11 +1027,20 @@ config CRYPTO_SHA256 Used by the btrfs filesystem, Ceph, NFS, and SMB. config CRYPTO_SHA2_HACL - tristate "SHA-224 and SHA-256 and SHA-384 and SHA-512" + tristate "SHA-2 (HACL*)" select CRYPTO_HASH help SHA-2 secure hash algorithms (FIPS 180, ISO/IEC 10118-3) from HACL* + This is a formally-verified implementation of SHA-2 ported + from the HACL* project. + + This module provides the following algorithms: + - SHA-224 + - SHA-256 + - SHA-384 + - SHA-512 + config CRYPTO_SHA512 tristate "SHA-384 and SHA-512" select CRYPTO_HASH diff --git a/crypto/Makefile b/crypto/Makefile index 2c88f3c8ce4db..d2706951763eb 100644 --- a/crypto/Makefile +++ b/crypto/Makefile @@ -77,7 +77,9 @@ obj-$(CONFIG_CRYPTO_MD5) += md5.o obj-$(CONFIG_CRYPTO_RMD160) += rmd160.o obj-$(CONFIG_CRYPTO_SHA1) += sha1_generic.o obj-$(CONFIG_CRYPTO_SHA256) += sha256_generic.o -obj-$(CONFIG_CRYPTO_SHA2_HACL) += sha2-hacl-generated.o sha2-hacl.o +sha2_hacl-y := sha2-hacl-generated.o +sha2_hacl-y += sha2-hacl.o +obj-$(CONFIG_CRYPTO_SHA2_HACL) += sha2_hacl.o obj-$(CONFIG_CRYPTO_SHA512) += sha512_generic.o obj-$(CONFIG_CRYPTO_SHA3) += sha3_generic.o obj-$(CONFIG_CRYPTO_SM3) += sm3.o From b1d172374779510b68d2eb05a297e23e01b4ab52 Mon Sep 17 00:00:00 2001 From: armfazh Date: Tue, 5 Dec 2023 10:48:36 -0800 Subject: [PATCH 11/18] Loading module manually, so we check whether it loads ok. --- zeta/test-artifacts/config-um | 2 +- zeta/test-artifacts/test-script.sh | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/zeta/test-artifacts/config-um b/zeta/test-artifacts/config-um index b7c9b183457c6..cd8025db42d49 100644 --- a/zeta/test-artifacts/config-um +++ b/zeta/test-artifacts/config-um @@ -1406,7 +1406,7 @@ CONFIG_CRYPTO_TEST=m # # HACL implementation # -CONFIG_CRYPTO_SHA2_HACL=y +CONFIG_CRYPTO_SHA2_HACL=m # end of HACL implementation # diff --git a/zeta/test-artifacts/test-script.sh b/zeta/test-artifacts/test-script.sh index 3a7b53c6db47d..f4777ebbdb3db 100755 --- a/zeta/test-artifacts/test-script.sh +++ b/zeta/test-artifacts/test-script.sh @@ -1,6 +1,7 @@ #!/bin/busybox sh echo "tcrypt: starting CRYPTO_SHA2_HACL" +modprobe sha2-hacl modprobe tcrypt mode=300 alg=sha224-hacl sec=2 modprobe tcrypt mode=300 alg=sha256-hacl sec=2 modprobe tcrypt mode=300 alg=sha384-hacl sec=2 From 376f49921e8e2c89196016b68ec813a4fa3e1cf1 Mon Sep 17 00:00:00 2001 From: armfazh Date: Tue, 5 Dec 2023 15:06:38 -0800 Subject: [PATCH 12/18] Fixing format of documentation strings for SHA2. --- crypto/sha2-hacl-generated.c | 82 ++++++++++++++++++------------------ 1 file changed, 42 insertions(+), 40 deletions(-) diff --git a/crypto/sha2-hacl-generated.c b/crypto/sha2-hacl-generated.c index 2084b2a19dd62..29a7136ed1b6f 100644 --- a/crypto/sha2-hacl-generated.c +++ b/crypto/sha2-hacl-generated.c @@ -191,9 +191,9 @@ void Hacl_SHA2_Scalar32_sha224_finish(uint32_t *st, uint8_t *h) memcpy(h, hbuf, (uint32_t)28U * sizeof(uint8_t)); } -/** -Reset an existing state to the initial hash state with empty data. -*/ +/* + * Reset an existing state to the initial hash state with empty data. + */ void Hacl_Streaming_SHA2_init_256(struct Hacl_Streaming_MD_state_32_s *s) { @@ -347,13 +347,13 @@ update_224_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *data, return Hacl_Streaming_Types_Success; } -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_256` -(since the last call to `init_256`) exceeds 2^61-1 bytes. - -This function is identical to the update function for SHA2_224. -*/ +/* + * Feed an arbitrary amount of data into the hash. This function returns 0 for + * success, or 1 if the combined length of all of the data passed to + * `update_256` (since the last call to `init_256`) exceeds 2^61-1 bytes. + * + * This function is identical to the update function for SHA2_224. + */ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *input, uint32_t input_len) @@ -361,12 +361,13 @@ Hacl_Streaming_SHA2_update_256(struct Hacl_Streaming_MD_state_32_s *p, return update_224_256(p, input, input_len); } -/** -Write the resulting hash into `dst`, an array of 32 bytes. The state remains -valid after a call to `finish_256`, meaning the user may feed more data into -the hash via `update_256`. (The finish_256 function operates on an internal copy -of the state and therefore does not invalidate the client-held state `p`.) -*/ +/* + * Write the resulting hash into `dst`, an array of 32 bytes. The state remains + * valid after a call to `finish_256`, meaning the user may feed more data into + * the hash via `update_256`. (The finish_256 function operates on an internal + * copy of the state and therefore does not invalidate the client-held state + * `p`.) + */ void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) { @@ -400,9 +401,9 @@ void Hacl_Streaming_SHA2_finish_256(struct Hacl_Streaming_MD_state_32_s *p, Hacl_SHA2_Scalar32_sha256_finish(tmp_block_state, dst); } -/** -Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 32 bytes. + */ void Hacl_Streaming_SHA2_hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst) { @@ -441,11 +442,11 @@ Hacl_Streaming_SHA2_update_224(struct Hacl_Streaming_MD_state_32_s *p, return update_224_256(p, input, input_len); } -/** -Write the resulting hash into `dst`, an array of 28 bytes. The state remains -valid after a call to `finish_224`, meaning the user may feed more data into -the hash via `update_224`. -*/ +/* + * Write the resulting hash into `dst`, an array of 28 bytes. The state remains + * valid after a call to `finish_224`, meaning the user may feed more data into + * the hash via `update_224`. + */ void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, uint8_t *dst) { @@ -478,9 +479,9 @@ void Hacl_Streaming_SHA2_finish_224(struct Hacl_Streaming_MD_state_32_s *p, Hacl_SHA2_Scalar32_sha224_finish(tmp_block_state, dst); } -/** -Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. -*/ +/* + * Hash `input`, of len `input_len`, into `dst`, an array of 28 bytes. + */ void Hacl_Streaming_SHA2_hash_224(uint8_t *input, uint32_t input_len, uint8_t *dst) { @@ -836,13 +837,13 @@ update_384_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *data, return Hacl_Streaming_Types_Success; } -/** -Feed an arbitrary amount of data into the hash. This function returns 0 for -success, or 1 if the combined length of all of the data passed to `update_512` -(since the last call to `init_512`) exceeds 2^125-1 bytes. - -This function is identical to the update function for SHA2_384. -*/ +/* + * Feed an arbitrary amount of data into the hash. This function returns 0 for + * success, or 1 if the combined length of all of the data passed to + * `update_512` (since the last call to `init_512`) exceeds 2^125-1 bytes. + * + * This function is identical to the update function for SHA2_384. + */ Hacl_Streaming_Types_error_code Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *input, uint32_t input_len) @@ -850,12 +851,13 @@ Hacl_Streaming_SHA2_update_512(struct Hacl_Streaming_MD_state_64_s *p, return update_384_512(p, input, input_len); } -/** -Write the resulting hash into `dst`, an array of 64 bytes. The state remains -valid after a call to `finish_512`, meaning the user may feed more data into -the hash via `update_512`. (The finish_512 function operates on an internal copy -of the state and therefore does not invalidate the client-held state `p`.) -*/ +/* + * Write the resulting hash into `dst`, an array of 64 bytes. The state remains + * valid after a call to `finish_512`, meaning the user may feed more data into + * the hash via `update_512`. (The finish_512 function operates on an internal + * copy of the state and therefore does not invalidate the client-held state + * `p`.) + */ void Hacl_Streaming_SHA2_finish_512(struct Hacl_Streaming_MD_state_64_s *p, uint8_t *dst) { From d5fd9d312a7b51c66085320df1d2a772f79c79a4 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Tue, 24 Oct 2023 14:53:07 +0200 Subject: [PATCH 13/18] hacl blake2 --- crypto/Kconfig | 17 + crypto/Makefile | 1 + crypto/blake2-hacl-generated.c | 1368 ++++++++++++++++++++++++++++++++ crypto/blake2-hacl.c | 208 +++++ crypto/hacl_hash.h | 125 +++ crypto/hacl_lib.h | 22 + 6 files changed, 1741 insertions(+) create mode 100644 crypto/blake2-hacl-generated.c create mode 100644 crypto/blake2-hacl.c diff --git a/crypto/Kconfig b/crypto/Kconfig index d4fd42bc33da8..1bd9aa2341cce 100644 --- a/crypto/Kconfig +++ b/crypto/Kconfig @@ -921,6 +921,23 @@ config CRYPTO_BLAKE2B See https://blake2.net for further information. +config CRYPTO_BLAKE2_HACL + tristate "HACL Blake2" + select CRYPTO_HASH + help + BLAKE2 cryptographic hash function (RFC 7693) + + This is a formally verified implementation of BLAKE2s and BLAKE2b, ported + from the HACL* project. + + This module provides the following algorithms: + - blake2b-160 + - blake2b-256 + - blake2b-384 + - blake2b-512 + - blake2s-160 + - blake2s-256 + config CRYPTO_CMAC tristate "CMAC (Cipher-based MAC)" select CRYPTO_HASH diff --git a/crypto/Makefile b/crypto/Makefile index d2706951763eb..19fbbfac8a498 100644 --- a/crypto/Makefile +++ b/crypto/Makefile @@ -89,6 +89,7 @@ obj-$(CONFIG_CRYPTO_WP512) += wp512.o CFLAGS_wp512.o := $(call cc-option,-fno-schedule-insns) # https://gcc.gnu.org/bugzilla/show_bug.cgi?id=79149 obj-$(CONFIG_CRYPTO_BLAKE2B) += blake2b_generic.o CFLAGS_blake2b_generic.o := -Wframe-larger-than=4096 # https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105930 +obj-$(CONFIG_CRYPTO_BLAKE2_HACL) += blake2-hacl.o blake2-hacl-generated.o obj-$(CONFIG_CRYPTO_ECB) += ecb.o obj-$(CONFIG_CRYPTO_CBC) += cbc.o obj-$(CONFIG_CRYPTO_CFB) += cfb.o diff --git a/crypto/blake2-hacl-generated.c b/crypto/blake2-hacl-generated.c new file mode 100644 index 0000000000000..3c8289b37baad --- /dev/null +++ b/crypto/blake2-hacl-generated.c @@ -0,0 +1,1368 @@ +/* + * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation + * Copyright (c) 2022-2023 HACL* Contributors + * Copyright (c) 2023 Cryspen + */ + +#include "hacl_hash.h" +#include "hacl_lib.h" + +static void blake2b_update_block(uint64_t *wv, uint64_t *hash, bool flag, + FStar_UInt128_uint128 totlen, uint8_t *d) +{ + uint64_t m_w[16U] = { 0U }; + KRML_MAYBE_FOR16(i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint64_t *os = m_w; + uint8_t *bj = d + i * (uint32_t)8U; + uint64_t u = load64_le(bj); uint64_t r = u; + uint64_t x = r; os[i] = x;); + uint64_t mask[4U] = { 0U }; + uint64_t wv_14; + if (flag) { + wv_14 = (uint64_t)0xFFFFFFFFFFFFFFFFU; + } else { + wv_14 = (uint64_t)0U; + } + uint64_t wv_15 = (uint64_t)0U; + mask[0U] = FStar_UInt128_uint128_to_uint64(totlen); + mask[1U] = FStar_UInt128_uint128_to_uint64( + FStar_UInt128_shift_right(totlen, (uint32_t)64U)); + mask[2U] = wv_14; + mask[3U] = wv_15; + memcpy(wv, hash, (uint32_t)16U * sizeof(uint64_t)); + uint64_t *wv3 = wv + (uint32_t)12U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv3; + uint64_t x = wv3[i] ^ mask[i]; os[i] = x;); + KRML_MAYBE_FOR12( + i0, (uint32_t)0U, (uint32_t)12U, (uint32_t)1U, + uint32_t start_idx = i0 % (uint32_t)10U * (uint32_t)16U; + uint64_t m_st[16U] = { 0U }; uint64_t *r0 = m_st; + uint64_t *r1 = m_st + (uint32_t)4U; + uint64_t *r20 = m_st + (uint32_t)8U; + uint64_t *r30 = m_st + (uint32_t)12U; + uint32_t s0 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)0U]; + uint32_t s1 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)1U]; + uint32_t s2 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)2U]; + uint32_t s3 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)3U]; + uint32_t s4 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)4U]; + uint32_t s5 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)5U]; + uint32_t s6 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)6U]; + uint32_t s7 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)7U]; + uint32_t s8 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)8U]; + uint32_t s9 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)9U]; + uint32_t s10 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)10U]; + uint32_t s11 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)11U]; + uint32_t s12 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)12U]; + uint32_t s13 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)13U]; + uint32_t s14 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)14U]; + uint32_t s15 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)15U]; + uint64_t uu____0 = m_w[s2]; uint64_t uu____1 = m_w[s4]; + uint64_t uu____2 = m_w[s6]; r0[0U] = m_w[s0]; r0[1U] = uu____0; + r0[2U] = uu____1; r0[3U] = uu____2; uint64_t uu____3 = m_w[s3]; + uint64_t uu____4 = m_w[s5]; uint64_t uu____5 = m_w[s7]; + r1[0U] = m_w[s1]; r1[1U] = uu____3; r1[2U] = uu____4; + r1[3U] = uu____5; uint64_t uu____6 = m_w[s10]; + uint64_t uu____7 = m_w[s12]; uint64_t uu____8 = m_w[s14]; + r20[0U] = m_w[s8]; r20[1U] = uu____6; r20[2U] = uu____7; + r20[3U] = uu____8; uint64_t uu____9 = m_w[s11]; + uint64_t uu____10 = m_w[s13]; uint64_t uu____11 = m_w[s15]; + r30[0U] = m_w[s9]; r30[1U] = uu____9; r30[2U] = uu____10; + r30[3U] = uu____11; uint64_t *x = m_st; + uint64_t *y = m_st + (uint32_t)4U; + uint64_t *z = m_st + (uint32_t)8U; + uint64_t *w = m_st + (uint32_t)12U; uint32_t a = (uint32_t)0U; + uint32_t b0 = (uint32_t)1U; uint32_t c0 = (uint32_t)2U; + uint32_t d10 = (uint32_t)3U; + uint64_t *wv_a0 = wv + a * (uint32_t)4U; + uint64_t *wv_b0 = wv + b0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a0; + uint64_t x1 = wv_a0[i] + wv_b0[i]; os[i] = x1;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a0; + uint64_t x1 = wv_a0[i] + x[i]; os[i] = x1;); + uint64_t *wv_a1 = wv + d10 * (uint32_t)4U; + uint64_t *wv_b1 = wv + a * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a1; + uint64_t x1 = wv_a1[i] ^ wv_b1[i]; os[i] = x1;); + uint64_t *r10 = wv_a1; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = r10; + uint64_t x1 = r10[i]; + uint64_t x10 = x1 >> (uint32_t)32U | + x1 << (uint32_t)32U; + os[i] = x10;); + uint64_t *wv_a2 = wv + c0 * (uint32_t)4U; + uint64_t *wv_b2 = wv + d10 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a2; + uint64_t x1 = wv_a2[i] + wv_b2[i]; os[i] = x1;); + uint64_t *wv_a3 = wv + b0 * (uint32_t)4U; + uint64_t *wv_b3 = wv + c0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a3; + uint64_t x1 = wv_a3[i] ^ wv_b3[i]; os[i] = x1;); + uint64_t *r12 = wv_a3; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = r12; + uint64_t x1 = r12[i]; + uint64_t x10 = x1 >> (uint32_t)24U | + x1 << (uint32_t)40U; + os[i] = x10;); + uint64_t *wv_a4 = wv + a * (uint32_t)4U; + uint64_t *wv_b4 = wv + b0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a4; + uint64_t x1 = wv_a4[i] + wv_b4[i]; os[i] = x1;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a4; + uint64_t x1 = wv_a4[i] + y[i]; os[i] = x1;); + uint64_t *wv_a5 = wv + d10 * (uint32_t)4U; + uint64_t *wv_b5 = wv + a * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a5; + uint64_t x1 = wv_a5[i] ^ wv_b5[i]; os[i] = x1;); + uint64_t *r13 = wv_a5; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = r13; + uint64_t x1 = r13[i]; + uint64_t x10 = x1 >> (uint32_t)16U | + x1 << (uint32_t)48U; + os[i] = x10;); + uint64_t *wv_a6 = wv + c0 * (uint32_t)4U; + uint64_t *wv_b6 = wv + d10 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a6; + uint64_t x1 = wv_a6[i] + wv_b6[i]; os[i] = x1;); + uint64_t *wv_a7 = wv + b0 * (uint32_t)4U; + uint64_t *wv_b7 = wv + c0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a7; + uint64_t x1 = wv_a7[i] ^ wv_b7[i]; os[i] = x1;); + uint64_t *r14 = wv_a7; KRML_MAYBE_FOR4( + i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = r14; + uint64_t x1 = r14[i]; + uint64_t x10 = x1 >> (uint32_t)63U | x1 << (uint32_t)1U; + os[i] = x10;); + uint64_t *r15 = wv + (uint32_t)4U; + uint64_t *r21 = wv + (uint32_t)8U; + uint64_t *r31 = wv + (uint32_t)12U; uint64_t *r110 = r15; + uint64_t x00 = r110[1U]; uint64_t x10 = r110[2U]; + uint64_t x20 = r110[3U]; uint64_t x30 = r110[0U]; + r110[0U] = x00; r110[1U] = x10; r110[2U] = x20; r110[3U] = x30; + uint64_t *r111 = r21; uint64_t x01 = r111[2U]; + uint64_t x11 = r111[3U]; uint64_t x21 = r111[0U]; + uint64_t x31 = r111[1U]; r111[0U] = x01; r111[1U] = x11; + r111[2U] = x21; r111[3U] = x31; uint64_t *r112 = r31; + uint64_t x02 = r112[3U]; uint64_t x12 = r112[0U]; + uint64_t x22 = r112[1U]; uint64_t x32 = r112[2U]; + r112[0U] = x02; r112[1U] = x12; r112[2U] = x22; r112[3U] = x32; + uint32_t a0 = (uint32_t)0U; uint32_t b = (uint32_t)1U; + uint32_t c = (uint32_t)2U; uint32_t d1 = (uint32_t)3U; + uint64_t *wv_a = wv + a0 * (uint32_t)4U; + uint64_t *wv_b8 = wv + b * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a; + uint64_t x1 = wv_a[i] + wv_b8[i]; os[i] = x1;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a; + uint64_t x1 = wv_a[i] + z[i]; os[i] = x1;); + uint64_t *wv_a8 = wv + d1 * (uint32_t)4U; + uint64_t *wv_b9 = wv + a0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a8; + uint64_t x1 = wv_a8[i] ^ wv_b9[i]; os[i] = x1;); + uint64_t *r16 = wv_a8; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = r16; + uint64_t x1 = r16[i]; + uint64_t x13 = x1 >> (uint32_t)32U | + x1 << (uint32_t)32U; + os[i] = x13;); + uint64_t *wv_a9 = wv + c * (uint32_t)4U; + uint64_t *wv_b10 = wv + d1 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a9; + uint64_t x1 = wv_a9[i] + wv_b10[i]; + os[i] = x1;); + uint64_t *wv_a10 = wv + b * (uint32_t)4U; + uint64_t *wv_b11 = wv + c * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a10; + uint64_t x1 = wv_a10[i] ^ wv_b11[i]; + os[i] = x1;); + uint64_t *r17 = wv_a10; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = r17; + uint64_t x1 = r17[i]; + uint64_t x13 = x1 >> (uint32_t)24U | + x1 << (uint32_t)40U; + os[i] = x13;); + uint64_t *wv_a11 = wv + a0 * (uint32_t)4U; + uint64_t *wv_b12 = wv + b * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a11; + uint64_t x1 = wv_a11[i] + wv_b12[i]; + os[i] = x1;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a11; + uint64_t x1 = wv_a11[i] + w[i]; os[i] = x1;); + uint64_t *wv_a12 = wv + d1 * (uint32_t)4U; + uint64_t *wv_b13 = wv + a0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a12; + uint64_t x1 = wv_a12[i] ^ wv_b13[i]; + os[i] = x1;); + uint64_t *r18 = wv_a12; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = r18; + uint64_t x1 = r18[i]; + uint64_t x13 = x1 >> (uint32_t)16U | + x1 << (uint32_t)48U; + os[i] = x13;); + uint64_t *wv_a13 = wv + c * (uint32_t)4U; + uint64_t *wv_b14 = wv + d1 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a13; + uint64_t x1 = wv_a13[i] + wv_b14[i]; + os[i] = x1;); + uint64_t *wv_a14 = wv + b * (uint32_t)4U; + uint64_t *wv_b = wv + c * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = wv_a14; + uint64_t x1 = wv_a14[i] ^ wv_b[i]; os[i] = x1;); + uint64_t *r19 = wv_a14; KRML_MAYBE_FOR4( + i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = r19; + uint64_t x1 = r19[i]; + uint64_t x13 = x1 >> (uint32_t)63U | x1 << (uint32_t)1U; + os[i] = x13;); + uint64_t *r113 = wv + (uint32_t)4U; + uint64_t *r2 = wv + (uint32_t)8U; + uint64_t *r3 = wv + (uint32_t)12U; uint64_t *r11 = r113; + uint64_t x03 = r11[3U]; uint64_t x13 = r11[0U]; + uint64_t x23 = r11[1U]; uint64_t x33 = r11[2U]; r11[0U] = x03; + r11[1U] = x13; r11[2U] = x23; r11[3U] = x33; + uint64_t *r114 = r2; uint64_t x04 = r114[2U]; + uint64_t x14 = r114[3U]; uint64_t x24 = r114[0U]; + uint64_t x34 = r114[1U]; r114[0U] = x04; r114[1U] = x14; + r114[2U] = x24; r114[3U] = x34; uint64_t *r115 = r3; + uint64_t x0 = r115[1U]; uint64_t x1 = r115[2U]; + uint64_t x2 = r115[3U]; uint64_t x3 = r115[0U]; r115[0U] = x0; + r115[1U] = x1; r115[2U] = x2; r115[3U] = x3;); + uint64_t *s0 = hash; + uint64_t *s1 = hash + (uint32_t)4U; + uint64_t *r0 = wv; + uint64_t *r1 = wv + (uint32_t)4U; + uint64_t *r2 = wv + (uint32_t)8U; + uint64_t *r3 = wv + (uint32_t)12U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = s0; + uint64_t x = s0[i] ^ r0[i]; os[i] = x;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = s0; + uint64_t x = s0[i] ^ r2[i]; os[i] = x;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = s1; + uint64_t x = s1[i] ^ r1[i]; os[i] = x;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint64_t *os = s1; + uint64_t x = s1[i] ^ r3[i]; os[i] = x;); +} + +void Hacl_Blake2b_32_blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn) +{ + uint64_t *r0 = hash; + uint64_t *r1 = hash + (uint32_t)4U; + uint64_t *r2 = hash + (uint32_t)8U; + uint64_t *r3 = hash + (uint32_t)12U; + uint64_t iv0 = Hacl_Impl_Blake2_Constants_ivTable_B[0U]; + uint64_t iv1 = Hacl_Impl_Blake2_Constants_ivTable_B[1U]; + uint64_t iv2 = Hacl_Impl_Blake2_Constants_ivTable_B[2U]; + uint64_t iv3 = Hacl_Impl_Blake2_Constants_ivTable_B[3U]; + uint64_t iv4 = Hacl_Impl_Blake2_Constants_ivTable_B[4U]; + uint64_t iv5 = Hacl_Impl_Blake2_Constants_ivTable_B[5U]; + uint64_t iv6 = Hacl_Impl_Blake2_Constants_ivTable_B[6U]; + uint64_t iv7 = Hacl_Impl_Blake2_Constants_ivTable_B[7U]; + r2[0U] = iv0; + r2[1U] = iv1; + r2[2U] = iv2; + r2[3U] = iv3; + r3[0U] = iv4; + r3[1U] = iv5; + r3[2U] = iv6; + r3[3U] = iv7; + uint64_t kk_shift_8 = (uint64_t)kk << (uint32_t)8U; + uint64_t iv0_ = iv0 ^ + ((uint64_t)0x01010000U ^ (kk_shift_8 ^ (uint64_t)nn)); + r0[0U] = iv0_; + r0[1U] = iv1; + r0[2U] = iv2; + r0[3U] = iv3; + r1[0U] = iv4; + r1[1U] = iv5; + r1[2U] = iv6; + r1[3U] = iv7; +} + +void Hacl_Blake2b_32_blake2b_update_key(uint64_t *wv, uint64_t *hash, + uint32_t kk, uint8_t *k, uint32_t ll) +{ + FStar_UInt128_uint128 lb = + FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U); + uint8_t b[128U] = { 0U }; + memcpy(b, k, kk * sizeof(uint8_t)); + if (ll == (uint32_t)0U) { + blake2b_update_block(wv, hash, true, lb, b); + } else { + blake2b_update_block(wv, hash, false, lb, b); + } + Lib_Memzero0_memzero(b, (uint32_t)128U, uint8_t); +} + +void Hacl_Blake2b_32_blake2b_update_multi(uint32_t len, uint64_t *wv, + uint64_t *hash, + FStar_UInt128_uint128 prev, + uint8_t *blocks, uint32_t nb) +{ + for (uint32_t i = (uint32_t)0U; i < nb; i++) { + FStar_UInt128_uint128 totlen = FStar_UInt128_add_mod( + prev, FStar_UInt128_uint64_to_uint128( + (uint64_t)((i + (uint32_t)1U) * + (uint32_t)128U))); + uint8_t *b = blocks + i * (uint32_t)128U; + blake2b_update_block(wv, hash, false, totlen, b); + } +} + +void Hacl_Blake2b_32_blake2b_update_last(uint32_t len, uint64_t *wv, + uint64_t *hash, + FStar_UInt128_uint128 prev, + uint32_t rem, uint8_t *d) +{ + uint8_t b[128U] = { 0U }; + uint8_t *last = d + len - rem; + memcpy(b, last, rem * sizeof(uint8_t)); + FStar_UInt128_uint128 totlen = FStar_UInt128_add_mod( + prev, FStar_UInt128_uint64_to_uint128((uint64_t)len)); + blake2b_update_block(wv, hash, true, totlen, b); + Lib_Memzero0_memzero(b, (uint32_t)128U, uint8_t); +} + +static void blake2b_update_blocks(uint32_t len, uint64_t *wv, uint64_t *hash, + FStar_UInt128_uint128 prev, uint8_t *blocks) +{ + uint32_t nb0 = len / (uint32_t)128U; + uint32_t rem0 = len % (uint32_t)128U; + struct K___uint32_t_uint32_t_s scrut; + if (rem0 == (uint32_t)0U && nb0 > (uint32_t)0U) { + uint32_t nb_ = nb0 - (uint32_t)1U; + uint32_t rem_ = (uint32_t)128U; + scrut = ((struct K___uint32_t_uint32_t_s){ .fst = nb_, + .snd = rem_ }); + } else { + scrut = ((struct K___uint32_t_uint32_t_s){ .fst = nb0, + .snd = rem0 }); + } + uint32_t nb = scrut.fst; + uint32_t rem = scrut.snd; + Hacl_Blake2b_32_blake2b_update_multi(len, wv, hash, prev, blocks, nb); + Hacl_Blake2b_32_blake2b_update_last(len, wv, hash, prev, rem, blocks); +} + +static inline void blake2b_update(uint64_t *wv, uint64_t *hash, uint32_t kk, + uint8_t *k, uint32_t ll, uint8_t *d) +{ + FStar_UInt128_uint128 lb = + FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)128U); + if (kk > (uint32_t)0U) { + Hacl_Blake2b_32_blake2b_update_key(wv, hash, kk, k, ll); + if (!(ll == (uint32_t)0U)) { + blake2b_update_blocks(ll, wv, hash, lb, d); + return; + } + return; + } + blake2b_update_blocks( + ll, wv, hash, + FStar_UInt128_uint64_to_uint128((uint64_t)(uint32_t)0U), d); +} + +void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, + uint64_t *hash) +{ + uint8_t b[64U] = { 0U }; + uint8_t *first = b; + uint8_t *second = b + (uint32_t)32U; + uint64_t *row0 = hash; + uint64_t *row1 = hash + (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + store64_le(first + i * (uint32_t)8U, row0[i]);); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + store64_le(second + i * (uint32_t)8U, row1[i]);); + uint8_t *final = b; + memcpy(output, final, nn * sizeof(uint8_t)); + Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t); +} + +/** +Write the BLAKE2b digest of message `d` using key `k` into `output`. + +@param nn Length of the to-be-generated digest with 1 <= `nn` <= 64. +@param output Pointer to `nn` bytes of memory where the digest is written to. +@param ll Length of the input message. +@param d Pointer to `ll` bytes of memory where the input message is read from. +@param kk Length of the key. Can be 0. +@param k Pointer to `kk` bytes of memory where the key is read from. +*/ +void Hacl_Blake2b_32_blake2b(uint32_t nn, uint8_t *output, uint32_t ll, + uint8_t *d, uint32_t kk, uint8_t *k) +{ + uint64_t b[16U] = { 0U }; + uint64_t b1[16U] = { 0U }; + Hacl_Blake2b_32_blake2b_init(b, kk, nn); + blake2b_update(b1, b, kk, k, ll, d); + Hacl_Blake2b_32_blake2b_finish(nn, output, b); + Lib_Memzero0_memzero(b1, (uint32_t)16U, uint64_t); + Lib_Memzero0_memzero(b, (uint32_t)16U, uint64_t); +} + +static inline void blake2s_update_block(uint32_t *wv, uint32_t *hash, bool flag, + uint64_t totlen, uint8_t *d) +{ + uint32_t m_w[16U] = { 0U }; + KRML_MAYBE_FOR16(i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, + uint32_t *os = m_w; + uint8_t *bj = d + i * (uint32_t)4U; + uint32_t u = load32_le(bj); uint32_t r = u; + uint32_t x = r; os[i] = x;); + uint32_t mask[4U] = { 0U }; + uint32_t wv_14; + if (flag) { + wv_14 = (uint32_t)0xFFFFFFFFU; + } else { + wv_14 = (uint32_t)0U; + } + uint32_t wv_15 = (uint32_t)0U; + mask[0U] = (uint32_t)totlen; + mask[1U] = (uint32_t)(totlen >> (uint32_t)32U); + mask[2U] = wv_14; + mask[3U] = wv_15; + memcpy(wv, hash, (uint32_t)16U * sizeof(uint32_t)); + uint32_t *wv3 = wv + (uint32_t)12U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv3; + uint32_t x = wv3[i] ^ mask[i]; os[i] = x;); + KRML_MAYBE_FOR10( + i0, (uint32_t)0U, (uint32_t)10U, (uint32_t)1U, + uint32_t start_idx = i0 % (uint32_t)10U * (uint32_t)16U; + uint32_t m_st[16U] = { 0U }; uint32_t *r0 = m_st; + uint32_t *r1 = m_st + (uint32_t)4U; + uint32_t *r20 = m_st + (uint32_t)8U; + uint32_t *r30 = m_st + (uint32_t)12U; + uint32_t s0 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)0U]; + uint32_t s1 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)1U]; + uint32_t s2 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)2U]; + uint32_t s3 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)3U]; + uint32_t s4 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)4U]; + uint32_t s5 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)5U]; + uint32_t s6 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)6U]; + uint32_t s7 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)7U]; + uint32_t s8 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)8U]; + uint32_t s9 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)9U]; + uint32_t s10 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)10U]; + uint32_t s11 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)11U]; + uint32_t s12 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)12U]; + uint32_t s13 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)13U]; + uint32_t s14 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)14U]; + uint32_t s15 = + Hacl_Impl_Blake2_Constants_sigmaTable[start_idx + + (uint32_t)15U]; + uint32_t uu____0 = m_w[s2]; uint32_t uu____1 = m_w[s4]; + uint32_t uu____2 = m_w[s6]; r0[0U] = m_w[s0]; r0[1U] = uu____0; + r0[2U] = uu____1; r0[3U] = uu____2; uint32_t uu____3 = m_w[s3]; + uint32_t uu____4 = m_w[s5]; uint32_t uu____5 = m_w[s7]; + r1[0U] = m_w[s1]; r1[1U] = uu____3; r1[2U] = uu____4; + r1[3U] = uu____5; uint32_t uu____6 = m_w[s10]; + uint32_t uu____7 = m_w[s12]; uint32_t uu____8 = m_w[s14]; + r20[0U] = m_w[s8]; r20[1U] = uu____6; r20[2U] = uu____7; + r20[3U] = uu____8; uint32_t uu____9 = m_w[s11]; + uint32_t uu____10 = m_w[s13]; uint32_t uu____11 = m_w[s15]; + r30[0U] = m_w[s9]; r30[1U] = uu____9; r30[2U] = uu____10; + r30[3U] = uu____11; uint32_t *x = m_st; + uint32_t *y = m_st + (uint32_t)4U; + uint32_t *z = m_st + (uint32_t)8U; + uint32_t *w = m_st + (uint32_t)12U; uint32_t a = (uint32_t)0U; + uint32_t b0 = (uint32_t)1U; uint32_t c0 = (uint32_t)2U; + uint32_t d10 = (uint32_t)3U; + uint32_t *wv_a0 = wv + a * (uint32_t)4U; + uint32_t *wv_b0 = wv + b0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a0; + uint32_t x1 = wv_a0[i] + wv_b0[i]; os[i] = x1;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a0; + uint32_t x1 = wv_a0[i] + x[i]; os[i] = x1;); + uint32_t *wv_a1 = wv + d10 * (uint32_t)4U; + uint32_t *wv_b1 = wv + a * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a1; + uint32_t x1 = wv_a1[i] ^ wv_b1[i]; os[i] = x1;); + uint32_t *r10 = wv_a1; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = r10; + uint32_t x1 = r10[i]; + uint32_t x10 = x1 >> (uint32_t)16U | + x1 << (uint32_t)16U; + os[i] = x10;); + uint32_t *wv_a2 = wv + c0 * (uint32_t)4U; + uint32_t *wv_b2 = wv + d10 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a2; + uint32_t x1 = wv_a2[i] + wv_b2[i]; os[i] = x1;); + uint32_t *wv_a3 = wv + b0 * (uint32_t)4U; + uint32_t *wv_b3 = wv + c0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a3; + uint32_t x1 = wv_a3[i] ^ wv_b3[i]; os[i] = x1;); + uint32_t *r12 = wv_a3; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = r12; + uint32_t x1 = r12[i]; + uint32_t x10 = x1 >> (uint32_t)12U | + x1 << (uint32_t)20U; + os[i] = x10;); + uint32_t *wv_a4 = wv + a * (uint32_t)4U; + uint32_t *wv_b4 = wv + b0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a4; + uint32_t x1 = wv_a4[i] + wv_b4[i]; os[i] = x1;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a4; + uint32_t x1 = wv_a4[i] + y[i]; os[i] = x1;); + uint32_t *wv_a5 = wv + d10 * (uint32_t)4U; + uint32_t *wv_b5 = wv + a * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a5; + uint32_t x1 = wv_a5[i] ^ wv_b5[i]; os[i] = x1;); + uint32_t *r13 = wv_a5; KRML_MAYBE_FOR4( + i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = r13; + uint32_t x1 = r13[i]; + uint32_t x10 = x1 >> (uint32_t)8U | x1 << (uint32_t)24U; + os[i] = x10;); + uint32_t *wv_a6 = wv + c0 * (uint32_t)4U; + uint32_t *wv_b6 = wv + d10 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a6; + uint32_t x1 = wv_a6[i] + wv_b6[i]; os[i] = x1;); + uint32_t *wv_a7 = wv + b0 * (uint32_t)4U; + uint32_t *wv_b7 = wv + c0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a7; + uint32_t x1 = wv_a7[i] ^ wv_b7[i]; os[i] = x1;); + uint32_t *r14 = wv_a7; KRML_MAYBE_FOR4( + i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = r14; + uint32_t x1 = r14[i]; + uint32_t x10 = x1 >> (uint32_t)7U | x1 << (uint32_t)25U; + os[i] = x10;); + uint32_t *r15 = wv + (uint32_t)4U; + uint32_t *r21 = wv + (uint32_t)8U; + uint32_t *r31 = wv + (uint32_t)12U; uint32_t *r110 = r15; + uint32_t x00 = r110[1U]; uint32_t x10 = r110[2U]; + uint32_t x20 = r110[3U]; uint32_t x30 = r110[0U]; + r110[0U] = x00; r110[1U] = x10; r110[2U] = x20; r110[3U] = x30; + uint32_t *r111 = r21; uint32_t x01 = r111[2U]; + uint32_t x11 = r111[3U]; uint32_t x21 = r111[0U]; + uint32_t x31 = r111[1U]; r111[0U] = x01; r111[1U] = x11; + r111[2U] = x21; r111[3U] = x31; uint32_t *r112 = r31; + uint32_t x02 = r112[3U]; uint32_t x12 = r112[0U]; + uint32_t x22 = r112[1U]; uint32_t x32 = r112[2U]; + r112[0U] = x02; r112[1U] = x12; r112[2U] = x22; r112[3U] = x32; + uint32_t a0 = (uint32_t)0U; uint32_t b = (uint32_t)1U; + uint32_t c = (uint32_t)2U; uint32_t d1 = (uint32_t)3U; + uint32_t *wv_a = wv + a0 * (uint32_t)4U; + uint32_t *wv_b8 = wv + b * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a; + uint32_t x1 = wv_a[i] + wv_b8[i]; os[i] = x1;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a; + uint32_t x1 = wv_a[i] + z[i]; os[i] = x1;); + uint32_t *wv_a8 = wv + d1 * (uint32_t)4U; + uint32_t *wv_b9 = wv + a0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a8; + uint32_t x1 = wv_a8[i] ^ wv_b9[i]; os[i] = x1;); + uint32_t *r16 = wv_a8; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = r16; + uint32_t x1 = r16[i]; + uint32_t x13 = x1 >> (uint32_t)16U | + x1 << (uint32_t)16U; + os[i] = x13;); + uint32_t *wv_a9 = wv + c * (uint32_t)4U; + uint32_t *wv_b10 = wv + d1 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a9; + uint32_t x1 = wv_a9[i] + wv_b10[i]; + os[i] = x1;); + uint32_t *wv_a10 = wv + b * (uint32_t)4U; + uint32_t *wv_b11 = wv + c * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a10; + uint32_t x1 = wv_a10[i] ^ wv_b11[i]; + os[i] = x1;); + uint32_t *r17 = wv_a10; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = r17; + uint32_t x1 = r17[i]; + uint32_t x13 = x1 >> (uint32_t)12U | + x1 << (uint32_t)20U; + os[i] = x13;); + uint32_t *wv_a11 = wv + a0 * (uint32_t)4U; + uint32_t *wv_b12 = wv + b * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a11; + uint32_t x1 = wv_a11[i] + wv_b12[i]; + os[i] = x1;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a11; + uint32_t x1 = wv_a11[i] + w[i]; os[i] = x1;); + uint32_t *wv_a12 = wv + d1 * (uint32_t)4U; + uint32_t *wv_b13 = wv + a0 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a12; + uint32_t x1 = wv_a12[i] ^ wv_b13[i]; + os[i] = x1;); + uint32_t *r18 = wv_a12; KRML_MAYBE_FOR4( + i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = r18; + uint32_t x1 = r18[i]; + uint32_t x13 = x1 >> (uint32_t)8U | x1 << (uint32_t)24U; + os[i] = x13;); + uint32_t *wv_a13 = wv + c * (uint32_t)4U; + uint32_t *wv_b14 = wv + d1 * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a13; + uint32_t x1 = wv_a13[i] + wv_b14[i]; + os[i] = x1;); + uint32_t *wv_a14 = wv + b * (uint32_t)4U; + uint32_t *wv_b = wv + c * (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = wv_a14; + uint32_t x1 = wv_a14[i] ^ wv_b[i]; os[i] = x1;); + uint32_t *r19 = wv_a14; KRML_MAYBE_FOR4( + i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = r19; + uint32_t x1 = r19[i]; + uint32_t x13 = x1 >> (uint32_t)7U | x1 << (uint32_t)25U; + os[i] = x13;); + uint32_t *r113 = wv + (uint32_t)4U; + uint32_t *r2 = wv + (uint32_t)8U; + uint32_t *r3 = wv + (uint32_t)12U; uint32_t *r11 = r113; + uint32_t x03 = r11[3U]; uint32_t x13 = r11[0U]; + uint32_t x23 = r11[1U]; uint32_t x33 = r11[2U]; r11[0U] = x03; + r11[1U] = x13; r11[2U] = x23; r11[3U] = x33; + uint32_t *r114 = r2; uint32_t x04 = r114[2U]; + uint32_t x14 = r114[3U]; uint32_t x24 = r114[0U]; + uint32_t x34 = r114[1U]; r114[0U] = x04; r114[1U] = x14; + r114[2U] = x24; r114[3U] = x34; uint32_t *r115 = r3; + uint32_t x0 = r115[1U]; uint32_t x1 = r115[2U]; + uint32_t x2 = r115[3U]; uint32_t x3 = r115[0U]; r115[0U] = x0; + r115[1U] = x1; r115[2U] = x2; r115[3U] = x3;); + uint32_t *s0 = hash; + uint32_t *s1 = hash + (uint32_t)4U; + uint32_t *r0 = wv; + uint32_t *r1 = wv + (uint32_t)4U; + uint32_t *r2 = wv + (uint32_t)8U; + uint32_t *r3 = wv + (uint32_t)12U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = s0; + uint32_t x = s0[i] ^ r0[i]; os[i] = x;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = s0; + uint32_t x = s0[i] ^ r2[i]; os[i] = x;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = s1; + uint32_t x = s1[i] ^ r1[i]; os[i] = x;); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + uint32_t *os = s1; + uint32_t x = s1[i] ^ r3[i]; os[i] = x;); +} + +void Hacl_Blake2s_32_blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn) +{ + uint32_t *r0 = hash; + uint32_t *r1 = hash + (uint32_t)4U; + uint32_t *r2 = hash + (uint32_t)8U; + uint32_t *r3 = hash + (uint32_t)12U; + uint32_t iv0 = Hacl_Impl_Blake2_Constants_ivTable_S[0U]; + uint32_t iv1 = Hacl_Impl_Blake2_Constants_ivTable_S[1U]; + uint32_t iv2 = Hacl_Impl_Blake2_Constants_ivTable_S[2U]; + uint32_t iv3 = Hacl_Impl_Blake2_Constants_ivTable_S[3U]; + uint32_t iv4 = Hacl_Impl_Blake2_Constants_ivTable_S[4U]; + uint32_t iv5 = Hacl_Impl_Blake2_Constants_ivTable_S[5U]; + uint32_t iv6 = Hacl_Impl_Blake2_Constants_ivTable_S[6U]; + uint32_t iv7 = Hacl_Impl_Blake2_Constants_ivTable_S[7U]; + r2[0U] = iv0; + r2[1U] = iv1; + r2[2U] = iv2; + r2[3U] = iv3; + r3[0U] = iv4; + r3[1U] = iv5; + r3[2U] = iv6; + r3[3U] = iv7; + uint32_t kk_shift_8 = kk << (uint32_t)8U; + uint32_t iv0_ = iv0 ^ ((uint32_t)0x01010000U ^ (kk_shift_8 ^ nn)); + r0[0U] = iv0_; + r0[1U] = iv1; + r0[2U] = iv2; + r0[3U] = iv3; + r1[0U] = iv4; + r1[1U] = iv5; + r1[2U] = iv6; + r1[3U] = iv7; +} + +void Hacl_Blake2s_32_blake2s_update_key(uint32_t *wv, uint32_t *hash, + uint32_t kk, uint8_t *k, uint32_t ll) +{ + uint64_t lb = (uint64_t)(uint32_t)64U; + uint8_t b[64U] = { 0U }; + memcpy(b, k, kk * sizeof(uint8_t)); + if (ll == (uint32_t)0U) { + blake2s_update_block(wv, hash, true, lb, b); + } else { + blake2s_update_block(wv, hash, false, lb, b); + } + Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t); +} + +void Hacl_Blake2s_32_blake2s_update_multi(uint32_t len, uint32_t *wv, + uint32_t *hash, uint64_t prev, + uint8_t *blocks, uint32_t nb) +{ + for (uint32_t i = (uint32_t)0U; i < nb; i++) { + uint64_t totlen = + prev + (uint64_t)((i + (uint32_t)1U) * (uint32_t)64U); + uint8_t *b = blocks + i * (uint32_t)64U; + blake2s_update_block(wv, hash, false, totlen, b); + } +} + +void Hacl_Blake2s_32_blake2s_update_last(uint32_t len, uint32_t *wv, + uint32_t *hash, uint64_t prev, + uint32_t rem, uint8_t *d) +{ + uint8_t b[64U] = { 0U }; + uint8_t *last = d + len - rem; + memcpy(b, last, rem * sizeof(uint8_t)); + uint64_t totlen = prev + (uint64_t)len; + blake2s_update_block(wv, hash, true, totlen, b); + Lib_Memzero0_memzero(b, (uint32_t)64U, uint8_t); +} + +static void blake2s_update_blocks(uint32_t len, uint32_t *wv, uint32_t *hash, + uint64_t prev, uint8_t *blocks) +{ + uint32_t nb0 = len / (uint32_t)64U; + uint32_t rem0 = len % (uint32_t)64U; + struct K___uint32_t_uint32_t_s scrut; + if (rem0 == (uint32_t)0U && nb0 > (uint32_t)0U) { + uint32_t nb_ = nb0 - (uint32_t)1U; + uint32_t rem_ = (uint32_t)64U; + scrut = ((struct K___uint32_t_uint32_t_s){ .fst = nb_, + .snd = rem_ }); + } else { + scrut = ((struct K___uint32_t_uint32_t_s){ .fst = nb0, + .snd = rem0 }); + } + uint32_t nb = scrut.fst; + uint32_t rem = scrut.snd; + Hacl_Blake2s_32_blake2s_update_multi(len, wv, hash, prev, blocks, nb); + Hacl_Blake2s_32_blake2s_update_last(len, wv, hash, prev, rem, blocks); +} + +static inline void blake2s_update(uint32_t *wv, uint32_t *hash, uint32_t kk, + uint8_t *k, uint32_t ll, uint8_t *d) +{ + uint64_t lb = (uint64_t)(uint32_t)64U; + if (kk > (uint32_t)0U) { + Hacl_Blake2s_32_blake2s_update_key(wv, hash, kk, k, ll); + if (!(ll == (uint32_t)0U)) { + blake2s_update_blocks(ll, wv, hash, lb, d); + return; + } + return; + } + blake2s_update_blocks(ll, wv, hash, (uint64_t)(uint32_t)0U, d); +} + +void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, + uint32_t *hash) +{ + uint8_t b[32U] = { 0U }; + uint8_t *first = b; + uint8_t *second = b + (uint32_t)16U; + uint32_t *row0 = hash; + uint32_t *row1 = hash + (uint32_t)4U; + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + store32_le(first + i * (uint32_t)4U, row0[i]);); + KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, + store32_le(second + i * (uint32_t)4U, row1[i]);); + uint8_t *final = b; + memcpy(output, final, nn * sizeof(uint8_t)); + Lib_Memzero0_memzero(b, (uint32_t)32U, uint8_t); +} + +/** +Write the BLAKE2s digest of message `d` using key `k` into `output`. + +@param nn Length of to-be-generated digest with 1 <= `nn` <= 32. +@param output Pointer to `nn` bytes of memory where the digest is written to. +@param ll Length of the input message. +@param d Pointer to `ll` bytes of memory where the input message is read from. +@param kk Length of the key. Can be 0. +@param k Pointer to `kk` bytes of memory where the key is read from. +*/ +void Hacl_Blake2s_32_blake2s(uint32_t nn, uint8_t *output, uint32_t ll, + uint8_t *d, uint32_t kk, uint8_t *k) +{ + uint32_t b[16U] = { 0U }; + uint32_t b1[16U] = { 0U }; + Hacl_Blake2s_32_blake2s_init(b, kk, nn); + blake2s_update(b1, b, kk, k, ll, d); + Hacl_Blake2s_32_blake2s_finish(nn, output, b); + Lib_Memzero0_memzero(b1, (uint32_t)16U, uint32_t); + Lib_Memzero0_memzero(b, (uint32_t)16U, uint32_t); +} + +/** + (Re-)initialization function when there is no key +*/ +void Hacl_Streaming_Blake2_blake2s_32_no_key_init( + struct Hacl_Streaming_Blake2_blake2s_32_state_s *s1) +{ + struct Hacl_Streaming_Blake2_blake2s_32_state_s scrut = *s1; + uint8_t *buf = scrut.buf; + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s block_state = + scrut.block_state; + KRML_HOST_IGNORE((void *)(uint8_t)0U); + Hacl_Blake2s_32_blake2s_init(block_state.snd, (uint32_t)0U, + (uint32_t)32U); + struct Hacl_Streaming_Blake2_blake2s_32_state_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; + s1[0U] = tmp; +} + +/** + Update function when there is no key; 0 = success, 1 = max length exceeded +*/ +Hacl_Streaming_Types_error_code Hacl_Streaming_Blake2_blake2s_32_no_key_update( + struct Hacl_Streaming_Blake2_blake2s_32_state_s *p, uint8_t *data, + uint32_t len) +{ + struct Hacl_Streaming_Blake2_blake2s_32_state_s s1 = *p; + uint64_t total_len = s1.total_len; + if ((uint64_t)len > (uint64_t)0xffffffffffffffffU - total_len) { + return Hacl_Streaming_Types_MaximumLengthExceeded; + } + uint32_t sz; + if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len > (uint64_t)0U) { + sz = (uint32_t)64U; + } else { + sz = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); + } + if (len <= (uint32_t)64U - sz) { + struct Hacl_Streaming_Blake2_blake2s_32_state_s s2 = *p; + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s + block_state1 = s2.block_state; + uint8_t *buf = s2.buf; + uint64_t total_len1 = s2.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + uint8_t *buf2 = buf + sz1; + memcpy(buf2, data, len * sizeof(uint8_t)); + uint64_t total_len2 = total_len1 + (uint64_t)len; + *p = ((struct Hacl_Streaming_Blake2_blake2s_32_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); + } else if (sz == (uint32_t)0U) { + struct Hacl_Streaming_Blake2_blake2s_32_state_s s2 = *p; + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s + block_state1 = s2.block_state; + uint8_t *buf = s2.buf; + uint64_t total_len1 = s2.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + if (!(sz1 == (uint32_t)0U)) { + uint64_t prevlen = total_len1 - (uint64_t)sz1; + uint32_t *wv = block_state1.fst; + uint32_t *hash = block_state1.snd; + uint32_t nb = (uint32_t)1U; + Hacl_Blake2s_32_blake2s_update_multi( + (uint32_t)64U, wv, hash, prevlen, buf, nb); + } + uint32_t ite; + if ((uint64_t)len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + (uint64_t)len > (uint64_t)0U) { + ite = (uint32_t)64U; + } else { + ite = (uint32_t)((uint64_t)len % + (uint64_t)(uint32_t)64U); + } + uint32_t n_blocks = (len - ite) / (uint32_t)64U; + uint32_t data1_len = n_blocks * (uint32_t)64U; + uint32_t data2_len = len - data1_len; + uint8_t *data1 = data; + uint8_t *data2 = data + data1_len; + uint32_t *wv = block_state1.fst; + uint32_t *hash = block_state1.snd; + uint32_t nb = data1_len / (uint32_t)64U; + Hacl_Blake2s_32_blake2s_update_multi(data1_len, wv, hash, + total_len1, data1, nb); + uint8_t *dst = buf; + memcpy(dst, data2, data2_len * sizeof(uint8_t)); + *p = ((struct Hacl_Streaming_Blake2_blake2s_32_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)len }); + } else { + uint32_t diff = (uint32_t)64U - sz; + uint8_t *data1 = data; + uint8_t *data2 = data + diff; + struct Hacl_Streaming_Blake2_blake2s_32_state_s s2 = *p; + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s + block_state10 = s2.block_state; + uint8_t *buf0 = s2.buf; + uint64_t total_len10 = s2.total_len; + uint32_t sz10; + if (total_len10 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len10 > (uint64_t)0U) { + sz10 = (uint32_t)64U; + } else { + sz10 = (uint32_t)(total_len10 % + (uint64_t)(uint32_t)64U); + } + uint8_t *buf2 = buf0 + sz10; + memcpy(buf2, data1, diff * sizeof(uint8_t)); + uint64_t total_len2 = total_len10 + (uint64_t)diff; + *p = ((struct Hacl_Streaming_Blake2_blake2s_32_state_s){ + .block_state = block_state10, + .buf = buf0, + .total_len = total_len2 }); + struct Hacl_Streaming_Blake2_blake2s_32_state_s s20 = *p; + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s + block_state1 = s20.block_state; + uint8_t *buf = s20.buf; + uint64_t total_len1 = s20.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)64U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)64U); + } + if (!(sz1 == (uint32_t)0U)) { + uint64_t prevlen = total_len1 - (uint64_t)sz1; + uint32_t *wv = block_state1.fst; + uint32_t *hash = block_state1.snd; + uint32_t nb = (uint32_t)1U; + Hacl_Blake2s_32_blake2s_update_multi( + (uint32_t)64U, wv, hash, prevlen, buf, nb); + } + uint32_t ite; + if ((uint64_t)(len - diff) % (uint64_t)(uint32_t)64U == + (uint64_t)0U && + (uint64_t)(len - diff) > (uint64_t)0U) { + ite = (uint32_t)64U; + } else { + ite = (uint32_t)((uint64_t)(len - diff) % + (uint64_t)(uint32_t)64U); + } + uint32_t n_blocks = (len - diff - ite) / (uint32_t)64U; + uint32_t data1_len = n_blocks * (uint32_t)64U; + uint32_t data2_len = len - diff - data1_len; + uint8_t *data11 = data2; + uint8_t *data21 = data2 + data1_len; + uint32_t *wv = block_state1.fst; + uint32_t *hash = block_state1.snd; + uint32_t nb = data1_len / (uint32_t)64U; + Hacl_Blake2s_32_blake2s_update_multi(data1_len, wv, hash, + total_len1, data11, nb); + uint8_t *dst = buf; + memcpy(dst, data21, data2_len * sizeof(uint8_t)); + *p = ((struct Hacl_Streaming_Blake2_blake2s_32_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)(len - diff) }); + } + return Hacl_Streaming_Types_Success; +} + +/** + Finish function when there is no key +*/ +void Hacl_Streaming_Blake2_blake2s_32_no_key_finish( + struct Hacl_Streaming_Blake2_blake2s_32_state_s *p, uint8_t *dst) +{ + struct Hacl_Streaming_Blake2_blake2s_32_state_s scrut = *p; + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s block_state = + scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)64U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)64U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)64U); + } + uint8_t *buf_1 = buf_; + uint32_t wv0[16U] = { 0U }; + uint32_t b[16U] = { 0U }; + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s tmp_block_state = { + .fst = wv0, .snd = b + }; + uint32_t *src_b = block_state.snd; + uint32_t *dst_b = tmp_block_state.snd; + memcpy(dst_b, src_b, (uint32_t)16U * sizeof(uint32_t)); + uint64_t prev_len = total_len - (uint64_t)r; + uint32_t ite; + if (r % (uint32_t)64U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)64U; + } else { + ite = r % (uint32_t)64U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + uint32_t *wv1 = tmp_block_state.fst; + uint32_t *hash0 = tmp_block_state.snd; + uint32_t nb = (uint32_t)0U; + Hacl_Blake2s_32_blake2s_update_multi((uint32_t)0U, wv1, hash0, prev_len, + buf_multi, nb); + uint64_t prev_len_last = total_len - (uint64_t)r; + uint32_t *wv = tmp_block_state.fst; + uint32_t *hash = tmp_block_state.snd; + Hacl_Blake2s_32_blake2s_update_last(r, wv, hash, prev_len_last, r, + buf_last); + Hacl_Blake2s_32_blake2s_finish((uint32_t)32U, dst, tmp_block_state.snd); +} + +/** + (Re)-initialization function when there is no key +*/ +void Hacl_Streaming_Blake2_blake2b_32_no_key_init( + struct Hacl_Streaming_Blake2_blake2b_32_state_s *s1) +{ + struct Hacl_Streaming_Blake2_blake2b_32_state_s scrut = *s1; + uint8_t *buf = scrut.buf; + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s block_state = + scrut.block_state; + KRML_HOST_IGNORE((void *)(uint8_t)0U); + Hacl_Blake2b_32_blake2b_init(block_state.snd, (uint32_t)0U, + (uint32_t)64U); + struct Hacl_Streaming_Blake2_blake2b_32_state_s tmp = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; + s1[0U] = tmp; +} + +/** + Update function when there is no key; 0 = success, 1 = max length exceeded +*/ +Hacl_Streaming_Types_error_code Hacl_Streaming_Blake2_blake2b_32_no_key_update( + struct Hacl_Streaming_Blake2_blake2b_32_state_s *p, uint8_t *data, + uint32_t len) +{ + struct Hacl_Streaming_Blake2_blake2b_32_state_s s1 = *p; + uint64_t total_len = s1.total_len; + if ((uint64_t)len > (uint64_t)0xffffffffffffffffU - total_len) { + return Hacl_Streaming_Types_MaximumLengthExceeded; + } + uint32_t sz; + if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len > (uint64_t)0U) { + sz = (uint32_t)128U; + } else { + sz = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); + } + if (len <= (uint32_t)128U - sz) { + struct Hacl_Streaming_Blake2_blake2b_32_state_s s2 = *p; + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s + block_state1 = s2.block_state; + uint8_t *buf = s2.buf; + uint64_t total_len1 = s2.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + uint8_t *buf2 = buf + sz1; + memcpy(buf2, data, len * sizeof(uint8_t)); + uint64_t total_len2 = total_len1 + (uint64_t)len; + *p = ((struct Hacl_Streaming_Blake2_blake2b_32_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len2 }); + } else if (sz == (uint32_t)0U) { + struct Hacl_Streaming_Blake2_blake2b_32_state_s s2 = *p; + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s + block_state1 = s2.block_state; + uint8_t *buf = s2.buf; + uint64_t total_len1 = s2.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + if (!(sz1 == (uint32_t)0U)) { + uint64_t prevlen = total_len1 - (uint64_t)sz1; + uint64_t *wv = block_state1.fst; + uint64_t *hash = block_state1.snd; + uint32_t nb = (uint32_t)1U; + Hacl_Blake2b_32_blake2b_update_multi( + (uint32_t)128U, wv, hash, + FStar_UInt128_uint64_to_uint128(prevlen), buf, + nb); + } + uint32_t ite; + if ((uint64_t)len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + (uint64_t)len > (uint64_t)0U) { + ite = (uint32_t)128U; + } else { + ite = (uint32_t)((uint64_t)len % + (uint64_t)(uint32_t)128U); + } + uint32_t n_blocks = (len - ite) / (uint32_t)128U; + uint32_t data1_len = n_blocks * (uint32_t)128U; + uint32_t data2_len = len - data1_len; + uint8_t *data1 = data; + uint8_t *data2 = data + data1_len; + uint64_t *wv = block_state1.fst; + uint64_t *hash = block_state1.snd; + uint32_t nb = data1_len / (uint32_t)128U; + Hacl_Blake2b_32_blake2b_update_multi( + data1_len, wv, hash, + FStar_UInt128_uint64_to_uint128(total_len1), data1, nb); + uint8_t *dst = buf; + memcpy(dst, data2, data2_len * sizeof(uint8_t)); + *p = ((struct Hacl_Streaming_Blake2_blake2b_32_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)len }); + } else { + uint32_t diff = (uint32_t)128U - sz; + uint8_t *data1 = data; + uint8_t *data2 = data + diff; + struct Hacl_Streaming_Blake2_blake2b_32_state_s s2 = *p; + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s + block_state10 = s2.block_state; + uint8_t *buf0 = s2.buf; + uint64_t total_len10 = s2.total_len; + uint32_t sz10; + if (total_len10 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len10 > (uint64_t)0U) { + sz10 = (uint32_t)128U; + } else { + sz10 = (uint32_t)(total_len10 % + (uint64_t)(uint32_t)128U); + } + uint8_t *buf2 = buf0 + sz10; + memcpy(buf2, data1, diff * sizeof(uint8_t)); + uint64_t total_len2 = total_len10 + (uint64_t)diff; + *p = ((struct Hacl_Streaming_Blake2_blake2b_32_state_s){ + .block_state = block_state10, + .buf = buf0, + .total_len = total_len2 }); + struct Hacl_Streaming_Blake2_blake2b_32_state_s s20 = *p; + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s + block_state1 = s20.block_state; + uint8_t *buf = s20.buf; + uint64_t total_len1 = s20.total_len; + uint32_t sz1; + if (total_len1 % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len1 > (uint64_t)0U) { + sz1 = (uint32_t)128U; + } else { + sz1 = (uint32_t)(total_len1 % (uint64_t)(uint32_t)128U); + } + if (!(sz1 == (uint32_t)0U)) { + uint64_t prevlen = total_len1 - (uint64_t)sz1; + uint64_t *wv = block_state1.fst; + uint64_t *hash = block_state1.snd; + uint32_t nb = (uint32_t)1U; + Hacl_Blake2b_32_blake2b_update_multi( + (uint32_t)128U, wv, hash, + FStar_UInt128_uint64_to_uint128(prevlen), buf, + nb); + } + uint32_t ite; + if ((uint64_t)(len - diff) % (uint64_t)(uint32_t)128U == + (uint64_t)0U && + (uint64_t)(len - diff) > (uint64_t)0U) { + ite = (uint32_t)128U; + } else { + ite = (uint32_t)((uint64_t)(len - diff) % + (uint64_t)(uint32_t)128U); + } + uint32_t n_blocks = (len - diff - ite) / (uint32_t)128U; + uint32_t data1_len = n_blocks * (uint32_t)128U; + uint32_t data2_len = len - diff - data1_len; + uint8_t *data11 = data2; + uint8_t *data21 = data2 + data1_len; + uint64_t *wv = block_state1.fst; + uint64_t *hash = block_state1.snd; + uint32_t nb = data1_len / (uint32_t)128U; + Hacl_Blake2b_32_blake2b_update_multi( + data1_len, wv, hash, + FStar_UInt128_uint64_to_uint128(total_len1), data11, + nb); + uint8_t *dst = buf; + memcpy(dst, data21, data2_len * sizeof(uint8_t)); + *p = ((struct Hacl_Streaming_Blake2_blake2b_32_state_s){ + .block_state = block_state1, + .buf = buf, + .total_len = total_len1 + (uint64_t)(len - diff) }); + } + return Hacl_Streaming_Types_Success; +} + +/** + Finish function when there is no key +*/ +void Hacl_Streaming_Blake2_blake2b_32_no_key_finish( + struct Hacl_Streaming_Blake2_blake2b_32_state_s *p, uint8_t *dst) +{ + struct Hacl_Streaming_Blake2_blake2b_32_state_s scrut = *p; + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s block_state = + scrut.block_state; + uint8_t *buf_ = scrut.buf; + uint64_t total_len = scrut.total_len; + uint32_t r; + if (total_len % (uint64_t)(uint32_t)128U == (uint64_t)0U && + total_len > (uint64_t)0U) { + r = (uint32_t)128U; + } else { + r = (uint32_t)(total_len % (uint64_t)(uint32_t)128U); + } + uint8_t *buf_1 = buf_; + uint64_t wv0[16U] = { 0U }; + uint64_t b[16U] = { 0U }; + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s tmp_block_state = { + .fst = wv0, .snd = b + }; + uint64_t *src_b = block_state.snd; + uint64_t *dst_b = tmp_block_state.snd; + memcpy(dst_b, src_b, (uint32_t)16U * sizeof(uint64_t)); + uint64_t prev_len = total_len - (uint64_t)r; + uint32_t ite; + if (r % (uint32_t)128U == (uint32_t)0U && r > (uint32_t)0U) { + ite = (uint32_t)128U; + } else { + ite = r % (uint32_t)128U; + } + uint8_t *buf_last = buf_1 + r - ite; + uint8_t *buf_multi = buf_1; + uint64_t *wv1 = tmp_block_state.fst; + uint64_t *hash0 = tmp_block_state.snd; + uint32_t nb = (uint32_t)0U; + Hacl_Blake2b_32_blake2b_update_multi( + (uint32_t)0U, wv1, hash0, + FStar_UInt128_uint64_to_uint128(prev_len), buf_multi, nb); + uint64_t prev_len_last = total_len - (uint64_t)r; + uint64_t *wv = tmp_block_state.fst; + uint64_t *hash = tmp_block_state.snd; + Hacl_Blake2b_32_blake2b_update_last( + r, wv, hash, FStar_UInt128_uint64_to_uint128(prev_len_last), r, + buf_last); + Hacl_Blake2b_32_blake2b_finish((uint32_t)64U, dst, tmp_block_state.snd); +} diff --git a/crypto/blake2-hacl.c b/crypto/blake2-hacl.c new file mode 100644 index 0000000000000..96cadffc8d3f8 --- /dev/null +++ b/crypto/blake2-hacl.c @@ -0,0 +1,208 @@ +/* GPLv2 or MIT License + * + * Copyright (c) 2023 Cryspen + * + */ + +#include +#include +#include + +#include "hacl_hash.h" +#include "hacl_lib.h" + +int hacl_blake2b_init(struct shash_desc *desc) +{ + unsigned int outlen = crypto_shash_digestsize(desc->tfm); + struct Hacl_Streaming_Blake2_blake2b_32_state_s *state = + shash_desc_ctx(desc); + uint8_t *buf = (uint8_t *)kmalloc((uint32_t)128U, sizeof(uint8_t)); + uint64_t *wv = (uint64_t *)kmalloc((uint32_t)16U, sizeof(uint64_t)); + uint64_t *b = (uint64_t *)kmalloc((uint32_t)16U, sizeof(uint64_t)); + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s block_state = { + .fst = wv, .snd = b + }; + struct Hacl_Streaming_Blake2_blake2b_32_state_s s1 = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; + state[0] = s1; + Hacl_Blake2b_32_blake2b_init(block_state.snd, (uint32_t)0U, + (uint32_t)outlen); + return 0; +} +EXPORT_SYMBOL(hacl_blake2b_init); + +int hacl_blake2b_update_generic(struct shash_desc *desc, const u8 *in, + unsigned int inlen) +{ + struct Hacl_Streaming_Blake2_blake2b_32_state_s *sctx = + shash_desc_ctx(desc); + Hacl_Streaming_Blake2_blake2b_32_no_key_update(sctx, (u8 *)in, inlen); + return 0; +} +EXPORT_SYMBOL(hacl_blake2b_update_generic); + +int hacl_blake2b_final_generic(struct shash_desc *desc, u8 *out) +{ + struct Hacl_Streaming_Blake2_blake2b_32_state_s *sctx = + shash_desc_ctx(desc); + Hacl_Streaming_Blake2_blake2b_32_no_key_finish(sctx, out); + struct Hacl_Streaming_Blake2_blake2b_32_state_s scrut = *sctx; + uint8_t *buf = scrut.buf; + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s block_state = + scrut.block_state; + uint64_t *wv = block_state.fst; + uint64_t *b = block_state.snd; + kfree(wv); + kfree(b); + kfree(buf); + return 0; +} +EXPORT_SYMBOL(hacl_blake2b_final_generic); + +#define BLAKE2B_ALG(name, driver_name, digest_size) \ + { \ + .base.cra_name = name, .base.cra_driver_name = driver_name, \ + .base.cra_priority = 100, \ + .base.cra_blocksize = BLAKE2B_BLOCK_SIZE, \ + .base.cra_module = THIS_MODULE, .digestsize = digest_size, \ + .init = hacl_blake2b_init, \ + .update = hacl_blake2b_update_generic, \ + .final = hacl_blake2b_final_generic, \ + .descsize = sizeof( \ + struct Hacl_Streaming_Blake2_blake2b_32_state_s), \ + } + +static struct shash_alg blake2_generic_hacl_algs[] = { + BLAKE2B_ALG("blake2b-160", "blake2b-160-generic-hacl", + BLAKE2B_160_HASH_SIZE), + BLAKE2B_ALG("blake2b-256", "blake2b-256-generic-hacl", + BLAKE2B_256_HASH_SIZE), + BLAKE2B_ALG("blake2b-384", "blake2b-384-generic-hacl", + BLAKE2B_384_HASH_SIZE), + BLAKE2B_ALG("blake2b-512", "blake2b-512-generic-hacl", + BLAKE2B_512_HASH_SIZE), +}; + +static int __init blake2_generic_hacl_mod_init(void) +{ + return crypto_register_shashes(blake2_generic_hacl_algs, + ARRAY_SIZE(blake2_generic_hacl_algs)); +} + +static void __exit blake2_generic_hacl_mod_fini(void) +{ + crypto_unregister_shashes(blake2_generic_hacl_algs, + ARRAY_SIZE(blake2_generic_hacl_algs)); +} + +subsys_initcall(blake2_generic_hacl_mod_init); +module_exit(blake2_generic_hacl_mod_fini); + +MODULE_LICENSE("GPLv2 or MIT"); +MODULE_DESCRIPTION( + "Formally Verified Generic BLAKE2 Secure Hash Algorithm from HACL*"); + +MODULE_ALIAS_CRYPTO("blake2b-160"); +MODULE_ALIAS_CRYPTO("blake2b-160-generic-hacl"); +MODULE_ALIAS_CRYPTO("blake2b-256"); +MODULE_ALIAS_CRYPTO("blake2b-256-generic-hacl"); +MODULE_ALIAS_CRYPTO("blake2b-384"); +MODULE_ALIAS_CRYPTO("blake2b-384-generic-hacl"); +MODULE_ALIAS_CRYPTO("blake2b-512"); +MODULE_ALIAS_CRYPTO("blake2b-512-generic-hacl"); + +int hacl_blake2s_init(struct shash_desc *desc) +{ + unsigned int outlen = crypto_shash_digestsize(desc->tfm); + struct Hacl_Streaming_Blake2_blake2s_32_state_s *state = + shash_desc_ctx(desc); + uint8_t *buf = (uint8_t *)kmalloc((uint32_t)64U, sizeof(uint8_t)); + uint32_t *wv = (uint32_t *)kmalloc((uint32_t)16U, sizeof(uint32_t)); + uint32_t *b = (uint32_t *)kmalloc((uint32_t)16U, sizeof(uint32_t)); + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s block_state = { + .fst = wv, .snd = b + }; + struct Hacl_Streaming_Blake2_blake2s_32_state_s s1 = { + .block_state = block_state, + .buf = buf, + .total_len = (uint64_t)(uint32_t)0U + }; + state[0] = s1; + Hacl_Blake2s_32_blake2s_init(block_state.snd, (uint32_t)0U, + (uint32_t)outlen); + return 0; +} +EXPORT_SYMBOL(hacl_blake2s_init); + +int hacl_blake2s_update_generic(struct shash_desc *desc, const u8 *in, + unsigned int inlen) +{ + struct Hacl_Streaming_Blake2_blake2s_32_state_s *sctx = + shash_desc_ctx(desc); + Hacl_Streaming_Blake2_blake2s_32_no_key_update(sctx, (u8 *)in, inlen); + return 0; +} +EXPORT_SYMBOL(hacl_blake2s_update_generic); + +int hacl_blake2s_final_generic(struct shash_desc *desc, u8 *out) +{ + struct Hacl_Streaming_Blake2_blake2s_32_state_s *sctx = + shash_desc_ctx(desc); + Hacl_Streaming_Blake2_blake2s_32_no_key_finish(sctx, out); + struct Hacl_Streaming_Blake2_blake2s_32_state_s scrut = *sctx; + uint8_t *buf = scrut.buf; + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s block_state = + scrut.block_state; + uint32_t *wv = block_state.fst; + uint32_t *b = block_state.snd; + kfree(wv); + kfree(b); + kfree(buf); + return 0; +} +EXPORT_SYMBOL(hacl_blake2s_final_generic); + +#define BLAKE2S_ALG(name, driver_name, digest_size) \ + { \ + .base.cra_name = name, .base.cra_driver_name = driver_name, \ + .base.cra_priority = 100, \ + .base.cra_blocksize = BLAKE2S_BLOCK_SIZE, \ + .base.cra_module = THIS_MODULE, .digestsize = digest_size, \ + .init = hacl_blake2s_init, \ + .update = hacl_blake2s_update_generic, \ + .final = hacl_blake2s_final_generic, \ + .descsize = sizeof( \ + struct Hacl_Streaming_Blake2_blake2s_32_state_s), \ + } + +static struct shash_alg blake2s_generic_hacl_algs[] = { + BLAKE2S_ALG("blake2s-160", "blake2s-160-generic-hacl", 20), + BLAKE2S_ALG("blake2s-256", "blake2s-256-generic-hacl", 32), +}; + +static int __init blake2s_generic_hacl_mod_init(void) +{ + return crypto_register_shashes(blake2s_generic_hacl_algs, + ARRAY_SIZE(blake2s_generic_hacl_algs)); +} + +static void __exit blake2s_generic_hacl_mod_fini(void) +{ + crypto_unregister_shashes(blake2s_generic_hacl_algs, + ARRAY_SIZE(blake2s_generic_hacl_algs)); +} + +subsys_initcall(blake2s_generic_hacl_mod_init); +module_exit(blake2s_generic_hacl_mod_fini); + +MODULE_LICENSE("GPLv2 or MIT"); +MODULE_DESCRIPTION( + "Formally Verified Generic BLAKE2 Secure Hash Algorithm from HACL*"); + +MODULE_ALIAS_CRYPTO("blake2s-160"); +MODULE_ALIAS_CRYPTO("blake2s-160-generic-hacl"); +MODULE_ALIAS_CRYPTO("blake2s-256"); +MODULE_ALIAS_CRYPTO("blake2s-256-generic-hacl"); diff --git a/crypto/hacl_hash.h b/crypto/hacl_hash.h index 80d8dd4ef2249..3f5f44d38abef 100644 --- a/crypto/hacl_hash.h +++ b/crypto/hacl_hash.h @@ -223,4 +223,129 @@ void Hacl_Streaming_SHA2_finish_384(struct Hacl_Streaming_MD_state_64_s *p, void Hacl_Streaming_SHA2_hash_384(uint8_t *input, uint32_t input_len, uint8_t *dst); +struct Hacl_Streaming_Blake2_blake2s_32_block_state_s { + uint32_t *fst; + uint32_t *snd; +}; + +struct Hacl_Streaming_Blake2_blake2b_32_block_state_s { + uint64_t *fst; + uint64_t *snd; +}; + +struct Hacl_Streaming_Blake2_blake2s_32_state_s { + struct Hacl_Streaming_Blake2_blake2s_32_block_state_s block_state; + uint8_t *buf; + uint64_t total_len; +}; + +struct Hacl_Streaming_Blake2_blake2b_32_state_s { + struct Hacl_Streaming_Blake2_blake2b_32_block_state_s block_state; + uint8_t *buf; + uint64_t total_len; +}; + +struct K___uint32_t_uint32_t_s { + uint32_t fst; + uint32_t snd; +}; + +void Hacl_Blake2b_32_blake2b_init(uint64_t *hash, uint32_t kk, uint32_t nn); + +void Hacl_Blake2s_32_blake2s_init(uint32_t *hash, uint32_t kk, uint32_t nn); + +/** + (Re-)initialization function when there is no key +*/ +void Hacl_Streaming_Blake2_blake2s_32_no_key_init( + struct Hacl_Streaming_Blake2_blake2s_32_state_s *s1); + +/** + Update function when there is no key; 0 = success, 1 = max length exceeded +*/ +Hacl_Streaming_Types_error_code Hacl_Streaming_Blake2_blake2s_32_no_key_update( + struct Hacl_Streaming_Blake2_blake2s_32_state_s *p, uint8_t *data, + uint32_t len); + +/** + Finish function when there is no key +*/ +void Hacl_Streaming_Blake2_blake2s_32_no_key_finish( + struct Hacl_Streaming_Blake2_blake2s_32_state_s *p, uint8_t *dst); + +/** + (Re)-initialization function when there is no key +*/ +void Hacl_Streaming_Blake2_blake2b_32_no_key_init( + struct Hacl_Streaming_Blake2_blake2b_32_state_s *s1); + +/** + Update function when there is no key; 0 = success, 1 = max length exceeded +*/ +Hacl_Streaming_Types_error_code Hacl_Streaming_Blake2_blake2b_32_no_key_update( + struct Hacl_Streaming_Blake2_blake2b_32_state_s *p, uint8_t *data, + uint32_t len); + +/** + Finish function when there is no key +*/ +void Hacl_Streaming_Blake2_blake2b_32_no_key_finish( + struct Hacl_Streaming_Blake2_blake2b_32_state_s *p, uint8_t *dst); + +static const uint32_t Hacl_Impl_Blake2_Constants_sigmaTable[160U] = { + (uint32_t)0U, (uint32_t)1U, (uint32_t)2U, (uint32_t)3U, + (uint32_t)4U, (uint32_t)5U, (uint32_t)6U, (uint32_t)7U, + (uint32_t)8U, (uint32_t)9U, (uint32_t)10U, (uint32_t)11U, + (uint32_t)12U, (uint32_t)13U, (uint32_t)14U, (uint32_t)15U, + (uint32_t)14U, (uint32_t)10U, (uint32_t)4U, (uint32_t)8U, + (uint32_t)9U, (uint32_t)15U, (uint32_t)13U, (uint32_t)6U, + (uint32_t)1U, (uint32_t)12U, (uint32_t)0U, (uint32_t)2U, + (uint32_t)11U, (uint32_t)7U, (uint32_t)5U, (uint32_t)3U, + (uint32_t)11U, (uint32_t)8U, (uint32_t)12U, (uint32_t)0U, + (uint32_t)5U, (uint32_t)2U, (uint32_t)15U, (uint32_t)13U, + (uint32_t)10U, (uint32_t)14U, (uint32_t)3U, (uint32_t)6U, + (uint32_t)7U, (uint32_t)1U, (uint32_t)9U, (uint32_t)4U, + (uint32_t)7U, (uint32_t)9U, (uint32_t)3U, (uint32_t)1U, + (uint32_t)13U, (uint32_t)12U, (uint32_t)11U, (uint32_t)14U, + (uint32_t)2U, (uint32_t)6U, (uint32_t)5U, (uint32_t)10U, + (uint32_t)4U, (uint32_t)0U, (uint32_t)15U, (uint32_t)8U, + (uint32_t)9U, (uint32_t)0U, (uint32_t)5U, (uint32_t)7U, + (uint32_t)2U, (uint32_t)4U, (uint32_t)10U, (uint32_t)15U, + (uint32_t)14U, (uint32_t)1U, (uint32_t)11U, (uint32_t)12U, + (uint32_t)6U, (uint32_t)8U, (uint32_t)3U, (uint32_t)13U, + (uint32_t)2U, (uint32_t)12U, (uint32_t)6U, (uint32_t)10U, + (uint32_t)0U, (uint32_t)11U, (uint32_t)8U, (uint32_t)3U, + (uint32_t)4U, (uint32_t)13U, (uint32_t)7U, (uint32_t)5U, + (uint32_t)15U, (uint32_t)14U, (uint32_t)1U, (uint32_t)9U, + (uint32_t)12U, (uint32_t)5U, (uint32_t)1U, (uint32_t)15U, + (uint32_t)14U, (uint32_t)13U, (uint32_t)4U, (uint32_t)10U, + (uint32_t)0U, (uint32_t)7U, (uint32_t)6U, (uint32_t)3U, + (uint32_t)9U, (uint32_t)2U, (uint32_t)8U, (uint32_t)11U, + (uint32_t)13U, (uint32_t)11U, (uint32_t)7U, (uint32_t)14U, + (uint32_t)12U, (uint32_t)1U, (uint32_t)3U, (uint32_t)9U, + (uint32_t)5U, (uint32_t)0U, (uint32_t)15U, (uint32_t)4U, + (uint32_t)8U, (uint32_t)6U, (uint32_t)2U, (uint32_t)10U, + (uint32_t)6U, (uint32_t)15U, (uint32_t)14U, (uint32_t)9U, + (uint32_t)11U, (uint32_t)3U, (uint32_t)0U, (uint32_t)8U, + (uint32_t)12U, (uint32_t)2U, (uint32_t)13U, (uint32_t)7U, + (uint32_t)1U, (uint32_t)4U, (uint32_t)10U, (uint32_t)5U, + (uint32_t)10U, (uint32_t)2U, (uint32_t)8U, (uint32_t)4U, + (uint32_t)7U, (uint32_t)6U, (uint32_t)1U, (uint32_t)5U, + (uint32_t)15U, (uint32_t)11U, (uint32_t)9U, (uint32_t)14U, + (uint32_t)3U, (uint32_t)12U, (uint32_t)13U +}; + +static const uint32_t Hacl_Impl_Blake2_Constants_ivTable_S[8U] = { + (uint32_t)0x6A09E667U, (uint32_t)0xBB67AE85U, (uint32_t)0x3C6EF372U, + (uint32_t)0xA54FF53AU, (uint32_t)0x510E527FU, (uint32_t)0x9B05688CU, + (uint32_t)0x1F83D9ABU, (uint32_t)0x5BE0CD19U +}; + +static const uint64_t Hacl_Impl_Blake2_Constants_ivTable_B[8U] = { + (uint64_t)0x6A09E667F3BCC908U, (uint64_t)0xBB67AE8584CAA73BU, + (uint64_t)0x3C6EF372FE94F82BU, (uint64_t)0xA54FF53A5F1D36F1U, + (uint64_t)0x510E527FADE682D1U, (uint64_t)0x9B05688C2B3E6C1FU, + (uint64_t)0x1F83D9ABFB41BD6BU, (uint64_t)0x5BE0CD19137E2179U +}; + #endif // CRYPTO_HACL_HASH_H_ diff --git a/crypto/hacl_lib.h b/crypto/hacl_lib.h index 12a9a3c2fcac4..312c913daac4d 100644 --- a/crypto/hacl_lib.h +++ b/crypto/hacl_lib.h @@ -21,6 +21,11 @@ static inline u128 FStar_UInt128_shift_left(u128 x, u32 y) return (x << y); } +inline static u128 FStar_UInt128_shift_right(u128 x, u32 y) +{ + return x >> y; +} + static inline u128 FStar_UInt128_add(u128 x, u128 y) { return (x + y); @@ -31,6 +36,16 @@ static inline u128 FStar_UInt128_uint64_to_uint128(u64 x) return ((u128)x); } +inline static u64 FStar_UInt128_uint128_to_uint64(u32 x) +{ + return (u64)x; +} + +inline static u128 FStar_UInt128_add_mod(u128 x, u128 y) +{ + return x + y; +} + /* * Loads and stores. These avoid undefined behavior due to unaligned memory * accesses, via memcpy. @@ -40,6 +55,10 @@ static inline u128 FStar_UInt128_uint64_to_uint128(u64 x) #define store32_be(b, i) put_unaligned_be32(i, b); #define load64_be(b) (get_unaligned_be64(b)) #define store64_be(b, i) put_unaligned_be64(i, b); +#define load32_le(b) (get_unaligned_le32(b)) +#define load64_le(b) (get_unaligned_le64(b)) +#define store32_le(b, i) put_unaligned_le32(i, b); +#define store64_le(b, i) put_unaligned_le64(i, b); static inline void store128_be(u8 *buf, u128 x) { @@ -231,4 +250,7 @@ static inline void store128_be(u8 *buf, u128 x) #define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x) #endif +#define Lib_Memzero0_memzero(dst, len, t) memzero_explicit(dst, len * sizeof(t)) +#define KRML_HOST_IGNORE(x) (void)(x) + #endif // CRYPTO_HACL_LIB_H_ From 44b9e44f16f835fa43abaee937efbec91eb7c3bb Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Tue, 24 Oct 2023 17:16:04 +0200 Subject: [PATCH 14/18] run ci --- .github/workflows/crypto-test-harness.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/crypto-test-harness.yml b/.github/workflows/crypto-test-harness.yml index 19e1791e838c8..67fc1a643eec1 100644 --- a/.github/workflows/crypto-test-harness.yml +++ b/.github/workflows/crypto-test-harness.yml @@ -3,7 +3,6 @@ name: Linux on: pull_request: - branches: ["cf-zeta"] workflow_dispatch: jobs: From af336bc13d820e28500acb0465ed0509a62e6245 Mon Sep 17 00:00:00 2001 From: armfazh Date: Tue, 5 Dec 2023 13:51:02 -0800 Subject: [PATCH 15/18] Fixing license and compilation module. --- crypto/Kconfig | 6 +- crypto/Makefile | 4 +- crypto/blake2-hacl-generated.c | 5 ++ crypto/blake2-hacl.c | 117 +++++++++++++-------------------- 4 files changed, 55 insertions(+), 77 deletions(-) diff --git a/crypto/Kconfig b/crypto/Kconfig index 1bd9aa2341cce..cfa1edd9b1333 100644 --- a/crypto/Kconfig +++ b/crypto/Kconfig @@ -922,13 +922,13 @@ config CRYPTO_BLAKE2B See https://blake2.net for further information. config CRYPTO_BLAKE2_HACL - tristate "HACL Blake2" + tristate "BLAKE2 (HACL*)" select CRYPTO_HASH help BLAKE2 cryptographic hash function (RFC 7693) - This is a formally verified implementation of BLAKE2s and BLAKE2b, ported - from the HACL* project. + This is a formally-verified implementation of BLAKE2b and BLAKE2s, + ported from the HACL* project. This module provides the following algorithms: - blake2b-160 diff --git a/crypto/Makefile b/crypto/Makefile index 19fbbfac8a498..1f281468093c0 100644 --- a/crypto/Makefile +++ b/crypto/Makefile @@ -89,7 +89,9 @@ obj-$(CONFIG_CRYPTO_WP512) += wp512.o CFLAGS_wp512.o := $(call cc-option,-fno-schedule-insns) # https://gcc.gnu.org/bugzilla/show_bug.cgi?id=79149 obj-$(CONFIG_CRYPTO_BLAKE2B) += blake2b_generic.o CFLAGS_blake2b_generic.o := -Wframe-larger-than=4096 # https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105930 -obj-$(CONFIG_CRYPTO_BLAKE2_HACL) += blake2-hacl.o blake2-hacl-generated.o +blake2_hacl-y := blake2-hacl-generated.o +blake2_hacl-y += blake2-hacl.o +obj-$(CONFIG_CRYPTO_BLAKE2_HACL) += blake2_hacl.o obj-$(CONFIG_CRYPTO_ECB) += ecb.o obj-$(CONFIG_CRYPTO_CBC) += cbc.o obj-$(CONFIG_CRYPTO_CFB) += cfb.o diff --git a/crypto/blake2-hacl-generated.c b/crypto/blake2-hacl-generated.c index 3c8289b37baad..18276198b577a 100644 --- a/crypto/blake2-hacl-generated.c +++ b/crypto/blake2-hacl-generated.c @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: GPL-2.0 OR MIT /* * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation * Copyright (c) 2022-2023 HACL* Contributors * Copyright (c) 2023 Cryspen + * + * This is a formally-verified implementation of BLAKE2 produced by HACL*. */ #include "hacl_hash.h" @@ -1366,3 +1369,5 @@ void Hacl_Streaming_Blake2_blake2b_32_no_key_finish( buf_last); Hacl_Blake2b_32_blake2b_finish((uint32_t)64U, dst, tmp_block_state.snd); } + +MODULE_LICENSE("Dual MIT/GPL"); diff --git a/crypto/blake2-hacl.c b/crypto/blake2-hacl.c index 96cadffc8d3f8..c01134be02ea3 100644 --- a/crypto/blake2-hacl.c +++ b/crypto/blake2-hacl.c @@ -1,7 +1,8 @@ -/* GPLv2 or MIT License - * +// SPDX-License-Identifier: GPL-2.0 OR MIT +/* * Copyright (c) 2023 Cryspen * + * This is a formally-verified implementation of BLAKE2 produced by HACL*. */ #include @@ -34,17 +35,17 @@ int hacl_blake2b_init(struct shash_desc *desc) } EXPORT_SYMBOL(hacl_blake2b_init); -int hacl_blake2b_update_generic(struct shash_desc *desc, const u8 *in, - unsigned int inlen) +int hacl_blake2b_update(struct shash_desc *desc, const u8 *in, + unsigned int inlen) { struct Hacl_Streaming_Blake2_blake2b_32_state_s *sctx = shash_desc_ctx(desc); Hacl_Streaming_Blake2_blake2b_32_no_key_update(sctx, (u8 *)in, inlen); return 0; } -EXPORT_SYMBOL(hacl_blake2b_update_generic); +EXPORT_SYMBOL(hacl_blake2b_update); -int hacl_blake2b_final_generic(struct shash_desc *desc, u8 *out) +int hacl_blake2b_final(struct shash_desc *desc, u8 *out) { struct Hacl_Streaming_Blake2_blake2b_32_state_s *sctx = shash_desc_ctx(desc); @@ -60,7 +61,7 @@ int hacl_blake2b_final_generic(struct shash_desc *desc, u8 *out) kfree(buf); return 0; } -EXPORT_SYMBOL(hacl_blake2b_final_generic); +EXPORT_SYMBOL(hacl_blake2b_final); #define BLAKE2B_ALG(name, driver_name, digest_size) \ { \ @@ -68,52 +69,12 @@ EXPORT_SYMBOL(hacl_blake2b_final_generic); .base.cra_priority = 100, \ .base.cra_blocksize = BLAKE2B_BLOCK_SIZE, \ .base.cra_module = THIS_MODULE, .digestsize = digest_size, \ - .init = hacl_blake2b_init, \ - .update = hacl_blake2b_update_generic, \ - .final = hacl_blake2b_final_generic, \ + .init = hacl_blake2b_init, .update = hacl_blake2b_update, \ + .final = hacl_blake2b_final, \ .descsize = sizeof( \ struct Hacl_Streaming_Blake2_blake2b_32_state_s), \ } -static struct shash_alg blake2_generic_hacl_algs[] = { - BLAKE2B_ALG("blake2b-160", "blake2b-160-generic-hacl", - BLAKE2B_160_HASH_SIZE), - BLAKE2B_ALG("blake2b-256", "blake2b-256-generic-hacl", - BLAKE2B_256_HASH_SIZE), - BLAKE2B_ALG("blake2b-384", "blake2b-384-generic-hacl", - BLAKE2B_384_HASH_SIZE), - BLAKE2B_ALG("blake2b-512", "blake2b-512-generic-hacl", - BLAKE2B_512_HASH_SIZE), -}; - -static int __init blake2_generic_hacl_mod_init(void) -{ - return crypto_register_shashes(blake2_generic_hacl_algs, - ARRAY_SIZE(blake2_generic_hacl_algs)); -} - -static void __exit blake2_generic_hacl_mod_fini(void) -{ - crypto_unregister_shashes(blake2_generic_hacl_algs, - ARRAY_SIZE(blake2_generic_hacl_algs)); -} - -subsys_initcall(blake2_generic_hacl_mod_init); -module_exit(blake2_generic_hacl_mod_fini); - -MODULE_LICENSE("GPLv2 or MIT"); -MODULE_DESCRIPTION( - "Formally Verified Generic BLAKE2 Secure Hash Algorithm from HACL*"); - -MODULE_ALIAS_CRYPTO("blake2b-160"); -MODULE_ALIAS_CRYPTO("blake2b-160-generic-hacl"); -MODULE_ALIAS_CRYPTO("blake2b-256"); -MODULE_ALIAS_CRYPTO("blake2b-256-generic-hacl"); -MODULE_ALIAS_CRYPTO("blake2b-384"); -MODULE_ALIAS_CRYPTO("blake2b-384-generic-hacl"); -MODULE_ALIAS_CRYPTO("blake2b-512"); -MODULE_ALIAS_CRYPTO("blake2b-512-generic-hacl"); - int hacl_blake2s_init(struct shash_desc *desc) { unsigned int outlen = crypto_shash_digestsize(desc->tfm); @@ -137,17 +98,17 @@ int hacl_blake2s_init(struct shash_desc *desc) } EXPORT_SYMBOL(hacl_blake2s_init); -int hacl_blake2s_update_generic(struct shash_desc *desc, const u8 *in, - unsigned int inlen) +int hacl_blake2s_update(struct shash_desc *desc, const u8 *in, + unsigned int inlen) { struct Hacl_Streaming_Blake2_blake2s_32_state_s *sctx = shash_desc_ctx(desc); Hacl_Streaming_Blake2_blake2s_32_no_key_update(sctx, (u8 *)in, inlen); return 0; } -EXPORT_SYMBOL(hacl_blake2s_update_generic); +EXPORT_SYMBOL(hacl_blake2s_update); -int hacl_blake2s_final_generic(struct shash_desc *desc, u8 *out) +int hacl_blake2s_final(struct shash_desc *desc, u8 *out) { struct Hacl_Streaming_Blake2_blake2s_32_state_s *sctx = shash_desc_ctx(desc); @@ -163,7 +124,7 @@ int hacl_blake2s_final_generic(struct shash_desc *desc, u8 *out) kfree(buf); return 0; } -EXPORT_SYMBOL(hacl_blake2s_final_generic); +EXPORT_SYMBOL(hacl_blake2s_final); #define BLAKE2S_ALG(name, driver_name, digest_size) \ { \ @@ -171,38 +132,48 @@ EXPORT_SYMBOL(hacl_blake2s_final_generic); .base.cra_priority = 100, \ .base.cra_blocksize = BLAKE2S_BLOCK_SIZE, \ .base.cra_module = THIS_MODULE, .digestsize = digest_size, \ - .init = hacl_blake2s_init, \ - .update = hacl_blake2s_update_generic, \ - .final = hacl_blake2s_final_generic, \ + .init = hacl_blake2s_init, .update = hacl_blake2s_update, \ + .final = hacl_blake2s_final, \ .descsize = sizeof( \ struct Hacl_Streaming_Blake2_blake2s_32_state_s), \ } -static struct shash_alg blake2s_generic_hacl_algs[] = { - BLAKE2S_ALG("blake2s-160", "blake2s-160-generic-hacl", 20), - BLAKE2S_ALG("blake2s-256", "blake2s-256-generic-hacl", 32), +static struct shash_alg blake2_hacl_algs[] = { + BLAKE2B_ALG("blake2b-160", "blake2b-160-hacl", BLAKE2B_160_HASH_SIZE), + BLAKE2B_ALG("blake2b-256", "blake2b-256-hacl", BLAKE2B_256_HASH_SIZE), + BLAKE2B_ALG("blake2b-384", "blake2b-384-hacl", BLAKE2B_384_HASH_SIZE), + BLAKE2B_ALG("blake2b-512", "blake2b-512-hacl", BLAKE2B_512_HASH_SIZE), + BLAKE2S_ALG("blake2s-160", "blake2s-160-hacl", 20), + BLAKE2S_ALG("blake2s-256", "blake2s-256-hacl", 32), }; -static int __init blake2s_generic_hacl_mod_init(void) +static int __init blake2_hacl_mod_init(void) { - return crypto_register_shashes(blake2s_generic_hacl_algs, - ARRAY_SIZE(blake2s_generic_hacl_algs)); + return crypto_register_shashes(blake2_hacl_algs, + ARRAY_SIZE(blake2_hacl_algs)); } -static void __exit blake2s_generic_hacl_mod_fini(void) +static void __exit blake2_hacl_mod_fini(void) { - crypto_unregister_shashes(blake2s_generic_hacl_algs, - ARRAY_SIZE(blake2s_generic_hacl_algs)); + crypto_unregister_shashes(blake2_hacl_algs, + ARRAY_SIZE(blake2_hacl_algs)); } -subsys_initcall(blake2s_generic_hacl_mod_init); -module_exit(blake2s_generic_hacl_mod_fini); +subsys_initcall(blake2_hacl_mod_init); +module_exit(blake2_hacl_mod_fini); -MODULE_LICENSE("GPLv2 or MIT"); -MODULE_DESCRIPTION( - "Formally Verified Generic BLAKE2 Secure Hash Algorithm from HACL*"); +MODULE_LICENSE("Dual MIT/GPL"); +MODULE_DESCRIPTION("Formally Verified BLAKE2 Secure Hash Algorithm from HACL*"); +MODULE_ALIAS_CRYPTO("blake2b-160"); +MODULE_ALIAS_CRYPTO("blake2b-160-hacl"); +MODULE_ALIAS_CRYPTO("blake2b-256"); +MODULE_ALIAS_CRYPTO("blake2b-256-hacl"); +MODULE_ALIAS_CRYPTO("blake2b-384"); +MODULE_ALIAS_CRYPTO("blake2b-384-hacl"); +MODULE_ALIAS_CRYPTO("blake2b-512"); +MODULE_ALIAS_CRYPTO("blake2b-512-hacl"); MODULE_ALIAS_CRYPTO("blake2s-160"); -MODULE_ALIAS_CRYPTO("blake2s-160-generic-hacl"); +MODULE_ALIAS_CRYPTO("blake2s-160-hacl"); MODULE_ALIAS_CRYPTO("blake2s-256"); -MODULE_ALIAS_CRYPTO("blake2s-256-generic-hacl"); +MODULE_ALIAS_CRYPTO("blake2s-256-hacl"); From b6ce904db680093e7bc77167d5f1541b64180044 Mon Sep 17 00:00:00 2001 From: armfazh Date: Tue, 5 Dec 2023 14:48:12 -0800 Subject: [PATCH 16/18] Running Blake2 in CI. --- zeta/test-artifacts/config-um | 1 + zeta/test-artifacts/test-script.sh | 9 +++++++++ 2 files changed, 10 insertions(+) diff --git a/zeta/test-artifacts/config-um b/zeta/test-artifacts/config-um index cd8025db42d49..7a04c13f35446 100644 --- a/zeta/test-artifacts/config-um +++ b/zeta/test-artifacts/config-um @@ -1407,6 +1407,7 @@ CONFIG_CRYPTO_TEST=m # HACL implementation # CONFIG_CRYPTO_SHA2_HACL=m +CONFIG_CRYPTO_BLAKE2_HACL=m # end of HACL implementation # diff --git a/zeta/test-artifacts/test-script.sh b/zeta/test-artifacts/test-script.sh index f4777ebbdb3db..b97297a0949d6 100755 --- a/zeta/test-artifacts/test-script.sh +++ b/zeta/test-artifacts/test-script.sh @@ -7,6 +7,15 @@ modprobe tcrypt mode=300 alg=sha256-hacl sec=2 modprobe tcrypt mode=300 alg=sha384-hacl sec=2 modprobe tcrypt mode=300 alg=sha512-hacl sec=2 +echo "tcrypt: starting CRYPTO_BLAKE2_HACL" +modprobe blake2-hacl +modprobe tcrypt mode=300 alg=blake2b-160-hacl sec=2 +modprobe tcrypt mode=300 alg=blake2b-256-hacl sec=2 +modprobe tcrypt mode=300 alg=blake2b-384-hacl sec=2 +modprobe tcrypt mode=300 alg=blake2b-512-hacl sec=2 +modprobe tcrypt mode=300 alg=blake2s-160-hacl sec=2 +modprobe tcrypt mode=300 alg=blake2s-256-hacl sec=2 + echo "tcrypt: starting SHA2 (256) test" echo "tcrypt: testing sha256 generic implementation" modprobe tcrypt mode=300 alg=sha256-generic sec=2 From 5960a03630348d781491248378b1e53f9e436f89 Mon Sep 17 00:00:00 2001 From: armfazh Date: Tue, 5 Dec 2023 15:01:30 -0800 Subject: [PATCH 17/18] Fixing documentation strings for BLAKE2. --- crypto/blake2-hacl-generated.c | 75 ++++++++++++++++++---------------- 1 file changed, 39 insertions(+), 36 deletions(-) diff --git a/crypto/blake2-hacl-generated.c b/crypto/blake2-hacl-generated.c index 18276198b577a..c8b3d09a9ed2a 100644 --- a/crypto/blake2-hacl-generated.c +++ b/crypto/blake2-hacl-generated.c @@ -444,15 +444,16 @@ void Hacl_Blake2b_32_blake2b_finish(uint32_t nn, uint8_t *output, } /** -Write the BLAKE2b digest of message `d` using key `k` into `output`. - -@param nn Length of the to-be-generated digest with 1 <= `nn` <= 64. -@param output Pointer to `nn` bytes of memory where the digest is written to. -@param ll Length of the input message. -@param d Pointer to `ll` bytes of memory where the input message is read from. -@param kk Length of the key. Can be 0. -@param k Pointer to `kk` bytes of memory where the key is read from. -*/ + * Hacl_Blake2b_32_blake2b() - Write the BLAKE2b digest of message `d` using + * key `k` into `output`. + * @nn: Length of the to-be-generated digest with 1 <= `nn` <= 64. + * @output: Pointer to `nn` bytes of memory where the digest is written to. + * @ll: Length of the input message. + * @d: Pointer to `ll` bytes of memory where the input message is + * read from. + * @kk: Length of the key. Can be 0. + * @k: Pointer to `kk` bytes of memory where the key is read from. + */ void Hacl_Blake2b_32_blake2b(uint32_t nn, uint8_t *output, uint32_t ll, uint8_t *d, uint32_t kk, uint8_t *k) { @@ -886,15 +887,17 @@ void Hacl_Blake2s_32_blake2s_finish(uint32_t nn, uint8_t *output, } /** -Write the BLAKE2s digest of message `d` using key `k` into `output`. - -@param nn Length of to-be-generated digest with 1 <= `nn` <= 32. -@param output Pointer to `nn` bytes of memory where the digest is written to. -@param ll Length of the input message. -@param d Pointer to `ll` bytes of memory where the input message is read from. -@param kk Length of the key. Can be 0. -@param k Pointer to `kk` bytes of memory where the key is read from. -*/ + * Hacl_Blake2s_32_blake2s() - Write the BLAKE2s digest of message `d` using + * key `k` into `output`. + * + * @nn: Length of to-be-generated digest with 1 <= `nn` <= 32. + * @output: Pointer to `nn` bytes of memory where the digest is written to. + * @ll: Length of the input message. + * @d: Pointer to `ll` bytes of memory where the input message is read + * from. + * @kk: Length of the key. Can be 0. + * @k: Pointer to `kk` bytes of memory where the key is read from. + */ void Hacl_Blake2s_32_blake2s(uint32_t nn, uint8_t *output, uint32_t ll, uint8_t *d, uint32_t kk, uint8_t *k) { @@ -907,9 +910,9 @@ void Hacl_Blake2s_32_blake2s(uint32_t nn, uint8_t *output, uint32_t ll, Lib_Memzero0_memzero(b, (uint32_t)16U, uint32_t); } -/** - (Re-)initialization function when there is no key -*/ +/* + * (Re-)initialization function when there is no key + */ void Hacl_Streaming_Blake2_blake2s_32_no_key_init( struct Hacl_Streaming_Blake2_blake2s_32_state_s *s1) { @@ -928,9 +931,9 @@ void Hacl_Streaming_Blake2_blake2s_32_no_key_init( s1[0U] = tmp; } -/** - Update function when there is no key; 0 = success, 1 = max length exceeded -*/ +/* + * Update function when there is no key; 0 = success, 1 = max length exceeded + */ Hacl_Streaming_Types_error_code Hacl_Streaming_Blake2_blake2s_32_no_key_update( struct Hacl_Streaming_Blake2_blake2s_32_state_s *p, uint8_t *data, uint32_t len) @@ -1085,9 +1088,9 @@ Hacl_Streaming_Types_error_code Hacl_Streaming_Blake2_blake2s_32_no_key_update( return Hacl_Streaming_Types_Success; } -/** - Finish function when there is no key -*/ +/* + * Finish function when there is no key + */ void Hacl_Streaming_Blake2_blake2s_32_no_key_finish( struct Hacl_Streaming_Blake2_blake2s_32_state_s *p, uint8_t *dst) { @@ -1134,9 +1137,9 @@ void Hacl_Streaming_Blake2_blake2s_32_no_key_finish( Hacl_Blake2s_32_blake2s_finish((uint32_t)32U, dst, tmp_block_state.snd); } -/** - (Re)-initialization function when there is no key -*/ +/* + * (Re)-initialization function when there is no key + */ void Hacl_Streaming_Blake2_blake2b_32_no_key_init( struct Hacl_Streaming_Blake2_blake2b_32_state_s *s1) { @@ -1155,9 +1158,9 @@ void Hacl_Streaming_Blake2_blake2b_32_no_key_init( s1[0U] = tmp; } -/** - Update function when there is no key; 0 = success, 1 = max length exceeded -*/ +/* + * Update function when there is no key; 0 = success, 1 = max length exceeded + */ Hacl_Streaming_Types_error_code Hacl_Streaming_Blake2_blake2b_32_no_key_update( struct Hacl_Streaming_Blake2_blake2b_32_state_s *p, uint8_t *data, uint32_t len) @@ -1319,9 +1322,9 @@ Hacl_Streaming_Types_error_code Hacl_Streaming_Blake2_blake2b_32_no_key_update( return Hacl_Streaming_Types_Success; } -/** - Finish function when there is no key -*/ +/* + * Finish function when there is no key + */ void Hacl_Streaming_Blake2_blake2b_32_no_key_finish( struct Hacl_Streaming_Blake2_blake2b_32_state_s *p, uint8_t *dst) { From c9ab2b1da436178aacf0a161d366cafcc07b0a74 Mon Sep 17 00:00:00 2001 From: Karthik Bhargavan Date: Fri, 15 Dec 2023 12:28:49 +0100 Subject: [PATCH 18/18] fixed blake2 finish to truncate output --- crypto/blake2-hacl.c | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/crypto/blake2-hacl.c b/crypto/blake2-hacl.c index c01134be02ea3..f8f190e733e21 100644 --- a/crypto/blake2-hacl.c +++ b/crypto/blake2-hacl.c @@ -49,7 +49,11 @@ int hacl_blake2b_final(struct shash_desc *desc, u8 *out) { struct Hacl_Streaming_Blake2_blake2b_32_state_s *sctx = shash_desc_ctx(desc); - Hacl_Streaming_Blake2_blake2b_32_no_key_finish(sctx, out); + u8 full_hash[64]; + int outlen = crypto_shash_digestsize(desc->tfm); + Hacl_Streaming_Blake2_blake2b_32_no_key_finish(sctx, full_hash); + memcpy(out,full_hash,outlen); + struct Hacl_Streaming_Blake2_blake2b_32_state_s scrut = *sctx; uint8_t *buf = scrut.buf; struct Hacl_Streaming_Blake2_blake2b_32_block_state_s block_state = @@ -112,7 +116,10 @@ int hacl_blake2s_final(struct shash_desc *desc, u8 *out) { struct Hacl_Streaming_Blake2_blake2s_32_state_s *sctx = shash_desc_ctx(desc); - Hacl_Streaming_Blake2_blake2s_32_no_key_finish(sctx, out); + u8 full_hash[32]; + int outlen = crypto_shash_digestsize(desc->tfm); + Hacl_Streaming_Blake2_blake2s_32_no_key_finish(sctx, full_hash); + memcpy(out,full_hash,outlen); struct Hacl_Streaming_Blake2_blake2s_32_state_s scrut = *sctx; uint8_t *buf = scrut.buf; struct Hacl_Streaming_Blake2_blake2s_32_block_state_s block_state =