diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c index 49cd5a1f08..afc224ddad 100644 --- a/mlkem/src/indcpa.c +++ b/mlkem/src/indcpa.c @@ -40,6 +40,7 @@ #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) +#define mlk_enc_getnoise_eta1_eta2 MLK_ADD_PARAM_SET(mlk_enc_getnoise_eta1_eta2) /* End of parameter set namespacing */ /************************************************* @@ -371,6 +372,8 @@ __contract__( * * Description: Computes and fills the pv and e polyvec * structures needed by mlk_keypair_derand(). + * Uses x4-batched versions of `poly_getnoise` to leverage + * batched x4-batched Keccak-f1600. * * Arguments: - pv: Pointer to output polynomial vector * - e: Pointer to output polynomial vector @@ -413,10 +416,63 @@ __contract__( #endif /* MLKEM_K == 4 */ } +/************************************************* + * Name: mlk_enc_getnoise_eta1_eta2 + * + * Description: Computes and fills the sp, ep, and epp polynomial + * structures needed by mlk_indcpa_enc(). + * Uses x4-batched versions of `poly_getnoise` to leverage + * batched x4-batched Keccak-f1600. + * + * Arguments: - sp: Pointer to output polynomial vector + * - ep: Pointer to output polynomial vector + * - epp: Pointer to output polynomial + * - coins: seed bytes for sampling + * + * Specification: Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt)]. + * steps 9 - 16 + **************************************************/ +static void mlk_enc_getnoise_eta1_eta2(mlk_polyvec *sp, mlk_polyvec *ep, + mlk_poly *epp, + const uint8_t coins[MLKEM_SYMBYTES]) +__contract__( + requires(memory_no_alias(sp, sizeof(mlk_polyvec))) + requires(memory_no_alias(ep, sizeof(mlk_polyvec))) + requires(memory_no_alias(epp, sizeof(mlk_poly))) + requires(memory_no_alias(coins, MLKEM_SYMBYTES)) + assigns(memory_slice(sp, sizeof(mlk_polyvec))) + assigns(memory_slice(ep, sizeof(mlk_polyvec))) + assigns(memory_slice(epp, sizeof(mlk_poly))) + ensures(forall(k0, 0, MLKEM_K, array_abs_bound(sp->vec[k0].coeffs, 0, MLKEM_N, MLKEM_ETA1 + 1))) + ensures(forall(k1, 0, MLKEM_K, array_abs_bound(ep->vec[k1].coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1))) + ensures(array_abs_bound(epp->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1)) +) +{ +#if MLKEM_K == 2 + mlk_poly_getnoise_eta1122_4x(&sp->vec[0], &sp->vec[1], &ep->vec[0], + &ep->vec[1], coins, 0, 1, 2, 3); + mlk_poly_getnoise_eta2(epp, coins, 4); +#elif MLKEM_K == 3 + /* + * In this call, only the first three output buffers are needed. + * The last parameter is a dummy that's overwritten later. + */ + mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], NULL, coins, + 0, 1, 2, 0xFF /* irrelevant */); + /* The fourth output buffer in this call _is_ used. */ + mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], epp, coins, + 3, 4, 5, 6); +#elif MLKEM_K == 4 + mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], &sp->vec[3], + coins, 0, 1, 2, 3); + mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], &ep->vec[3], + coins, 4, 5, 6, 7); + mlk_poly_getnoise_eta2(epp, coins, 8); +#endif /* MLKEM_K == 4 */ +} + /* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF]. - * - We use x4-batched versions of `poly_getnoise` to leverage - * batched x4-batched Keccak-f1600. * - We use a different implementation of `gen_matrix()` which * uses x4-batched Keccak-f1600 (see `mlk_gen_matrix()` above). * - We use a mulcache to speed up matrix-vector multiplication. @@ -541,27 +597,7 @@ int mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES], mlk_gen_matrix(at, seed, 1 /* transpose */); -#if MLKEM_K == 2 - mlk_poly_getnoise_eta1122_4x(&sp->vec[0], &sp->vec[1], &ep->vec[0], - &ep->vec[1], coins, 0, 1, 2, 3); - mlk_poly_getnoise_eta2(epp, coins, 4); -#elif MLKEM_K == 3 - /* - * In this call, only the first three output buffers are needed. - * The last parameter is a dummy that's overwritten later. - */ - mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], NULL, coins, - 0, 1, 2, 0xFF /* irrelevant */); - /* The fourth output buffer in this call _is_ used. */ - mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], epp, coins, - 3, 4, 5, 6); -#elif MLKEM_K == 4 - mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], &sp->vec[3], - coins, 0, 1, 2, 3); - mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], &ep->vec[3], - coins, 4, 5, 6, 7); - mlk_poly_getnoise_eta2(epp, coins, 8); -#endif /* MLKEM_K == 4 */ + mlk_enc_getnoise_eta1_eta2(sp, ep, epp, coins); mlk_polyvec_ntt(sp); @@ -655,3 +691,4 @@ int mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES], #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/enc_getnoise_eta1_eta2/Makefile b/proofs/cbmc/enc_getnoise_eta1_eta2/Makefile new file mode 100644 index 0000000000..52a9b9a57e --- /dev/null +++ b/proofs/cbmc/enc_getnoise_eta1_eta2/Makefile @@ -0,0 +1,66 @@ +# 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 = enc_getnoise_eta1_eta2_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_enc_getnoise_eta1_eta2 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_enc_getnoise_eta1_eta2 + +# Note that the called function mlk_poly_getnoise_eta2_4x() is actually +# just #define'd to be mlk_poly_getnoise_eta1_4x() +ifeq ($(MLKEM_K),2) +USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1122_4x +USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2 +else ifeq ($(MLKEM_K),3) +USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1_4x +else # MLKEM_K must be 4 +USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1_4x +USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2 +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 --slice-formula + +FUNCTION_NAME = mlk_enc_getnoise_eta1_eta2 + +# 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 +# ("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/enc_getnoise_eta1_eta2/enc_getnoise_eta1_eta2_harness.c b/proofs/cbmc/enc_getnoise_eta1_eta2/enc_getnoise_eta1_eta2_harness.c new file mode 100644 index 0000000000..836df9f72c --- /dev/null +++ b/proofs/cbmc/enc_getnoise_eta1_eta2/enc_getnoise_eta1_eta2_harness.c @@ -0,0 +1,23 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +#define mlk_enc_getnoise_eta1_eta2 MLK_NAMESPACE(enc_getnoise_eta1_eta2) +void mlk_enc_getnoise_eta1_eta2(mlk_polyvec *sp, mlk_polyvec *ep, mlk_poly *epp, + const uint8_t coins[MLKEM_SYMBYTES]); + +void harness(void) +{ + mlk_polyvec *sp, *ep; + mlk_poly *epp; + uint8_t *coins; + + { + /* Dummy use of `free` to work around CBMC issue #8814. */ + free(NULL); + } + + mlk_enc_getnoise_eta1_eta2(sp, ep, epp, coins); +} diff --git a/proofs/cbmc/indcpa_enc/Makefile b/proofs/cbmc/indcpa_enc/Makefile index f9ace04beb..c1937f2533 100644 --- a/proofs/cbmc/indcpa_enc/Makefile +++ b/proofs/cbmc/indcpa_enc/Makefile @@ -22,15 +22,7 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c CHECK_FUNCTION_CONTRACTS=mlk_indcpa_enc USE_FUNCTION_CONTRACTS = mlk_poly_frommsg USE_FUNCTION_CONTRACTS += mlk_gen_matrix -ifeq ($(MLKEM_K),2) -USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1122_4x -USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2 -else ifeq ($(MLKEM_K),3) -USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1_4x -else ifeq ($(MLKEM_K),4) -USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1_4x -USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2 -endif +USE_FUNCTION_CONTRACTS += mlk_enc_getnoise_eta1_eta2 USE_FUNCTION_CONTRACTS += mlk_polyvec_ntt USE_FUNCTION_CONTRACTS += mlk_polyvec_mulcache_compute