From 6bde8181ce2a8f553586c6edf2521e2e032de62b Mon Sep 17 00:00:00 2001 From: willieyz Date: Mon, 1 Dec 2025 11:52:20 +0800 Subject: [PATCH 01/13] CBMC: Add proofs on top of native functions (poly_ntt_native) This commit adds CBMC proofs for the native function `mld_ntt_native`, called `poly_ntt_native` The following changes are included: - Add `dummy_backend.h` as a mock backend for `poly_ntt_native`. - Apply the same harness file and construct function contract reference from `poly_ntt`. - Use the following function contracts: - `mld_ntt_native` - `mld_poly_ntt_c` - Introduce a new CBMC contract pattern `array_unchanged` in `cbmc.h`, which is used to verify the fallback behavior inside `mld_ntt_native`. Signed-off-by: willieyz --- mldsa/mldsa_native.S | 1 + mldsa/mldsa_native.c | 1 + mldsa/src/cbmc.h | 24 +++++++- mldsa/src/native/api.h | 17 +++++- proofs/cbmc/dummy_backend.h | 16 ++++++ proofs/cbmc/poly_ntt_native/Makefile | 55 +++++++++++++++++++ .../poly_ntt_native/poly_ntt_native_harness.c | 10 ++++ 7 files changed, 122 insertions(+), 2 deletions(-) create mode 100644 proofs/cbmc/dummy_backend.h create mode 100644 proofs/cbmc/poly_ntt_native/Makefile create mode 100644 proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c diff --git a/mldsa/mldsa_native.S b/mldsa/mldsa_native.S index cfed7a76c..9c3d31671 100644 --- a/mldsa/mldsa_native.S +++ b/mldsa/mldsa_native.S @@ -550,6 +550,7 @@ #undef MLD_NATIVE_API_H #undef MLD_NATIVE_FUNC_FALLBACK #undef MLD_NATIVE_FUNC_SUCCESS +#undef MLD_NTT_BOUND /* mldsa/src/native/meta.h */ #undef MLD_NATIVE_META_H #if defined(MLD_SYS_AARCH64) diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 9a5e2f318..0ee34ae5b 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -547,6 +547,7 @@ #undef MLD_NATIVE_API_H #undef MLD_NATIVE_FUNC_FALLBACK #undef MLD_NATIVE_FUNC_SUCCESS +#undef MLD_NTT_BOUND /* mldsa/src/native/meta.h */ #undef MLD_NATIVE_META_H #if defined(MLD_SYS_AARCH64) diff --git a/mldsa/src/cbmc.h b/mldsa/src/cbmc.h index 72b8538f0..b1208440b 100644 --- a/mldsa/src/cbmc.h +++ b/mldsa/src/cbmc.h @@ -8,7 +8,6 @@ /*************************************************** * Basic replacements for __CPROVER_XXX contracts ***************************************************/ - #ifndef CBMC #define __contract__(x) @@ -16,6 +15,7 @@ #define cassert(x) #else /* !CBMC */ + #include #define __contract__(x) x @@ -128,6 +128,28 @@ #define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \ array_bound_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), (qvar_lb), \ (qvar_ub), (array_var), (value_lb), (value_ub)) + +#define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var) \ + __CPROVER_forall \ + { \ + unsigned qvar; \ + ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + ((array_var)[(qvar)]) == (old(* (int16_t (*)[(qvar_ub)])(array_var)))[(qvar)] \ + } + +#define array_unchanged(array_var, N) \ + array_unchanged_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), 0, (N), (array_var)) + +#define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var) \ + __CPROVER_forall \ + { \ + unsigned qvar; \ + ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + ((array_var)[(qvar)]) == (old(* (uint64_t (*)[(qvar_ub)])(array_var)))[(qvar)] \ + } + +#define array_unchanged_u64(array_var, N) \ + array_unchanged_u64_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), 0, (N), (array_var)) /* clang-format on */ /* Wrapper around array_bound operating on absolute values. diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 333bb0c7b..421c7dfa5 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -38,6 +38,12 @@ */ #define MLD_NATIVE_FUNC_FALLBACK (-1) +/* Bound on absolute value of coefficients after NTT. + * + * NOTE: This is the same bound as in ntt.h and has to be kept + * in sync. */ +#define MLD_NTT_BOUND (9 * MLDSA_Q) + /* * This is the C<->native interface allowing for the drop-in of * native code for performance critical arithmetic components of ML-DSA. @@ -67,7 +73,16 @@ * * Arguments: - int32_t p[MLDSA_N]: pointer to in/output polynomial **************************************************/ -static MLD_INLINE int mld_ntt_native(int32_t p[MLDSA_N]); +static MLD_INLINE int mld_ntt_native(int32_t p[MLDSA_N]) +__contract__( + requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLDSA_N, MLD_NTT_BOUND)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(p, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_NTT */ diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h new file mode 100644 index 000000000..bfdfc6e48 --- /dev/null +++ b/proofs/cbmc/dummy_backend.h @@ -0,0 +1,16 @@ +/* + * Copyright (c) The mldsa-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ + +#ifndef MLD_DUMMY_ARITH_BACKEND_H +#define MLD_DUMMY_ARITH_BACKEND_H + + +#define MLD_USE_NATIVE_NTT + + + +#include "../../mldsa/src/native/api.h" + +#endif /* !MLD_DUMMY_ARITH_BACKEND_H */ diff --git a/proofs/cbmc/poly_ntt_native/Makefile b/proofs/cbmc/poly_ntt_native/Makefile new file mode 100644 index 000000000..80d47f049 --- /dev/null +++ b/proofs/cbmc/poly_ntt_native/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 = poly_ntt_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 = poly_ntt_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_ntt +USE_FUNCTION_CONTRACTS=mld_ntt_native mld_poly_ntt_c +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 = poly_ntt + +# 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 diff --git a/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c b/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c new file mode 100644 index 000000000..a1720228f --- /dev/null +++ b/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ + mld_poly *a; + mld_poly_ntt(a); +} From 28aa07c603e2031dbc9dae91805d9c10c81a4785 Mon Sep 17 00:00:00 2001 From: willieyz Date: Mon, 1 Dec 2025 18:25:29 +0800 Subject: [PATCH 02/13] CBMC: Add proofs on top of native functions (poly_invntt_tomont_native) - This commit adds CBMC proofs for the native function `mld_intt_native`, called `poly_invntt_tomont_native` - This following changes are include: - Apply the same harness file and construct function contract, reference from `poly_invntt_tomnot`. - Use the following function contracts: - `mld_intt_native` - `mld_poly_invntt_tomont_c` - Add MLD_INTT_BOUND in api.h - Add `MLD_USE_NATIVE_INTT` in dummy_backend.h Signed-off-by: willieyz --- mldsa/mldsa_native.S | 1 + mldsa/mldsa_native.c | 1 + mldsa/src/native/api.h | 17 +++++- proofs/cbmc/dummy_backend.h | 2 +- .../cbmc/poly_invntt_tomont_native/Makefile | 55 +++++++++++++++++++ .../poly_invntt_tomont_native_harness.c | 10 ++++ 6 files changed, 84 insertions(+), 2 deletions(-) create mode 100644 proofs/cbmc/poly_invntt_tomont_native/Makefile create mode 100644 proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c diff --git a/mldsa/mldsa_native.S b/mldsa/mldsa_native.S index 9c3d31671..3861e94bb 100644 --- a/mldsa/mldsa_native.S +++ b/mldsa/mldsa_native.S @@ -547,6 +547,7 @@ #endif /* MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */ #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) /* mldsa/src/native/api.h */ +#undef MLD_INTT_BOUND #undef MLD_NATIVE_API_H #undef MLD_NATIVE_FUNC_FALLBACK #undef MLD_NATIVE_FUNC_SUCCESS diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 0ee34ae5b..c394c051b 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -544,6 +544,7 @@ #endif /* MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */ #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) /* mldsa/src/native/api.h */ +#undef MLD_INTT_BOUND #undef MLD_NATIVE_API_H #undef MLD_NATIVE_FUNC_FALLBACK #undef MLD_NATIVE_FUNC_SUCCESS diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 421c7dfa5..ecb870a19 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -44,6 +44,12 @@ * in sync. */ #define MLD_NTT_BOUND (9 * MLDSA_Q) +/* Absolute exclusive upper bound for the output of the inverse NTT + * + * NOTE: This is the same bound as in ntt.h and has to be kept + * in sync. */ +#define MLD_INTT_BOUND MLDSA_Q + /* * This is the C<->native interface allowing for the drop-in of * native code for performance critical arithmetic components of ML-DSA. @@ -126,7 +132,16 @@ static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N]); * * Arguments: - uint32_t p[MLDSA_N]: pointer to in/output polynomial **************************************************/ -static MLD_INLINE int mld_intt_native(int32_t p[MLDSA_N]); +static MLD_INLINE int mld_intt_native(int32_t p[MLDSA_N]) +__contract__( + requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) + requires(array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLDSA_N, MLD_INTT_BOUND)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(p, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(p, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_INTT */ #if defined(MLD_USE_NATIVE_REJ_UNIFORM) diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index bfdfc6e48..7cfa95490 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -8,7 +8,7 @@ #define MLD_USE_NATIVE_NTT - +#define MLD_USE_NATIVE_INTT #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/poly_invntt_tomont_native/Makefile b/proofs/cbmc/poly_invntt_tomont_native/Makefile new file mode 100644 index 000000000..fa1a0b623 --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_native/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 = poly_invntt_tomont_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 = poly_invntt_tomont_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_invntt_tomont +USE_FUNCTION_CONTRACTS=mld_intt_native mld_poly_invntt_tomont_c +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 = poly_invntt_tomont_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 + +# This function is large enough to need... +CBMC_OBJECT_BITS = 9 + +# 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 diff --git a/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c b/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c new file mode 100644 index 000000000..27fc2b9d6 --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ + mld_poly *a; + mld_poly_invntt_tomont(a); +} From f51cc270c6ce239dccbc7eed8c9faca0772658f9 Mon Sep 17 00:00:00 2001 From: willieyz Date: Wed, 3 Dec 2025 13:46:26 +0800 Subject: [PATCH 03/13] CBMC: Add proofs on top of native functions (rej_uniform_native) - This commit adds CBMC proofs for the native function `mld_rej_uniform_native`, called `rej_uniform_native` - This following changes are include: - Apply the same harness file and construct function contract reference from `rej_uniform`. - Use the following function contracts: - `mld_rej_uniform_native` - `mld_rej_uniform_c` - Add `MLD_USE_NATIVE_REJ_UNIFORM` in dummy_backend.h Signed-off-by: willieyz --- mldsa/src/native/api.h | 11 +++- mldsa/src/poly.c | 1 - proofs/cbmc/dummy_backend.h | 2 +- proofs/cbmc/rej_uniform_native/Makefile | 55 +++++++++++++++++++ .../rej_uniform_native_harness.c | 19 +++++++ 5 files changed, 85 insertions(+), 3 deletions(-) create mode 100644 proofs/cbmc/rej_uniform_native/Makefile create mode 100644 proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index ecb870a19..7d37a7826 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -164,7 +164,16 @@ __contract__( **************************************************/ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len, const uint8_t *buf, - unsigned buflen); + unsigned buflen) +__contract__( + requires(len <= MLDSA_N) + requires(buflen <= ( 5 * 168) && buflen % 3 == 0) + requires(memory_no_alias(r, sizeof(int32_t) * len)) + requires(memory_no_alias(buf, buflen)) + assigns(memory_slice(r, sizeof(int32_t) * len)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) + ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> array_bound(r, 0, (unsigned) return_value, 0, MLDSA_Q)) +); #endif /* MLD_USE_NATIVE_REJ_UNIFORM */ #if defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index e60fc306b..907734948 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -368,7 +368,6 @@ __contract__( ensures(array_bound(a, 0, return_value, 0, MLDSA_Q)) ) { -/* TODO: CBMC proof based on mld_rej_uniform_native */ #if defined(MLD_USE_NATIVE_REJ_UNIFORM) int ret; mld_assert_bound(a, offset, 0, MLDSA_Q); diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 7cfa95490..38c4c6a27 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -9,7 +9,7 @@ #define MLD_USE_NATIVE_NTT #define MLD_USE_NATIVE_INTT - +#define MLD_USE_NATIVE_REJ_UNIFORM #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/rej_uniform_native/Makefile b/proofs/cbmc/rej_uniform_native/Makefile new file mode 100644 index 000000000..15447a074 --- /dev/null +++ b/proofs/cbmc/rej_uniform_native/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 = rej_uniform_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 = rej_uniform_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mld_rej_uniform +USE_FUNCTION_CONTRACTS=mld_rej_uniform_native mld_rej_uniform_c +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 = mld_rej_uniform_native_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 + +# 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 diff --git a/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c b/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c new file mode 100644 index 000000000..e4b909748 --- /dev/null +++ b/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +static unsigned int mld_rej_uniform(int32_t *a, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen); + +void harness(void) +{ + int32_t *a; + unsigned int target; + unsigned int offset; + const uint8_t *buf; + unsigned int buflen; + + mld_rej_uniform(a, target, offset, buf, buflen); +} From 3aff17722a72e73fda9c9481e05dae957e278c7a Mon Sep 17 00:00:00 2001 From: willieyz Date: Wed, 3 Dec 2025 17:37:59 +0800 Subject: [PATCH 04/13] CBMC: Add proofs on top of native functions (rej_eta_native) - This commit adds CBMC proofs for following the native function: `mld_rej_uniform_eta2_native` and `mld_rej_uniform_eta4_native`, called `rej_eta_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from rej_eta. - Use the following function contracts: - mld_rej_eta_c - mld_rej_uniform_eta2_native - mld_rej_uniform_eta4_native - Add `MLD_USE_NATIVE_REJ_UNIFORM_ETA2`, `MLD_USE_NATIVE_REJ_UNIFORM_ETA4` in dummy_backend.h Signed-off-by: willieyz --- mldsa/src/native/api.h | 22 ++++++- mldsa/src/poly_kl.c | 2 - proofs/cbmc/dummy_backend.h | 2 + proofs/cbmc/rej_eta_native/Makefile | 62 +++++++++++++++++++ .../rej_eta_native/rej_eta_native_harness.c | 19 ++++++ 5 files changed, 103 insertions(+), 4 deletions(-) create mode 100644 proofs/cbmc/rej_eta_native/Makefile create mode 100644 proofs/cbmc/rej_eta_native/rej_eta_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 7d37a7826..abc604769 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -196,7 +196,16 @@ __contract__( **************************************************/ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len, const uint8_t *buf, - unsigned buflen); + unsigned buflen) +__contract__( + requires(len <= MLDSA_N) + requires(buflen <= (2 * 136)) + requires(memory_no_alias(r, sizeof(int32_t) * len)) + requires(memory_no_alias(buf, buflen)) + assigns(memory_slice(r, sizeof(int32_t) * len)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) + ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))) +); #endif /* MLD_USE_NATIVE_REJ_UNIFORM_ETA2 */ #if defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) @@ -219,7 +228,16 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len, **************************************************/ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len, const uint8_t *buf, - unsigned buflen); + unsigned buflen) +__contract__( + requires(len <= MLDSA_N) + requires(buflen <= (2 * 136)) + requires(memory_no_alias(r, sizeof(int32_t) * len)) + requires(memory_no_alias(buf, buflen)) + assigns(memory_slice(r, sizeof(int32_t) * len)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len)) + ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))) +); #endif /* MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */ #if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_32) diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index ba7ba25b2..b43ac275a 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -313,7 +313,6 @@ __contract__( ensures(array_abs_bound(a, 0, return_value, MLDSA_ETA + 1)) ) { -/* TODO: CBMC proof based on mld_rej_uniform_eta2_native */ #if MLDSA_ETA == 2 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA2) int ret; mld_assert_abs_bound(a, offset, MLDSA_ETA + 1); @@ -327,7 +326,6 @@ __contract__( return res; } } -/* TODO: CBMC proof based on mld_rej_uniform_eta4_native */ #elif MLDSA_ETA == 4 && defined(MLD_USE_NATIVE_REJ_UNIFORM_ETA4) int ret; mld_assert_abs_bound(a, offset, MLDSA_ETA + 1); diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 38c4c6a27..621bf0192 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -10,6 +10,8 @@ #define MLD_USE_NATIVE_NTT #define MLD_USE_NATIVE_INTT #define MLD_USE_NATIVE_REJ_UNIFORM +#define MLD_USE_NATIVE_REJ_UNIFORM_ETA2 +#define MLD_USE_NATIVE_REJ_UNIFORM_ETA4 #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/rej_eta_native/Makefile b/proofs/cbmc/rej_eta_native/Makefile new file mode 100644 index 000000000..76fb0b117 --- /dev/null +++ b/proofs/cbmc/rej_eta_native/Makefile @@ -0,0 +1,62 @@ +# 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 = rej_eta_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 = rej_eta_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=mld_rej_eta +USE_FUNCTION_CONTRACTS= mld_rej_eta_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_rej_uniform_eta2_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_rej_uniform_eta4_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_rej_uniform_eta2_native +endif +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = mld_rej_eta_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 + +# 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 diff --git a/proofs/cbmc/rej_eta_native/rej_eta_native_harness.c b/proofs/cbmc/rej_eta_native/rej_eta_native_harness.c new file mode 100644 index 000000000..b540b7bf9 --- /dev/null +++ b/proofs/cbmc/rej_eta_native/rej_eta_native_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +static unsigned int mld_rej_eta(int32_t *a, unsigned int target, + unsigned int offset, const uint8_t *buf, + unsigned int buflen); + +void harness(void) +{ + int32_t *a; + unsigned int target; + unsigned int offset; + const uint8_t *buf; + unsigned int buflen; + + mld_rej_eta(a, target, offset, buf, buflen); +} From a296abd40d09997e89d5b4c5a9ec28a14e98b7e5 Mon Sep 17 00:00:00 2001 From: willieyz Date: Wed, 3 Dec 2025 19:09:45 +0800 Subject: [PATCH 05/13] CBMC: Add proofs on top of native functions (poly_decompose_native) - This commit adds CBMC proofs for following the native function: `mld_poly_decompose_32_native`, `mld_poly_decompose_88_native`. called `poly_decompose_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from `poly_decompose`. - Use the following function contracts: - mld_poly_decompose_c - mld_poly_decompose_32_native - mld_poly_decompose_88_native - Add `MLD_USE_NATIVE_POLY_DECOMPOSE_32`, `MLD_USE_NATIVE_POLY_DECOMPOSE_88` in dummy_backend.h Signed-off-by: willieyz --- mldsa/src/native/api.h | 30 ++++++++- mldsa/src/poly_kl.c | 2 - proofs/cbmc/dummy_backend.h | 2 + proofs/cbmc/poly_decompose_native/Makefile | 62 +++++++++++++++++++ .../poly_decompose_native_harness.c | 11 ++++ 5 files changed, 103 insertions(+), 4 deletions(-) create mode 100644 proofs/cbmc/poly_decompose_native/Makefile create mode 100644 proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index abc604769..3e182efef 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -258,7 +258,20 @@ __contract__( * - const int32_t *a: input polynomial **************************************************/ static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0, - const int32_t *a); + const int32_t *a) +__contract__( + requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) + assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a1, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(a0, 0, MLDSA_N, MLDSA_GAMMA2+1)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_DECOMPOSE_32 */ #if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) @@ -279,7 +292,20 @@ static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0, * - const int32_t *a: input polynomial **************************************************/ static MLD_INLINE int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0, - const int32_t *a); + const int32_t *a) +__contract__( + requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N)) + assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a1, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(a0, 0, MLDSA_N, MLDSA_GAMMA2+1)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_DECOMPOSE_88 */ #if defined(MLD_USE_NATIVE_POLY_CADDQ) diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index b43ac275a..5933099bf 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -75,7 +75,6 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) #if defined(MLD_USE_NATIVE_POLY_DECOMPOSE_88) && MLD_CONFIG_PARAMETER_SET == 44 int ret; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - /* TODO: proof */ ret = mld_poly_decompose_88_native(a1->coeffs, a0->coeffs, a->coeffs); if (ret == MLD_NATIVE_FUNC_SUCCESS) { @@ -88,7 +87,6 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a) (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) int ret; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); - /* TODO: proof */ ret = mld_poly_decompose_32_native(a1->coeffs, a0->coeffs, a->coeffs); if (ret == MLD_NATIVE_FUNC_SUCCESS) { diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 621bf0192..5ecb6e0b3 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -12,6 +12,8 @@ #define MLD_USE_NATIVE_REJ_UNIFORM #define MLD_USE_NATIVE_REJ_UNIFORM_ETA2 #define MLD_USE_NATIVE_REJ_UNIFORM_ETA4 +#define MLD_USE_NATIVE_POLY_DECOMPOSE_32 +#define MLD_USE_NATIVE_POLY_DECOMPOSE_88 #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/poly_decompose_native/Makefile b/proofs/cbmc/poly_decompose_native/Makefile new file mode 100644 index 000000000..1f084308e --- /dev/null +++ b/proofs/cbmc/poly_decompose_native/Makefile @@ -0,0 +1,62 @@ +# 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 = poly_decompose_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 = poly_decompose_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_decompose +USE_FUNCTION_CONTRACTS= mld_poly_decompose_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_poly_decompose_88_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_poly_decompose_32_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_poly_decompose_32_native +endif +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 = poly_decompose_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 + +# 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 diff --git a/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c b/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c new file mode 100644 index 000000000..309afec1e --- /dev/null +++ b/proofs/cbmc/poly_decompose_native/poly_decompose_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + + +void harness(void) +{ + mld_poly *a0, *a1, *a; + mld_poly_decompose(a1, a0, a); +} From 22b5d422c6fa3f3dcda773e3c7f62b8175c5cf3d Mon Sep 17 00:00:00 2001 From: willieyz Date: Mon, 1 Dec 2025 17:32:23 +0800 Subject: [PATCH 06/13] CBMC: Add proofs on top of native functions (mld_poly_caddq_native) - This commit adds CBMC proofs for the native function `mld_poly_caddq_native`, called `poly_caddq_native` - This following changes are include: - Apply the same harness file and construct function contract reference from `poly_caddq`. - Use the following function contracts: - `mld_poly_caddq_c` - `mld_poly_caddq_native` - Add `MLD_USE_NATIVE_POLY_CADDQ` in dummy_backend.h Signed-off-by: willieyz --- mldsa/src/native/api.h | 11 +++- proofs/cbmc/dummy_backend.h | 1 + proofs/cbmc/poly_caddq_native/Makefile | 55 +++++++++++++++++++ .../poly_caddq_native_harness.c | 11 ++++ 4 files changed, 77 insertions(+), 1 deletion(-) create mode 100644 proofs/cbmc/poly_caddq_native/Makefile create mode 100644 proofs/cbmc/poly_caddq_native/poly_caddq_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 3e182efef..aefaa7dc7 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -317,7 +317,16 @@ __contract__( * * Arguments: - int32_t *a: pointer to input/output polynomial **************************************************/ -static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N]); +static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N]) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(array_abs_bound(a, 0, MLDSA_N, MLDSA_Q)) + assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(a, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_CADDQ */ #if defined(MLD_USE_NATIVE_POLY_USE_HINT_32) diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 5ecb6e0b3..70d0b6dea 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -14,6 +14,7 @@ #define MLD_USE_NATIVE_REJ_UNIFORM_ETA4 #define MLD_USE_NATIVE_POLY_DECOMPOSE_32 #define MLD_USE_NATIVE_POLY_DECOMPOSE_88 +#define MLD_USE_NATIVE_POLY_CADDQ #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/poly_caddq_native/Makefile b/proofs/cbmc/poly_caddq_native/Makefile new file mode 100644 index 000000000..94fc09e8b --- /dev/null +++ b/proofs/cbmc/poly_caddq_native/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 =poly_caddq_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 = poly_caddq_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_caddq +USE_FUNCTION_CONTRACTS=mld_poly_caddq_native mld_poly_caddq_c +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 = poly_caddq_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 + +# 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 diff --git a/proofs/cbmc/poly_caddq_native/poly_caddq_native_harness.c b/proofs/cbmc/poly_caddq_native/poly_caddq_native_harness.c new file mode 100644 index 000000000..93de3b5b5 --- /dev/null +++ b/proofs/cbmc/poly_caddq_native/poly_caddq_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + + +void harness(void) +{ + mld_poly *a; + mld_poly_caddq(a); +} From 81e3cb04b11152b92c67e5e9e65e189a398ba949 Mon Sep 17 00:00:00 2001 From: willieyz Date: Thu, 4 Dec 2025 10:38:57 +0800 Subject: [PATCH 07/13] CBMC: Add proofs on top of native functions (poly_use_hint_native) - This commit adds CBMC proofs for following the native function: `mld_poly_use_hint_32_native`, `mld_poly_use_hint_88_native`. called `poly_use_hint_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from `poly_use_hint`. - Use the following function contracts: - mld_poly_use_hint_c - mld_poly_use_hint_32_native - mld_poly_use_hint_88_native - Add `MLD_USE_NATIVE_POLY_USE_HINT_32`, `MLD_USE_NATIVE_POLY_USE_HINT_88` in dummy_backend.h Signed-off-by: willieyz --- mldsa/src/native/api.h | 26 +++++++- mldsa/src/poly_kl.c | 2 - proofs/cbmc/dummy_backend.h | 2 + proofs/cbmc/poly_use_hint_native/Makefile | 62 +++++++++++++++++++ .../poly_use_hint_native_harness.c | 11 ++++ 5 files changed, 99 insertions(+), 4 deletions(-) create mode 100644 proofs/cbmc/poly_use_hint_native/Makefile create mode 100644 proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index aefaa7dc7..8374c3ff0 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -342,7 +342,18 @@ __contract__( * - const int32_t *h: pointer to input hint polynomial **************************************************/ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a, - const int32_t *h); + const int32_t *h) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(b, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(b, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_USE_HINT_32 */ #if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) @@ -358,7 +369,18 @@ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a, * - const int32_t *h: pointer to input hint polynomial **************************************************/ static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a, - const int32_t *h); + const int32_t *h) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N)) + requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q)) + requires(array_bound(h, 0, MLDSA_N, 0, 2)) + assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(b, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(b, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLY_USE_HINT_88 */ #if defined(MLD_USE_NATIVE_POLY_CHKNORM) diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index 5933099bf..03094df80 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -158,7 +158,6 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) int ret; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - /* TODO: proof */ ret = mld_poly_use_hint_88_native(b->coeffs, a->coeffs, h->coeffs); if (ret == MLD_NATIVE_FUNC_SUCCESS) { @@ -170,7 +169,6 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h) int ret; mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q); mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - /* TODO: proof */ ret = mld_poly_use_hint_32_native(b->coeffs, a->coeffs, h->coeffs); if (ret == MLD_NATIVE_FUNC_SUCCESS) { diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 70d0b6dea..638dd68ef 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -15,6 +15,8 @@ #define MLD_USE_NATIVE_POLY_DECOMPOSE_32 #define MLD_USE_NATIVE_POLY_DECOMPOSE_88 #define MLD_USE_NATIVE_POLY_CADDQ +#define MLD_USE_NATIVE_POLY_USE_HINT_32 +#define MLD_USE_NATIVE_POLY_USE_HINT_88 #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/poly_use_hint_native/Makefile b/proofs/cbmc/poly_use_hint_native/Makefile new file mode 100644 index 000000000..800f888cd --- /dev/null +++ b/proofs/cbmc/poly_use_hint_native/Makefile @@ -0,0 +1,62 @@ +# 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 = poly_use_hint_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 = poly_use_hint_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_use_hint +USE_FUNCTION_CONTRACTS=mld_poly_use_hint_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_88_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_32_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_poly_use_hint_32_native +endif +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 = poly_use_hint_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 + +# 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 diff --git a/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c b/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c new file mode 100644 index 000000000..360de6d3f --- /dev/null +++ b/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + + +void harness(void) +{ + mld_poly *a, *b, *h; + mld_poly_use_hint(b, a, h); +} From b0e5eb87be29d5546df7772f401b1f19dea3f7ad Mon Sep 17 00:00:00 2001 From: willieyz Date: Thu, 4 Dec 2025 11:20:18 +0800 Subject: [PATCH 08/13] CBMC: Add proofs on top of native functions (poly_chknorm_native) - This commit adds CBMC proofs for following the native function: `mld_poly_chknorm_native`, called `poly_chknorm_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from `poly_chknorm_native`. - Use the following function contracts: - `mld_poly_chknorm_c` - `mld_poly_chknorm_native` - Add `MLD_USE_NATIVE_POLY_CHKNORM` in dummy_backend.h Signed-off-by: willieyz --- mldsa/mldsa_native.S | 1 + mldsa/mldsa_native.c | 1 + mldsa/src/native/api.h | 15 ++++- mldsa/src/poly.c | 1 - proofs/cbmc/dummy_backend.h | 1 + proofs/cbmc/poly_chknorm_native/Makefile | 55 +++++++++++++++++++ .../poly_chknorm_native_harness.c | 13 +++++ 7 files changed, 85 insertions(+), 2 deletions(-) create mode 100644 proofs/cbmc/poly_chknorm_native/Makefile create mode 100644 proofs/cbmc/poly_chknorm_native/poly_chknorm_native_harness.c diff --git a/mldsa/mldsa_native.S b/mldsa/mldsa_native.S index 3861e94bb..7b895a4a5 100644 --- a/mldsa/mldsa_native.S +++ b/mldsa/mldsa_native.S @@ -552,6 +552,7 @@ #undef MLD_NATIVE_FUNC_FALLBACK #undef MLD_NATIVE_FUNC_SUCCESS #undef MLD_NTT_BOUND +#undef REDUCE32_RANGE_MAX /* mldsa/src/native/meta.h */ #undef MLD_NATIVE_META_H #if defined(MLD_SYS_AARCH64) diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index c394c051b..79661a7ff 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -549,6 +549,7 @@ #undef MLD_NATIVE_FUNC_FALLBACK #undef MLD_NATIVE_FUNC_SUCCESS #undef MLD_NTT_BOUND +#undef REDUCE32_RANGE_MAX /* mldsa/src/native/meta.h */ #undef MLD_NATIVE_META_H #if defined(MLD_SYS_AARCH64) diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 8374c3ff0..2bc9cdbf4 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -50,6 +50,12 @@ * in sync. */ #define MLD_INTT_BOUND MLDSA_Q +/* Absolute bound for range of mld_reduce32() + * + * NOTE: This is the same bound as in reduce.h and has to be kept + * in sync. */ +/* check-magic: 6283009 == (REDUCE32_DOMAIN_MAX - 255 * MLDSA_Q + 1) */ +#define REDUCE32_RANGE_MAX 6283009 /* * This is the C<->native interface allowing for the drop-in of * native code for performance critical arithmetic components of ML-DSA. @@ -396,7 +402,14 @@ __contract__( * Returns 0 if the infinity norm is strictly smaller than B, and 1 * otherwise. B must not be larger than MLDSA_Q - REDUCE32_RANGE_MAX. **************************************************/ -static MLD_INLINE int mld_poly_chknorm_native(const int32_t *a, int32_t B); +static MLD_INLINE int mld_poly_chknorm_native(const int32_t *a, int32_t B) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(0 <= B && B <= MLDSA_Q - REDUCE32_RANGE_MAX) + requires(array_bound(a, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == 0) == array_abs_bound(a, 0, MLDSA_N, B)) +); #endif /* MLD_USE_NATIVE_POLY_CHKNORM */ #if defined(MLD_USE_NATIVE_POLYZ_UNPACK_17) diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index 907734948..757df9e6c 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -703,7 +703,6 @@ MLD_INTERNAL_API uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B) { #if defined(MLD_USE_NATIVE_POLY_CHKNORM) - /* TODO: proof */ int ret; int success; mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX); diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 638dd68ef..5beb8181d 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -17,6 +17,7 @@ #define MLD_USE_NATIVE_POLY_CADDQ #define MLD_USE_NATIVE_POLY_USE_HINT_32 #define MLD_USE_NATIVE_POLY_USE_HINT_88 +#define MLD_USE_NATIVE_POLY_CHKNORM #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/poly_chknorm_native/Makefile b/proofs/cbmc/poly_chknorm_native/Makefile new file mode 100644 index 000000000..6643b2158 --- /dev/null +++ b/proofs/cbmc/poly_chknorm_native/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 =poly_chknorm_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 = poly_chknorm_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm +USE_FUNCTION_CONTRACTS=mld_poly_chknorm_native mld_poly_chknorm_c +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 = poly_chknorm_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 + +# 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 diff --git a/proofs/cbmc/poly_chknorm_native/poly_chknorm_native_harness.c b/proofs/cbmc/poly_chknorm_native/poly_chknorm_native_harness.c new file mode 100644 index 000000000..890886154 --- /dev/null +++ b/proofs/cbmc/poly_chknorm_native/poly_chknorm_native_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_kl.h" + + +void harness(void) +{ + mld_poly *a; + uint32_t r; + int32_t B; + r = mld_poly_chknorm(a, B); +} From feb44c1a81c8a618b17f6359ac978fff1f71a672 Mon Sep 17 00:00:00 2001 From: willieyz Date: Thu, 4 Dec 2025 11:41:49 +0800 Subject: [PATCH 09/13] CBMC: Add proofs on top of native functions (polyz_unpack_native) - This commit adds CBMC proofs for following the native function: `mld_polyz_unpack_17_native` and `mld_polyz_unpack_19_native`. called `polyz_unpack_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from `polyz_unpack`. - Use the following function contracts: - `mld_polyz_unpack_c` - `mld_polyz_unpack_17_native` - `mld_polyz_unpack_17_native` - Add `MLD_USE_NATIVE_POLYZ_UNPACK_17`, `MLD_USE_NATIVE_POLYZ_UNPACK_19` in dummy_backend.h Signed-off-by: willieyz --- mldsa/src/native/api.h | 20 +++++- mldsa/src/poly_kl.c | 2 - proofs/cbmc/dummy_backend.h | 2 + proofs/cbmc/polyz_unpack_native/Makefile | 62 +++++++++++++++++++ .../polyz_unpack_native_harness.c | 11 ++++ 5 files changed, 93 insertions(+), 4 deletions(-) create mode 100644 proofs/cbmc/polyz_unpack_native/Makefile create mode 100644 proofs/cbmc/polyz_unpack_native/polyz_unpack_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 2bc9cdbf4..3439bd828 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -423,7 +423,15 @@ __contract__( * Arguments: - int32_t *r: pointer to output polynomial * - const uint8_t *a: byte array with bit-packed polynomial **************************************************/ -static MLD_INLINE int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a); +static MLD_INLINE int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a) +__contract__( + requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(r, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(r, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYZ_UNPACK_17 */ #if defined(MLD_USE_NATIVE_POLYZ_UNPACK_19) @@ -437,7 +445,15 @@ static MLD_INLINE int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a); * Arguments: - int32_t *r: pointer to output polynomial * - const uint8_t *a: byte array with bit-packed polynomial **************************************************/ -static MLD_INLINE int mld_polyz_unpack_19_native(int32_t *r, const uint8_t *a); +static MLD_INLINE int mld_polyz_unpack_19_native(int32_t *r, const uint8_t *a) +__contract__( + requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES)) + assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(r, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(r, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYZ_UNPACK_19 */ #if defined(MLD_USE_NATIVE_POINTWISE_MONTGOMERY) diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index 03094df80..1e1a5bf38 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -861,7 +861,6 @@ MLD_INTERNAL_API void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) { #if defined(MLD_USE_NATIVE_POLYZ_UNPACK_17) && MLD_CONFIG_PARAMETER_SET == 44 - /* TODO: proof */ int ret; ret = mld_polyz_unpack_17_native(r->coeffs, a); if (ret == MLD_NATIVE_FUNC_SUCCESS) @@ -871,7 +870,6 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES]) } #elif defined(MLD_USE_NATIVE_POLYZ_UNPACK_19) && \ (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87) - /* TODO: proof */ int ret; ret = mld_polyz_unpack_19_native(r->coeffs, a); if (ret == MLD_NATIVE_FUNC_SUCCESS) diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 5beb8181d..ace5e525d 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -18,6 +18,8 @@ #define MLD_USE_NATIVE_POLY_USE_HINT_32 #define MLD_USE_NATIVE_POLY_USE_HINT_88 #define MLD_USE_NATIVE_POLY_CHKNORM +#define MLD_USE_NATIVE_POLYZ_UNPACK_17 +#define MLD_USE_NATIVE_POLYZ_UNPACK_19 #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/polyz_unpack_native/Makefile b/proofs/cbmc/polyz_unpack_native/Makefile new file mode 100644 index 000000000..af621ba54 --- /dev/null +++ b/proofs/cbmc/polyz_unpack_native/Makefile @@ -0,0 +1,62 @@ +# 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 = polyz_unpack_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 = polyz_unpack_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_unpack +USE_FUNCTION_CONTRACTS=mld_polyz_unpack_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_polyz_unpack_17_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_polyz_unpack_19_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_polyz_unpack_19_native +endif +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 = polyz_unpack_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 + +# 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 diff --git a/proofs/cbmc/polyz_unpack_native/polyz_unpack_native_harness.c b/proofs/cbmc/polyz_unpack_native/polyz_unpack_native_harness.c new file mode 100644 index 000000000..0dd46b69b --- /dev/null +++ b/proofs/cbmc/polyz_unpack_native/polyz_unpack_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly_kl.h" + +void harness(void) +{ + mld_poly *a; + uint8_t *b; + mld_polyz_unpack(a, b); +} From 923c773426458ee0e1f622f2aa630034ee0b97e7 Mon Sep 17 00:00:00 2001 From: willieyz Date: Mon, 1 Dec 2025 18:56:19 +0800 Subject: [PATCH 10/13] CBMC: Add proofs on top of native functions (mld_poly_pointwise_montgomery_native) - This commit adds CBMC proofs for the native function `mld_poly_pointwise_montgomery_native`, called `poly_pointwise_montgomery_native` - This following changes are include: - Apply the same harness file and construct function contract, reference from `poly_pointwise_montgomery`. - Use the following function contracts: - `mld_poly_pointwise_montgomery_native` - `mld_poly_pointwise_montgomery_c` - Add `MLD_USE_NATIVE_POINTWISE_MONTGOMERY` in dummy_backend.h Signed-off-by: willieyz --- mldsa/src/native/api.h | 15 ++++- mldsa/src/poly.c | 1 - proofs/cbmc/dummy_backend.h | 1 + .../poly_pointwise_montgomery_native/Makefile | 55 +++++++++++++++++++ ...poly_pointwise_montgomery_native_harness.c | 10 ++++ 5 files changed, 80 insertions(+), 2 deletions(-) create mode 100644 proofs/cbmc/poly_pointwise_montgomery_native/Makefile create mode 100644 proofs/cbmc/poly_pointwise_montgomery_native/poly_pointwise_montgomery_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 3439bd828..509f6f03e 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -471,7 +471,20 @@ __contract__( * - const int32_t b[MLDSA_N]: second input polynomial **************************************************/ static MLD_INLINE int mld_poly_pointwise_montgomery_native( - int32_t c[MLDSA_N], const int32_t a[MLDSA_N], const int32_t b[MLDSA_N]); + int32_t c[MLDSA_N], const int32_t a[MLDSA_N], const int32_t b[MLDSA_N]) +__contract__( + requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N)) + requires(array_abs_bound(a, 0, MLDSA_N, MLD_NTT_BOUND)) + requires(array_abs_bound(b, 0, MLDSA_N, MLD_NTT_BOUND)) + assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(c, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(a, 0, MLDSA_N, MLD_NTT_BOUND)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_abs_bound(b, 0, MLDSA_N, MLD_NTT_BOUND)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(c, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POINTWISE_MONTGOMERY */ #if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c index 757df9e6c..04e402060 100644 --- a/mldsa/src/poly.c +++ b/mldsa/src/poly.c @@ -244,7 +244,6 @@ void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a, const mld_poly *b) { #if defined(MLD_USE_NATIVE_POINTWISE_MONTGOMERY) - /* TODO: proof */ int ret; mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND); mld_assert_abs_bound(b->coeffs, MLDSA_N, MLD_NTT_BOUND); diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index ace5e525d..3af7f0b1f 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -20,6 +20,7 @@ #define MLD_USE_NATIVE_POLY_CHKNORM #define MLD_USE_NATIVE_POLYZ_UNPACK_17 #define MLD_USE_NATIVE_POLYZ_UNPACK_19 +#define MLD_USE_NATIVE_POINTWISE_MONTGOMERY #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/poly_pointwise_montgomery_native/Makefile b/proofs/cbmc/poly_pointwise_montgomery_native/Makefile new file mode 100644 index 000000000..9e82db17c --- /dev/null +++ b/proofs/cbmc/poly_pointwise_montgomery_native/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 = poly_pointwise_montgomery_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 = poly_pointwise_montgomery_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery +USE_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery_native mld_poly_pointwise_montgomery_c +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 = poly_pointwise_montgomery_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 + +# This function is large enough to need... +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/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 diff --git a/proofs/cbmc/poly_pointwise_montgomery_native/poly_pointwise_montgomery_native_harness.c b/proofs/cbmc/poly_pointwise_montgomery_native/poly_pointwise_montgomery_native_harness.c new file mode 100644 index 000000000..d885c2d5d --- /dev/null +++ b/proofs/cbmc/poly_pointwise_montgomery_native/poly_pointwise_montgomery_native_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "poly.h" + +void harness(void) +{ + mld_poly *a, *b, *c; + mld_poly_pointwise_montgomery(c, a, b); +} From c8821e5be19dd5223792a1ac74799d774a57bdeb Mon Sep 17 00:00:00 2001 From: willieyz Date: Thu, 4 Dec 2025 12:54:29 +0800 Subject: [PATCH 11/13] CBMC: Add proofs on top of native functions(polyvecl_pointwise_acc_montgomery_native) - This commit adds CBMC proofs for following the native function: `mld_polyvecl_pointwise_acc_montgomery_l4_native`, `mld_polyvecl_pointwise_acc_montgomery_l5_native` and `mld_polyvecl_pointwise_acc_montgomery_l7_native` called `polyvecl_pointwise_acc_montgomery_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from `polyvecl_pointwise_acc_montgomery`. - Use the following function contracts: - `mld_polyvecl_pointwise_acc_montgomery_l4_native` - `mld_polyvecl_pointwise_acc_montgomery_l5_native` - `mld_polyvecl_pointwise_acc_montgomery_l7_native` - Add `MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4`, `MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5`, `MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7` in dummy_backend.h Signed-off-by: willieyz --- mldsa/src/native/api.h | 45 ++++++++++++- mldsa/src/polyvec.c | 3 - proofs/cbmc/dummy_backend.h | 3 + .../Makefile | 64 +++++++++++++++++++ ..._pointwise_acc_montgomery_native_harness.c | 11 ++++ 5 files changed, 120 insertions(+), 6 deletions(-) create mode 100644 proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/Makefile create mode 100644 proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/polyvecl_pointwise_acc_montgomery_native_harness.c diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 509f6f03e..c52d345d9 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -504,7 +504,20 @@ __contract__( **************************************************/ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native( int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N], - const int32_t v[4][MLDSA_N]); + const int32_t v[4][MLDSA_N]) +__contract__( + requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(u, sizeof(int32_t) * 4 * MLDSA_N)) + requires(memory_no_alias(v, sizeof(int32_t) * 4 * MLDSA_N)) + requires(forall(l0, 0, 4, + array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) + requires(forall(l1, 0, 4, + array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 */ #if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5) @@ -524,7 +537,20 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native( **************************************************/ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native( int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N], - const int32_t v[5][MLDSA_N]); + const int32_t v[5][MLDSA_N]) +__contract__( + requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(u, sizeof(int32_t) * 5 * MLDSA_N)) + requires(memory_no_alias(v, sizeof(int32_t) * 5 * MLDSA_N)) + requires(forall(l0, 0, 5, + array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) + requires(forall(l1, 0, 5, + array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5 */ #if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7) @@ -544,7 +570,20 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native( **************************************************/ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native( int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N], - const int32_t v[7][MLDSA_N]); + const int32_t v[7][MLDSA_N]) +__contract__( + requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N)) + requires(memory_no_alias(u, sizeof(int32_t) * 7 * MLDSA_N)) + requires(memory_no_alias(v, sizeof(int32_t) * 7 * MLDSA_N)) + requires(forall(l0, 0, 7, + array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q))) + requires(forall(l1, 0, 7, + array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q)) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N)) +); #endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 */ #endif /* !MLD_NATIVE_API_H */ diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index 975b35b3e..13f052337 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -375,7 +375,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, { #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); @@ -389,7 +388,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, } #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); @@ -403,7 +401,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, } #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); diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h index 3af7f0b1f..92a11b566 100644 --- a/proofs/cbmc/dummy_backend.h +++ b/proofs/cbmc/dummy_backend.h @@ -21,6 +21,9 @@ #define MLD_USE_NATIVE_POLYZ_UNPACK_17 #define MLD_USE_NATIVE_POLYZ_UNPACK_19 #define MLD_USE_NATIVE_POINTWISE_MONTGOMERY +#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 #include "../../mldsa/src/native/api.h" diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/Makefile new file mode 100644 index 000000000..5b507f981 --- /dev/null +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/Makefile @@ -0,0 +1,64 @@ +# 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_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 = polyvecl_pointwise_acc_montgomery_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +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_polyvecl_pointwise_acc_montgomery_c +ifeq ($(MLD_CONFIG_PARAMETER_SET),44) + USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l4_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),65) + USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l5_native +else ifeq ($(MLD_CONFIG_PARAMETER_SET),87) + USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l7_native +endif +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_smt_only --z3 +CBMCFLAGS += --slice-formula +CBMCFLAGS += --no-array-field-sensitivity + +FUNCTION_NAME = polyvecl_pointwise_acc_montgomery_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 + +# 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 diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/polyvecl_pointwise_acc_montgomery_native_harness.c b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/polyvecl_pointwise_acc_montgomery_native_harness.c new file mode 100644 index 000000000..927d5a220 --- /dev/null +++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/polyvecl_pointwise_acc_montgomery_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "polyvec.h" + +void harness(void) +{ + mld_poly *a; + mld_polyvecl *b, *c; + mld_polyvecl_pointwise_acc_montgomery(a, b, c); +} From a519069e1a3ce3b7c584bbf9e959edc428fb3be8 Mon Sep 17 00:00:00 2001 From: willieyz Date: Thu, 4 Dec 2025 14:26:01 +0800 Subject: [PATCH 12/13] CBMC: Add proofs on top of native functions (keccakf1600_permute_native) - This commit adds CBMC proofs for following the native function: `mld_keccak_f1600_x1_native`, called `keccakf1600_permute_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from `keccakf1600_permute`. - Use the following function contracts: - `mld_keccak_f1600_x1_native` - Add `MLD_USE_FIPS202_X1_NATIVE` in dummy_backend_fips202_x1.h Signed-off-by: willieyz --- mldsa/src/fips202/native/api.h | 10 +++- proofs/cbmc/dummy_backend_fips202_x1.h | 14 +++++ .../cbmc/keccakf1600_permute_native/Makefile | 55 +++++++++++++++++++ .../keccakf1600_permute_native_harness.c | 10 ++++ 4 files changed, 87 insertions(+), 2 deletions(-) create mode 100644 proofs/cbmc/dummy_backend_fips202_x1.h create mode 100644 proofs/cbmc/keccakf1600_permute_native/Makefile create mode 100644 proofs/cbmc/keccakf1600_permute_native/keccakf1600_permute_native_harness.c diff --git a/mldsa/src/fips202/native/api.h b/mldsa/src/fips202/native/api.h index c527b6a26..4e5ba3376 100644 --- a/mldsa/src/fips202/native/api.h +++ b/mldsa/src/fips202/native/api.h @@ -46,8 +46,14 @@ */ #if defined(MLD_USE_FIPS202_X1_NATIVE) -static MLD_INLINE int mld_keccak_f1600_x1_native(uint64_t *state); -#endif +static MLD_INLINE int mld_keccak_f1600_x1_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 1)) +); +#endif /* MLD_USE_FIPS202_X1_NATIVE */ #if defined(MLD_USE_FIPS202_X4_NATIVE) static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state); #endif diff --git a/proofs/cbmc/dummy_backend_fips202_x1.h b/proofs/cbmc/dummy_backend_fips202_x1.h new file mode 100644 index 000000000..fb71bdc31 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x1.h @@ -0,0 +1,14 @@ +/* + * Copyright (c) The mldsa-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ + +#ifndef MLD_DUMMY_FIPS202X1_BACKEND_H +#define MLD_DUMMY_FIPS202X1_BACKEND_H + + +#define MLD_USE_FIPS202_X1_NATIVE + +#include "../../mldsa/src/fips202/native/api.h" + +#endif /* !MLD_DUMMY_FIPS202X1_BACKEND_H */ diff --git a/proofs/cbmc/keccakf1600_permute_native/Makefile b/proofs/cbmc/keccakf1600_permute_native/Makefile new file mode 100644 index 000000000..ce5f5a76e --- /dev/null +++ b/proofs/cbmc/keccakf1600_permute_native/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 = keccakf1600_permute_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 = keccakf1600_permute_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLD_CONFIG_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x1.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)keccakf1600_permute +USE_FUNCTION_CONTRACTS=mld_keccak_f1600_x1_native +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 = mld_keccakf1600_permute_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 + +# 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 diff --git a/proofs/cbmc/keccakf1600_permute_native/keccakf1600_permute_native_harness.c b/proofs/cbmc/keccakf1600_permute_native/keccakf1600_permute_native_harness.c new file mode 100644 index 000000000..5647efb41 --- /dev/null +++ b/proofs/cbmc/keccakf1600_permute_native/keccakf1600_permute_native_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include + +void harness(void) +{ + uint64_t *a; + mld_keccakf1600_permute(a); +} From 6c5e234709b472678793f2b274d955ec93295500 Mon Sep 17 00:00:00 2001 From: willieyz Date: Thu, 4 Dec 2025 14:34:01 +0800 Subject: [PATCH 13/13] CBMC: Add proofs on top of native functions (keccakf1600x4_permute_native) - This commit adds CBMC proofs for following the native function: `mld_keccak_f1600_x4_native`, called `keccakf1600x4_permute_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from `keccakf1600x4_permute`. - Use the following function contracts: - `mld_keccak_f1600_x4_native` - Add `MLD_USE_FIPS202_X4_NATIVE` in dummy_backend_fips202_x4.h Signed-off-by: willieyz --- mldsa/src/fips202/native/api.h | 10 ++- proofs/cbmc/dummy_backend_fips202_x4.h | 14 ++++ .../keccakf1600x4_permute_native/Makefile | 67 +++++++++++++++++++ .../keccakf1600x4_permute_native_harness.c | 12 ++++ 4 files changed, 101 insertions(+), 2 deletions(-) create mode 100644 proofs/cbmc/dummy_backend_fips202_x4.h create mode 100644 proofs/cbmc/keccakf1600x4_permute_native/Makefile create mode 100644 proofs/cbmc/keccakf1600x4_permute_native/keccakf1600x4_permute_native_harness.c diff --git a/mldsa/src/fips202/native/api.h b/mldsa/src/fips202/native/api.h index 4e5ba3376..4625c9a1a 100644 --- a/mldsa/src/fips202/native/api.h +++ b/mldsa/src/fips202/native/api.h @@ -55,7 +55,13 @@ __contract__( ); #endif /* MLD_USE_FIPS202_X1_NATIVE */ #if defined(MLD_USE_FIPS202_X4_NATIVE) -static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state); -#endif +static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4)) + ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS) + ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 4)) +); +#endif /* MLD_USE_FIPS202_X4_NATIVE */ #endif /* !MLD_FIPS202_NATIVE_API_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x4.h b/proofs/cbmc/dummy_backend_fips202_x4.h new file mode 100644 index 000000000..d84df09c5 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x4.h @@ -0,0 +1,14 @@ +/* + * Copyright (c) The mldsa-native project authors + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + */ + +#ifndef MLD_DUMMY_FIPS202X4_BACKEND_H +#define MLD_DUMMY_FIPS202X4_BACKEND_H + + +#define MLD_USE_FIPS202_X4_NATIVE + +#include "../../mldsa/src/fips202/native/api.h" + +#endif /* !MLD_DUMMY_FIPS202X4_BACKEND_H */ diff --git a/proofs/cbmc/keccakf1600x4_permute_native/Makefile b/proofs/cbmc/keccakf1600x4_permute_native/Makefile new file mode 100644 index 000000000..a0900c114 --- /dev/null +++ b/proofs/cbmc/keccakf1600x4_permute_native/Makefile @@ -0,0 +1,67 @@ +# Copyright (c) The mldsa-native project authors +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = keccakf1600x4_permute_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 = keccakf1600x4_permute_native + +DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLD_CONFIG_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x4.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)keccakf1600x4_permute +USE_FUNCTION_CONTRACTS=mld_keccak_f1600_x4_native +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 + +# For this proof we tell CBMC to +# - not decompose arrays into their individual cells +# - to slice constraints that are not in the cone of influence of the proof obligations +# These options simplify them modelling of arrays and produce much more compact +# SMT files, leaving all array-type reasoning to the SMT solver. +# +# For functions that use large and multi-dimensional arrays, this yields +# a substantial improvement in proof performance. +CBMCFLAGS += --no-array-field-sensitivity +CBMCFLAGS += --slice-formula + +FUNCTION_NAME = mld_keccakf1600x4_permute_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 + +# 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 +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/keccakf1600x4_permute_native/keccakf1600x4_permute_native_harness.c b/proofs/cbmc/keccakf1600x4_permute_native/keccakf1600x4_permute_native_harness.c new file mode 100644 index 000000000..ed72d896b --- /dev/null +++ b/proofs/cbmc/keccakf1600x4_permute_native/keccakf1600x4_permute_native_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) The mldsa-native project authors +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint64_t *s; + mld_keccakf1600x4_permute(s); +}