From 52df632f3bf24ad3c8aca98c99d59b55e1af2a7b Mon Sep 17 00:00:00 2001 From: willieyz Date: Mon, 29 Dec 2025 14:01:29 +0800 Subject: [PATCH] CBMC: Prove mld_polymat_permute_bitrev_to_custom on top of native API Refactor the polynomial matrix permutation to enable CBMC verification when using native backend implementations. The current implementation causes CBMC proof timeouts due to nested loops over two-dimensional polynomial matrices, similar to the issue described in (https://github.com/diffblue/cbmc/issues/8796). This refactoring decomposes the matrix-level operation into vector-level components with explicit contracts. As a result, CBMC can verify each component independently, avoiding the nested-loop state explosion while preserving safety verification for the native backend. Signed-off-by: willieyz --- mldsa/src/native/api.h | 11 +++- mldsa/src/polyvec.c | 55 ++++++++++++++----- proofs/cbmc/dummy_backend.h | 1 + .../polymat_permute_bitrev_to_custom/Makefile | 2 +- .../Makefile | 55 +++++++++++++++++++ ...olyvecl_permute_bitrev_to_custom_harness.c | 12 ++++ .../Makefile | 54 ++++++++++++++++++ ..._permute_bitrev_to_custom_native_harness.c | 12 ++++ scripts/check-contracts | 3 + 9 files changed, 189 insertions(+), 16 deletions(-) create mode 100644 proofs/cbmc/polyvecl_permute_bitrev_to_custom/Makefile create mode 100644 proofs/cbmc/polyvecl_permute_bitrev_to_custom/polyvecl_permute_bitrev_to_custom_harness.c create mode 100644 proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/Makefile create mode 100644 proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/polyvecl_permute_bitrev_to_custom_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index e210ff2a4..0f1fdeb16 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -122,7 +122,16 @@ set if there are native implementations for NTT and INTT." * Arguments: - int32_t p[MLDSA_N]: pointer to in/output polynomial * **************************************************/ -static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N]); +static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N]) +__contract__( + /* We don't specify that this should be a permutation, but only + * that it does not change the bound established at the end of + * mld_polyvec_matrix_expand. + */ + requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) + ensures(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q))); #endif /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index 95f7677f6..f6cc08386 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -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_permute_bitrev_to_custom \ + MLD_ADD_PARAM_SET(mld_polyvecl_permute_bitrev_to_custom) #define mld_polyvecl_pointwise_acc_montgomery_c \ MLD_ADD_PARAM_SET(mld_polyvecl_pointwise_acc_montgomery_c) @@ -34,6 +36,37 @@ * of coefficients. * No-op unless a native backend with a custom ordering is used. */ + +static void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v) +__contract__( + /* We don't specify that this should be a permutation, but only + * that it does not change the bound established at the end of + * mld_polyvec_matrix_expand. + */ + requires(memory_no_alias(v, sizeof(mld_polyvecl))) + requires(forall(x, 0, MLDSA_L, + array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) + assigns(memory_slice(v, sizeof(mld_polyvecl))) + ensures(forall(x, 0, MLDSA_L, + array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) +{ +#if defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER) + unsigned i; + for (i = 0; i < MLDSA_L; i++) + __loop__( + assigns(i, memory_slice(v, sizeof(mld_polyvecl))) + invariant(i <= MLDSA_L) + invariant(forall(x, 0, MLDSA_L, + array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) + { + mld_poly_permute_bitrev_to_custom(v->vec[i].coeffs); + } +#else /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ + /* Nothing to do */ + (void)v; +#endif /* !MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ +} + static void mld_polymat_permute_bitrev_to_custom(mld_polymat *mat) __contract__( /* We don't specify that this should be a permutation, but only @@ -48,23 +81,16 @@ __contract__( array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) ) { -#if defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER) - /* TODO: proof */ - unsigned int i, j; + unsigned int i; for (i = 0; i < MLDSA_K; i++) + __loop__( + assigns(i, memory_slice(mat, sizeof(mld_polymat))) + invariant(i <= MLDSA_K) + invariant(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, + array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))) { - for (j = 0; j < MLDSA_L; j++) - { - mld_poly_permute_bitrev_to_custom(mat->vec[i].vec[j].coeffs); - } + mld_polyvecl_permute_bitrev_to_custom(&mat->vec[i]); } - -#else /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ - - /* Nothing to do */ - ((void)mat); - -#endif /* !MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ } #endif /* !MLD_CONFIG_REDUCE_RAM */ @@ -925,4 +951,5 @@ 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_permute_bitrev_to_custom #undef mld_polyvecl_pointwise_acc_montgomery_c diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 92a11b566..0fff57564 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -24,6 +24,7 @@ #define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 #define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5 #define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 +#define MLD_USE_NATIVE_NTT_CUSTOM_ORDER #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile b/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile index 59a2fb467..690eef038 100644 --- a/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c CHECK_FUNCTION_CONTRACTS=mld_polymat_permute_bitrev_to_custom -USE_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/polyvecl_permute_bitrev_to_custom/Makefile b/proofs/cbmc/polyvecl_permute_bitrev_to_custom/Makefile new file mode 100644 index 000000000..370d3571e --- /dev/null +++ b/proofs/cbmc/polyvecl_permute_bitrev_to_custom/Makefile @@ -0,0 +1,55 @@ +# 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_permute_bitrev_to_custom_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_permute_bitrev_to_custom + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c + +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom +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 --slice-formula --no-array-field-sensitivity + +FUNCTION_NAME = polyvecl_permute_bitrev_to_custom + +# 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/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 diff --git a/proofs/cbmc/polyvecl_permute_bitrev_to_custom/polyvecl_permute_bitrev_to_custom_harness.c b/proofs/cbmc/polyvecl_permute_bitrev_to_custom/polyvecl_permute_bitrev_to_custom_harness.c new file mode 100644 index 000000000..83d58ff7c --- /dev/null +++ b/proofs/cbmc/polyvecl_permute_bitrev_to_custom/polyvecl_permute_bitrev_to_custom_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "polyvec.h" + +void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v); + +void harness(void) +{ + mld_polyvecl *v; + mld_polyvecl_permute_bitrev_to_custom(v); +} diff --git a/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/Makefile b/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/Makefile new file mode 100644 index 000000000..893a26dec --- /dev/null +++ b/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/Makefile @@ -0,0 +1,54 @@ +# Copyright (c) The mlkem-native project authors +# 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_permute_bitrev_to_custom_native_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_polyvecl_permute_bitrev_to_custom_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += +UNWINDSET += + +REMOVE_FUNCTION_BODY += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c + +CHECK_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom +USE_FUNCTION_CONTRACTS= mld_poly_permute_bitrev_to_custom +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 --no-array-field-sensitivity + +FUNCTION_NAME = mld_polyvecl_permute_bitrev_to_custom_native + +# 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 +CBMC_OBJECT_BITS = 10 + +# 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/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 diff --git a/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/polyvecl_permute_bitrev_to_custom_native_harness.c b/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/polyvecl_permute_bitrev_to_custom_native_harness.c new file mode 100644 index 000000000..83d58ff7c --- /dev/null +++ b/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/polyvecl_permute_bitrev_to_custom_native_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "polyvec.h" + +void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v); + +void harness(void) +{ + mld_polyvecl *v; + mld_polyvecl_permute_bitrev_to_custom(v); +} diff --git a/scripts/check-contracts b/scripts/check-contracts index 610458b13..2ad5a114e 100755 --- a/scripts/check-contracts +++ b/scripts/check-contracts @@ -43,6 +43,9 @@ def gen_contracts(): def is_exception(funcname): # The functions passing this filter are known not to have a proof + if funcname == 'poly_permute_bitrev_to_custom': + return True + if funcname.endswith("_native") or funcname.endswith("_asm"): # CBMC proofs are axiomatized against contracts of the backends return True