Add Optimized and HOL Light verified AVX2 Keccak x4

Author: manastasova

crypto/fipsmodule/CMakeLists.txt

@@ -342,6 +342,14 @@ if(ARCH STREQUAL "aarch64")
   )
 endif()
 
+if((ARCH STREQUAL "x86_64") AND UNIX AND NOT MY_ASSEMBLER_IS_TOO_OLD_FOR_AVX)
+  set(S2N_BIGNUM_INCLUDE_DIR "${AWSLC_SOURCE_DIR}/third_party/s2n-bignum/s2n-bignum-imported/include")
+  list(APPEND BCM_ASM_SOURCES
+          ${AWSLC_SOURCE_DIR}/third_party/s2n-bignum/s2n-bignum-to-be-imported/x86/sha3/sha3_keccak4_f1600_alt.S
+  )
+endif()
+
+
 # mlkem-native assembly files can be compiled on Unix platforms for x86_64 and arm64 only.
 if((ARCH STREQUAL "aarch64") AND UNIX)
 

crypto/fipsmodule/sha/keccak1600.c

@@ -39,6 +39,18 @@ static const uint64_t iotas[] = {
     0x8000000080008008ULL
 };
 
+#if defined(OPENSSL_X86_64)
+static const uint64_t keccak_rho8[4] = {
+    0x0605040302010007ULL, 0x0E0D0C0B0A09080FULL,
+    0x0605040302010007ULL, 0x0E0D0C0B0A09080FULL
+};
+
+static const uint64_t keccak_rho56[4] = {
+    0x0007060504030201ULL, 0x080F0E0D0C0B0A09ULL,
+    0x0007060504030201ULL, 0x080F0E0D0C0B0A09ULL
+};
+#endif
+
 #if !defined(KECCAK1600_ASM)
 
 static const uint8_t rhotates[KECCAK1600_ROWS][KECCAK1600_ROWS] = {
@@ -449,6 +461,13 @@ static void Keccak1600_x4(uint64_t A[4][KECCAK1600_ROWS][KECCAK1600_ROWS]) {
 #endif
 #endif
 
+#if defined(KECCAK1600_S2N_BIGNUM_ASM) && defined(OPENSSL_X86_64)
+    if (CRYPTO_is_AVX2_capable()) {
+        sha3_keccak4_f1600_alt((uint64_t *)A, iotas, keccak_rho8, keccak_rho56);
+        return;
+    }
+#endif
+
     // Fallback: 4x individual KeccakF1600 calls (each with their own dispatch)
     KeccakF1600(A[0]);
     KeccakF1600(A[1]);

third_party/s2n-bignum/s2n-bignum-imported/include/s2n-bignum.h

@@ -1116,7 +1116,11 @@ extern void sha3_keccak2_f1600_alt(uint64_t a[S2N_BIGNUM_STATIC 50],const uint64
 // Batched 4-way Keccak-f1600 permutation for SHA3
 // Inputs a[100], rc[24]; output a[100]
 extern void sha3_keccak4_f1600(uint64_t a[S2N_BIGNUM_STATIC 100],const uint64_t rc[S2N_BIGNUM_STATIC 24]);
+#ifdef __x86_64__
+extern void sha3_keccak4_f1600_alt(uint64_t a[S2N_BIGNUM_STATIC 100],const uint64_t rc[S2N_BIGNUM_STATIC 24],const uint64_t rho8[S2N_BIGNUM_STATIC 4],const uint64_t rho56[S2N_BIGNUM_STATIC 4]);
+#else
 extern void sha3_keccak4_f1600_alt(uint64_t a[S2N_BIGNUM_STATIC 100],const uint64_t rc[S2N_BIGNUM_STATIC 24]);
+#endif
 extern void sha3_keccak4_f1600_alt2(uint64_t a[S2N_BIGNUM_STATIC 100],const uint64_t rc[S2N_BIGNUM_STATIC 24]);
 
 // Point addition on CC curve SM2 in Montgomery-Jacobian coordinates