HOL-Light: Add x86 AVX2 nttunpack proof

Signed-off-by: Jake Massimo <jakemas@amazon.com>

Author: jakemas

.github/workflows/hol_light.yml

@@ -165,6 +165,8 @@ jobs:
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
           - name: mldsa_intt
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
+          - name: mldsa_nttunpack
+            needs: ["mldsa_specs.ml", "mldsa_utils.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

BIBLIOGRAPHY.md

@@ -250,6 +250,7 @@ source code and documentation.
   - [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c)
   - [proofs/hol_light/x86_64/mldsa/mldsa_intt.S](proofs/hol_light/x86_64/mldsa/mldsa_intt.S)
   - [proofs/hol_light/x86_64/mldsa/mldsa_ntt.S](proofs/hol_light/x86_64/mldsa/mldsa_ntt.S)
+  - [proofs/hol_light/x86_64/mldsa/mldsa_nttunpack.S](proofs/hol_light/x86_64/mldsa/mldsa_nttunpack.S)
 
 ### `Round3_Spec`
 

dev/x86_64/src/arith_native_x86_64.h

@@ -61,7 +61,16 @@ __contract__(
 );
 
 #define mld_nttunpack_avx2 MLD_NAMESPACE(nttunpack_avx2)
-void mld_nttunpack_avx2(int32_t *r);
+void mld_nttunpack_avx2(int32_t *r)
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  /* Output is a permutation of input: every output coefficient
+   * is some input coefficient */
+  ensures(forall(i, 0, MLDSA_N, exists(j, 0, MLDSA_N,
+    r[i] == old(*(int32_t (*)[MLDSA_N])r)[j])))
+);
 
 #define mld_rej_uniform_avx2 MLD_NAMESPACE(mld_rej_uniform_avx2)
 MLD_MUST_CHECK_RETURN_VALUE

dev/x86_64/src/nttunpack.S

@@ -13,13 +13,12 @@
  *   https://github.com/pq-crystals/dilithium/tree/master/avx2
  */
 
- /*
+/*
  * This file is derived from the public domain
  * AVX2 Dilithium implementation @[REF_AVX2].
  */
 
- #include "../../../common.h"
-
+#include "../../../common.h"
 #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \
     !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
 /* simpasm: header-end */

mldsa/src/native/x86_64/src/arith_native_x86_64.h

@@ -61,7 +61,16 @@ __contract__(
 );
 
 #define mld_nttunpack_avx2 MLD_NAMESPACE(nttunpack_avx2)
-void mld_nttunpack_avx2(int32_t *r);
+void mld_nttunpack_avx2(int32_t *r)
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  /* Output is a permutation of input: every output coefficient
+   * is some input coefficient */
+  ensures(forall(i, 0, MLDSA_N, exists(j, 0, MLDSA_N,
+    r[i] == old(*(int32_t (*)[MLDSA_N])r)[j])))
+);
 
 #define mld_rej_uniform_avx2 MLD_NAMESPACE(mld_rej_uniform_avx2)
 MLD_MUST_CHECK_RETURN_VALUE

mldsa/src/native/x86_64/src/nttunpack.S

@@ -13,13 +13,12 @@
  *   https://github.com/pq-crystals/dilithium/tree/master/avx2
  */
 
- /*
+/*
  * This file is derived from the public domain
  * AVX2 Dilithium implementation @[REF_AVX2].
  */
 
- #include "../../../common.h"
-
+#include "../../../common.h"
 #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \
     !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
 

proofs/cbmc/nttunpack_native_x86_64/Makefile

@@ -0,0 +1,57 @@
+# 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 = nttunpack_native_x86_64_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 = nttunpack_native_x86_64
+
+# 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/x86_64/meta.h\"" -DMLD_CHECK_APIS
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
+
+CHECK_FUNCTION_CONTRACTS=mld_poly_permute_bitrev_to_custom
+USE_FUNCTION_CONTRACTS=mld_nttunpack_avx2 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 = nttunpack_native_x86_64
+
+# 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/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/nttunpack_native_x86_64/nttunpack_native_x86_64_harness.c

@@ -0,0 +1,19 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <stdint.h>
+#include <stdlib.h>
+#include "cbmc.h"
+#include "params.h"
+
+void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N]);
+
+void harness(void)
+{
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+  int32_t *r;
+  mld_poly_permute_bitrev_to_custom(r);
+}

proofs/hol_light/README.md

@@ -54,3 +54,4 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
 - AArch64 poly_caddq: [mldsa_poly_caddq.S](aarch64/mldsa/mldsa_poly_caddq.S)
 - x86_64 forward NTT: [mldsa_ntt.S](x86_64/mldsa/mldsa_ntt.S)
 - x86_64 inverse NTT: [mldsa_intt.S](x86_64/mldsa/mldsa_intt.S)
+- x86_64 NTT unpack:  [mldsa_nttunpack.S](x86_64/mldsa/mldsa_nttunpack.S)

proofs/hol_light/x86_64/Makefile

@@ -50,7 +50,9 @@ endif
 
 SPLIT=tr ';' '\n'
 
-OBJ = mldsa/mldsa_ntt.o mldsa/mldsa_intt.o
+OBJ = mldsa/mldsa_ntt.o \
+      mldsa/mldsa_intt.o \
+      mldsa/mldsa_nttunpack.o
 
 # Build object files from assembly sources
 $(OBJ): %.o : %.S