diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h index 0f1fdeb16..4ffde019c 100644 --- a/mldsa/src/native/api.h +++ b/mldsa/src/native/api.h @@ -131,7 +131,8 @@ __contract__( requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N)) requires(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q)) assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N)) - ensures(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q))); + ensures(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q)) +); #endif /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index f6cc08386..5d8b939cb 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -25,8 +25,6 @@ * with native backends, which are currently not yet namespaced. */ #define mld_polymat_permute_bitrev_to_custom \ MLD_ADD_PARAM_SET(mld_polymat_permute_bitrev_to_custom) -#define mld_polyvecl_permute_bitrev_to_custom \ - MLD_ADD_PARAM_SET(mld_polyvecl_permute_bitrev_to_custom) #define mld_polyvecl_pointwise_acc_montgomery_c \ MLD_ADD_PARAM_SET(mld_polyvecl_pointwise_acc_montgomery_c) @@ -37,36 +35,6 @@ * No-op unless a native backend with a custom ordering is used. */ -static void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v) -__contract__( - /* We don't specify that this should be a permutation, but only - * that it does not change the bound established at the end of - * mld_polyvec_matrix_expand. - */ - requires(memory_no_alias(v, sizeof(mld_polyvecl))) - requires(forall(x, 0, MLDSA_L, - array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q))) - assigns(memory_slice(v, sizeof(mld_polyvecl))) - ensures(forall(x, 0, MLDSA_L, - array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) -{ -#if defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER) - unsigned i; - for (i = 0; i < MLDSA_L; i++) - __loop__( - assigns(i, memory_slice(v, sizeof(mld_polyvecl))) - invariant(i <= MLDSA_L) - invariant(forall(x, 0, MLDSA_L, - array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) - { - mld_poly_permute_bitrev_to_custom(v->vec[i].coeffs); - } -#else /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ - /* Nothing to do */ - (void)v; -#endif /* !MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ -} - static void mld_polymat_permute_bitrev_to_custom(mld_polymat *mat) __contract__( /* We don't specify that this should be a permutation, but only @@ -81,16 +49,36 @@ __contract__( array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) ) { - unsigned int i; +#if defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER) + + unsigned int i, j; for (i = 0; i < MLDSA_K; i++) __loop__( - assigns(i, memory_slice(mat, sizeof(mld_polymat))) + assigns(i, j, memory_slice(mat, sizeof(mld_polymat))) invariant(i <= MLDSA_K) invariant(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, - array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))) + array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) + ) { - mld_polyvecl_permute_bitrev_to_custom(&mat->vec[i]); + for (j = 0; j < MLDSA_L; j++) + __loop__( + assigns(j, memory_slice(mat, sizeof(mld_polymat))) + invariant(i <= MLDSA_K) + invariant(j <= MLDSA_L) + invariant(forall(k2, 0, MLDSA_K, forall(l2, 0, MLDSA_L, + array_bound(mat->vec[k2].vec[l2].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) + ) + { + mld_poly_permute_bitrev_to_custom(mat->vec[i].vec[j].coeffs); + } } + +#else /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ + + /* Nothing to do */ + ((void)mat); + +#endif /* !MLD_USE_NATIVE_NTT_CUSTOM_ORDER */ } #endif /* !MLD_CONFIG_REDUCE_RAM */ @@ -951,5 +939,4 @@ void mld_polyveck_unpack_t0(mld_polyveck *p, /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ #undef mld_polymat_permute_bitrev_to_custom -#undef mld_polyvecl_permute_bitrev_to_custom #undef mld_polyvecl_pointwise_acc_montgomery_c diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix index be333f2e1..fcc051d53 100644 --- a/nix/cbmc/default.nix +++ b/nix/cbmc/default.nix @@ -21,10 +21,10 @@ buildEnv { cbmc = cbmc.overrideAttrs (old: rec { version = "6.8.0"; src = fetchFromGitHub { - owner = "diffblue"; + owner = "tautschnig"; repo = "cbmc"; - hash = "sha256-PT6AYiwkplCeyMREZnGZA0BKl4ZESRC02/9ibKg7mYU="; - tag = "cbmc-6.8.0"; + hash = "sha256-ng1zjICpmoHUWkG1PuLRmLtaUBmEALpRgNEpbsrnMV8="; + rev = "4f514dbd70c89e3bae03a59f1dc9837acf25885c"; }; }); litani = callPackage ./litani.nix { }; # 1.29.0 diff --git a/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile b/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile index 690eef038..59a2fb467 100644 --- a/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c CHECK_FUNCTION_CONTRACTS=mld_polymat_permute_bitrev_to_custom -USE_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom +USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/Makefile b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/Makefile similarity index 83% rename from proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/Makefile rename to proofs/cbmc/polymat_permute_bitrev_to_custom_native/Makefile index 893a26dec..5e902d274 100644 --- a/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/Makefile +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/Makefile @@ -1,27 +1,26 @@ -# Copyright (c) The mlkem-native project authors # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = polyvecl_permute_bitrev_to_custom_native_harness +HARNESS_FILE = polymat_permute_bitrev_to_custom_native_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = mld_polyvecl_permute_bitrev_to_custom_native +PROOF_UID = polymat_permute_bitrev_to_custom_native DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" INCLUDES += -UNWINDSET += REMOVE_FUNCTION_BODY += +UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c -CHECK_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom -USE_FUNCTION_CONTRACTS= mld_poly_permute_bitrev_to_custom +CHECK_FUNCTION_CONTRACTS=mld_polymat_permute_bitrev_to_custom +USE_FUNCTION_CONTRACTS=mld_poly_permute_bitrev_to_custom APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,14 +28,16 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 --slice-formula --no-array-field-sensitivity -FUNCTION_NAME = mld_polyvecl_permute_bitrev_to_custom_native +FUNCTION_NAME = polymat_permute_bitrev_to_custom_native # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will # restrict the number of EXPENSIVE CBMC jobs running at once. See the # documentation in Makefile.common under the "Job Pools" heading for details. # EXPENSIVE = true -CBMC_OBJECT_BITS = 10 + +# 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 diff --git a/proofs/cbmc/polyvecl_permute_bitrev_to_custom/polyvecl_permute_bitrev_to_custom_harness.c b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/polymat_permute_bitrev_to_custom_native_harness.c similarity index 54% rename from proofs/cbmc/polyvecl_permute_bitrev_to_custom/polyvecl_permute_bitrev_to_custom_harness.c rename to proofs/cbmc/polymat_permute_bitrev_to_custom_native/polymat_permute_bitrev_to_custom_native_harness.c index 83d58ff7c..a35bc954e 100644 --- a/proofs/cbmc/polyvecl_permute_bitrev_to_custom/polyvecl_permute_bitrev_to_custom_harness.c +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/polymat_permute_bitrev_to_custom_native_harness.c @@ -3,10 +3,10 @@ #include "polyvec.h" -void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v); +void mld_polymat_permute_bitrev_to_custom(mld_polymat *mat); void harness(void) { - mld_polyvecl *v; - mld_polyvecl_permute_bitrev_to_custom(v); + mld_polymat *mat; + mld_polymat_permute_bitrev_to_custom(mat); } diff --git a/proofs/cbmc/polyvecl_permute_bitrev_to_custom/Makefile b/proofs/cbmc/polyvecl_permute_bitrev_to_custom/Makefile deleted file mode 100644 index 370d3571e..000000000 --- a/proofs/cbmc/polyvecl_permute_bitrev_to_custom/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = polyvecl_permute_bitrev_to_custom_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = polyvecl_permute_bitrev_to_custom - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c - -CHECK_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom -USE_FUNCTION_CONTRACTS= -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 --slice-formula --no-array-field-sensitivity - -FUNCTION_NAME = polyvecl_permute_bitrev_to_custom - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 12 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/polyvecl_permute_bitrev_to_custom_native_harness.c b/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/polyvecl_permute_bitrev_to_custom_native_harness.c deleted file mode 100644 index 83d58ff7c..000000000 --- a/proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/polyvecl_permute_bitrev_to_custom_native_harness.c +++ /dev/null @@ -1,12 +0,0 @@ -// Copyright (c) The mldsa-native project authors -// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -#include "polyvec.h" - -void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v); - -void harness(void) -{ - mld_polyvecl *v; - mld_polyvecl_permute_bitrev_to_custom(v); -}