Skip to content

Port: Hoist default C backend into separate functions #735

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mkannwischer merged 11 commits into from
Dec 3, 2025
Merged

Port: Hoist default C backend into separate functions #735

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
aa25aba
Hoist default C backend into separate functions (mld_poly_ntt_c)
willieyz Nov 21, 2025
ab8246f
Hoist default C backend into separate functions(mld_poly_caddq_c)
willieyz Nov 24, 2025
a21fd43
Hoist default C backend into separate functions(mld_poly_invntt_tomon…
willieyz Nov 24, 2025
e4929ec
Hoist default C backend into separate functions(mld_poly_pointwise_mo…
willieyz Nov 24, 2025
c2fa513
Hoist default C backend into separate functions(mld_rej_uniform_c)
willieyz Nov 24, 2025
f2362e2
Hoist default C backend into separate functions(mld_polyvecl_pointwis…
willieyz Nov 24, 2025
bdeeb01
Hoist default C backend into separate functions(mld_poly_decompose_c)
willieyz Nov 24, 2025
0e4dbb1
Hoist default C backend into separate functions(mld_poly_use_hint_c)
willieyz Nov 24, 2025
f907f99
Hoist default C backend into separate functions(mld_polyz_unpack_c)
willieyz Nov 24, 2025
c262d71
Hoist default C backend into separate functions(mld_rej_eta_c)
willieyz Nov 24, 2025
088d716
Hoist default C backend into separate functions(mld_poly_chknorm_c)
willieyz Nov 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
137 changes: 78 additions & 59 deletions mldsa/src/polyvec.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@
* with native backends, which are currently not yet namespaced. */
#define mld_polymat_permute_bitrev_to_custom \
MLD_ADD_PARAM_SET(mld_polymat_permute_bitrev_to_custom)
#define mld_polyvecl_pointwise_acc_montgomery_c \
MLD_ADD_PARAM_SET(mld_polyvecl_pointwise_acc_montgomery_c)

/* Helper function to ensure that the polynomial entries in the output
* of mld_polyvec_matrix_expand use the standard (bitreversed) ordering
Expand Down Expand Up @@ -323,54 +325,95 @@ void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a,
mld_assert_abs_bound_2d(r->vec, MLDSA_L, MLDSA_N, MLDSA_Q);
}

MLD_INTERNAL_API
void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
const mld_polyvecl *v)
MLD_STATIC_TESTABLE void mld_polyvecl_pointwise_acc_montgomery_c(
mld_poly *w, const mld_polyvecl *u, const mld_polyvecl *v)
__contract__(
requires(memory_no_alias(w, sizeof(mld_poly)))
requires(memory_no_alias(u, sizeof(mld_polyvecl)))
requires(memory_no_alias(v, sizeof(mld_polyvecl)))
requires(forall(l0, 0, MLDSA_L,
array_bound(u->vec[l0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
requires(forall(l1, 0, MLDSA_L,
array_abs_bound(v->vec[l1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
assigns(memory_slice(w, sizeof(mld_poly)))
ensures(array_abs_bound(w->coeffs, 0, MLDSA_N, MLDSA_Q))
)
{
unsigned int i, j;
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
#if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) && \
MLD_CONFIG_PARAMETER_SET == 44
for (i = 0; i < MLDSA_N; i++)
__loop__(
assigns(i, j, memory_slice(w, sizeof(mld_poly)))
invariant(i <= MLDSA_N)
invariant(array_abs_bound(w->coeffs, 0, i, MLDSA_Q))
)
{
/* TODO: proof */
int ret;
ret = mld_polyvecl_pointwise_acc_montgomery_l4_native(
w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
(const int32_t(*)[MLDSA_N])v->vec);
if (ret == MLD_NATIVE_FUNC_SUCCESS)
int64_t t = 0;
int32_t r;
for (j = 0; j < MLDSA_L; j++)
__loop__(
assigns(j, t)
invariant(j <= MLDSA_L)
invariant(t >= -(int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
invariant(t <= (int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
)
{
mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
return;
t += (int64_t)u->vec[j].coeffs[i] * v->vec[j].coeffs[i];
}

r = mld_montgomery_reduce(t);
w->coeffs[i] = r;
}

mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
}

MLD_INTERNAL_API
void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
const mld_polyvecl *v)
{
#if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) && \
MLD_CONFIG_PARAMETER_SET == 44
/* TODO: proof */
int ret;
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
ret = mld_polyvecl_pointwise_acc_montgomery_l4_native(
w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
(const int32_t(*)[MLDSA_N])v->vec);
Comment on lines +382 to +384
Copy link
Contributor

@hanno-becker hanno-becker Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This cast business is not very nice. I wonder if we should modify the native API to streamline this. Not an issue for this PR.

Copy link
Contributor

@mkannwischer mkannwischer Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

mlkem-native has

    ret = mlk_polyvec_basemul_acc_montgomery_cached_k2_native(
        r->coeffs, (const int16_t *)a, (const int16_t *)b,
        (const int16_t *)b_cache);

Is that better?

if (ret == MLD_NATIVE_FUNC_SUCCESS)
{
mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
return;
}
#elif defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5) && \
MLD_CONFIG_PARAMETER_SET == 65
/* TODO: proof */
int ret;
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
ret = mld_polyvecl_pointwise_acc_montgomery_l5_native(
w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
(const int32_t(*)[MLDSA_N])v->vec);
if (ret == MLD_NATIVE_FUNC_SUCCESS)
{
/* TODO: proof */
int ret;
ret = mld_polyvecl_pointwise_acc_montgomery_l5_native(
w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
(const int32_t(*)[MLDSA_N])v->vec);
if (ret == MLD_NATIVE_FUNC_SUCCESS)
{
mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
return;
}
mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
return;
}
#elif defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7) && \
MLD_CONFIG_PARAMETER_SET == 87
/* TODO: proof */
int ret;
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
ret = mld_polyvecl_pointwise_acc_montgomery_l7_native(
w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
(const int32_t(*)[MLDSA_N])v->vec);
if (ret == MLD_NATIVE_FUNC_SUCCESS)
{
/* TODO: proof */
int ret;
ret = mld_polyvecl_pointwise_acc_montgomery_l7_native(
w->coeffs, (const int32_t(*)[MLDSA_N])u->vec,
(const int32_t(*)[MLDSA_N])v->vec);
if (ret == MLD_NATIVE_FUNC_SUCCESS)
{
mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
return;
}
mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
return;
}
#endif /* !(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 && \
MLD_CONFIG_PARAMETER_SET == 44) && \
Expand All @@ -386,32 +429,7 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
* The worst case is ML-DSA-87: 7 * (9Q-1) * (Q-1) < 2**52
* (and likewise for negative values)
*/

for (i = 0; i < MLDSA_N; i++)
__loop__(
assigns(i, j, memory_slice(w, sizeof(mld_poly)))
invariant(i <= MLDSA_N)
invariant(array_abs_bound(w->coeffs, 0, i, MLDSA_Q))
)
{
int64_t t = 0;
int32_t r;
for (j = 0; j < MLDSA_L; j++)
__loop__(
assigns(j, t)
invariant(j <= MLDSA_L)
invariant(t >= -(int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
invariant(t <= (int64_t)j*(MLDSA_Q - 1)*(MLD_NTT_BOUND - 1))
)
{
t += (int64_t)u->vec[j].coeffs[i] * v->vec[j].coeffs[i];
}

r = mld_montgomery_reduce(t);
w->coeffs[i] = r;
}

mld_assert_abs_bound(w->coeffs, MLDSA_N, MLDSA_Q);
mld_polyvecl_pointwise_acc_montgomery_c(w, u, v);
}

MLD_INTERNAL_API
Expand Down Expand Up @@ -864,3 +882,4 @@ void mld_polyveck_unpack_t0(mld_polyveck *p,
/* To facilitate single-compilation-unit (SCU) builds, undefine all macros.
* Don't modify by hand -- this is auto-generated by scripts/autogen. */
#undef mld_polymat_permute_bitrev_to_custom
#undef mld_polyvecl_pointwise_acc_montgomery_c
2 changes: 1 addition & 1 deletion proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c

CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_acc_montgomery
USE_FUNCTION_CONTRACTS=mld_montgomery_reduce
USE_FUNCTION_CONTRACTS= mld_polyvecl_pointwise_acc_montgomery_c
APPLY_LOOP_CONTRACTS=on
USE_DYNAMIC_FRAMES=1

Expand Down
57 changes: 57 additions & 0 deletions proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 = polyvecl_pointwise_acc_montgomery_c_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 = polyvecl_pointwise_acc_montgomery_c

DEFINES +=
INCLUDES +=

REMOVE_FUNCTION_BODY +=
UNWINDSET +=

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c

CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery_c
USE_FUNCTION_CONTRACTS=mld_montgomery_reduce
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_polyvecl_pointwise_acc_montgomery_c

# 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 = 12

# 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
18 changes: 18 additions & 0 deletions ...fs/cbmc/polyvecl_pointwise_acc_montgomery_c/polyvecl_pointwise_acc_montgomery_c_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// Copyright (c) The mldsa-native project authors
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT

#include "polyvec.h"


// Prototype for the function under test
#define mld_polyvecl_pointwise_acc_montgomery_c \
MLD_ADD_PARAM_SET(mld_polyvecl_pointwise_acc_montgomery_c)
void mld_polyvecl_pointwise_acc_montgomery_c(mld_poly *a, mld_polyvecl *b,
mld_polyvecl *c);

void harness(void)
{
mld_poly *a;
mld_polyvecl *b, *c;
mld_polyvecl_pointwise_acc_montgomery_c(a, b, c);
}