ML-DSA aarch64 rejection sampling proof

.github/workflows/hol_light.yml

@@ -9,6 +9,7 @@ on:
     branches: ["main"]
     paths:
      - '.github/workflows/hol_light.yml'
+     - 'proofs/hol_light/common/**/*.ml'
      - 'proofs/hol_light/aarch64/Makefile'
      - 'proofs/hol_light/aarch64/**/*.S'
      - 'proofs/hol_light/aarch64/**/*.ml'
@@ -23,6 +24,7 @@ on:
     branches: ["main"]
     paths:
       - '.github/workflows/hol_light.yml'
+      - 'proofs/hol_light/common/**/*.ml'
       - 'proofs/hol_light/aarch64/Makefile'
       - 'proofs/hol_light/aarch64/**/*.S'
       - 'proofs/hol_light/aarch64/**/*.ml'
@@ -79,8 +81,12 @@ jobs:
       matrix:
         proof:
           # Dependencies on {name}.{S,ml} are implicit
+          - name: mldsa_ntt
+            needs: ["mldsa_specs.ml", "mldsa_zetas.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
           - name: mldsa_poly_caddq
             needs: ["aarch64_utils.ml"]
+          - name: mldsa_rej_uniform
+            needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_table.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
@@ -106,8 +112,8 @@ jobs:
             done
           done
 
-          # Always re-run upon change to nix files for HOL-Light
-          if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/aarch64/Makefile"* ]]; then
+          # Always re-run upon change to nix files, common specs, or HOL-Light config
+          if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/aarch64/Makefile"* ]] || [[ "$changed_files" == *"proofs/hol_light/common/"* ]]; then
             run_needed=1
           fi
 
@@ -153,7 +159,7 @@ jobs:
             # TODO: Enable when we have a cheaper proof
             # make -C proofs/hol_light/x86_64 mldsa/mldsa_ntt.o
             # echo 'needs "x86_64/proofs/mldsa_ntt.ml";;' | hol.sh
-            echo 'needs "x86/proofs/base.ml";; needs "x86_64/proofs/mldsa_specs.ml";; #quit;;' | hol.sh
+            echo 'needs "x86/proofs/base.ml";; needs "common/mldsa_specs.ml";; #quit;;' | hol.sh
   hol_light_proofs_x86_64:
     needs: [ hol_light_bytecode_x86_64 ]
     strategy:
@@ -190,8 +196,8 @@ jobs:
             done
           done
 
-          # Always re-run upon change to nix files for HOL-Light
-          if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86_64/Makefile"* ]]; then
+          # Always re-run upon change to nix files, common specs, or HOL-Light config
+          if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86_64/Makefile"* ]] || [[ "$changed_files" == *"proofs/hol_light/common/"* ]]; then
             run_needed=1
           fi
 

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -50,7 +50,20 @@ extern const uint8_t mld_polyz_unpack_19_indices[];
 #define MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN (2 * 136)
 
 #define mld_ntt_asm MLD_NAMESPACE(ntt_asm)
-void mld_ntt_asm(int32_t *, const int32_t *, const int32_t *);
+void mld_ntt_asm(int32_t *r, const int32_t *zetas_l123456,
+                 const int32_t *zetas_l78)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_ntt.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
+  requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456)
+  requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: off */
+  ensures(array_abs_bound(r, 0, MLDSA_N, 75423753))
+  /* check-magic: on */
+);
 
 #define mld_intt_asm MLD_NAMESPACE(intt_asm)
 void mld_intt_asm(int32_t *, const int32_t *, const int32_t *);

dev/aarch64_opt/src/arith_native_aarch64.h

@@ -50,7 +50,20 @@ extern const uint8_t mld_polyz_unpack_19_indices[];
 #define MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN (2 * 136)
 
 #define mld_ntt_asm MLD_NAMESPACE(ntt_asm)
-void mld_ntt_asm(int32_t *, const int32_t *, const int32_t *);
+void mld_ntt_asm(int32_t *r, const int32_t *zetas_l123456,
+                 const int32_t *zetas_l78)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_ntt.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
+  requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456)
+  requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: off */
+  ensures(array_abs_bound(r, 0, MLDSA_N, 75423753))
+  /* check-magic: on */
+);
 
 #define mld_intt_asm MLD_NAMESPACE(intt_asm)
 void mld_intt_asm(int32_t *, const int32_t *, const int32_t *);

mldsa/src/native/aarch64/src/arith_native_aarch64.h

@@ -50,7 +50,20 @@ extern const uint8_t mld_polyz_unpack_19_indices[];
 #define MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN (2 * 136)
 
 #define mld_ntt_asm MLD_NAMESPACE(ntt_asm)
-void mld_ntt_asm(int32_t *, const int32_t *, const int32_t *);
+void mld_ntt_asm(int32_t *r, const int32_t *zetas_l123456,
+                 const int32_t *zetas_l78)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_ntt.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
+  requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456)
+  requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: off */
+  ensures(array_abs_bound(r, 0, MLDSA_N, 75423753))
+  /* check-magic: on */
+);
 
 #define mld_intt_asm MLD_NAMESPACE(intt_asm)
 void mld_intt_asm(int32_t *, const int32_t *, const int32_t *);

proofs/cbmc/ntt_native_aarch64/Makefile

@@ -0,0 +1,58 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = ntt_native_aarch64_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = ntt_native_aarch64
+
+# We need to set MLD_CHECK_APIS as otherwise mldsa/src/native/api.h won't be
+# included, which contains the CBMC specifications.
+DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/aarch64/meta.h\"" -DMLD_CHECK_APIS
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c $(SRCDIR)/mldsa/src/native/aarch64/src/aarch64_zetas.c
+
+CHECK_FUNCTION_CONTRACTS=mld_ntt_native
+USE_FUNCTION_CONTRACTS=mld_ntt_asm
+USE_FUNCTION_CONTRACTS+=mld_sys_check_capability
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = ntt_native_aarch64
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/src/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

proofs/cbmc/ntt_native_aarch64/ntt_native_aarch64_harness.c

@@ -0,0 +1,16 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <stdint.h>
+#include "cbmc.h"
+#include "params.h"
+
+
+int mld_ntt_native(int32_t data[MLDSA_N]);
+
+void harness(void)
+{
+  int32_t *r;
+  int t;
+  t = mld_ntt_native(r);
+}

proofs/hol_light/aarch64/Makefile

@@ -53,7 +53,9 @@ endif
 
 SPLIT=tr ';' '\n'
 
-OBJ = mldsa/mldsa_poly_caddq.o
+OBJ = mldsa/mldsa_ntt.o \
+      mldsa/mldsa_poly_caddq.o \
+      mldsa/mldsa_rej_uniform.o
 
 # According to
 # https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms,