pq-code-package · jakemas · Feb 6, 2026
@@ -189,6 +189,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: mldsa_pointwise
             needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
           - name: mldsa_pointwise_acc_l4

@@ -253,6 +253,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)
   - [proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S)
   - [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S)
   - [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S)

@@ -60,7 +60,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

@@ -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 */

@@ -60,7 +60,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

@@ -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)
 

@@ -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
@@ -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);
+}
@@ -60,6 +60,7 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
   * AArch64 pointwise multiplication-accumulation (l=7): [mldsa_pointwise_acc_l7.S](aarch64/mldsa/mldsa_pointwise_acc_l7.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)
   * x86_64 pointwise multiplication: [mldsa_pointwise.S](x86_64/mldsa/mldsa_pointwise.S)
   * x86_64 pointwise multiplication-accumulation (l=4): [mldsa_pointwise_acc_l4.S](x86_64/mldsa/mldsa_pointwise_acc_l4.S)
   * x86_64 pointwise multiplication-accumulation (l=5): [mldsa_pointwise_acc_l5.S](x86_64/mldsa/mldsa_pointwise_acc_l5.S)

@@ -40,6 +40,39 @@ let bitmap = define
  `bitmap [] n = 0 /\
   bitmap (CONS i t) n = bitval(numbit i n) + 2 * bitmap t n`;;
 
+(* ------------------------------------------------------------------------- *)
+(* AVX2 "nttunpack" ordering: 8x8 transpose within each 64-element block.    *)
+(* Maps (block, lane, offset) -> (block, offset, lane), where                *)
+(* block = i DIV 64, lane = (i MOD 64) DIV 8, offset = i MOD 8.              *)
+(* This is the intra-block component of the full AVX2 NTT ordering.          *)
+(* ------------------------------------------------------------------------- *)
+
+let nttunpack_order = new_definition
+  `nttunpack_order i =
+   let block = i DIV 64 in
+   let pos = i MOD 64 in
+   let lane = pos DIV 8 in
+   let offset = pos MOD 8 in
+   64 * block + 8 * offset + lane`;;
+
+let nttunpack_unorder = new_definition
+  `nttunpack_unorder i =
+   let block = i DIV 64 in
+   let pos = i MOD 64 in
+   let lane = pos MOD 8 in
+   let offset = pos DIV 8 in
+   64 * block + 8 * lane + offset`;;
+
+let pack_nttunpack = new_definition
+  `pack_nttunpack l = list_of_seq (\i. EL (nttunpack_order i) l) 256`;;
+
+let unpack_nttunpack = new_definition
+  `unpack_nttunpack l = list_of_seq (\i. EL (nttunpack_unorder i) l) 256`;;
+
+(* The full AVX2 NTT order is bitreverse8 composed with nttunpack_order:     *)
+(* the nttunpack is the intra-block transpose component, and bitreverse8     *)
+(* provides the inter-block reordering on top.                               *)
+(* MLDSA_AVX2_NTT_ORDER_DECOMPOSE below proves the relationship.            *)
 let mldsa_avx2_ntt_order = define
  `mldsa_avx2_ntt_order i =
     bitreverse8(64 * (i DIV 64) + ((i MOD 64) DIV 8) + 8 * (i MOD 8))`;;
@@ -92,6 +125,15 @@ let MLDSA_AVX2_NTT_ORDER_CLAUSES = end_itlist CONJ (map
   GEN_REWRITE_CONV I [BITREVERSE8_CLAUSES])
  (map (curry mk_comb `mldsa_avx2_ntt_order` o mk_small_numeral) (0--255)));;
 
+(* mldsa_avx2_ntt_order decomposes as bitreverse8 after nttunpack_order.     *)
+let MLDSA_AVX2_NTT_ORDER_DECOMPOSE = prove
+ (`!i. i < 256
+       ==> mldsa_avx2_ntt_order i = bitreverse8(nttunpack_order i)`,
+  CONV_TAC EXPAND_CASES_CONV THEN CONV_TAC NUM_REDUCE_CONV THEN
+  REWRITE_TAC[mldsa_avx2_ntt_order; nttunpack_order; LET_DEF; LET_END_DEF] THEN
+  CONV_TAC NUM_REDUCE_CONV THEN
+  REWRITE_TAC[bitreverse8] THEN CONV_TAC(DEPTH_CONV WORD_RED_CONV));;
+
 let MLDSA_FORWARD_NTT_ALT = prove
  (`mldsa_forward_ntt f k =
    isum (0..255)

@@ -50,7 +50,8 @@ endif
 
 SPLIT=tr ';' '\n'
 
-OBJ = mldsa/mldsa_ntt.o mldsa/mldsa_intt.o mldsa/mldsa_pointwise.o \
+OBJ = mldsa/mldsa_ntt.o mldsa/mldsa_intt.o mldsa/mldsa_nttunpack.o \
+      mldsa/mldsa_pointwise.o \
       mldsa/mldsa_pointwise_acc_l4.o \
       mldsa/mldsa_pointwise_acc_l5.o \
       mldsa/mldsa_pointwise_acc_l7.o

@@ -105,5 +105,6 @@ Currently this includes:
 - ML-DSA Arithmetic:
   * x86_64 forward NTT: [mldsa_ntt.S](mldsa/mldsa_ntt.S)
   * x86_64 inverse NTT: [mldsa_intt.S](mldsa/mldsa_intt.S)
+  * x86_64 NTT unpack:  [mldsa_nttunpack.S](mldsa/mldsa_nttunpack.S)
 
 The NTT and inverse NTT functions are optimized using AVX2 instructions and follow the s2n-bignum x86_64 assembly verification patterns.