Skip to content

Commit

Permalink
Integrate Vectorized SHA3
Browse files Browse the repository at this point in the history
  • Loading branch information
mamonet committed Dec 1, 2023
1 parent 3f8e5a4 commit 650268c
Show file tree
Hide file tree
Showing 8 changed files with 13,221 additions and 0 deletions.
13 changes: 13 additions & 0 deletions config/config.json
Original file line number Diff line number Diff line change
Expand Up @@ -325,6 +325,16 @@
"file": "Hacl_Frodo_KEM.c",
"features": "std"
}
],
"sha3-mb": [
{
"file": "Hacl_SHA3_Scalar.c",
"features": "std"
},
{
"file": "Hacl_SHA3_Vec256.c",
"features": "vec256"
}
]
},
"vale_sources": {
Expand Down Expand Up @@ -497,6 +507,9 @@
],
"aead": [
"aead.cc"
],
"sha3-mb": [
"sha3-mb.cc"
]
},
"benchmarks": {
Expand Down
13 changes: 13 additions & 0 deletions config/default_config.cmake
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ set(SOURCES_std
${PROJECT_SOURCE_DIR}/src/EverCrypt_Chacha20Poly1305.c
${PROJECT_SOURCE_DIR}/src/EverCrypt_Poly1305.c
${PROJECT_SOURCE_DIR}/src/EverCrypt_AEAD.c
${PROJECT_SOURCE_DIR}/src/Hacl_SHA3_Scalar.c
)
set(SOURCES_vec256
${PROJECT_SOURCE_DIR}/src/Hacl_Hash_Blake2b_Simd256.c
Expand All @@ -64,6 +65,7 @@ set(SOURCES_vec256
${PROJECT_SOURCE_DIR}/src/Hacl_HPKE_Curve51_CP256_SHA256.c
${PROJECT_SOURCE_DIR}/src/Hacl_HPKE_Curve51_CP256_SHA512.c
${PROJECT_SOURCE_DIR}/src/Hacl_HPKE_P256_CP256_SHA256.c
${PROJECT_SOURCE_DIR}/src/Hacl_SHA3_Vec256.c
)
set(SOURCES_vec128
${PROJECT_SOURCE_DIR}/src/Hacl_Hash_Blake2s_Simd128.c
Expand Down Expand Up @@ -239,6 +241,9 @@ set(INCLUDES
${PROJECT_SOURCE_DIR}/include/EverCrypt_Chacha20Poly1305.h
${PROJECT_SOURCE_DIR}/include/EverCrypt_Poly1305.h
${PROJECT_SOURCE_DIR}/include/EverCrypt_AEAD.h
${PROJECT_SOURCE_DIR}/include/internal/Hacl_SHA3_Scalar.h
${PROJECT_SOURCE_DIR}/include/Hacl_SHA3_Scalar.h
${PROJECT_SOURCE_DIR}/include/Hacl_SHA3_Vec256.h
)
set(PUBLIC_INCLUDES
${PROJECT_SOURCE_DIR}/include/Hacl_NaCl.h
Expand Down Expand Up @@ -349,6 +354,8 @@ set(PUBLIC_INCLUDES
${PROJECT_SOURCE_DIR}/include/EverCrypt_Chacha20Poly1305.h
${PROJECT_SOURCE_DIR}/include/EverCrypt_Poly1305.h
${PROJECT_SOURCE_DIR}/include/EverCrypt_AEAD.h
${PROJECT_SOURCE_DIR}/include/Hacl_SHA3_Scalar.h
${PROJECT_SOURCE_DIR}/include/Hacl_SHA3_Vec256.h
)
set(ALGORITHMS
nacl
Expand All @@ -373,6 +380,7 @@ set(ALGORITHMS
rsapss
hpke
frodo
sha3-mb
)
set(INCLUDE_PATHS
${PROJECT_SOURCE_DIR}/include
Expand Down Expand Up @@ -406,6 +414,7 @@ set(TEST_SOURCES
${PROJECT_SOURCE_DIR}/tests/nacl.cc
${PROJECT_SOURCE_DIR}/tests/evercrypt.cc
${PROJECT_SOURCE_DIR}/tests/aead.cc
${PROJECT_SOURCE_DIR}/tests/sha3-mb.cc
)
set(BENCHMARK_SOURCES
${PROJECT_SOURCE_DIR}/benchmarks/blake.cc
Expand Down Expand Up @@ -474,6 +483,7 @@ set(ALGORITHM_TEST_FILES
TEST_FILES_nacl
TEST_FILES_evercrypt
TEST_FILES_aead
TEST_FILES_sha3_mb
)
set(TEST_FILES_detection
detection.cc
Expand Down Expand Up @@ -541,3 +551,6 @@ set(TEST_FILES_evercrypt
set(TEST_FILES_aead
aead.cc
)
set(TEST_FILES_sha3_mb
sha3-mb.cc
)
67 changes: 67 additions & 0 deletions include/Hacl_SHA3_Scalar.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
/* MIT License
*
* Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
* Copyright (c) 2022-2023 HACL* Contributors
*
* 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_SHA3_Scalar_H
#define __Hacl_SHA3_Scalar_H

#if defined(__cplusplus)
extern "C" {
#endif

#include <string.h>
#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"

void
Hacl_SHA3_Scalar_shake128_hacl(
uint32_t inputByteLen,
uint8_t *input,
uint32_t outputByteLen,
uint8_t *output
);

void
Hacl_SHA3_Scalar_shake256_hacl(
uint32_t inputByteLen,
uint8_t *input,
uint32_t outputByteLen,
uint8_t *output
);

void Hacl_SHA3_Scalar_sha3_224(uint32_t inputByteLen, uint8_t *input, uint8_t *output);

void Hacl_SHA3_Scalar_sha3_256(uint32_t inputByteLen, uint8_t *input, uint8_t *output);

void Hacl_SHA3_Scalar_sha3_384(uint32_t inputByteLen, uint8_t *input, uint8_t *output);

void Hacl_SHA3_Scalar_sha3_512(uint32_t inputByteLen, uint8_t *input, uint8_t *output);

#if defined(__cplusplus)
}
#endif

#define __Hacl_SHA3_Scalar_H_DEFINED
#endif
146 changes: 146 additions & 0 deletions include/Hacl_SHA3_Vec256.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,146 @@
/* MIT License
*
* Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
* Copyright (c) 2022-2023 HACL* Contributors
*
* 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_SHA3_Vec256_H
#define __Hacl_SHA3_Vec256_H

#if defined(__cplusplus)
extern "C" {
#endif

#include <string.h>
#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"

typedef void *Hacl_SHA3_Vec256_disjoint4_4;

typedef struct K____uint8_t___uint8_t__s
{
uint8_t *fst;
uint8_t *snd;
}
K____uint8_t___uint8_t_;

typedef struct K____uint8_t__K____uint8_t___uint8_t__s
{
uint8_t *fst;
K____uint8_t___uint8_t_ snd;
}
K____uint8_t__K____uint8_t___uint8_t_;

typedef struct K____uint8_t___uint8_t____K____uint8_t___uint8_t__s
{
uint8_t *fst;
K____uint8_t__K____uint8_t___uint8_t_ snd;
}
K____uint8_t___uint8_t____K____uint8_t___uint8_t_;

void
Hacl_SHA3_Vec256_shake128_vec256(
uint32_t inputByteLen,
uint8_t *input0,
uint8_t *input1,
uint8_t *input2,
uint8_t *input3,
uint32_t outputByteLen,
uint8_t *output0,
uint8_t *output1,
uint8_t *output2,
uint8_t *output3
);

void
Hacl_SHA3_Vec256_shake256_vec256(
uint32_t inputByteLen,
uint8_t *input0,
uint8_t *input1,
uint8_t *input2,
uint8_t *input3,
uint32_t outputByteLen,
uint8_t *output0,
uint8_t *output1,
uint8_t *output2,
uint8_t *output3
);

void
Hacl_SHA3_Vec256_sha3_224_vec256(
uint32_t inputByteLen,
uint8_t *input0,
uint8_t *input1,
uint8_t *input2,
uint8_t *input3,
uint8_t *output0,
uint8_t *output1,
uint8_t *output2,
uint8_t *output3
);

void
Hacl_SHA3_Vec256_sha3_256_vec256(
uint32_t inputByteLen,
uint8_t *input0,
uint8_t *input1,
uint8_t *input2,
uint8_t *input3,
uint8_t *output0,
uint8_t *output1,
uint8_t *output2,
uint8_t *output3
);

void
Hacl_SHA3_Vec256_sha3_384_vec256(
uint32_t inputByteLen,
uint8_t *input0,
uint8_t *input1,
uint8_t *input2,
uint8_t *input3,
uint8_t *output0,
uint8_t *output1,
uint8_t *output2,
uint8_t *output3
);

void
Hacl_SHA3_Vec256_sha3_512_vec256(
uint32_t inputByteLen,
uint8_t *input0,
uint8_t *input1,
uint8_t *input2,
uint8_t *input3,
uint8_t *output0,
uint8_t *output1,
uint8_t *output2,
uint8_t *output3
);

#if defined(__cplusplus)
}
#endif

#define __Hacl_SHA3_Vec256_H_DEFINED
#endif
51 changes: 51 additions & 0 deletions include/internal/Hacl_SHA3_Scalar.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
/* MIT License
*
* Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
* Copyright (c) 2022-2023 HACL* Contributors
*
* 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 __internal_Hacl_SHA3_Scalar_H
#define __internal_Hacl_SHA3_Scalar_H

#if defined(__cplusplus)
extern "C" {
#endif

#include <string.h>
#include "krml/internal/types.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/target.h"

#include "../Hacl_SHA3_Scalar.h"

extern const uint32_t Hacl_Impl_SHA3_Vec_keccak_rotc[24U];

extern const uint32_t Hacl_Impl_SHA3_Vec_keccak_piln[24U];

extern const uint64_t Hacl_Impl_SHA3_Vec_keccak_rndc[24U];

#if defined(__cplusplus)
}
#endif

#define __internal_Hacl_SHA3_Scalar_H_DEFINED
#endif
Loading

0 comments on commit 650268c

Please sign in to comment.