HOL-Light/x86_64: Replace Keccakx4 intrinsics with AVX2 assembly and prove correct

.github/workflows/hol_light.yml

@@ -96,15 +96,15 @@ jobs:
           - name: mldsa_poly_chknorm
             needs: ["aarch64_utils.ml"]
           - name: keccak_f1600_x1_scalar
-            needs: ["keccak_spec.ml"]
+            needs: ["keccak_spec.ml", "keccak_constants.ml"]
           - name: keccak_f1600_x1_v84a
-            needs: ["keccak_spec.ml"]
+            needs: ["keccak_spec.ml", "keccak_constants.ml"]
           - name: keccak_f1600_x2_v84a
-            needs: ["keccak_spec.ml"]
+            needs: ["keccak_spec.ml", "keccak_constants.ml"]
           - name: keccak_f1600_x4_v8a_scalar
-            needs: ["keccak_spec.ml"]
+            needs: ["keccak_spec.ml", "keccak_utils.ml", "keccak_constants.ml"]
           - name: keccak_f1600_x4_v8a_v84a_scalar
-            needs: ["keccak_spec.ml"]
+            needs: ["keccak_spec.ml", "keccak_utils.ml", "keccak_constants.ml"]
     name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
     runs-on: pqcp-arm64
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
@@ -197,6 +197,8 @@ jobs:
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
           - name: mldsa_pointwise_acc_l7
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
+          - name: keccak_f1600_x4_avx2
+            needs: ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"]
     name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
     runs-on: pqcp-x64
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

README.md

@@ -61,12 +61,7 @@ We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to
 
 **Note:** The `MLD_CONFIG_REDUCE_RAM` configuration option is not currently covered by CBMC proofs.
 
-HOL-Light functional correctness proofs can be found in [proofs/hol_light](proofs/hol_light). So far, the following functions have been proven correct:
-
-- AArch64 poly_caddq [poly_caddq_asm.S](mldsa/src/native/aarch64/src/poly_caddq_asm.S)
-- x86_64 NTT [ntt.S](mldsa/src/native/x86_64/src/ntt.S)
-
-These proofs utilize the verification infrastructure in [s2n-bignum](https://github.com/awslabs/s2n-bignum).
+HOL-Light functional correctness proofs can be found in [proofs/hol_light](proofs/hol_light). See the [HOL-Light README](proofs/hol_light/README.md) for the list of functions that have been proven correct. These proofs utilize the verification infrastructure in [s2n-bignum](https://github.com/awslabs/s2n-bignum).
 
 Finally, [proofs/isabelle](proofs/isabelle/compress) contains proofs in [Isabelle/HOL](https://isabelle.in.tum.de/) of the correctness of
 different approaches for computing the scalar decomposition routines used in ML-DSA. Those are still experimental and do not yet operate

dev/fips202/aarch64/src/keccakf1600_round_constants.c

@@ -1,9 +1,14 @@
 /*
- * Copyright (c) The mlkem-native project authors
  * Copyright (c) The mldsa-native project authors
  * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
  */
 
+/*
+ * WARNING: This file is auto-generated from scripts/autogen
+ *          in the mldsa-native repository.
+ *          Do not modify it directly.
+ */
+
 #include "../../../../common.h"
 
 #if (defined(MLD_FIPS202_AARCH64_NEED_X1_SCALAR) ||                  \

mldsa/src/fips202/native/x86_64/xkcp.h → dev/fips202/x86_64/keccak_f1600_x4_avx2.h

@@ -4,28 +4,31 @@
  * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
  */
 
-#ifndef MLD_FIPS202_NATIVE_X86_64_XKCP_H
-#define MLD_FIPS202_NATIVE_X86_64_XKCP_H
+#ifndef MLD_DEV_FIPS202_X86_64_KECCAK_F1600_X4_AVX2_H
+#define MLD_DEV_FIPS202_X86_64_KECCAK_F1600_X4_AVX2_H
 
 #include "../../../common.h"
 
-#define MLD_FIPS202_X86_64_XKCP
+#define MLD_FIPS202_X86_64_NEED_X4_AVX2
+
+/* Part of backend API */
+#define MLD_USE_FIPS202_X4_NATIVE
 
 #if !defined(__ASSEMBLER__)
 #include "../api.h"
-#include "src/KeccakP_1600_times4_SIMD256.h"
-
-#define MLD_USE_FIPS202_X4_NATIVE
+#include "src/fips202_native_x86_64.h"
 MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state)
 {
   if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2))
   {
     return MLD_NATIVE_FUNC_FALLBACK;
   }
-  mld_keccakf1600x4_permute24(state);
+
+  mld_keccak_f1600_x4_avx2(state, mld_keccakf1600_round_constants,
+                           mld_keccak_rho8, mld_keccak_rho56);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* !__ASSEMBLER__ */
 
-#endif /* !MLD_FIPS202_NATIVE_X86_64_XKCP_H */
+#endif /* !MLD_DEV_FIPS202_X86_64_KECCAK_F1600_X4_AVX2_H */

dev/fips202/x86_64/src/fips202_native_x86_64.h

@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) The mlkem-native project authors
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+#ifndef MLD_DEV_FIPS202_X86_64_SRC_FIPS202_NATIVE_X86_64_H
+#define MLD_DEV_FIPS202_X86_64_SRC_FIPS202_NATIVE_X86_64_H
+
+#include "../../../../cbmc.h"
+#include "../../../../common.h"
+
+/* TODO: Reconsider whether this check is needed -- x86_64 is always
+ * little-endian, so the backend selection already implies this. */
+#ifndef MLD_SYS_LITTLE_ENDIAN
+#error Expecting a little-endian platform
+#endif
+
+#define mld_keccakf1600_round_constants \
+  MLD_NAMESPACE(keccakf1600_round_constants)
+MLD_INTERNAL_DATA_DECLARATION const uint64_t
+    mld_keccakf1600_round_constants[24];
+
+#define mld_keccak_rho8 MLD_NAMESPACE(keccak_rho8)
+MLD_INTERNAL_DATA_DECLARATION const uint64_t mld_keccak_rho8[4];
+
+#define mld_keccak_rho56 MLD_NAMESPACE(keccak_rho56)
+MLD_INTERNAL_DATA_DECLARATION const uint64_t mld_keccak_rho56[4];
+
+#define mld_keccak_f1600_x4_avx2 MLD_NAMESPACE(keccak_f1600_x4_avx2)
+void mld_keccak_f1600_x4_avx2(uint64_t states[100], const uint64_t rc[24],
+                              const uint64_t rho8[4], const uint64_t rho56[4])
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2.ml */
+__contract__(
+  requires(memory_no_alias(states, sizeof(uint64_t) * 25 * 4))
+  requires(rc == mld_keccakf1600_round_constants)
+  requires(rho8 == mld_keccak_rho8)
+  requires(rho56 == mld_keccak_rho56)
+  assigns(memory_slice(states, sizeof(uint64_t) * 25 * 4))
+);
+
+#endif /* !MLD_DEV_FIPS202_X86_64_SRC_FIPS202_NATIVE_X86_64_H */