diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index afc224dda..b7b746f7d 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -35,8 +35,6 @@ #define mlk_pack_ciphertext MLK_ADD_PARAM_SET(mlk_pack_ciphertext) #define mlk_unpack_ciphertext MLK_ADD_PARAM_SET(mlk_unpack_ciphertext) #define mlk_matvec_mul MLK_ADD_PARAM_SET(mlk_matvec_mul) -#define mlk_polyvec_permute_bitrev_to_custom \ - MLK_ADD_PARAM_SET(mlk_polyvec_permute_bitrev_to_custom) #define mlk_polymat_permute_bitrev_to_custom \ MLK_ADD_PARAM_SET(mlk_polymat_permute_bitrev_to_custom) #define mlk_keypair_getnoise_eta1 MLK_ADD_PARAM_SET(mlk_keypair_getnoise_eta1) @@ -179,41 +177,6 @@ static void mlk_unpack_ciphertext(mlk_polyvec *b, mlk_poly *v, mlk_poly_decompress_dv(v, c + MLKEM_POLYVECCOMPRESSEDBYTES_DU); } -/* Helper function to ensure that the polynomial entries in the output - * of gen_matrix use the standard (bitreversed) ordering of coefficients. - * No-op unless a native backend with a custom ordering is used. - * - * We don't inline this into gen_matrix to avoid having to split the CBMC - * proof for gen_matrix based on MLK_USE_NATIVE_NTT_CUSTOM_ORDER. */ -static void mlk_polyvec_permute_bitrev_to_custom(mlk_polyvec *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 mlk_gen_matrix. */ - requires(memory_no_alias(v, sizeof(mlk_polyvec))) - requires(forall(x, 0, MLKEM_K, - array_bound(v->vec[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) - assigns(memory_slice(v, sizeof(mlk_polyvec))) - ensures(forall(x, 0, MLKEM_K, - array_bound(v->vec[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) -{ -#if defined(MLK_USE_NATIVE_NTT_CUSTOM_ORDER) - unsigned i; - for (i = 0; i < MLKEM_K; i++) - __loop__( - assigns(i, memory_slice(v, sizeof(mlk_polyvec))) - invariant(i <= MLKEM_K) - invariant(forall(x, 0, MLKEM_K, - array_bound(v->vec[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q))) - decreases(MLKEM_K - i)) - { - mlk_poly_permute_bitrev_to_custom(v->vec[i].coeffs); - } -#else /* MLK_USE_NATIVE_NTT_CUSTOM_ORDER */ - /* Nothing to do */ - (void)v; -#endif /* !MLK_USE_NATIVE_NTT_CUSTOM_ORDER */ -} - static void mlk_polymat_permute_bitrev_to_custom(mlk_polymat *a) __contract__( /* We don't specify that this should be a permutation, but only @@ -225,17 +188,32 @@ __contract__( ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K, array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))) { - unsigned i; +#if defined(MLK_USE_NATIVE_NTT_CUSTOM_ORDER) + unsigned i, j; for (i = 0; i < MLKEM_K; i++) __loop__( - assigns(i, memory_slice(a, sizeof(mlk_polymat))) - invariant(i <= MLKEM_K) - invariant(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K, - array_bound(a->vec[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) - decreases(MLKEM_K - i)) + assigns(i, j, memory_slice(a, sizeof(mlk_polymat))) + invariant(i <= MLKEM_K) + invariant(forall(x2, 0, MLKEM_K, forall(y2, 0, MLKEM_K, + array_bound(a->vec[x2].vec[y2].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) + decreases(MLKEM_K - i)) { - mlk_polyvec_permute_bitrev_to_custom(&a->vec[i]); + for (j = 0; j < MLKEM_K; j++) + __loop__( + assigns(j, memory_slice(a, sizeof(mlk_polymat))) + invariant(i <= MLKEM_K) + invariant(j <= MLKEM_K) + invariant(forall(x3, 0, MLKEM_K, forall(y3, 0, MLKEM_K, + array_bound(a->vec[x3].vec[y3].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))) + decreases(MLKEM_K - j)) + { + mlk_poly_permute_bitrev_to_custom(a->vec[i].vec[j].coeffs); + } } +#else /* MLK_USE_NATIVE_NTT_CUSTOM_ORDER */ + /* Nothing to do */ + (void)a; +#endif /* !MLK_USE_NATIVE_NTT_CUSTOM_ORDER */ } /* Reference: `gen_matrix()` in the reference implementation @[REF]. @@ -688,7 +666,6 @@ int mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], #undef mlk_pack_ciphertext #undef mlk_unpack_ciphertext #undef mlk_matvec_mul -#undef mlk_polyvec_permute_bitrev_to_custom #undef mlk_polymat_permute_bitrev_to_custom #undef mlk_keypair_getnoise_eta1 #undef mlk_enc_getnoise_eta1_eta2 diff --git a/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile b/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile index 81276abcf..bf570eaa3 100644 --- a/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c CHECK_FUNCTION_CONTRACTS=mlk_polymat_permute_bitrev_to_custom -USE_FUNCTION_CONTRACTS=mlk_polyvec_permute_bitrev_to_custom +USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/polyvec_permute_bitrev_to_custom_native/Makefile b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/Makefile similarity index 87% rename from proofs/cbmc/polyvec_permute_bitrev_to_custom_native/Makefile rename to proofs/cbmc/polymat_permute_bitrev_to_custom_native/Makefile index 747bf0a97..f92687421 100644 --- a/proofs/cbmc/polyvec_permute_bitrev_to_custom_native/Makefile +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/Makefile @@ -4,11 +4,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = polyvec_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 = mlk_polyvec_permute_bitrev_to_custom_native +PROOF_UID = mlk_polymat_permute_bitrev_to_custom_native DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\"" INCLUDES += @@ -19,7 +19,7 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c -CHECK_FUNCTION_CONTRACTS=mlk_polyvec_permute_bitrev_to_custom +CHECK_FUNCTION_CONTRACTS=mlk_polymat_permute_bitrev_to_custom USE_FUNCTION_CONTRACTS=mlk_poly_permute_bitrev_to_custom APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,14 +28,14 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = mlk_polyvec_permute_bitrev_to_custom_native +FUNCTION_NAME = mlk_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 +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/polyvec_permute_bitrev_to_custom/polyvec_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 71% rename from proofs/cbmc/polyvec_permute_bitrev_to_custom/polyvec_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 e824f72e1..d79177c7c 100644 --- a/proofs/cbmc/polyvec_permute_bitrev_to_custom/polyvec_permute_bitrev_to_custom_harness.c +++ b/proofs/cbmc/polymat_permute_bitrev_to_custom_native/polymat_permute_bitrev_to_custom_native_harness.c @@ -5,7 +5,7 @@ #include #include "poly_k.h" -void mlk_polyvec_permute_bitrev_to_custom(mlk_polyvec *v); +void mlk_polymat_permute_bitrev_to_custom(mlk_polymat *a); void harness(void) { @@ -14,6 +14,6 @@ void harness(void) free(NULL); } - mlk_polyvec *v; - mlk_polyvec_permute_bitrev_to_custom(v); + mlk_polymat *a; + mlk_polymat_permute_bitrev_to_custom(a); } diff --git a/proofs/cbmc/polyvec_permute_bitrev_to_custom/Makefile b/proofs/cbmc/polyvec_permute_bitrev_to_custom/Makefile deleted file mode 100644 index 023b4db8f..000000000 --- a/proofs/cbmc/polyvec_permute_bitrev_to_custom/Makefile +++ /dev/null @@ -1,53 +0,0 @@ -# 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 = polyvec_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 = mlk_polyvec_permute_bitrev_to_custom - -DEFINES += -INCLUDES += -UNWINDSET += - -REMOVE_FUNCTION_BODY += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c - -CHECK_FUNCTION_CONTRACTS=mlk_polyvec_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 - -FUNCTION_NAME = mlk_polyvec_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 -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 -# ("mlkem/src/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/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/polyvec_permute_bitrev_to_custom_native/polyvec_permute_bitrev_to_custom_native_harness.c b/proofs/cbmc/polyvec_permute_bitrev_to_custom_native/polyvec_permute_bitrev_to_custom_native_harness.c deleted file mode 100644 index e824f72e1..000000000 --- a/proofs/cbmc/polyvec_permute_bitrev_to_custom_native/polyvec_permute_bitrev_to_custom_native_harness.c +++ /dev/null @@ -1,19 +0,0 @@ -// Copyright (c) The mlkem-native project authors -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: MIT-0 - -#include -#include "poly_k.h" - -void mlk_polyvec_permute_bitrev_to_custom(mlk_polyvec *v); - -void harness(void) -{ - { - /* Dummy use of `free` to work around CBMC issue #8814. */ - free(NULL); - } - - mlk_polyvec *v; - mlk_polyvec_permute_bitrev_to_custom(v); -}