Add Optimized and HOL Light verified AVX2 Keccak x4

crypto/fipsmodule/CMakeLists.txt

@@ -250,6 +250,9 @@ if((((ARCH STREQUAL "x86_64") AND NOT MY_ASSEMBLER_IS_TOO_OLD_FOR_512AVX) OR
     ${S2N_BIGNUM_DIR}/curve25519/edwards25519_scalarmulbase_alt.S
     ${S2N_BIGNUM_DIR}/curve25519/edwards25519_scalarmuldouble.S
     ${S2N_BIGNUM_DIR}/curve25519/edwards25519_scalarmuldouble_alt.S
+
+    ${S2N_BIGNUM_DIR}/sha3/sha3_keccak_f1600.S
+    ${S2N_BIGNUM_DIR}/sha3/sha3_keccak4_f1600_alt.S
   )
 
   if(ARCH STREQUAL "x86_64")
@@ -264,7 +267,6 @@ if((((ARCH STREQUAL "x86_64") AND NOT MY_ASSEMBLER_IS_TOO_OLD_FOR_512AVX) OR
                 ${S2N_BIGNUM_DIR}/curve25519/curve25519_x25519_alt.S
                 ${S2N_BIGNUM_DIR}/curve25519/curve25519_x25519base.S
                 ${S2N_BIGNUM_DIR}/curve25519/curve25519_x25519base_alt.S
-                ${S2N_BIGNUM_DIR}/sha3/sha3_keccak_f1600.S
     )
   elseif(ARCH STREQUAL "aarch64")
     # byte-level interface for aarch64 s2n-bignum x25519 are in
@@ -303,14 +305,8 @@ if((((ARCH STREQUAL "x86_64") AND NOT MY_ASSEMBLER_IS_TOO_OLD_FOR_512AVX) OR
     # (gcc supports it since gcc8, clang supports it since clang7)
     check_compiler("neon_sha3_check.c" MY_ASSEMBLER_SUPPORTS_NEON_SHA3_EXTENSION "-march=armv8.4-a+sha3")
 
-    list(APPEND BCM_ASM_SOURCES
-                # Scalar Keccak-x1 assembly from s2n-bignum/mlkem-native
-                ${S2N_BIGNUM_DIR}/sha3/sha3_keccak_f1600.S
-
-                # Batched Keccak-x4 assembly from s2n-bignum
-                # Scalar version for Neoverse N1
-                ${S2N_BIGNUM_DIR}/sha3/sha3_keccak4_f1600_alt.S
-    )
+    # Note: Scalar Keccak-x1 and Batched Neoverse N1 Keccak-x4 assembly from s2n-bignum
+    # are included in the common s2n-bignum block above
 
     if(MY_ASSEMBLER_SUPPORTS_NEON_SHA3_EXTENSION)
         list(APPEND BCM_ASM_SOURCES

crypto/fipsmodule/sha/keccak1600.c

@@ -33,6 +33,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] = {
@@ -315,7 +327,7 @@ void Keccak1600_Squeeze(uint64_t A[KECCAK1600_ROWS][KECCAK1600_ROWS], uint8_t *o
 // Scalar implementation from OpenSSL provided by keccak1600-armv8.pl
 extern void KeccakF1600_hw(uint64_t state[25]);
 
-#if defined(OPENSSL_AARCH64)
+#if defined(OPENSSL_AARCH64) || defined(OPENSSL_X86_64)
 static void keccak_log_dispatch(size_t id) {
 #if BORINGSSL_DISPATCH_TEST
     BORINGSSL_function_hit[id] = 1;
@@ -366,6 +378,7 @@ void KeccakF1600(uint64_t A[KECCAK1600_ROWS][KECCAK1600_ROWS]) {
     KeccakF1600_hw((uint64_t *) A);
 
 #elif defined(OPENSSL_X86_64)
+    keccak_log_dispatch(9); // kFlag_sha3_keccak_f1600
     sha3_keccak_f1600((uint64_t *)A, iotas);
 #endif
 }
@@ -443,6 +456,14 @@ 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()) {
+        keccak_log_dispatch(10); // kFlag_sha3_keccak4_f1600_alt
+        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]);

crypto/impl_dispatch_test.cc

@@ -31,6 +31,7 @@ class ImplDispatchTest : public ::testing::Test {
     aes_hw_ = CRYPTO_is_AESNI_capable();
     avx_movbe_ = CRYPTO_is_AVX_capable() && CRYPTO_is_MOVBE_capable();
     aes_vpaes_ = CRYPTO_is_SSSE3_capable();
+    is_avx2_ = CRYPTO_is_AVX2_capable();
     ifma_avx512 = CRYPTO_is_AVX512IFMA_capable();
     sha_ext_ =
     // sha_ext_ isn't enabled on 32-bit x86 architectures.
@@ -85,13 +86,13 @@ class ImplDispatchTest : public ::testing::Test {
         true;
 #else
         false;
+#endif
 #endif
     have_s2n_bignum_asm_ =
 #if defined(KECCAK1600_S2N_BIGNUM_ASM)
         true;
 #else
         false;
-#endif
 #endif
   }
 
@@ -122,10 +123,12 @@ class ImplDispatchTest : public ::testing::Test {
   bool aes_hw_ = false;
   bool aes_vpaes_ = false;
   bool sha_ext_ = false;
+  bool have_s2n_bignum_asm_ = false;
 #if defined(OPENSSL_X86) || defined(OPENSSL_X86_64)
   bool vaes_vpclmulqdq_ = false;
   bool avx_movbe_ = false;
   bool is_x86_64_ = false;
+  bool is_avx2_ = false;
   bool is_assembler_too_old = false;
   bool is_assembler_too_old_avx512 = false;
   bool ifma_avx512 = false;
@@ -138,7 +141,6 @@ class ImplDispatchTest : public ::testing::Test {
   bool neoverse_v1_ = false;
   bool neoverse_v2_ = false;
   bool assembler_has_neon_sha3_extension_ = false;
-  bool have_s2n_bignum_asm_ = false;
 #endif
 
 };
@@ -156,6 +158,8 @@ constexpr size_t kFlag_sha256_hw = 6;
 constexpr size_t kFlag_aesni_gcm_encrypt = 2;
 constexpr size_t kFlag_aes_gcm_encrypt_avx512 = 7;
 constexpr size_t kFlag_RSAZ_mod_exp_avx512_x2 = 8;
+constexpr size_t kFlag_sha3_keccak_f1600 = 9;
+constexpr size_t kFlag_sha3_keccak4_f1600_alt = 10;
 #else // AARCH64
 constexpr size_t kFlag_aes_gcm_enc_kernel = 2;
 constexpr size_t kFlag_aesv8_gcm_8x_enc_128 = 7;
@@ -297,8 +301,24 @@ TEST_F(ImplDispatchTest, SHA3_512) {
         SHA3_512(in, 32, out);
       });
 }
+#endif // OPENSSL_AARCH64
 
 TEST_F(ImplDispatchTest, SHAKE256_Batched) {
+#if defined(OPENSSL_X86_64) || defined(OPENSSL_X86)
+  // Assembly dispatch logic for Keccak-x4 on x86:
+  // - For platforms with AVX2 support, we use batched Keccak assembly from s2n-bignum
+  //   (`sha3_keccak4_f1600_alt()`).
+  // - Otherwise, fall back to scalar Keccak implementation from s2n-bignum,
+  //   (`sha3_keccak_f1600()`).
+  AssertFunctionsHit(
+      {
+          {kFlag_sha3_keccak4_f1600_alt,
+           have_s2n_bignum_asm_ &&
+           is_avx2_ },
+           {kFlag_sha3_keccak_f1600,
+           have_s2n_bignum_asm_ && is_x86_64_ && !is_avx2_ },
+      },
+#else // AARCH64
   // Assembly dispatch logic for Keccak-x4 on AArch64:
   // - For Neoverse N1, we use scalar batched hybrid Keccak assembly from s2n-bignum
   //   (`sha3_keccak4_f1600_alt()`) leveraging Neon and scalar assembly with
@@ -342,14 +362,13 @@ TEST_F(ImplDispatchTest, SHAKE256_Batched) {
 	       !(assembler_has_neon_sha3_extension_ && sha3_ext_)
 	   ) },
       },
+#endif
       [] {
         const uint8_t in[32] = {0};
         uint8_t out0[32], out1[32], out2[32], out3[32];
         SHAKE256_x4(in, in, in, in, 32, out0, out1, out2, out3, 32);
       });
 }
-#endif // OPENSSL_AARCH64
-
 
 #if defined(OPENSSL_X86) || defined(OPENSSL_X86_64)
 static bssl::UniquePtr<BIGNUM> GetBIGNUM(FileTest *t, const char *attr);

crypto/internal.h

@@ -1288,6 +1288,8 @@ OPENSSL_INLINE int boringssl_fips_break_test(const char *test) {
 //   6: sha256_block_data_order_shaext
 //   7: aes_gcm_encrypt_avx512
 //   8: RSAZ_mod_exp_avx512_x2
+//   9: sha3_keccak_f1600
+//  10: sha3_keccak4_f1600_alt
 // On AARCH64:
 //   0: aes_hw_ctr32_encrypt_blocks
 //   1: aes_hw_encrypt

third_party/s2n-bignum/META.yml

@@ -1,5 +1,5 @@
 name: s2n-bignum-imported
 source: awslabs/s2n-bignum.git
-commit: 2b5350cf955a32d2f7aced172f7bd28dd85a8587
+commit: 4b5f8214e85b6b239077c278825b7fa9c2ab9cf5
 target: main
-imported-at: 2025-09-05T04:04:05+0000
+imported-at: 2026-03-16T15:51:12+0000

third_party/s2n-bignum/s2n-bignum-imported/README.md

@@ -11,9 +11,11 @@ tuned for highest performance both by hand and using automatic optimization
 techniques such as the [SLOTHY](https://github.com/slothy-optimizer/slothy)
 superoptimizer, and each function is accompanied by a machine-checked formal
 proof in [HOL-Light](https://hol-light.github.io/) that its mathematical
-result is correct, based on a formal model of the underlying machine. Each
-function is moreover written in a constant-time style to avoid timing
-side-channels.
+result is correct, based on a formal model of the underlying machine.
+Moreover, each function is written in a constant-time style to avoid timing
+side-channels. For a detailed analysis of the formal verification process, the
+assumptions made, and the correspondence of formal models with reality, please
+refer to the [s2n-bignum soundness review](doc/s2n_bignum_soundness.md).
 
 For the SHA-3 and ML-KEM code currently part of s2n-bignum, some of the
 comments in the main part of this README do not apply exactly. See the section

third_party/s2n-bignum/s2n-bignum-imported/arm/Makefile

@@ -146,6 +146,7 @@ BIGNUM_OBJ = curve25519/bignum_add_p25519.o \
              curve25519/bignum_invsqrt_p25519_alt.o \
              curve25519/bignum_madd_n25519.o \
              curve25519/bignum_madd_n25519_alt.o \
+             curve25519/bignum_mod_m25519.o \
              curve25519/bignum_mod_m25519_4.o \
              curve25519/bignum_mod_n25519.o \
              curve25519/bignum_mod_n25519_4.o \
@@ -358,6 +359,7 @@ BIGNUM_OBJ = curve25519/bignum_add_p25519.o \
              secp256k1/bignum_triple_p256k1.o \
              sha3/sha3_keccak_f1600.o \
              sha3/sha3_keccak_f1600_alt.o \
+             sha3/sha3_keccak_f1600_alt2.o \
              sha3/sha3_keccak2_f1600.o \
              sha3/sha3_keccak2_f1600_alt.o \
              sha3/sha3_keccak4_f1600.o \
@@ -408,7 +410,9 @@ OBJ = $(POINT_OBJ) $(BIGNUM_OBJ)
 
 TUTORIAL_PROOFS = $(wildcard tutorial/*.ml)
 
-TUTORIAL_OBJ = $(TUTORIAL_PROOFS:.ml=.o) tutorial/rel_loop2.o \
+TUTORIAL_OBJ = $(filter-out tutorial/safety.o, $(TUTORIAL_PROOFS:.ml=.o)) \
+    curve25519/bignum_mod_n25519.o p256/bignum_mux_4.o \
+    tutorial/rel_loop2.o \
     tutorial/rel_simp2.o tutorial/rel_veceq2.o tutorial/rel_equivtac2.o \
     tutorial/rel_reordertac2.o tutorial/rodata_local.o
 
@@ -517,6 +521,11 @@ sm2/sm2_montjscalarmul_alt.native: sm2/sm2_montjadd_alt.native sm2/sm2_montjdoub
 
 # Tutorial
 
+# safety tutorial does not have safety.o and uses existing ones
+tutorial/safety.native: tutorial/safety.ml proofs/bignum_mux_4.ml \
+                        curve25519/bignum_mod_n25519.o ; \
+  ../tools/build-proof.sh "$<" "$(HOLLIGHT)" "$@"
+# other tutorials have their .o files
 .SECONDEXPANSION:
 tutorial/%.native: tutorial/%.ml tutorial/%.o ; ../tools/build-proof.sh "$<" "$(HOLLIGHT)" "$@"
 # Additional dependencies on .o files

third_party/s2n-bignum/s2n-bignum-imported/arm/allowed_asm

@@ -52,6 +52,10 @@
 : lsl$
 : lsr$
 : madd$
+: mla$
+: mla.2s$
+: mla.4s$
+: mla.8h$
 : mls$
 : mls.2s$
 : mls.8h$

third_party/s2n-bignum/s2n-bignum-imported/arm/curve25519/Makefile

@@ -29,6 +29,7 @@ OBJ = bignum_add_p25519.o \
       bignum_invsqrt_p25519_alt.o \
       bignum_madd_n25519.o \
       bignum_madd_n25519_alt.o \
+      bignum_mod_m25519.o \
       bignum_mod_m25519_4.o \
       bignum_mod_n25519.o \
       bignum_mod_n25519_4.o \