Integrate Vectorized SHA3

config/config.json

@@ -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": {

config/default_config.cmake

@@ -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
@@ -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
@@ -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
@@ -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
@@ -373,6 +380,7 @@ set(ALGORITHMS
 	rsapss
 	hpke
 	frodo
+	sha3-mb
 )
 set(INCLUDE_PATHS
 	${PROJECT_SOURCE_DIR}/include

examples/cmake/blake-example.cc

@@ -5,7 +5,7 @@
  *    - http://www.apache.org/licenses/LICENSE-2.0
  *    - http://opensource.org/licenses/MIT
  */
-#include "Hacl_Hash_Blake2.h"
+#include "Hacl_Hash_Blake2b.h"
 
 using namespace std;
 
@@ -35,8 +35,8 @@ int main(int argc, char const *argv[])
     uint32_t key_len = 0;
     uint8_t *key = 0;
 
-    Hacl_Blake2b_32_blake2b(
-        output_len, output, message_len, (uint8_t *)message, key_len, key);
+    Hacl_Hash_Blake2b_hash_with_key(
+        output, output_len, (uint8_t *)message,message_len, key, key_len);
 
     print_hex_ln(output_len, output);
 

include/Hacl_SHA3_Scalar.h

@@ -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

include/Hacl_SHA3_Vec256.h

@@ -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

include/internal/Hacl_SHA3_Scalar.h

@@ -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