pq-code-package · mkannwischer · Jan 7, 2026
@@ -290,7 +290,6 @@
 #undef mld_polyveck_pack_t0
 #undef mld_polyveck_pack_w1
 #undef mld_polyveck_pointwise_poly_montgomery
-#undef mld_polyveck_power2round
 #undef mld_polyveck_reduce
 #undef mld_polyveck_shiftl
 #undef mld_polyveck_sub

@@ -286,7 +286,6 @@
 #undef mld_polyveck_pack_t0
 #undef mld_polyveck_pack_w1
 #undef mld_polyveck_pointwise_poly_montgomery
-#undef mld_polyveck_power2round
 #undef mld_polyveck_reduce
 #undef mld_polyveck_shiftl
 #undef mld_polyveck_sub

@@ -713,30 +713,6 @@ uint32_t mld_polyveck_chknorm(const mld_polyveck *v, int32_t bound)
   return t;
 }
 
-MLD_INTERNAL_API
-void mld_polyveck_power2round(mld_polyveck *v1, mld_polyveck *v0,
-                              const mld_polyveck *v)
-{
-  unsigned int i;
-  mld_assert_bound_2d(v->vec, MLDSA_K, MLDSA_N, 0, MLDSA_Q);
-
-  for (i = 0; i < MLDSA_K; ++i)
-  __loop__(
-    assigns(i, memory_slice(v0, sizeof(mld_polyveck)), memory_slice(v1, sizeof(mld_polyveck)))
-    invariant(i <= MLDSA_K)
-    invariant(forall(k1, 0, i, array_bound(v0->vec[k1].coeffs, 0, MLDSA_N, -(MLD_2_POW_D/2)+1, (MLD_2_POW_D/2)+1)))
-    invariant(forall(k2, 0, i, array_bound(v1->vec[k2].coeffs, 0, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1)))
-  )
-  {
-    mld_poly_power2round(&v1->vec[i], &v0->vec[i], &v->vec[i]);
-  }
-
-  mld_assert_bound_2d(v0->vec, MLDSA_K, MLDSA_N, -(MLD_2_POW_D / 2) + 1,
-                      (MLD_2_POW_D / 2) + 1);
-  mld_assert_bound_2d(v1->vec, MLDSA_K, MLDSA_N, 0,
-                      ((MLDSA_Q - 1) / MLD_2_POW_D) + 1);
-}
-
 MLD_INTERNAL_API
 void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0)
 {

@@ -442,35 +442,6 @@ __contract__(
   ensures((return_value == 0) == forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, B)))
 );
 
-#define mld_polyveck_power2round MLD_NAMESPACE_KL(polyveck_power2round)
-/*************************************************
- * Name:        mld_polyveck_power2round
- *
- * Description: For all coefficients a of polynomials in vector of length
- *MLDSA_K, compute a0, a1 such that a mod^+ MLDSA_Q = a1*2^MLDSA_D + a0 with
- *-2^{MLDSA_D-1} < a0 <= 2^{MLDSA_D-1}. Assumes coefficients to be standard
- *representatives.
- *
- * Arguments:   - mld_polyveck *v1: pointer to output vector of polynomials with
- *                              coefficients a1
- *              - mld_polyveck *v0: pointer to output vector of polynomials with
- *                              coefficients a0
- *              - const mld_polyveck *v: pointer to input vector
- **************************************************/
-MLD_INTERNAL_API
-void mld_polyveck_power2round(mld_polyveck *v1, mld_polyveck *v0,
-                              const mld_polyveck *v)
-__contract__(
-  requires(memory_no_alias(v1, sizeof(mld_polyveck)))
-  requires(memory_no_alias(v0, sizeof(mld_polyveck)))
-  requires(memory_no_alias(v, sizeof(mld_polyveck)))
-  requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
-  assigns(memory_slice(v1, sizeof(mld_polyveck)))
-  assigns(memory_slice(v0, sizeof(mld_polyveck)))
-  ensures(forall(k1, 0, MLDSA_K, array_bound(v0->vec[k1].coeffs, 0, MLDSA_N, -(MLD_2_POW_D/2)+1, (MLD_2_POW_D/2)+1)))
-  ensures(forall(k2, 0, MLDSA_K, array_bound(v1->vec[k2].coeffs, 0, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1)))
-);
-
 #define mld_polyveck_decompose MLD_NAMESPACE_KL(polyveck_decompose)
 /*************************************************
  * Name:        mld_polyveck_decompose

@@ -51,6 +51,8 @@
   MLD_ADD_PARAM_SET(mld_attempt_signature_generation)
 #define mld_compute_t0_t1_tr_from_sk_components \
   MLD_ADD_PARAM_SET(mld_compute_t0_t1_tr_from_sk_components)
+#define mld_compute_t0_t1 MLD_ADD_PARAM_SET(mld_compute_t0_t1)
+#define mld_compute_t0_t1_foo MLD_ADD_PARAM_SET(mld_compute_t0_t1_foo)
 /* End of parameter set namespacing */
 
 
@@ -189,6 +191,99 @@ __contract__(
 #endif /* !MLD_CONFIG_SERIAL_FIPS202_ONLY */
 }
 
+static void mld_compute_t0_t1(mld_poly *t1, mld_poly *t0,
+                              const mld_polyvecl *matrow,
+                              const mld_polyvecl *s1, const mld_poly *s2,
+                              mld_poly *t)
+__contract__(
+  requires(memory_no_alias(t0, sizeof(mld_poly)))
+  requires(memory_no_alias(t1, sizeof(mld_poly)))
+  requires(memory_no_alias(matrow, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(s1, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(s2, sizeof(mld_poly)))
+  requires(memory_no_alias(t, sizeof(mld_poly)))
+  requires(forall(l0, 0, MLDSA_L, array_abs_bound(s1->vec[l0].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
+  requires(array_bound(s2->coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))
+  requires(forall(l1, 0, MLDSA_L, array_bound(matrow->vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
+  assigns(memory_slice(t, sizeof(mld_poly)))
+  assigns(memory_slice(t0, sizeof(mld_poly)))
+  assigns(memory_slice(t1, sizeof(mld_poly)))
+  ensures(array_bound(t0->coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))
+  ensures(array_bound(t1->coeffs, 0, MLDSA_N, 0, 1 << 10))
+)
+{
+  mld_polyvecl_pointwise_acc_montgomery(t, matrow, s1);
+  mld_poly_reduce(t);
+  mld_poly_invntt_tomont(t);
+
+  /* Add error vector s2 */
+  mld_poly_add(t, s2);
+
+  /* Reference: The following reduction is not present in the reference
+   *            implementation. Omitting this reduction requires the output of
+   *            the invntt to be small enough such that the addition of s2
+   *            does not result in absolute values >= MLDSA_Q. While our C,
+   *            x86_64, and AArch64 invntt implementations produce small
+   *            enough values for this to work out, it complicates the bounds
+   *            reasoning. We instead add an additional reduction, and can
+   *            consequently, relax the bounds requirements for the invntt.
+   */
+  mld_poly_reduce(t);
+
+
+  /* Decompose to get t1, t0 */
+  mld_poly_caddq(t);
+  mld_poly_power2round(t1, t0, t);
+}
+
+/* TODO remove this temp function*/
+static void mld_compute_t0_t1_foo(mld_polyveck *t1, mld_polyveck *t0,
+                                  mld_polymat *mat, const mld_polyvecl *s1,
+                                  const mld_polyveck *s2, mld_poly *t)
+__contract__(
+  requires(memory_no_alias(t0, sizeof(mld_polyveck)))
+  requires(memory_no_alias(t1, sizeof(mld_polyveck)))
+  requires(memory_no_alias(mat, sizeof(mld_polymat)))
+  requires(memory_no_alias(s1, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(s2, sizeof(mld_polyveck)))
+  requires(memory_no_alias(t, sizeof(mld_poly)))
+  requires(forall(l0, 0, MLDSA_L, array_abs_bound(s1->vec[l0].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
+  requires(forall(k0, 0, MLDSA_K, array_bound(s2->vec[k0].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)))
+  requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
+                                         array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
+  assigns(memory_slice(t0, sizeof(mld_polyveck)))
+  assigns(memory_slice(t1, sizeof(mld_polyveck)))
+  assigns(memory_slice(t, sizeof(mld_poly)))
+  ensures(forall(k1, 0, MLDSA_K, array_bound(t0->vec[k1].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)))
+  ensures(forall(k2, 0, MLDSA_K, array_bound(t1->vec[k2].coeffs, 0, MLDSA_N, 0, 1 << 10)))
+)
+{
+  unsigned int i;
+  for (i = 0; i < MLDSA_K; i++)
+  __loop__(
+    assigns(i, object_whole(t), memory_slice(t0, sizeof(mld_polyveck)), memory_slice(t1, sizeof(mld_polyveck)))
+    invariant(i <= MLDSA_K)
+    invariant(forall(k1, 0, i, array_bound(t0->vec[k1].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)))
+    invariant(forall(k2, 0, i, array_bound(t1->vec[k2].coeffs, 0, MLDSA_N, 0, 1 << 10)))
+  )
+  {
+#if 0
+  /* this works*/
+    mld_poly ttt0;
+    mld_poly ttt1;
+    const mld_polyvecl *row = mld_polymat_get_row(mat, i);
+    mld_compute_t0_t1(&ttt1, &ttt0, row, s1, &s2->vec[i], t);
+    /* TODO: remove this workaround */
+    t0->vec[i] = ttt0;
+    t1->vec[i] = ttt1;
+#else /* 0 */
+    /* thiis makes CBMC spin forver*/
+    const mld_polyvecl *row = mld_polymat_get_row(mat, i);
+    mld_compute_t0_t1(&t1->vec[i], &t0->vec[i], row, s1, &s2->vec[i], t);
+#endif /* !0 */
+  }
+}
+
 /*************************************************
  * Name:        mld_compute_t0_t1_tr_from_sk_components
  *
@@ -231,7 +326,7 @@ __contract__(
   int ret;
   MLD_ALLOC(mat, mld_polymat, 1);
   MLD_ALLOC(s1hat, mld_polyvecl, 1);
-  MLD_ALLOC(t, mld_polyveck, 1);
+  MLD_ALLOC(t, mld_poly, 1);
 
   if (mat == NULL || s1hat == NULL || t == NULL)
   {
@@ -242,30 +337,10 @@ __contract__(
   /* Expand matrix */
   mld_polyvec_matrix_expand(mat, rho);
 
-  /* Matrix-vector multiplication */
   *s1hat = *s1;
   mld_polyvecl_ntt(s1hat);
-  mld_polyvec_matrix_pointwise_montgomery(t, mat, s1hat);
-  mld_polyveck_reduce(t);
-  mld_polyveck_invntt_tomont(t);
-
-  /* Add error vector s2 */
-  mld_polyveck_add(t, s2);
-
-  /* Reference: The following reduction is not present in the reference
-   *            implementation. Omitting this reduction requires the output of
-   *            the invntt to be small enough such that the addition of s2 does
-   *            not result in absolute values >= MLDSA_Q. While our C, x86_64,
-   *            and AArch64 invntt implementations produce small enough
-   *            values for this to work out, it complicates the bounds
-   *            reasoning. We instead add an additional reduction, and can
-   *            consequently, relax the bounds requirements for the invntt.
-   */
-  mld_polyveck_reduce(t);
 
-  /* Decompose to get t1, t0 */
-  mld_polyveck_caddq(t);
-  mld_polyveck_power2round(t1, t0, t);
+  mld_compute_t0_t1_foo(t1, t0, mat, s1hat, s2, t);
 
   /* Pack public key and compute tr */
   mld_pack_pk(pk, rho, t1);
@@ -275,7 +350,7 @@ __contract__(
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(t, mld_polyveck, 1);
+  MLD_FREE(t, mld_poly, 1);
   MLD_FREE(s1hat, mld_polyvecl, 1);
   MLD_FREE(mat, mld_polymat, 1);
   return ret;
@@ -1392,5 +1467,7 @@ int crypto_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
 #undef mld_H
 #undef mld_attempt_signature_generation
 #undef mld_compute_t0_t1_tr_from_sk_components
+#undef mld_compute_t0_t1
+#undef mld_compute_t0_t1_foo
 #undef MLD_NONCE_UB
 #undef MLD_PRE_HASH_OID_LEN
@@ -0,0 +1,63 @@
+# 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 = compute_t0_t1_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 = mld_compute_t0_t1
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
+
+CHECK_FUNCTION_CONTRACTS=mld_compute_t0_t1
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_acc_montgomery
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_reduce
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_invntt_tomont
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_add
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_caddq
+USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)poly_power2round
+
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
+CBMCFLAGS += --slice-formula
+CBMCFLAGS += --no-array-field-sensitivity
+
+FUNCTION_NAME = mld_compute_t0_t1
+
+# 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 = 13
+
+# 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 "sign.h"
+
+static void mld_compute_t0_t1(mld_poly *t1, mld_poly *t0, mld_polyvecl *matrow,
+                              const mld_polyvecl *s1, const mld_poly *s2,
+                              mld_poly *t);
+void harness(void)
+{
+  mld_poly *t0;
+  mld_poly *t1;
+  mld_polyvecl *matrow;
+  mld_polyvecl *s1;
+  mld_poly *s2;
+  mld_poly *t;
+
+  mld_compute_t0_t1(t1, t0, matrow, s1, s2, t);
+}
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = polyveck_power2round_harness
+HARNESS_FILE = compute_t0_t1_foo_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 = polyveck_power2round
+PROOF_UID = mld_compute_t0_t1_foo
 
 DEFINES +=
 INCLUDES +=
@@ -17,18 +17,21 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c $(SRCDIR)/mldsa/src/polyvec.c
+
+CHECK_FUNCTION_CONTRACTS=mld_compute_t0_t1_foo
+USE_FUNCTION_CONTRACTS=mld_compute_t0_t1
 
-CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_power2round
-USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_power2round
 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 --slice-formula
+CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
+CBMCFLAGS += --slice-formula
+CBMCFLAGS += --no-array-field-sensitivity
 
-FUNCTION_NAME = polyveck_power2round
+FUNCTION_NAME = mld_compute_t0_t1_foo
 
 # 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
@@ -37,7 +40,7 @@ FUNCTION_NAME = polyveck_power2round
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 10
+CBMC_OBJECT_BITS = 13
 
 # 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