From 1134e410bd56eb7a3d8693ebcb23cdbc6a6161e2 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Fri, 17 Feb 2023 09:08:09 +0100 Subject: [PATCH 1/3] improved sha2-one-shot --- benchmarks/sha2.cc | 46 ++- config/config.json | 4 + config/default_config.cmake | 1 + include/Hacl_SHA2_Generic.h | 134 ++++++ include/Hacl_SHA2_Scalar32.h | 54 +++ include/MerkleTree.h | 551 +++++++++++++++++++++++++ include/config.h | 4 + include/msvc/config.h | 4 + src/Hacl_SHA2_Scalar32.c | 772 +++++++++++++++++++++++++++++++++++ 9 files changed, 1562 insertions(+), 8 deletions(-) create mode 100644 include/Hacl_SHA2_Generic.h create mode 100644 include/Hacl_SHA2_Scalar32.h create mode 100644 include/MerkleTree.h create mode 100644 include/config.h create mode 100644 include/msvc/config.h create mode 100644 src/Hacl_SHA2_Scalar32.c diff --git a/benchmarks/sha2.cc b/benchmarks/sha2.cc index 6864163c6..c149b43fd 100644 --- a/benchmarks/sha2.cc +++ b/benchmarks/sha2.cc @@ -7,14 +7,7 @@ */ #include "EverCrypt_Hash.h" #include "Hacl_Streaming_SHA2.h" - -#ifdef HACL_CAN_COMPILE_VEC128 -#include "Hacl_Hash_Blake2s_128.h" -#endif - -#ifdef HACL_CAN_COMPILE_VEC256 -#include "Hacl_Hash_Blake2b_256.h" -#endif +#include "Hacl_SHA2_Scalar32.h" #include "util.h" @@ -59,6 +52,29 @@ HACL_Sha2_oneshot(benchmark::State& state, Args&&... args) } } + +template +void +HACL_Sha2_new_oneshot(benchmark::State& state, Args&&... args) +{ + auto args_tuple = std::make_tuple(std::move(args)...); + + auto digest_len = std::get<0>(args_tuple); + auto expected_digest = std::get<1>(args_tuple); + auto hash = std::get<2>(args_tuple); + + bytes digest(digest_len, 0); + + for (auto _ : state) { + hash(digest.data(), input.size(), (uint8_t*)input.data()); + } + + if (digest != expected_digest) { + state.SkipWithError("Incorrect digest."); + return; + } +} + template void EverCrypt_Sha2_oneshot(benchmark::State& state, Args&&... args) @@ -162,6 +178,13 @@ BENCHMARK_CAPTURE(HACL_Sha2_oneshot, Hacl_Hash_SHA2_hash_224) ->Setup(DoSetup); +BENCHMARK_CAPTURE(HACL_Sha2_new_oneshot, + sha2_224_new, + HACL_HASH_SHA2_224_DIGEST_LENGTH, + expected_digest_sha2_224, + Hacl_SHA2_Scalar32_sha224) + ->Setup(DoSetup); + BENCHMARK_CAPTURE(EverCrypt_Sha2_oneshot, sha2_224, Spec_Hash_Definitions_SHA2_224, @@ -185,6 +208,13 @@ BENCHMARK_CAPTURE(HACL_Sha2_oneshot, Hacl_Hash_SHA2_hash_256) ->Setup(DoSetup); +BENCHMARK_CAPTURE(HACL_Sha2_new_oneshot, + sha2_256_new, + HACL_HASH_SHA2_256_DIGEST_LENGTH, + expected_digest_sha2_256, + Hacl_SHA2_Scalar32_sha256) + ->Setup(DoSetup); + BENCHMARK_CAPTURE(EverCrypt_Sha2_oneshot, sha2_256, Spec_Hash_Definitions_SHA2_256, diff --git a/config/config.json b/config/config.json index d67352aab..5aea179f8 100644 --- a/config/config.json +++ b/config/config.json @@ -191,6 +191,10 @@ "file": "Hacl_Hash_SHA2.c", "features": "std" }, + { + "file": "Hacl_SHA2_Scalar32.c", + "features": "std" + }, { "file": "Hacl_SHA2_Vec128.c", "features": "vec128" diff --git a/config/default_config.cmake b/config/default_config.cmake index d50381f6a..d2403768c 100644 --- a/config/default_config.cmake +++ b/config/default_config.cmake @@ -5,6 +5,7 @@ set(SOURCES_std ${PROJECT_SOURCE_DIR}/src/Hacl_Curve25519_51.c ${PROJECT_SOURCE_DIR}/src/Hacl_HMAC_DRBG.c ${PROJECT_SOURCE_DIR}/src/Hacl_HMAC.c + ${PROJECT_SOURCE_DIR}/src/Hacl_SHA2_Scalar32.c ${PROJECT_SOURCE_DIR}/src/Hacl_Hash_SHA2.c ${PROJECT_SOURCE_DIR}/src/Hacl_Hash_SHA1.c ${PROJECT_SOURCE_DIR}/src/Hacl_Hash_Blake2.c diff --git a/include/Hacl_SHA2_Generic.h b/include/Hacl_SHA2_Generic.h new file mode 100644 index 000000000..3a6a75483 --- /dev/null +++ b/include/Hacl_SHA2_Generic.h @@ -0,0 +1,134 @@ +/* MIT License + * + * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ + + +#ifndef __Hacl_SHA2_Generic_H +#define __Hacl_SHA2_Generic_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + + + + +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 + }; + +#if defined(__cplusplus) +} +#endif + +#define __Hacl_SHA2_Generic_H_DEFINED +#endif diff --git a/include/Hacl_SHA2_Scalar32.h b/include/Hacl_SHA2_Scalar32.h new file mode 100644 index 000000000..59ecdbe07 --- /dev/null +++ b/include/Hacl_SHA2_Scalar32.h @@ -0,0 +1,54 @@ +/* MIT License + * + * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ + + +#ifndef __Hacl_SHA2_Scalar32_H +#define __Hacl_SHA2_Scalar32_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + + +#include "Hacl_SHA2_Generic.h" +#include "Hacl_Krmllib.h" + +void Hacl_SHA2_Scalar32_sha224(uint8_t *dst, uint32_t input_len, uint8_t *input); + +void Hacl_SHA2_Scalar32_sha256(uint8_t *dst, uint32_t input_len, uint8_t *input); + +void Hacl_SHA2_Scalar32_sha384(uint8_t *dst, uint32_t input_len, uint8_t *input); + +void Hacl_SHA2_Scalar32_sha512(uint8_t *dst, uint32_t input_len, uint8_t *input); + +#if defined(__cplusplus) +} +#endif + +#define __Hacl_SHA2_Scalar32_H_DEFINED +#endif diff --git a/include/MerkleTree.h b/include/MerkleTree.h new file mode 100644 index 000000000..3b9ae523f --- /dev/null +++ b/include/MerkleTree.h @@ -0,0 +1,551 @@ +/* MIT License + * + * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ + + +#ifndef __MerkleTree_H +#define __MerkleTree_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + + +#include "Hacl_Spec.h" +#include "EverCrypt_Hash.h" + +typedef struct MerkleTree_Low_Datastructures_hash_vec_s +{ + uint32_t sz; + uint32_t cap; + uint8_t **vs; +} +MerkleTree_Low_Datastructures_hash_vec; + +typedef struct MerkleTree_Low_Datastructures_hash_vv_s +{ + uint32_t sz; + uint32_t cap; + MerkleTree_Low_Datastructures_hash_vec *vs; +} +MerkleTree_Low_Datastructures_hash_vv; + +typedef uint32_t hash_size_t; + +typedef uint64_t offset_t; + +typedef uint32_t index_t; + +typedef uint8_t *hash; + +typedef struct MerkleTree_Low_path_s +{ + uint32_t hash_size; + MerkleTree_Low_Datastructures_hash_vec hashes; +} +MerkleTree_Low_path; + +typedef MerkleTree_Low_path path; + +typedef MerkleTree_Low_path *path_p; + +typedef const MerkleTree_Low_path *const_path_p; + +typedef struct MerkleTree_Low_merkle_tree_s +{ + uint32_t hash_size; + uint64_t offset; + uint32_t i; + uint32_t j; + MerkleTree_Low_Datastructures_hash_vv hs; + bool rhs_ok; + MerkleTree_Low_Datastructures_hash_vec rhs; + uint8_t *mroot; + void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2); +} +MerkleTree_Low_merkle_tree; + +typedef MerkleTree_Low_merkle_tree merkle_tree; + +typedef MerkleTree_Low_merkle_tree *mt_p; + +typedef const MerkleTree_Low_merkle_tree *const_mt_p; + +/** + Constructor for hashes +*/ +uint8_t *mt_init_hash(uint32_t hash_size); + +/** + Destructor for hashes +*/ +void mt_free_hash(uint8_t *h); + +/** + Constructor for paths +*/ +MerkleTree_Low_path *mt_init_path(uint32_t hash_size); + +/** + Destructor for paths +*/ +void mt_free_path(MerkleTree_Low_path *path1); + +/** + Length of a path + + @param[in] p Path + + return The length of the path +*/ +uint32_t mt_get_path_length(const MerkleTree_Low_path *path1); + +/** + Insert hash into path + + @param[in] p Path + @param[in] hash Hash to insert +*/ +void mt_path_insert(MerkleTree_Low_path *path1, uint8_t *hash1); + +/** + Get step on a path + + @param[in] p Path + @param[in] i Path step index + + return The hash at step i of p +*/ +uint8_t *mt_get_path_step(const MerkleTree_Low_path *path1, uint32_t i); + +/** + Precondition predicate for mt_get_path_step +*/ +bool mt_get_path_step_pre(const MerkleTree_Low_path *path1, uint32_t i); + +/** + Construction with custom hash functions + + @param[in] hash_size Hash size (in bytes) + @param[in] i The initial hash + + return The new Merkle tree +*/ +MerkleTree_Low_merkle_tree +*mt_create_custom( + uint32_t hash_size, + uint8_t *i, + void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2) +); + +/** + Destruction + + @param[in] mt The Merkle tree +*/ +void mt_free(MerkleTree_Low_merkle_tree *mt); + +/** + Insertion + + @param[in] mt The Merkle tree + @param[in] v The tree does not take ownership of the hash, it makes a copy of its content. + + Note: The content of the hash will be overwritten with an arbitrary value. +*/ +void mt_insert(MerkleTree_Low_merkle_tree *mt, uint8_t *v); + +/** + Precondition predicate for mt_insert +*/ +bool mt_insert_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *v); + +/** + Getting the Merkle root + + @param[in] mt The Merkle tree + @param[out] root The Merkle root +*/ +void mt_get_root(const MerkleTree_Low_merkle_tree *mt, uint8_t *root); + +/** + Precondition predicate for mt_get_root +*/ +bool mt_get_root_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *root); + +/** + Getting a Merkle path + + @param[in] mt The Merkle tree + @param[in] idx The index of the target hash + @param[out] path A resulting Merkle path that contains the leaf hash. + @param[out] root The Merkle root + + return The number of elements in the tree + + Notes: + - The resulting path contains pointers to hashes in the tree, not copies of + the hash values. + - idx must be within the currently held indices in the tree (past the + last flush index). +*/ +uint32_t +mt_get_path( + const MerkleTree_Low_merkle_tree *mt, + uint64_t idx, + MerkleTree_Low_path *path1, + uint8_t *root +); + +/** + Precondition predicate for mt_get_path +*/ +bool +mt_get_path_pre( + const MerkleTree_Low_merkle_tree *mt, + uint64_t idx, + const MerkleTree_Low_path *path1, + uint8_t *root +); + +/** + Flush the Merkle tree + + @param[in] mt The Merkle tree +*/ +void mt_flush(MerkleTree_Low_merkle_tree *mt); + +/** + Precondition predicate for mt_flush +*/ +bool mt_flush_pre(const MerkleTree_Low_merkle_tree *mt); + +/** + Flush the Merkle tree up to a given index + + @param[in] mt The Merkle tree + @param[in] idx The index up to which to flush the tree +*/ +void mt_flush_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx); + +/** + Precondition predicate for mt_flush_to +*/ +bool mt_flush_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx); + +/** + Retract the Merkle tree down to a given index + + @param[in] mt The Merkle tree + @param[in] idx The index to retract the tree to + + Note: The element and idx will remain in the tree. +*/ +void mt_retract_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx); + +/** + Precondition predicate for mt_retract_to +*/ +bool mt_retract_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx); + +/** + Client-side verification + + @param[in] mt The Merkle tree + @param[in] tgt The index of the target hash + @param[in] max The maximum index + 1 of the tree when the path was generated + @param[in] path The Merkle path to verify + @param[in] root + + return true if the verification succeeded, false otherwise + + Note: max - tgt must be less than 2^32. +*/ +bool +mt_verify( + const MerkleTree_Low_merkle_tree *mt, + uint64_t tgt, + uint64_t max, + const MerkleTree_Low_path *path1, + uint8_t *root +); + +/** + Precondition predicate for mt_verify +*/ +bool +mt_verify_pre( + const MerkleTree_Low_merkle_tree *mt, + uint64_t tgt, + uint64_t max, + const MerkleTree_Low_path *path1, + uint8_t *root +); + +/** + Serialization size + + @param[in] mt The Merkle tree + + return the number of bytes required to serialize the tree +*/ +uint64_t mt_serialize_size(const MerkleTree_Low_merkle_tree *mt); + +/** + Merkle tree serialization + + @param[in] mt The Merkle tree + @param[out] buf The buffer to serialize the tree into + @param[in] len Length of buf + + return the number of bytes written + + Note: buf must be a buffer of size mt_serialize_size(mt) or larger, but + smaller than 2^32 (larger buffers are currently not supported). +*/ +uint64_t mt_serialize(const MerkleTree_Low_merkle_tree *mt, uint8_t *buf, uint64_t len); + +/** + Merkle tree deserialization + + @param[in] expected_hash_size Expected hash size to match hash_fun + @param[in] buf The buffer to deserialize the tree from + @param[in] len Length of buf + @param[in] hash_fun Hash function + + return pointer to the new tree if successful, NULL otherwise + + Note: buf must point to an allocated buffer. +*/ +MerkleTree_Low_merkle_tree +*mt_deserialize( + const uint8_t *buf, + uint64_t len, + void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2) +); + +/** + Path serialization + + @param[in] path The path + @param[out] buf The buffer to serialize the path into + @param[in] len Length of buf + + return the number of bytes written +*/ +uint64_t mt_serialize_path(const MerkleTree_Low_path *path1, uint8_t *buf, uint64_t len); + +/** + Path deserialization + + @param[in] buf The buffer to deserialize the path from + @param[in] len Length of buf + + return pointer to the new path if successful, NULL otherwise + + Note: buf must point to an allocated buffer. +*/ +MerkleTree_Low_path *mt_deserialize_path(const uint8_t *buf, uint64_t len); + +/** + Default hash function +*/ +void mt_sha256_compress(uint8_t *src1, uint8_t *src2, uint8_t *dst); + +/** + Construction wired to sha256 from EverCrypt + + @param[in] init The initial hash +*/ +MerkleTree_Low_merkle_tree *mt_create(uint8_t *init); + +typedef uint32_t MerkleTree_Low_index_t; + +extern uint32_t MerkleTree_Low_uint32_32_max; + +extern uint64_t MerkleTree_Low_uint32_max; + +extern uint64_t MerkleTree_Low_uint64_max; + +extern uint64_t MerkleTree_Low_offset_range_limit; + +typedef uint64_t MerkleTree_Low_offset_t; + +extern uint32_t MerkleTree_Low_merkle_tree_size_lg; + +bool MerkleTree_Low_uu___is_MT(MerkleTree_Low_merkle_tree projectee); + +typedef MerkleTree_Low_merkle_tree *MerkleTree_Low_mt_p; + +typedef const MerkleTree_Low_merkle_tree *MerkleTree_Low_const_mt_p; + +bool +MerkleTree_Low_merkle_tree_conditions( + uint64_t offset, + uint32_t i, + uint32_t j, + MerkleTree_Low_Datastructures_hash_vv hs, + bool rhs_ok, + MerkleTree_Low_Datastructures_hash_vec rhs, + uint8_t *mroot +); + +uint32_t MerkleTree_Low_offset_of(uint32_t i); + +void MerkleTree_Low_mt_free(MerkleTree_Low_merkle_tree *mt); + +bool MerkleTree_Low_mt_insert_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *v); + +void MerkleTree_Low_mt_insert(MerkleTree_Low_merkle_tree *mt, uint8_t *v); + +MerkleTree_Low_merkle_tree +*MerkleTree_Low_mt_create_custom( + uint32_t hsz, + uint8_t *init, + void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2) +); + +bool MerkleTree_Low_uu___is_Path(MerkleTree_Low_path projectee); + +typedef MerkleTree_Low_path *MerkleTree_Low_path_p; + +typedef const MerkleTree_Low_path *MerkleTree_Low_const_path_p; + +MerkleTree_Low_path *MerkleTree_Low_init_path(uint32_t hsz); + +void MerkleTree_Low_clear_path(MerkleTree_Low_path *p); + +void MerkleTree_Low_free_path(MerkleTree_Low_path *p); + +bool MerkleTree_Low_mt_get_root_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *rt); + +void MerkleTree_Low_mt_get_root(const MerkleTree_Low_merkle_tree *mt, uint8_t *rt); + +void MerkleTree_Low_mt_path_insert(uint32_t hsz, MerkleTree_Low_path *p, uint8_t *hp); + +uint32_t MerkleTree_Low_mt_get_path_length(const MerkleTree_Low_path *p); + +bool MerkleTree_Low_mt_get_path_step_pre(const MerkleTree_Low_path *p, uint32_t i); + +uint8_t *MerkleTree_Low_mt_get_path_step(const MerkleTree_Low_path *p, uint32_t i); + +bool +MerkleTree_Low_mt_get_path_pre( + const MerkleTree_Low_merkle_tree *mt, + uint64_t idx, + const MerkleTree_Low_path *p, + uint8_t *root +); + +uint32_t +MerkleTree_Low_mt_get_path( + const MerkleTree_Low_merkle_tree *mt, + uint64_t idx, + MerkleTree_Low_path *p, + uint8_t *root +); + +bool MerkleTree_Low_mt_flush_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx); + +void MerkleTree_Low_mt_flush_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx); + +bool MerkleTree_Low_mt_flush_pre(const MerkleTree_Low_merkle_tree *mt); + +void MerkleTree_Low_mt_flush(MerkleTree_Low_merkle_tree *mt); + +bool MerkleTree_Low_mt_retract_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t r); + +void MerkleTree_Low_mt_retract_to(MerkleTree_Low_merkle_tree *mt, uint64_t r); + +bool +MerkleTree_Low_mt_verify_pre( + const MerkleTree_Low_merkle_tree *mt, + uint64_t k, + uint64_t j, + const MerkleTree_Low_path *p, + uint8_t *rt +); + +bool +MerkleTree_Low_mt_verify( + const MerkleTree_Low_merkle_tree *mt, + uint64_t k, + uint64_t j, + const MerkleTree_Low_path *p, + uint8_t *rt +); + +typedef uint8_t MerkleTree_Low_Serialization_uint8_t; + +typedef uint16_t MerkleTree_Low_Serialization_uint16_t; + +typedef uint32_t MerkleTree_Low_Serialization_uint32_t; + +typedef uint64_t MerkleTree_Low_Serialization_uint64_t; + +typedef uint8_t *MerkleTree_Low_Serialization_uint8_p; + +typedef const uint8_t *MerkleTree_Low_Serialization_const_uint8_p; + +uint64_t MerkleTree_Low_Serialization_mt_serialize_size(const MerkleTree_Low_merkle_tree *mt); + +uint64_t +MerkleTree_Low_Serialization_mt_serialize( + const MerkleTree_Low_merkle_tree *mt, + uint8_t *output, + uint64_t sz +); + +MerkleTree_Low_merkle_tree +*MerkleTree_Low_Serialization_mt_deserialize( + const uint8_t *input, + uint64_t sz, + void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2) +); + +uint64_t +MerkleTree_Low_Serialization_mt_serialize_path( + const MerkleTree_Low_path *p, + uint8_t *output, + uint64_t sz +); + +MerkleTree_Low_path +*MerkleTree_Low_Serialization_mt_deserialize_path(const uint8_t *input, uint64_t sz); + +uint8_t *MerkleTree_Low_Hashfunctions_init_hash(uint32_t hsz); + +void MerkleTree_Low_Hashfunctions_free_hash(uint8_t *h); + +typedef void (*MerkleTree_Low_Hashfunctions_hash_fun_t)(uint8_t *x0, uint8_t *x1, uint8_t *x2); + +#if defined(__cplusplus) +} +#endif + +#define __MerkleTree_H_DEFINED +#endif diff --git a/include/config.h b/include/config.h new file mode 100644 index 000000000..d8bf2f048 --- /dev/null +++ b/include/config.h @@ -0,0 +1,4 @@ +#define TARGET_ARCHITECTURE TARGET_ARCHITECTURE_ID_ARM8 +#define HACL_CAN_COMPILE_VEC128 1 +#define Lib_IntVector_Intrinsics_vec256 void * +#define HACL_CAN_COMPILE_UINT128 1 diff --git a/include/msvc/config.h b/include/msvc/config.h new file mode 100644 index 000000000..d8bf2f048 --- /dev/null +++ b/include/msvc/config.h @@ -0,0 +1,4 @@ +#define TARGET_ARCHITECTURE TARGET_ARCHITECTURE_ID_ARM8 +#define HACL_CAN_COMPILE_VEC128 1 +#define Lib_IntVector_Intrinsics_vec256 void * +#define HACL_CAN_COMPILE_UINT128 1 diff --git a/src/Hacl_SHA2_Scalar32.c b/src/Hacl_SHA2_Scalar32.c new file mode 100644 index 000000000..4dd03d0ed --- /dev/null +++ b/src/Hacl_SHA2_Scalar32.c @@ -0,0 +1,772 @@ +/* MIT License + * + * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ + + +#include "Hacl_SHA2_Scalar32.h" + +#include "internal/Hacl_SHA2_Types.h" + +static inline void sha224_update1(uint8_t *block, 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 *b = block; + uint32_t u = load32_be(b); + ws[0U] = u; + uint32_t u0 = load32_be(b + (uint32_t)4U); + ws[1U] = u0; + uint32_t u1 = load32_be(b + (uint32_t)8U); + ws[2U] = u1; + uint32_t u2 = load32_be(b + (uint32_t)12U); + ws[3U] = u2; + uint32_t u3 = load32_be(b + (uint32_t)16U); + ws[4U] = u3; + uint32_t u4 = load32_be(b + (uint32_t)20U); + ws[5U] = u4; + uint32_t u5 = load32_be(b + (uint32_t)24U); + ws[6U] = u5; + uint32_t u6 = load32_be(b + (uint32_t)28U); + ws[7U] = u6; + uint32_t u7 = load32_be(b + (uint32_t)32U); + ws[8U] = u7; + uint32_t u8 = load32_be(b + (uint32_t)36U); + ws[9U] = u8; + uint32_t u9 = load32_be(b + (uint32_t)40U); + ws[10U] = u9; + uint32_t u10 = load32_be(b + (uint32_t)44U); + ws[11U] = u10; + uint32_t u11 = load32_be(b + (uint32_t)48U); + ws[12U] = u11; + uint32_t u12 = load32_be(b + (uint32_t)52U); + ws[13U] = u12; + uint32_t u13 = load32_be(b + (uint32_t)56U); + ws[14U] = u13; + uint32_t u14 = load32_be(b + (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_sha224(uint8_t *dst, uint32_t input_len, uint8_t *input) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + KRML_MAYBE_FOR8(i, + (uint32_t)0U, + (uint32_t)8U, + (uint32_t)1U, + uint32_t *os = st; + uint32_t x = Hacl_Impl_SHA2_Generic_h224[i]; + os[i] = x;); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + uint32_t blocks0 = input_len / (uint32_t)64U; + for (uint32_t i = (uint32_t)0U; i < blocks0; i++) + { + uint8_t *b0 = ib; + uint8_t *mb = b0 + i * (uint32_t)64U; + sha224_update1(mb, st); + } + uint32_t rem1 = input_len % (uint32_t)64U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + uint32_t blocks; + if (rem + (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 = len_ << (uint32_t)3U; + store64_be(totlen_buf, total_len_bits); + uint8_t *b00 = lb; + memcpy(last, b00, rem * sizeof (uint8_t)); + last[rem] = (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; + Hacl_Impl_SHA2_Types_uint8_2p scrut = { .fst = last00, .snd = last10 }; + uint8_t *l0 = scrut.fst; + uint8_t *l1 = scrut.snd; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + Hacl_Impl_SHA2_Types_uint8_2p scrut0 = { .fst = lb0, .snd = lb1 }; + uint8_t *last0 = scrut0.fst; + uint8_t *last1 = scrut0.snd; + sha224_update1(last0, st); + if (blocks > (uint32_t)1U) + { + sha224_update1(last1, st); + } + 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(rb, hbuf, (uint32_t)28U * sizeof (uint8_t)); +} + +static inline void sha256_update1(uint8_t *block, 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 *b = block; + uint32_t u = load32_be(b); + ws[0U] = u; + uint32_t u0 = load32_be(b + (uint32_t)4U); + ws[1U] = u0; + uint32_t u1 = load32_be(b + (uint32_t)8U); + ws[2U] = u1; + uint32_t u2 = load32_be(b + (uint32_t)12U); + ws[3U] = u2; + uint32_t u3 = load32_be(b + (uint32_t)16U); + ws[4U] = u3; + uint32_t u4 = load32_be(b + (uint32_t)20U); + ws[5U] = u4; + uint32_t u5 = load32_be(b + (uint32_t)24U); + ws[6U] = u5; + uint32_t u6 = load32_be(b + (uint32_t)28U); + ws[7U] = u6; + uint32_t u7 = load32_be(b + (uint32_t)32U); + ws[8U] = u7; + uint32_t u8 = load32_be(b + (uint32_t)36U); + ws[9U] = u8; + uint32_t u9 = load32_be(b + (uint32_t)40U); + ws[10U] = u9; + uint32_t u10 = load32_be(b + (uint32_t)44U); + ws[11U] = u10; + uint32_t u11 = load32_be(b + (uint32_t)48U); + ws[12U] = u11; + uint32_t u12 = load32_be(b + (uint32_t)52U); + ws[13U] = u12; + uint32_t u13 = load32_be(b + (uint32_t)56U); + ws[14U] = u13; + uint32_t u14 = load32_be(b + (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(uint8_t *dst, uint32_t input_len, uint8_t *input) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint32_t st[8U] = { 0U }; + KRML_MAYBE_FOR8(i, + (uint32_t)0U, + (uint32_t)8U, + (uint32_t)1U, + uint32_t *os = st; + uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; + os[i] = x;); + uint32_t rem = input_len % (uint32_t)64U; + uint64_t len_ = (uint64_t)input_len; + uint32_t blocks0 = input_len / (uint32_t)64U; + for (uint32_t i = (uint32_t)0U; i < blocks0; i++) + { + uint8_t *b0 = ib; + uint8_t *mb = b0 + i * (uint32_t)64U; + sha256_update1(mb, st); + } + uint32_t rem1 = input_len % (uint32_t)64U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + uint32_t blocks; + if (rem + (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 = len_ << (uint32_t)3U; + store64_be(totlen_buf, total_len_bits); + uint8_t *b00 = lb; + memcpy(last, b00, rem * sizeof (uint8_t)); + last[rem] = (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; + Hacl_Impl_SHA2_Types_uint8_2p scrut = { .fst = last00, .snd = last10 }; + uint8_t *l0 = scrut.fst; + uint8_t *l1 = scrut.snd; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + Hacl_Impl_SHA2_Types_uint8_2p scrut0 = { .fst = lb0, .snd = lb1 }; + uint8_t *last0 = scrut0.fst; + uint8_t *last1 = scrut0.snd; + sha256_update1(last0, st); + if (blocks > (uint32_t)1U) + { + sha256_update1(last1, st); + } + 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(rb, hbuf, (uint32_t)32U * sizeof (uint8_t)); +} + +static inline void sha384_update1(uint8_t *block, 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 *b = block; + uint64_t u = load64_be(b); + ws[0U] = u; + uint64_t u0 = load64_be(b + (uint32_t)8U); + ws[1U] = u0; + uint64_t u1 = load64_be(b + (uint32_t)16U); + ws[2U] = u1; + uint64_t u2 = load64_be(b + (uint32_t)24U); + ws[3U] = u2; + uint64_t u3 = load64_be(b + (uint32_t)32U); + ws[4U] = u3; + uint64_t u4 = load64_be(b + (uint32_t)40U); + ws[5U] = u4; + uint64_t u5 = load64_be(b + (uint32_t)48U); + ws[6U] = u5; + uint64_t u6 = load64_be(b + (uint32_t)56U); + ws[7U] = u6; + uint64_t u7 = load64_be(b + (uint32_t)64U); + ws[8U] = u7; + uint64_t u8 = load64_be(b + (uint32_t)72U); + ws[9U] = u8; + uint64_t u9 = load64_be(b + (uint32_t)80U); + ws[10U] = u9; + uint64_t u10 = load64_be(b + (uint32_t)88U); + ws[11U] = u10; + uint64_t u11 = load64_be(b + (uint32_t)96U); + ws[12U] = u11; + uint64_t u12 = load64_be(b + (uint32_t)104U); + ws[13U] = u12; + uint64_t u13 = load64_be(b + (uint32_t)112U); + ws[14U] = u13; + uint64_t u14 = load64_be(b + (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_sha384(uint8_t *dst, uint32_t input_len, uint8_t *input) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint64_t st[8U] = { 0U }; + KRML_MAYBE_FOR8(i, + (uint32_t)0U, + (uint32_t)8U, + (uint32_t)1U, + uint64_t *os = st; + uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; + os[i] = x;); + uint32_t rem = input_len % (uint32_t)128U; + FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); + uint32_t blocks0 = input_len / (uint32_t)128U; + for (uint32_t i = (uint32_t)0U; i < blocks0; i++) + { + uint8_t *b0 = ib; + uint8_t *mb = b0 + i * (uint32_t)128U; + sha384_update1(mb, st); + } + uint32_t rem1 = input_len % (uint32_t)128U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + uint32_t blocks; + if (rem + (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(len_, (uint32_t)3U); + store128_be(totlen_buf, total_len_bits); + uint8_t *b00 = lb; + memcpy(last, b00, rem * sizeof (uint8_t)); + last[rem] = (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; + Hacl_Impl_SHA2_Types_uint8_2p scrut = { .fst = last00, .snd = last10 }; + uint8_t *l0 = scrut.fst; + uint8_t *l1 = scrut.snd; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + Hacl_Impl_SHA2_Types_uint8_2p scrut0 = { .fst = lb0, .snd = lb1 }; + uint8_t *last0 = scrut0.fst; + uint8_t *last1 = scrut0.snd; + sha384_update1(last0, st); + if (blocks > (uint32_t)1U) + { + sha384_update1(last1, st); + } + 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(rb, hbuf, (uint32_t)48U * sizeof (uint8_t)); +} + +static inline void sha512_update1(uint8_t *block, 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 *b = block; + uint64_t u = load64_be(b); + ws[0U] = u; + uint64_t u0 = load64_be(b + (uint32_t)8U); + ws[1U] = u0; + uint64_t u1 = load64_be(b + (uint32_t)16U); + ws[2U] = u1; + uint64_t u2 = load64_be(b + (uint32_t)24U); + ws[3U] = u2; + uint64_t u3 = load64_be(b + (uint32_t)32U); + ws[4U] = u3; + uint64_t u4 = load64_be(b + (uint32_t)40U); + ws[5U] = u4; + uint64_t u5 = load64_be(b + (uint32_t)48U); + ws[6U] = u5; + uint64_t u6 = load64_be(b + (uint32_t)56U); + ws[7U] = u6; + uint64_t u7 = load64_be(b + (uint32_t)64U); + ws[8U] = u7; + uint64_t u8 = load64_be(b + (uint32_t)72U); + ws[9U] = u8; + uint64_t u9 = load64_be(b + (uint32_t)80U); + ws[10U] = u9; + uint64_t u10 = load64_be(b + (uint32_t)88U); + ws[11U] = u10; + uint64_t u11 = load64_be(b + (uint32_t)96U); + ws[12U] = u11; + uint64_t u12 = load64_be(b + (uint32_t)104U); + ws[13U] = u12; + uint64_t u13 = load64_be(b + (uint32_t)112U); + ws[14U] = u13; + uint64_t u14 = load64_be(b + (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(uint8_t *dst, uint32_t input_len, uint8_t *input) +{ + uint8_t *ib = input; + uint8_t *rb = dst; + uint64_t st[8U] = { 0U }; + KRML_MAYBE_FOR8(i, + (uint32_t)0U, + (uint32_t)8U, + (uint32_t)1U, + uint64_t *os = st; + uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; + os[i] = x;); + uint32_t rem = input_len % (uint32_t)128U; + FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); + uint32_t blocks0 = input_len / (uint32_t)128U; + for (uint32_t i = (uint32_t)0U; i < blocks0; i++) + { + uint8_t *b0 = ib; + uint8_t *mb = b0 + i * (uint32_t)128U; + sha512_update1(mb, st); + } + uint32_t rem1 = input_len % (uint32_t)128U; + uint8_t *b0 = ib; + uint8_t *lb = b0 + input_len - rem1; + uint32_t blocks; + if (rem + (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(len_, (uint32_t)3U); + store128_be(totlen_buf, total_len_bits); + uint8_t *b00 = lb; + memcpy(last, b00, rem * sizeof (uint8_t)); + last[rem] = (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; + Hacl_Impl_SHA2_Types_uint8_2p scrut = { .fst = last00, .snd = last10 }; + uint8_t *l0 = scrut.fst; + uint8_t *l1 = scrut.snd; + uint8_t *lb0 = l0; + uint8_t *lb1 = l1; + Hacl_Impl_SHA2_Types_uint8_2p scrut0 = { .fst = lb0, .snd = lb1 }; + uint8_t *last0 = scrut0.fst; + uint8_t *last1 = scrut0.snd; + sha512_update1(last0, st); + if (blocks > (uint32_t)1U) + { + sha512_update1(last1, st); + } + 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(rb, hbuf, (uint32_t)64U * sizeof (uint8_t)); +} + From e3769d6177f3bd679b18f913680cf906e66381a9 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Sun, 19 Feb 2023 14:32:28 +0100 Subject: [PATCH 2/3] calling streaming sha2 --- benchmarks/sha2.cc | 23 +- config/config.json | 4 - config/default_config.cmake | 1 - include/Hacl_SHA2_Scalar32.h | 54 --- src/Hacl_SHA2_Scalar32.c | 772 ----------------------------------- 5 files changed, 4 insertions(+), 850 deletions(-) delete mode 100644 include/Hacl_SHA2_Scalar32.h delete mode 100644 src/Hacl_SHA2_Scalar32.c diff --git a/benchmarks/sha2.cc b/benchmarks/sha2.cc index c149b43fd..544aa9b58 100644 --- a/benchmarks/sha2.cc +++ b/benchmarks/sha2.cc @@ -7,7 +7,6 @@ */ #include "EverCrypt_Hash.h" #include "Hacl_Streaming_SHA2.h" -#include "Hacl_SHA2_Scalar32.h" #include "util.h" @@ -175,14 +174,7 @@ BENCHMARK_CAPTURE(HACL_Sha2_oneshot, sha2_224, HACL_HASH_SHA2_224_DIGEST_LENGTH, expected_digest_sha2_224, - Hacl_Hash_SHA2_hash_224) - ->Setup(DoSetup); - -BENCHMARK_CAPTURE(HACL_Sha2_new_oneshot, - sha2_224_new, - HACL_HASH_SHA2_224_DIGEST_LENGTH, - expected_digest_sha2_224, - Hacl_SHA2_Scalar32_sha224) + Hacl_Streaming_SHA2_sha224) ->Setup(DoSetup); BENCHMARK_CAPTURE(EverCrypt_Sha2_oneshot, @@ -205,14 +197,7 @@ BENCHMARK_CAPTURE(HACL_Sha2_oneshot, sha2_256, HACL_HASH_SHA2_256_DIGEST_LENGTH, expected_digest_sha2_256, - Hacl_Hash_SHA2_hash_256) - ->Setup(DoSetup); - -BENCHMARK_CAPTURE(HACL_Sha2_new_oneshot, - sha2_256_new, - HACL_HASH_SHA2_256_DIGEST_LENGTH, - expected_digest_sha2_256, - Hacl_SHA2_Scalar32_sha256) + Hacl_Streaming_SHA2_sha256) ->Setup(DoSetup); BENCHMARK_CAPTURE(EverCrypt_Sha2_oneshot, @@ -235,7 +220,7 @@ BENCHMARK_CAPTURE(HACL_Sha2_oneshot, sha2_384, HACL_HASH_SHA2_384_DIGEST_LENGTH, expected_digest_sha2_384, - Hacl_Hash_SHA2_hash_384) + Hacl_Streaming_SHA2_sha384) ->Setup(DoSetup); BENCHMARK_CAPTURE(EverCrypt_Sha2_oneshot, @@ -258,7 +243,7 @@ BENCHMARK_CAPTURE(HACL_Sha2_oneshot, sha2_512, HACL_HASH_SHA2_512_DIGEST_LENGTH, expected_digest_sha2_512, - Hacl_Hash_SHA2_hash_512) + Hacl_Streaming_SHA2_sha512) ->Setup(DoSetup); BENCHMARK_CAPTURE(EverCrypt_Sha2_oneshot, diff --git a/config/config.json b/config/config.json index 5aea179f8..d67352aab 100644 --- a/config/config.json +++ b/config/config.json @@ -191,10 +191,6 @@ "file": "Hacl_Hash_SHA2.c", "features": "std" }, - { - "file": "Hacl_SHA2_Scalar32.c", - "features": "std" - }, { "file": "Hacl_SHA2_Vec128.c", "features": "vec128" diff --git a/config/default_config.cmake b/config/default_config.cmake index d2403768c..d50381f6a 100644 --- a/config/default_config.cmake +++ b/config/default_config.cmake @@ -5,7 +5,6 @@ set(SOURCES_std ${PROJECT_SOURCE_DIR}/src/Hacl_Curve25519_51.c ${PROJECT_SOURCE_DIR}/src/Hacl_HMAC_DRBG.c ${PROJECT_SOURCE_DIR}/src/Hacl_HMAC.c - ${PROJECT_SOURCE_DIR}/src/Hacl_SHA2_Scalar32.c ${PROJECT_SOURCE_DIR}/src/Hacl_Hash_SHA2.c ${PROJECT_SOURCE_DIR}/src/Hacl_Hash_SHA1.c ${PROJECT_SOURCE_DIR}/src/Hacl_Hash_Blake2.c diff --git a/include/Hacl_SHA2_Scalar32.h b/include/Hacl_SHA2_Scalar32.h deleted file mode 100644 index 59ecdbe07..000000000 --- a/include/Hacl_SHA2_Scalar32.h +++ /dev/null @@ -1,54 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __Hacl_SHA2_Scalar32_H -#define __Hacl_SHA2_Scalar32_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - - -#include "Hacl_SHA2_Generic.h" -#include "Hacl_Krmllib.h" - -void Hacl_SHA2_Scalar32_sha224(uint8_t *dst, uint32_t input_len, uint8_t *input); - -void Hacl_SHA2_Scalar32_sha256(uint8_t *dst, uint32_t input_len, uint8_t *input); - -void Hacl_SHA2_Scalar32_sha384(uint8_t *dst, uint32_t input_len, uint8_t *input); - -void Hacl_SHA2_Scalar32_sha512(uint8_t *dst, uint32_t input_len, uint8_t *input); - -#if defined(__cplusplus) -} -#endif - -#define __Hacl_SHA2_Scalar32_H_DEFINED -#endif diff --git a/src/Hacl_SHA2_Scalar32.c b/src/Hacl_SHA2_Scalar32.c deleted file mode 100644 index 4dd03d0ed..000000000 --- a/src/Hacl_SHA2_Scalar32.c +++ /dev/null @@ -1,772 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#include "Hacl_SHA2_Scalar32.h" - -#include "internal/Hacl_SHA2_Types.h" - -static inline void sha224_update1(uint8_t *block, 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 *b = block; - uint32_t u = load32_be(b); - ws[0U] = u; - uint32_t u0 = load32_be(b + (uint32_t)4U); - ws[1U] = u0; - uint32_t u1 = load32_be(b + (uint32_t)8U); - ws[2U] = u1; - uint32_t u2 = load32_be(b + (uint32_t)12U); - ws[3U] = u2; - uint32_t u3 = load32_be(b + (uint32_t)16U); - ws[4U] = u3; - uint32_t u4 = load32_be(b + (uint32_t)20U); - ws[5U] = u4; - uint32_t u5 = load32_be(b + (uint32_t)24U); - ws[6U] = u5; - uint32_t u6 = load32_be(b + (uint32_t)28U); - ws[7U] = u6; - uint32_t u7 = load32_be(b + (uint32_t)32U); - ws[8U] = u7; - uint32_t u8 = load32_be(b + (uint32_t)36U); - ws[9U] = u8; - uint32_t u9 = load32_be(b + (uint32_t)40U); - ws[10U] = u9; - uint32_t u10 = load32_be(b + (uint32_t)44U); - ws[11U] = u10; - uint32_t u11 = load32_be(b + (uint32_t)48U); - ws[12U] = u11; - uint32_t u12 = load32_be(b + (uint32_t)52U); - ws[13U] = u12; - uint32_t u13 = load32_be(b + (uint32_t)56U); - ws[14U] = u13; - uint32_t u14 = load32_be(b + (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_sha224(uint8_t *dst, uint32_t input_len, uint8_t *input) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint32_t st[8U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint32_t *os = st; - uint32_t x = Hacl_Impl_SHA2_Generic_h224[i]; - os[i] = x;); - uint32_t rem = input_len % (uint32_t)64U; - uint64_t len_ = (uint64_t)input_len; - uint32_t blocks0 = input_len / (uint32_t)64U; - for (uint32_t i = (uint32_t)0U; i < blocks0; i++) - { - uint8_t *b0 = ib; - uint8_t *mb = b0 + i * (uint32_t)64U; - sha224_update1(mb, st); - } - uint32_t rem1 = input_len % (uint32_t)64U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - uint32_t blocks; - if (rem + (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 = len_ << (uint32_t)3U; - store64_be(totlen_buf, total_len_bits); - uint8_t *b00 = lb; - memcpy(last, b00, rem * sizeof (uint8_t)); - last[rem] = (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; - Hacl_Impl_SHA2_Types_uint8_2p scrut = { .fst = last00, .snd = last10 }; - uint8_t *l0 = scrut.fst; - uint8_t *l1 = scrut.snd; - uint8_t *lb0 = l0; - uint8_t *lb1 = l1; - Hacl_Impl_SHA2_Types_uint8_2p scrut0 = { .fst = lb0, .snd = lb1 }; - uint8_t *last0 = scrut0.fst; - uint8_t *last1 = scrut0.snd; - sha224_update1(last0, st); - if (blocks > (uint32_t)1U) - { - sha224_update1(last1, st); - } - 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(rb, hbuf, (uint32_t)28U * sizeof (uint8_t)); -} - -static inline void sha256_update1(uint8_t *block, 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 *b = block; - uint32_t u = load32_be(b); - ws[0U] = u; - uint32_t u0 = load32_be(b + (uint32_t)4U); - ws[1U] = u0; - uint32_t u1 = load32_be(b + (uint32_t)8U); - ws[2U] = u1; - uint32_t u2 = load32_be(b + (uint32_t)12U); - ws[3U] = u2; - uint32_t u3 = load32_be(b + (uint32_t)16U); - ws[4U] = u3; - uint32_t u4 = load32_be(b + (uint32_t)20U); - ws[5U] = u4; - uint32_t u5 = load32_be(b + (uint32_t)24U); - ws[6U] = u5; - uint32_t u6 = load32_be(b + (uint32_t)28U); - ws[7U] = u6; - uint32_t u7 = load32_be(b + (uint32_t)32U); - ws[8U] = u7; - uint32_t u8 = load32_be(b + (uint32_t)36U); - ws[9U] = u8; - uint32_t u9 = load32_be(b + (uint32_t)40U); - ws[10U] = u9; - uint32_t u10 = load32_be(b + (uint32_t)44U); - ws[11U] = u10; - uint32_t u11 = load32_be(b + (uint32_t)48U); - ws[12U] = u11; - uint32_t u12 = load32_be(b + (uint32_t)52U); - ws[13U] = u12; - uint32_t u13 = load32_be(b + (uint32_t)56U); - ws[14U] = u13; - uint32_t u14 = load32_be(b + (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(uint8_t *dst, uint32_t input_len, uint8_t *input) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint32_t st[8U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint32_t *os = st; - uint32_t x = Hacl_Impl_SHA2_Generic_h256[i]; - os[i] = x;); - uint32_t rem = input_len % (uint32_t)64U; - uint64_t len_ = (uint64_t)input_len; - uint32_t blocks0 = input_len / (uint32_t)64U; - for (uint32_t i = (uint32_t)0U; i < blocks0; i++) - { - uint8_t *b0 = ib; - uint8_t *mb = b0 + i * (uint32_t)64U; - sha256_update1(mb, st); - } - uint32_t rem1 = input_len % (uint32_t)64U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - uint32_t blocks; - if (rem + (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 = len_ << (uint32_t)3U; - store64_be(totlen_buf, total_len_bits); - uint8_t *b00 = lb; - memcpy(last, b00, rem * sizeof (uint8_t)); - last[rem] = (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; - Hacl_Impl_SHA2_Types_uint8_2p scrut = { .fst = last00, .snd = last10 }; - uint8_t *l0 = scrut.fst; - uint8_t *l1 = scrut.snd; - uint8_t *lb0 = l0; - uint8_t *lb1 = l1; - Hacl_Impl_SHA2_Types_uint8_2p scrut0 = { .fst = lb0, .snd = lb1 }; - uint8_t *last0 = scrut0.fst; - uint8_t *last1 = scrut0.snd; - sha256_update1(last0, st); - if (blocks > (uint32_t)1U) - { - sha256_update1(last1, st); - } - 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(rb, hbuf, (uint32_t)32U * sizeof (uint8_t)); -} - -static inline void sha384_update1(uint8_t *block, 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 *b = block; - uint64_t u = load64_be(b); - ws[0U] = u; - uint64_t u0 = load64_be(b + (uint32_t)8U); - ws[1U] = u0; - uint64_t u1 = load64_be(b + (uint32_t)16U); - ws[2U] = u1; - uint64_t u2 = load64_be(b + (uint32_t)24U); - ws[3U] = u2; - uint64_t u3 = load64_be(b + (uint32_t)32U); - ws[4U] = u3; - uint64_t u4 = load64_be(b + (uint32_t)40U); - ws[5U] = u4; - uint64_t u5 = load64_be(b + (uint32_t)48U); - ws[6U] = u5; - uint64_t u6 = load64_be(b + (uint32_t)56U); - ws[7U] = u6; - uint64_t u7 = load64_be(b + (uint32_t)64U); - ws[8U] = u7; - uint64_t u8 = load64_be(b + (uint32_t)72U); - ws[9U] = u8; - uint64_t u9 = load64_be(b + (uint32_t)80U); - ws[10U] = u9; - uint64_t u10 = load64_be(b + (uint32_t)88U); - ws[11U] = u10; - uint64_t u11 = load64_be(b + (uint32_t)96U); - ws[12U] = u11; - uint64_t u12 = load64_be(b + (uint32_t)104U); - ws[13U] = u12; - uint64_t u13 = load64_be(b + (uint32_t)112U); - ws[14U] = u13; - uint64_t u14 = load64_be(b + (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_sha384(uint8_t *dst, uint32_t input_len, uint8_t *input) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint64_t st[8U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint64_t *os = st; - uint64_t x = Hacl_Impl_SHA2_Generic_h384[i]; - os[i] = x;); - uint32_t rem = input_len % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); - uint32_t blocks0 = input_len / (uint32_t)128U; - for (uint32_t i = (uint32_t)0U; i < blocks0; i++) - { - uint8_t *b0 = ib; - uint8_t *mb = b0 + i * (uint32_t)128U; - sha384_update1(mb, st); - } - uint32_t rem1 = input_len % (uint32_t)128U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - uint32_t blocks; - if (rem + (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(len_, (uint32_t)3U); - store128_be(totlen_buf, total_len_bits); - uint8_t *b00 = lb; - memcpy(last, b00, rem * sizeof (uint8_t)); - last[rem] = (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; - Hacl_Impl_SHA2_Types_uint8_2p scrut = { .fst = last00, .snd = last10 }; - uint8_t *l0 = scrut.fst; - uint8_t *l1 = scrut.snd; - uint8_t *lb0 = l0; - uint8_t *lb1 = l1; - Hacl_Impl_SHA2_Types_uint8_2p scrut0 = { .fst = lb0, .snd = lb1 }; - uint8_t *last0 = scrut0.fst; - uint8_t *last1 = scrut0.snd; - sha384_update1(last0, st); - if (blocks > (uint32_t)1U) - { - sha384_update1(last1, st); - } - 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(rb, hbuf, (uint32_t)48U * sizeof (uint8_t)); -} - -static inline void sha512_update1(uint8_t *block, 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 *b = block; - uint64_t u = load64_be(b); - ws[0U] = u; - uint64_t u0 = load64_be(b + (uint32_t)8U); - ws[1U] = u0; - uint64_t u1 = load64_be(b + (uint32_t)16U); - ws[2U] = u1; - uint64_t u2 = load64_be(b + (uint32_t)24U); - ws[3U] = u2; - uint64_t u3 = load64_be(b + (uint32_t)32U); - ws[4U] = u3; - uint64_t u4 = load64_be(b + (uint32_t)40U); - ws[5U] = u4; - uint64_t u5 = load64_be(b + (uint32_t)48U); - ws[6U] = u5; - uint64_t u6 = load64_be(b + (uint32_t)56U); - ws[7U] = u6; - uint64_t u7 = load64_be(b + (uint32_t)64U); - ws[8U] = u7; - uint64_t u8 = load64_be(b + (uint32_t)72U); - ws[9U] = u8; - uint64_t u9 = load64_be(b + (uint32_t)80U); - ws[10U] = u9; - uint64_t u10 = load64_be(b + (uint32_t)88U); - ws[11U] = u10; - uint64_t u11 = load64_be(b + (uint32_t)96U); - ws[12U] = u11; - uint64_t u12 = load64_be(b + (uint32_t)104U); - ws[13U] = u12; - uint64_t u13 = load64_be(b + (uint32_t)112U); - ws[14U] = u13; - uint64_t u14 = load64_be(b + (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(uint8_t *dst, uint32_t input_len, uint8_t *input) -{ - uint8_t *ib = input; - uint8_t *rb = dst; - uint64_t st[8U] = { 0U }; - KRML_MAYBE_FOR8(i, - (uint32_t)0U, - (uint32_t)8U, - (uint32_t)1U, - uint64_t *os = st; - uint64_t x = Hacl_Impl_SHA2_Generic_h512[i]; - os[i] = x;); - uint32_t rem = input_len % (uint32_t)128U; - FStar_UInt128_uint128 len_ = FStar_UInt128_uint64_to_uint128((uint64_t)input_len); - uint32_t blocks0 = input_len / (uint32_t)128U; - for (uint32_t i = (uint32_t)0U; i < blocks0; i++) - { - uint8_t *b0 = ib; - uint8_t *mb = b0 + i * (uint32_t)128U; - sha512_update1(mb, st); - } - uint32_t rem1 = input_len % (uint32_t)128U; - uint8_t *b0 = ib; - uint8_t *lb = b0 + input_len - rem1; - uint32_t blocks; - if (rem + (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(len_, (uint32_t)3U); - store128_be(totlen_buf, total_len_bits); - uint8_t *b00 = lb; - memcpy(last, b00, rem * sizeof (uint8_t)); - last[rem] = (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; - Hacl_Impl_SHA2_Types_uint8_2p scrut = { .fst = last00, .snd = last10 }; - uint8_t *l0 = scrut.fst; - uint8_t *l1 = scrut.snd; - uint8_t *lb0 = l0; - uint8_t *lb1 = l1; - Hacl_Impl_SHA2_Types_uint8_2p scrut0 = { .fst = lb0, .snd = lb1 }; - uint8_t *last0 = scrut0.fst; - uint8_t *last1 = scrut0.snd; - sha512_update1(last0, st); - if (blocks > (uint32_t)1U) - { - sha512_update1(last1, st); - } - 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(rb, hbuf, (uint32_t)64U * sizeof (uint8_t)); -} - From 98f154174eb391fdb200ba4513682e75e56fcbdc Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Sun, 19 Feb 2023 14:39:22 +0100 Subject: [PATCH 3/3] cleanup --- include/Hacl_SHA2_Generic.h | 134 --------- include/MerkleTree.h | 551 ------------------------------------ include/config.h | 4 - include/msvc/config.h | 4 - 4 files changed, 693 deletions(-) delete mode 100644 include/Hacl_SHA2_Generic.h delete mode 100644 include/MerkleTree.h delete mode 100644 include/config.h delete mode 100644 include/msvc/config.h diff --git a/include/Hacl_SHA2_Generic.h b/include/Hacl_SHA2_Generic.h deleted file mode 100644 index 3a6a75483..000000000 --- a/include/Hacl_SHA2_Generic.h +++ /dev/null @@ -1,134 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __Hacl_SHA2_Generic_H -#define __Hacl_SHA2_Generic_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - - - - -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 - }; - -#if defined(__cplusplus) -} -#endif - -#define __Hacl_SHA2_Generic_H_DEFINED -#endif diff --git a/include/MerkleTree.h b/include/MerkleTree.h deleted file mode 100644 index 3b9ae523f..000000000 --- a/include/MerkleTree.h +++ /dev/null @@ -1,551 +0,0 @@ -/* MIT License - * - * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - */ - - -#ifndef __MerkleTree_H -#define __MerkleTree_H - -#if defined(__cplusplus) -extern "C" { -#endif - -#include -#include "krml/internal/types.h" -#include "krml/lowstar_endianness.h" -#include "krml/internal/target.h" - - -#include "Hacl_Spec.h" -#include "EverCrypt_Hash.h" - -typedef struct MerkleTree_Low_Datastructures_hash_vec_s -{ - uint32_t sz; - uint32_t cap; - uint8_t **vs; -} -MerkleTree_Low_Datastructures_hash_vec; - -typedef struct MerkleTree_Low_Datastructures_hash_vv_s -{ - uint32_t sz; - uint32_t cap; - MerkleTree_Low_Datastructures_hash_vec *vs; -} -MerkleTree_Low_Datastructures_hash_vv; - -typedef uint32_t hash_size_t; - -typedef uint64_t offset_t; - -typedef uint32_t index_t; - -typedef uint8_t *hash; - -typedef struct MerkleTree_Low_path_s -{ - uint32_t hash_size; - MerkleTree_Low_Datastructures_hash_vec hashes; -} -MerkleTree_Low_path; - -typedef MerkleTree_Low_path path; - -typedef MerkleTree_Low_path *path_p; - -typedef const MerkleTree_Low_path *const_path_p; - -typedef struct MerkleTree_Low_merkle_tree_s -{ - uint32_t hash_size; - uint64_t offset; - uint32_t i; - uint32_t j; - MerkleTree_Low_Datastructures_hash_vv hs; - bool rhs_ok; - MerkleTree_Low_Datastructures_hash_vec rhs; - uint8_t *mroot; - void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2); -} -MerkleTree_Low_merkle_tree; - -typedef MerkleTree_Low_merkle_tree merkle_tree; - -typedef MerkleTree_Low_merkle_tree *mt_p; - -typedef const MerkleTree_Low_merkle_tree *const_mt_p; - -/** - Constructor for hashes -*/ -uint8_t *mt_init_hash(uint32_t hash_size); - -/** - Destructor for hashes -*/ -void mt_free_hash(uint8_t *h); - -/** - Constructor for paths -*/ -MerkleTree_Low_path *mt_init_path(uint32_t hash_size); - -/** - Destructor for paths -*/ -void mt_free_path(MerkleTree_Low_path *path1); - -/** - Length of a path - - @param[in] p Path - - return The length of the path -*/ -uint32_t mt_get_path_length(const MerkleTree_Low_path *path1); - -/** - Insert hash into path - - @param[in] p Path - @param[in] hash Hash to insert -*/ -void mt_path_insert(MerkleTree_Low_path *path1, uint8_t *hash1); - -/** - Get step on a path - - @param[in] p Path - @param[in] i Path step index - - return The hash at step i of p -*/ -uint8_t *mt_get_path_step(const MerkleTree_Low_path *path1, uint32_t i); - -/** - Precondition predicate for mt_get_path_step -*/ -bool mt_get_path_step_pre(const MerkleTree_Low_path *path1, uint32_t i); - -/** - Construction with custom hash functions - - @param[in] hash_size Hash size (in bytes) - @param[in] i The initial hash - - return The new Merkle tree -*/ -MerkleTree_Low_merkle_tree -*mt_create_custom( - uint32_t hash_size, - uint8_t *i, - void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2) -); - -/** - Destruction - - @param[in] mt The Merkle tree -*/ -void mt_free(MerkleTree_Low_merkle_tree *mt); - -/** - Insertion - - @param[in] mt The Merkle tree - @param[in] v The tree does not take ownership of the hash, it makes a copy of its content. - - Note: The content of the hash will be overwritten with an arbitrary value. -*/ -void mt_insert(MerkleTree_Low_merkle_tree *mt, uint8_t *v); - -/** - Precondition predicate for mt_insert -*/ -bool mt_insert_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *v); - -/** - Getting the Merkle root - - @param[in] mt The Merkle tree - @param[out] root The Merkle root -*/ -void mt_get_root(const MerkleTree_Low_merkle_tree *mt, uint8_t *root); - -/** - Precondition predicate for mt_get_root -*/ -bool mt_get_root_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *root); - -/** - Getting a Merkle path - - @param[in] mt The Merkle tree - @param[in] idx The index of the target hash - @param[out] path A resulting Merkle path that contains the leaf hash. - @param[out] root The Merkle root - - return The number of elements in the tree - - Notes: - - The resulting path contains pointers to hashes in the tree, not copies of - the hash values. - - idx must be within the currently held indices in the tree (past the - last flush index). -*/ -uint32_t -mt_get_path( - const MerkleTree_Low_merkle_tree *mt, - uint64_t idx, - MerkleTree_Low_path *path1, - uint8_t *root -); - -/** - Precondition predicate for mt_get_path -*/ -bool -mt_get_path_pre( - const MerkleTree_Low_merkle_tree *mt, - uint64_t idx, - const MerkleTree_Low_path *path1, - uint8_t *root -); - -/** - Flush the Merkle tree - - @param[in] mt The Merkle tree -*/ -void mt_flush(MerkleTree_Low_merkle_tree *mt); - -/** - Precondition predicate for mt_flush -*/ -bool mt_flush_pre(const MerkleTree_Low_merkle_tree *mt); - -/** - Flush the Merkle tree up to a given index - - @param[in] mt The Merkle tree - @param[in] idx The index up to which to flush the tree -*/ -void mt_flush_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx); - -/** - Precondition predicate for mt_flush_to -*/ -bool mt_flush_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx); - -/** - Retract the Merkle tree down to a given index - - @param[in] mt The Merkle tree - @param[in] idx The index to retract the tree to - - Note: The element and idx will remain in the tree. -*/ -void mt_retract_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx); - -/** - Precondition predicate for mt_retract_to -*/ -bool mt_retract_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx); - -/** - Client-side verification - - @param[in] mt The Merkle tree - @param[in] tgt The index of the target hash - @param[in] max The maximum index + 1 of the tree when the path was generated - @param[in] path The Merkle path to verify - @param[in] root - - return true if the verification succeeded, false otherwise - - Note: max - tgt must be less than 2^32. -*/ -bool -mt_verify( - const MerkleTree_Low_merkle_tree *mt, - uint64_t tgt, - uint64_t max, - const MerkleTree_Low_path *path1, - uint8_t *root -); - -/** - Precondition predicate for mt_verify -*/ -bool -mt_verify_pre( - const MerkleTree_Low_merkle_tree *mt, - uint64_t tgt, - uint64_t max, - const MerkleTree_Low_path *path1, - uint8_t *root -); - -/** - Serialization size - - @param[in] mt The Merkle tree - - return the number of bytes required to serialize the tree -*/ -uint64_t mt_serialize_size(const MerkleTree_Low_merkle_tree *mt); - -/** - Merkle tree serialization - - @param[in] mt The Merkle tree - @param[out] buf The buffer to serialize the tree into - @param[in] len Length of buf - - return the number of bytes written - - Note: buf must be a buffer of size mt_serialize_size(mt) or larger, but - smaller than 2^32 (larger buffers are currently not supported). -*/ -uint64_t mt_serialize(const MerkleTree_Low_merkle_tree *mt, uint8_t *buf, uint64_t len); - -/** - Merkle tree deserialization - - @param[in] expected_hash_size Expected hash size to match hash_fun - @param[in] buf The buffer to deserialize the tree from - @param[in] len Length of buf - @param[in] hash_fun Hash function - - return pointer to the new tree if successful, NULL otherwise - - Note: buf must point to an allocated buffer. -*/ -MerkleTree_Low_merkle_tree -*mt_deserialize( - const uint8_t *buf, - uint64_t len, - void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2) -); - -/** - Path serialization - - @param[in] path The path - @param[out] buf The buffer to serialize the path into - @param[in] len Length of buf - - return the number of bytes written -*/ -uint64_t mt_serialize_path(const MerkleTree_Low_path *path1, uint8_t *buf, uint64_t len); - -/** - Path deserialization - - @param[in] buf The buffer to deserialize the path from - @param[in] len Length of buf - - return pointer to the new path if successful, NULL otherwise - - Note: buf must point to an allocated buffer. -*/ -MerkleTree_Low_path *mt_deserialize_path(const uint8_t *buf, uint64_t len); - -/** - Default hash function -*/ -void mt_sha256_compress(uint8_t *src1, uint8_t *src2, uint8_t *dst); - -/** - Construction wired to sha256 from EverCrypt - - @param[in] init The initial hash -*/ -MerkleTree_Low_merkle_tree *mt_create(uint8_t *init); - -typedef uint32_t MerkleTree_Low_index_t; - -extern uint32_t MerkleTree_Low_uint32_32_max; - -extern uint64_t MerkleTree_Low_uint32_max; - -extern uint64_t MerkleTree_Low_uint64_max; - -extern uint64_t MerkleTree_Low_offset_range_limit; - -typedef uint64_t MerkleTree_Low_offset_t; - -extern uint32_t MerkleTree_Low_merkle_tree_size_lg; - -bool MerkleTree_Low_uu___is_MT(MerkleTree_Low_merkle_tree projectee); - -typedef MerkleTree_Low_merkle_tree *MerkleTree_Low_mt_p; - -typedef const MerkleTree_Low_merkle_tree *MerkleTree_Low_const_mt_p; - -bool -MerkleTree_Low_merkle_tree_conditions( - uint64_t offset, - uint32_t i, - uint32_t j, - MerkleTree_Low_Datastructures_hash_vv hs, - bool rhs_ok, - MerkleTree_Low_Datastructures_hash_vec rhs, - uint8_t *mroot -); - -uint32_t MerkleTree_Low_offset_of(uint32_t i); - -void MerkleTree_Low_mt_free(MerkleTree_Low_merkle_tree *mt); - -bool MerkleTree_Low_mt_insert_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *v); - -void MerkleTree_Low_mt_insert(MerkleTree_Low_merkle_tree *mt, uint8_t *v); - -MerkleTree_Low_merkle_tree -*MerkleTree_Low_mt_create_custom( - uint32_t hsz, - uint8_t *init, - void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2) -); - -bool MerkleTree_Low_uu___is_Path(MerkleTree_Low_path projectee); - -typedef MerkleTree_Low_path *MerkleTree_Low_path_p; - -typedef const MerkleTree_Low_path *MerkleTree_Low_const_path_p; - -MerkleTree_Low_path *MerkleTree_Low_init_path(uint32_t hsz); - -void MerkleTree_Low_clear_path(MerkleTree_Low_path *p); - -void MerkleTree_Low_free_path(MerkleTree_Low_path *p); - -bool MerkleTree_Low_mt_get_root_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *rt); - -void MerkleTree_Low_mt_get_root(const MerkleTree_Low_merkle_tree *mt, uint8_t *rt); - -void MerkleTree_Low_mt_path_insert(uint32_t hsz, MerkleTree_Low_path *p, uint8_t *hp); - -uint32_t MerkleTree_Low_mt_get_path_length(const MerkleTree_Low_path *p); - -bool MerkleTree_Low_mt_get_path_step_pre(const MerkleTree_Low_path *p, uint32_t i); - -uint8_t *MerkleTree_Low_mt_get_path_step(const MerkleTree_Low_path *p, uint32_t i); - -bool -MerkleTree_Low_mt_get_path_pre( - const MerkleTree_Low_merkle_tree *mt, - uint64_t idx, - const MerkleTree_Low_path *p, - uint8_t *root -); - -uint32_t -MerkleTree_Low_mt_get_path( - const MerkleTree_Low_merkle_tree *mt, - uint64_t idx, - MerkleTree_Low_path *p, - uint8_t *root -); - -bool MerkleTree_Low_mt_flush_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx); - -void MerkleTree_Low_mt_flush_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx); - -bool MerkleTree_Low_mt_flush_pre(const MerkleTree_Low_merkle_tree *mt); - -void MerkleTree_Low_mt_flush(MerkleTree_Low_merkle_tree *mt); - -bool MerkleTree_Low_mt_retract_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t r); - -void MerkleTree_Low_mt_retract_to(MerkleTree_Low_merkle_tree *mt, uint64_t r); - -bool -MerkleTree_Low_mt_verify_pre( - const MerkleTree_Low_merkle_tree *mt, - uint64_t k, - uint64_t j, - const MerkleTree_Low_path *p, - uint8_t *rt -); - -bool -MerkleTree_Low_mt_verify( - const MerkleTree_Low_merkle_tree *mt, - uint64_t k, - uint64_t j, - const MerkleTree_Low_path *p, - uint8_t *rt -); - -typedef uint8_t MerkleTree_Low_Serialization_uint8_t; - -typedef uint16_t MerkleTree_Low_Serialization_uint16_t; - -typedef uint32_t MerkleTree_Low_Serialization_uint32_t; - -typedef uint64_t MerkleTree_Low_Serialization_uint64_t; - -typedef uint8_t *MerkleTree_Low_Serialization_uint8_p; - -typedef const uint8_t *MerkleTree_Low_Serialization_const_uint8_p; - -uint64_t MerkleTree_Low_Serialization_mt_serialize_size(const MerkleTree_Low_merkle_tree *mt); - -uint64_t -MerkleTree_Low_Serialization_mt_serialize( - const MerkleTree_Low_merkle_tree *mt, - uint8_t *output, - uint64_t sz -); - -MerkleTree_Low_merkle_tree -*MerkleTree_Low_Serialization_mt_deserialize( - const uint8_t *input, - uint64_t sz, - void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2) -); - -uint64_t -MerkleTree_Low_Serialization_mt_serialize_path( - const MerkleTree_Low_path *p, - uint8_t *output, - uint64_t sz -); - -MerkleTree_Low_path -*MerkleTree_Low_Serialization_mt_deserialize_path(const uint8_t *input, uint64_t sz); - -uint8_t *MerkleTree_Low_Hashfunctions_init_hash(uint32_t hsz); - -void MerkleTree_Low_Hashfunctions_free_hash(uint8_t *h); - -typedef void (*MerkleTree_Low_Hashfunctions_hash_fun_t)(uint8_t *x0, uint8_t *x1, uint8_t *x2); - -#if defined(__cplusplus) -} -#endif - -#define __MerkleTree_H_DEFINED -#endif diff --git a/include/config.h b/include/config.h deleted file mode 100644 index d8bf2f048..000000000 --- a/include/config.h +++ /dev/null @@ -1,4 +0,0 @@ -#define TARGET_ARCHITECTURE TARGET_ARCHITECTURE_ID_ARM8 -#define HACL_CAN_COMPILE_VEC128 1 -#define Lib_IntVector_Intrinsics_vec256 void * -#define HACL_CAN_COMPILE_UINT128 1 diff --git a/include/msvc/config.h b/include/msvc/config.h deleted file mode 100644 index d8bf2f048..000000000 --- a/include/msvc/config.h +++ /dev/null @@ -1,4 +0,0 @@ -#define TARGET_ARCHITECTURE TARGET_ARCHITECTURE_ID_ARM8 -#define HACL_CAN_COMPILE_VEC128 1 -#define Lib_IntVector_Intrinsics_vec256 void * -#define HACL_CAN_COMPILE_UINT128 1