Deduplicate polyw1_pack in multilevel builds

mldsa/mldsa_native.c

@@ -280,6 +280,8 @@
 #undef MLDSA_ETA
 #undef MLDSA_GAMMA1
 #undef MLDSA_GAMMA2
+#undef MLDSA_GAMMA2_32
+#undef MLDSA_GAMMA2_88
 #undef MLDSA_K
 #undef MLDSA_L
 #undef MLDSA_N
@@ -294,6 +296,8 @@
 #undef MLDSA_POLYT1_PACKEDBYTES
 #undef MLDSA_POLYVECH_PACKEDBYTES
 #undef MLDSA_POLYW1_PACKEDBYTES
+#undef MLDSA_POLYW1_PACKEDBYTES_32
+#undef MLDSA_POLYW1_PACKEDBYTES_88
 #undef MLDSA_POLYZ_PACKEDBYTES
 #undef MLDSA_Q
 #undef MLDSA_Q_HALF
@@ -487,6 +491,8 @@
 #undef mld_polyt0_unpack
 #undef mld_polyt1_pack
 #undef mld_polyt1_unpack
+#undef mld_polyw1_pack_32
+#undef mld_polyw1_pack_88
 /* mldsa/src/randombytes.h */
 #undef MLD_RANDOMBYTES_H
 /* mldsa/src/reduce.h */

mldsa/mldsa_native_asm.S

@@ -287,6 +287,8 @@
 #undef MLDSA_ETA
 #undef MLDSA_GAMMA1
 #undef MLDSA_GAMMA2
+#undef MLDSA_GAMMA2_32
+#undef MLDSA_GAMMA2_88
 #undef MLDSA_K
 #undef MLDSA_L
 #undef MLDSA_N
@@ -301,6 +303,8 @@
 #undef MLDSA_POLYT1_PACKEDBYTES
 #undef MLDSA_POLYVECH_PACKEDBYTES
 #undef MLDSA_POLYW1_PACKEDBYTES
+#undef MLDSA_POLYW1_PACKEDBYTES_32
+#undef MLDSA_POLYW1_PACKEDBYTES_88
 #undef MLDSA_POLYZ_PACKEDBYTES
 #undef MLDSA_Q
 #undef MLDSA_Q_HALF
@@ -494,6 +498,8 @@
 #undef mld_polyt0_unpack
 #undef mld_polyt1_pack
 #undef mld_polyt1_unpack
+#undef mld_polyw1_pack_32
+#undef mld_polyw1_pack_88
 /* mldsa/src/randombytes.h */
 #undef MLD_RANDOMBYTES_H
 /* mldsa/src/reduce.h */

mldsa/src/params.h

@@ -14,6 +14,11 @@
 #define MLDSA_Q_HALF ((MLDSA_Q + 1) / 2)
 #define MLDSA_D 13
 
+#define MLDSA_GAMMA2_88 ((MLDSA_Q - 1) / 88)
+#define MLDSA_GAMMA2_32 ((MLDSA_Q - 1) / 32)
+#define MLDSA_POLYW1_PACKEDBYTES_88 192
+#define MLDSA_POLYW1_PACKEDBYTES_32 128
+
 #if MLD_CONFIG_PARAMETER_SET == 44
 
 #define MLDSA_K 4
@@ -22,11 +27,11 @@
 #define MLDSA_TAU 39
 #define MLDSA_BETA 78
 #define MLDSA_GAMMA1 (1 << 17)
-#define MLDSA_GAMMA2 ((MLDSA_Q - 1) / 88)
+#define MLDSA_GAMMA2 MLDSA_GAMMA2_88
 #define MLDSA_OMEGA 80
 #define MLDSA_CTILDEBYTES 32
 #define MLDSA_POLYZ_PACKEDBYTES 576
-#define MLDSA_POLYW1_PACKEDBYTES 192
+#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_88
 #define MLDSA_POLYETA_PACKEDBYTES 96
 
 #elif MLD_CONFIG_PARAMETER_SET == 65
@@ -37,11 +42,11 @@
 #define MLDSA_TAU 49
 #define MLDSA_BETA 196
 #define MLDSA_GAMMA1 (1 << 19)
-#define MLDSA_GAMMA2 ((MLDSA_Q - 1) / 32)
+#define MLDSA_GAMMA2 MLDSA_GAMMA2_32
 #define MLDSA_OMEGA 55
 #define MLDSA_CTILDEBYTES 48
 #define MLDSA_POLYZ_PACKEDBYTES 640
-#define MLDSA_POLYW1_PACKEDBYTES 128
+#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_32
 #define MLDSA_POLYETA_PACKEDBYTES 128
 
 #elif MLD_CONFIG_PARAMETER_SET == 87
@@ -52,11 +57,11 @@
 #define MLDSA_TAU 60
 #define MLDSA_BETA 120
 #define MLDSA_GAMMA1 (1 << 19)
-#define MLDSA_GAMMA2 ((MLDSA_Q - 1) / 32)
+#define MLDSA_GAMMA2 MLDSA_GAMMA2_32
 #define MLDSA_OMEGA 75
 #define MLDSA_CTILDEBYTES 64
 #define MLDSA_POLYZ_PACKEDBYTES 640
-#define MLDSA_POLYW1_PACKEDBYTES 128
+#define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_32
 #define MLDSA_POLYETA_PACKEDBYTES 96
 
 #endif /* MLD_CONFIG_PARAMETER_SET == 87 */

mldsa/src/poly.c

@@ -1005,6 +1005,58 @@ uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
   return mld_poly_chknorm_c(a, B);
 }
 
+#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
+#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
+    MLD_CONFIG_PARAMETER_SET == 44
+MLD_INTERNAL_API
+void mld_polyw1_pack_88(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_88],
+                        const mld_poly *a)
+{
+  unsigned int i;
+
+  mld_assert_bound(a->coeffs, MLDSA_N, 0,
+                   (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_88));
+
+  for (i = 0; i < MLDSA_N / 4; ++i)
+  __loop__(
+    invariant(i <= MLDSA_N/4)
+    decreases(MLDSA_N / 4 - i))
+  {
+    r[3 * i + 0] = (uint8_t)((a->coeffs[4 * i + 0]) & 0xFF);
+    r[3 * i + 0] |= (uint8_t)((a->coeffs[4 * i + 1] << 6) & 0xFF);
+    r[3 * i + 1] = (uint8_t)((a->coeffs[4 * i + 1] >> 2) & 0xFF);
+    r[3 * i + 1] |= (uint8_t)((a->coeffs[4 * i + 2] << 4) & 0xFF);
+    r[3 * i + 2] = (uint8_t)((a->coeffs[4 * i + 2] >> 4) & 0xFF);
+    r[3 * i + 2] |= (uint8_t)((a->coeffs[4 * i + 3] << 2) & 0xFF);
+  }
+}
+#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
+        */
+
+#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
+    (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
+MLD_INTERNAL_API
+void mld_polyw1_pack_32(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_32],
+                        const mld_poly *a)
+{
+  unsigned int i;
+
+  mld_assert_bound(a->coeffs, MLDSA_N, 0,
+                   (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2_32));
+
+  for (i = 0; i < MLDSA_N / 2; ++i)
+  __loop__(
+    invariant(i <= MLDSA_N/2)
+    decreases(MLDSA_N / 2 - i))
+  {
+    r[i] =
+        (uint8_t)((a->coeffs[2 * i + 0] | (a->coeffs[2 * i + 1] << 4)) & 0xFF);
+  }
+}
+#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
+          || MLD_CONFIG_PARAMETER_SET == 87 */
+#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
+
 #else  /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */
 MLD_EMPTY_CU(mld_poly)
 #endif /* MLD_CONFIG_MULTILEVEL_NO_SHARED */

mldsa/src/poly.h

@@ -378,4 +378,49 @@ __contract__(
   ensures((return_value == 0) == array_abs_bound(a->coeffs, 0, MLDSA_N, B))
 );
 
+#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
+#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
+#define mld_polyw1_pack_88 MLD_NAMESPACE(polyw1_pack_88)
+/**
+ * Bit-pack polynomial w1 for GAMMA2 = (MLDSA_Q-1)/88 (coefficients in [0, 43]).
+ * Input coefficients are assumed to be standard representatives.
+ *
+ * @param[out] r Pointer to output byte array (MLDSA_POLYW1_PACKEDBYTES_88).
+ * @param[in]  a Pointer to input polynomial.
+ */
+MLD_INTERNAL_API
+void mld_polyw1_pack_88(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_88],
+                        const mld_poly *a)
+__contract__(
+  requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES_88))
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_88)))
+  assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES_88))
+);
+#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
+        */
+
+#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
+    (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
+#define mld_polyw1_pack_32 MLD_NAMESPACE(polyw1_pack_32)
+/**
+ * Bit-pack polynomial w1 for GAMMA2 = (MLDSA_Q-1)/32 (coefficients in [0, 15]).
+ * Input coefficients are assumed to be standard representatives.
+ *
+ * @param[out] r Pointer to output byte array (MLDSA_POLYW1_PACKEDBYTES_32).
+ * @param[in]  a Pointer to input polynomial.
+ */
+MLD_INTERNAL_API
+void mld_polyw1_pack_32(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_32],
+                        const mld_poly *a)
+__contract__(
+  requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES_32))
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2_32)))
+  assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES_32))
+);
+#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
+          || MLD_CONFIG_PARAMETER_SET == 87 */
+#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
+
 #endif /* !MLD_POLY_H */

mldsa/src/poly_kl.c

@@ -893,38 +893,6 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES])
 
   mld_polyz_unpack_c(r, a);
 }
-
-MLD_INTERNAL_API
-void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a)
-{
-  unsigned int i;
-
-  mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
-
-#if MLD_CONFIG_PARAMETER_SET == 44
-  for (i = 0; i < MLDSA_N / 4; ++i)
-  __loop__(
-    invariant(i <= MLDSA_N/4)
-    decreases(MLDSA_N / 4 - i))
-  {
-    r[3 * i + 0] = (uint8_t)((a->coeffs[4 * i + 0]) & 0xFF);
-    r[3 * i + 0] |= (uint8_t)((a->coeffs[4 * i + 1] << 6) & 0xFF);
-    r[3 * i + 1] = (uint8_t)((a->coeffs[4 * i + 1] >> 2) & 0xFF);
-    r[3 * i + 1] |= (uint8_t)((a->coeffs[4 * i + 2] << 4) & 0xFF);
-    r[3 * i + 2] = (uint8_t)((a->coeffs[4 * i + 2] >> 4) & 0xFF);
-    r[3 * i + 2] |= (uint8_t)((a->coeffs[4 * i + 3] << 2) & 0xFF);
-  }
-#else  /* MLD_CONFIG_PARAMETER_SET == 44 */
-  for (i = 0; i < MLDSA_N / 2; ++i)
-  __loop__(
-    invariant(i <= MLDSA_N/2)
-    decreases(MLDSA_N / 2 - i))
-  {
-    r[i] =
-        (uint8_t)((a->coeffs[2 * i + 0] | (a->coeffs[2 * i + 1] << 4)) & 0xFF);
-  }
-#endif /* MLD_CONFIG_PARAMETER_SET != 44 */
-}
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
 
 /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. */

mldsa/src/poly_kl.h

@@ -306,20 +306,28 @@ __contract__(
 #define mld_polyw1_pack MLD_NAMESPACE_KL(polyw1_pack)
 /**
  * Bit-pack polynomial w1 with coefficients in [0, 15] or [0, 43]. Input
- * coefficients are assumed to be standard representatives.
+ * coefficients are assumed to be standard representatives. Dispatches to the
+ * value-specialized variant for the selected parameter set.
  *
  * @param[out] r Pointer to output byte array with at least
  *               MLDSA_POLYW1_PACKEDBYTES bytes.
  * @param[in]  a Pointer to input polynomial.
  */
-MLD_INTERNAL_API
-void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a)
+static MLD_INLINE void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES],
+                                       const mld_poly *a)
 __contract__(
   requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES))
   requires(memory_no_alias(a, sizeof(mld_poly)))
   requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
   assigns(memory_slice(r, MLDSA_POLYW1_PACKEDBYTES))
-);
+)
+{
+#if MLD_CONFIG_PARAMETER_SET == 44
+  mld_polyw1_pack_88(r, a);
+#else
+  mld_polyw1_pack_32(r, a);
+#endif
+}
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
 
 #endif /* !MLD_POLY_KL_H */

proofs/cbmc/poly_ntt_c/Makefile

@@ -26,7 +26,7 @@ USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
+CBMCFLAGS=--bitwuzla
 
 FUNCTION_NAME = mld_poly_ntt_c
 

proofs/cbmc/polyw1_pack/Makefile

@@ -17,10 +17,14 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c
 
 CHECK_FUNCTION_CONTRACTS=mld_polyw1_pack
-USE_FUNCTION_CONTRACTS=
+ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
+USE_FUNCTION_CONTRACTS=mld_polyw1_pack_88
+else
+USE_FUNCTION_CONTRACTS=mld_polyw1_pack_32
+endif
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

proofs/cbmc/polyw1_pack_32/Makefile

@@ -0,0 +1,40 @@
+# 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 = polyw1_pack_32_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 = polyw1_pack_32
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c
+
+ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
+CHECK_FUNCTION_CONTRACTS=
+else
+CHECK_FUNCTION_CONTRACTS=mld_polyw1_pack_32
+endif
+USE_FUNCTION_CONTRACTS=
+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 = polyw1_pack_32
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+include ../Makefile.common

proofs/cbmc/polyw1_pack_32/polyw1_pack_32_harness.c

@@ -0,0 +1,13 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "poly.h"
+
+void harness(void)
+{
+#if MLD_CONFIG_PARAMETER_SET != 44
+  mld_poly *a;
+  uint8_t *r;
+  mld_polyw1_pack_32(r, a);
+#endif
+}