From a94dd2055eae01154589dab92144e701dd8b9ec5 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 29 Apr 2026 14:15:21 +0800 Subject: [PATCH] Lowram: Share buffers with non-overlapping lifetimes in verify In mld_sign_verify_internal, introduce two unions to share buffers with non-overlapping lifetimes: - zcp_u: shares z (matrix-vector input) with cp (challenge polynomial), since z is dead after the matrix-vector multiplication. - reuse_u: shares mat, t1 and h. mat dies after matrix-vector mult, t1 (re-unpacked into the same slot) dies after polyveck_sub, and h (unpacked late) lives only from then through pack_w1. Replace mld_unpack_sig with explicit memcpy of c, mld_polyvecl_unpack_z and a deferred mld_unpack_hints, so the hint vector is unpacked only after the matrix-vector / t1 buffers are no longer needed. CBMC proofs are adjusted. Signed-off-by: Matthias J. Kannwischer --- integration/opentitan/reduce_alloc.patch | 6 +- mldsa/mldsa_native.c | 4 +- mldsa/mldsa_native.h | 18 ++-- mldsa/mldsa_native_asm.S | 4 +- mldsa/src/packing.c | 49 ++--------- mldsa/src/packing.h | 41 ++++----- mldsa/src/sign.c | 88 +++++++++++-------- .../Makefile | 8 +- .../sig_unpack_hints_harness.c} | 5 +- proofs/cbmc/sign_verify_internal/Makefile | 7 +- .../cbmc/unpack_hints/unpack_hints_harness.c | 15 ---- .../cbmc/{unpack_pk => unpack_pk_t1}/Makefile | 10 +-- .../unpack_pk_t1_harness.c} | 6 +- proofs/cbmc/unpack_sig/Makefile | 55 ------------ 14 files changed, 107 insertions(+), 209 deletions(-) rename proofs/cbmc/{unpack_hints => sig_unpack_hints}/Makefile (92%) rename proofs/cbmc/{unpack_sig/unpack_sig_harness.c => sig_unpack_hints/sig_unpack_hints_harness.c} (73%) delete mode 100644 proofs/cbmc/unpack_hints/unpack_hints_harness.c rename proofs/cbmc/{unpack_pk => unpack_pk_t1}/Makefile (90%) rename proofs/cbmc/{unpack_pk/unpack_pk_harness.c => unpack_pk_t1/unpack_pk_t1_harness.c} (70%) delete mode 100644 proofs/cbmc/unpack_sig/Makefile diff --git a/integration/opentitan/reduce_alloc.patch b/integration/opentitan/reduce_alloc.patch index 67c7ab992..f017e07b1 100644 --- a/integration/opentitan/reduce_alloc.patch +++ b/integration/opentitan/reduce_alloc.patch @@ -13,20 +13,20 @@ index be11f20..0000000 100644 - kOtcryptoMldsa44WorkBufferVerifyWords = 22464 / sizeof(uint32_t), + kOtcryptoMldsa44WorkBufferKeypairWords = 13600 / sizeof(uint32_t), + kOtcryptoMldsa44WorkBufferSignWords = 13120 / sizeof(uint32_t), -+ kOtcryptoMldsa44WorkBufferVerifyWords = 19392 / sizeof(uint32_t), ++ kOtcryptoMldsa44WorkBufferVerifyWords = 13184 / sizeof(uint32_t), - kOtcryptoMldsa65WorkBufferKeypairWords = 46304 / sizeof(uint32_t), - kOtcryptoMldsa65WorkBufferSignWords = 44768 / sizeof(uint32_t), - kOtcryptoMldsa65WorkBufferVerifyWords = 30720 / sizeof(uint32_t), + kOtcryptoMldsa65WorkBufferKeypairWords = 19744 / sizeof(uint32_t), + kOtcryptoMldsa65WorkBufferSignWords = 17248 / sizeof(uint32_t), -+ kOtcryptoMldsa65WorkBufferVerifyWords = 26624 / sizeof(uint32_t), ++ kOtcryptoMldsa65WorkBufferVerifyWords = 18368 / sizeof(uint32_t), - kOtcryptoMldsa87WorkBufferKeypairWords = 62688 / sizeof(uint32_t), - kOtcryptoMldsa87WorkBufferSignWords = 59104 / sizeof(uint32_t), - kOtcryptoMldsa87WorkBufferVerifyWords = 41216 / sizeof(uint32_t), + kOtcryptoMldsa87WorkBufferKeypairWords = 25888 / sizeof(uint32_t), + kOtcryptoMldsa87WorkBufferSignWords = 21344 / sizeof(uint32_t), -+ kOtcryptoMldsa87WorkBufferVerifyWords = 35072 / sizeof(uint32_t), ++ kOtcryptoMldsa87WorkBufferVerifyWords = 24768 / sizeof(uint32_t), }; diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 5f7b01325..2c645d411 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -264,8 +264,8 @@ #undef mld_pack_sig_z #undef mld_pack_sk_rho_key_tr_s2_t0 #undef mld_pack_sk_s1 -#undef mld_unpack_pk -#undef mld_unpack_sig +#undef mld_sig_unpack_hints +#undef mld_unpack_pk_t1 #undef mld_unpack_sk /* mldsa/src/params.h */ #undef MLDSA_BETA diff --git a/mldsa/mldsa_native.h b/mldsa/mldsa_native.h index aeb843f20..94e32c2b2 100644 --- a/mldsa/mldsa_native.h +++ b/mldsa/mldsa_native.h @@ -942,33 +942,33 @@ int MLD_API_NAMESPACE(pk_from_sk)( #define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48448 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 37056 #define MLD_TOTAL_ALLOC_44_SIGN 44704 -#define MLD_TOTAL_ALLOC_44_VERIFY 34720 +#define MLD_TOTAL_ALLOC_44_VERIFY 25472 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 49408 #define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 74592 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 60608 #define MLD_TOTAL_ALLOC_65_SIGN 69312 -#define MLD_TOTAL_ALLOC_65_VERIFY 56288 +#define MLD_TOTAL_ALLOC_65_VERIFY 42944 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 82176 #define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 115456 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 97472 #define MLD_TOTAL_ALLOC_87_SIGN 108224 -#define MLD_TOTAL_ALLOC_87_VERIFY 91360 +#define MLD_TOTAL_ALLOC_87_VERIFY 73920 #else /* MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM */ #define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 13600 -#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 23136 +#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 16928 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 21728 #define MLD_TOTAL_ALLOC_44_SIGN 13120 -#define MLD_TOTAL_ALLOC_44_VERIFY 19392 +#define MLD_TOTAL_ALLOC_44_VERIFY 13184 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 19744 -#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 31904 +#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 23648 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 30944 #define MLD_TOTAL_ALLOC_65_SIGN 17248 -#define MLD_TOTAL_ALLOC_65_VERIFY 26624 +#define MLD_TOTAL_ALLOC_65_VERIFY 18368 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 25888 -#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 42304 +#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 32000 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 41184 #define MLD_TOTAL_ALLOC_87_SIGN 21344 -#define MLD_TOTAL_ALLOC_87_VERIFY 35072 +#define MLD_TOTAL_ALLOC_87_VERIFY 24768 #endif /* !(MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM) */ /* check-magic: on */ diff --git a/mldsa/mldsa_native_asm.S b/mldsa/mldsa_native_asm.S index 785f94b4c..ef1173058 100644 --- a/mldsa/mldsa_native_asm.S +++ b/mldsa/mldsa_native_asm.S @@ -269,8 +269,8 @@ #undef mld_pack_sig_z #undef mld_pack_sk_rho_key_tr_s2_t0 #undef mld_pack_sk_s1 -#undef mld_unpack_pk -#undef mld_unpack_sig +#undef mld_sig_unpack_hints +#undef mld_unpack_pk_t1 #undef mld_unpack_sk /* mldsa/src/params.h */ #undef MLDSA_BETA diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c index 4e84f030d..fc63698c0 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -13,7 +13,6 @@ * This is to facilitate building multiple instances * of mldsa-native (e.g. with varying parameter sets) * within a single compilation unit. */ -#define mld_unpack_hints MLD_ADD_PARAM_SET(mld_unpack_hints) /* End of parameter set namespacing */ #if !defined(MLD_CONFIG_NO_KEYPAIR_API) @@ -39,12 +38,11 @@ void mld_pack_pk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES], #if !defined(MLD_CONFIG_NO_VERIFY_API) MLD_INTERNAL_API -void mld_unpack_pk(uint8_t rho[MLDSA_SEEDBYTES], mld_polyveck *t1, - const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES]) +void mld_unpack_pk_t1(mld_polyveck *t1, + const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES]) { unsigned int i; - mld_memcpy(rho, pk, MLDSA_SEEDBYTES); pk += MLDSA_SEEDBYTES; for (i = 0; i < MLDSA_K; ++i) @@ -173,30 +171,11 @@ void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi, #endif /* !MLD_CONFIG_NO_SIGN_API */ #if !defined(MLD_CONFIG_NO_VERIFY_API) -/************************************************* - * Name: mld_unpack_hints - * - * Description: Unpack raw hint bytes into a polyveck - * struct - * - * Arguments: - mld_polyveck *h: pointer to output hint vector h - * - const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES]: - * raw hint bytes - * - * Returns 1 in case of malformed hints; otherwise 0. - **************************************************/ -static int mld_unpack_hints( - mld_polyveck *h, const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES]) -__contract__( - requires(memory_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES)) - requires(memory_no_alias(h, sizeof(mld_polyveck))) - assigns(memory_slice(h, sizeof(mld_polyveck))) - /* All returned coefficients are either 0 or 1 */ - ensures(forall(k1, 0, MLDSA_K, - array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) - ensures(return_value >= 0 && return_value <= 1) -) +MLD_INTERNAL_API +int mld_sig_unpack_hints(mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES]) { + const uint8_t *packed_hints = + sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES; unsigned int i, j; unsigned int old_hint_count; @@ -269,21 +248,5 @@ __contract__( } #endif /* !MLD_CONFIG_NO_VERIFY_API */ -#if !defined(MLD_CONFIG_NO_VERIFY_API) -MLD_INTERNAL_API -int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z, - mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES]) -{ - mld_memcpy(c, sig, MLDSA_CTILDEBYTES); - sig += MLDSA_CTILDEBYTES; - - mld_polyvecl_unpack_z(z, sig); - sig += MLDSA_L * MLDSA_POLYZ_PACKEDBYTES; - - return mld_unpack_hints(h, sig); -} -#endif /* !MLD_CONFIG_NO_VERIFY_API */ - /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ -#undef mld_unpack_hints diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h index d29554563..0ab4aa816 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -159,24 +159,21 @@ __contract__( #endif /* !MLD_CONFIG_NO_SIGN_API */ #if !defined(MLD_CONFIG_NO_VERIFY_API) -#define mld_unpack_pk MLD_NAMESPACE_KL(unpack_pk) +#define mld_unpack_pk_t1 MLD_NAMESPACE_KL(unpack_pk_t1) /************************************************* - * Name: mld_unpack_pk + * Name: mld_unpack_pk_t1 * - * Description: Unpack public key pk = (rho, t1). + * Description: Unpack the t1 component of a public key pk = (rho, t1). * - * Arguments: - const uint8_t rho[]: output byte array for rho - * - const mld_polyveck *t1: pointer to output vector t1 + * Arguments: - mld_polyveck *t1: pointer to output vector t1 * - uint8_t pk[]: byte array containing bit-packed pk **************************************************/ MLD_INTERNAL_API -void mld_unpack_pk(uint8_t rho[MLDSA_SEEDBYTES], mld_polyveck *t1, - const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES]) +void mld_unpack_pk_t1(mld_polyveck *t1, + const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES]) __contract__( requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES)) - requires(memory_no_alias(rho, MLDSA_SEEDBYTES)) requires(memory_no_alias(t1, sizeof(mld_polyveck))) - assigns(memory_slice(rho, MLDSA_SEEDBYTES)) assigns(memory_slice(t1, sizeof(mld_polyveck))) ensures(forall(k0, 0, MLDSA_K, array_bound(t1->vec[k0].coeffs, 0, MLDSA_N, 0, 1 << 10))) @@ -239,34 +236,26 @@ __contract__( #endif /* !MLD_CONFIG_NO_SIGN_API */ #if !defined(MLD_CONFIG_NO_VERIFY_API) -#define mld_unpack_sig MLD_NAMESPACE_KL(unpack_sig) +#define mld_sig_unpack_hints MLD_NAMESPACE_KL(sig_unpack_hints) /************************************************* - * Name: mld_unpack_sig + * Name: mld_sig_unpack_hints * - * Description: Unpack signature sig = (c, z, h). + * Description: Unpack hint vector h from a signature buffer. * - * Arguments: - uint8_t *c: pointer to output challenge hash - * - mld_polyvecl *z: pointer to output vector z - * - mld_polyveck *h: pointer to output hint vector h - * - const uint8_t sig[]: byte array containing - * bit-packed signature + * Arguments: - mld_polyveck *h: pointer to output hint vector + * - const uint8_t sig[]: signature buffer + * (MLDSA_CRYPTO_BYTES); the hint bytes are read from + * the trailing MLDSA_POLYVECH_PACKEDBYTES. * - * Returns 1 in case of malformed signature; otherwise 0. + * Returns 1 in case of malformed hints; otherwise 0. **************************************************/ MLD_INTERNAL_API MLD_MUST_CHECK_RETURN_VALUE -int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z, - mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES]) +int mld_sig_unpack_hints(mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES]) __contract__( requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(c, MLDSA_CTILDEBYTES)) - requires(memory_no_alias(z, sizeof(mld_polyvecl))) requires(memory_no_alias(h, sizeof(mld_polyveck))) - assigns(memory_slice(c, MLDSA_CTILDEBYTES)) - assigns(memory_slice(z, sizeof(mld_polyvecl))) assigns(memory_slice(h, sizeof(mld_polyveck))) - ensures(forall(k0, 0, MLDSA_L, - array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ensures(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2))) ensures(return_value >= 0 && return_value <= 1) diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 3d59ce5cd..797313a75 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -1051,25 +1051,43 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, { int ret, cmp; + typedef union + { + mld_polyvecl z; + mld_poly cp; + } zcp_u; + mld_polyvecl *z; + mld_poly *cp; + + typedef union + { + mld_polymat mat; + mld_polyveck t1; + mld_polyveck h; + } reuse_u; + mld_polymat *mat; + mld_polyveck *t1; + mld_polyveck *h; + MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), context); - MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES, context); MLD_ALLOC(mu, uint8_t, MLDSA_CRHBYTES, context); MLD_ALLOC(c, uint8_t, MLDSA_CTILDEBYTES, context); MLD_ALLOC(c2, uint8_t, MLDSA_CTILDEBYTES, context); - MLD_ALLOC(cp, mld_poly, 1, context); - MLD_ALLOC(mat, mld_polymat, 1, context); - MLD_ALLOC(z, mld_polyvecl, 1, context); - MLD_ALLOC(t1, mld_polyveck, 1, context); - MLD_ALLOC(tmp, mld_polyveck, 1, context); - MLD_ALLOC(h, mld_polyveck, 1, context); + MLD_ALLOC(zcp, zcp_u, 1, context); + MLD_ALLOC(w1, mld_polyveck, 1, context); + MLD_ALLOC(reuse, reuse_u, 1, context); - if (buf == NULL || rho == NULL || mu == NULL || c == NULL || c2 == NULL || - cp == NULL || mat == NULL || z == NULL || t1 == NULL || tmp == NULL || - h == NULL) + if (buf == NULL || mu == NULL || c == NULL || c2 == NULL || zcp == NULL || + w1 == NULL || reuse == NULL) { ret = MLD_ERR_OUT_OF_MEMORY; goto cleanup; } + z = &zcp->z; + cp = &zcp->cp; + mat = &reuse->mat; + t1 = &reuse->t1; + h = &reuse->h; if (siglen != MLDSA_CRYPTO_BYTES) { @@ -1077,16 +1095,11 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, goto cleanup; } - mld_unpack_pk(rho, t1, pk); + mld_memcpy(c, sig, MLDSA_CTILDEBYTES); + mld_polyvecl_unpack_z(z, sig + MLDSA_CTILDEBYTES); - /* mld_unpack_sig and mld_polyvecl_chknorm signal failure through a - * single non-zero error code that's not yet aligned with MLD_ERR_XXX. - * Map it to MLD_ERR_FAIL explicitly. */ - if (mld_unpack_sig(c, z, h, sig)) - { - ret = MLD_ERR_FAIL; - goto cleanup; - } + /* mld_polyvecl_chknorm signals failure through a single non-zero error code + * that's not yet aligned with MLD_ERR_XXX. Map it to MLD_ERR_FAIL. */ if (mld_polyvecl_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA)) { ret = MLD_ERR_FAIL; @@ -1111,23 +1124,32 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, } /* Matrix-vector multiplication; compute Az - c2^dt1 */ + mld_polyvecl_ntt(z); + mld_polyvec_matrix_expand(mat, pk); + mld_polyvec_matrix_pointwise_montgomery(w1, mat, z); + mld_poly_challenge(cp, c); mld_poly_ntt(cp); + mld_unpack_pk_t1(t1, pk); mld_polyveck_shiftl(t1); mld_polyveck_ntt(t1); mld_polyveck_pointwise_poly_montgomery(t1, cp); - mld_polyvec_matrix_expand(mat, rho); - mld_polyvecl_ntt(z); - mld_polyvec_matrix_pointwise_montgomery(tmp, mat, z); - mld_polyveck_sub(tmp, t1); - mld_polyveck_reduce(tmp); - mld_polyveck_invntt_tomont(tmp); + mld_polyveck_sub(w1, t1); + mld_polyveck_reduce(w1); + mld_polyveck_invntt_tomont(w1); /* Reconstruct w1 */ - mld_polyveck_caddq(tmp); - mld_polyveck_use_hint(tmp, h); - mld_polyveck_pack_w1(buf, tmp); + mld_polyveck_caddq(w1); + /* mld_sig_unpack_hints signals failure through a single non-zero error + * code that's not yet aligned with MLD_ERR_XXX. Map it to MLD_ERR_FAIL. */ + if (mld_sig_unpack_hints(h, sig)) + { + ret = MLD_ERR_FAIL; + goto cleanup; + } + mld_polyveck_use_hint(w1, h); + mld_polyveck_pack_w1(buf, w1); /* Call random oracle and verify challenge */ mld_H(c2, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, buf, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0); @@ -1141,16 +1163,12 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, cleanup: /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ - MLD_FREE(h, mld_polyveck, 1, context); - MLD_FREE(tmp, mld_polyveck, 1, context); - MLD_FREE(t1, mld_polyveck, 1, context); - MLD_FREE(z, mld_polyvecl, 1, context); - MLD_FREE(mat, mld_polymat, 1, context); - MLD_FREE(cp, mld_poly, 1, context); + MLD_FREE(reuse, reuse_u, 1, context); + MLD_FREE(w1, mld_polyveck, 1, context); + MLD_FREE(zcp, zcp_u, 1, context); MLD_FREE(c2, uint8_t, MLDSA_CTILDEBYTES, context); MLD_FREE(c, uint8_t, MLDSA_CTILDEBYTES, context); MLD_FREE(mu, uint8_t, MLDSA_CRHBYTES, context); - MLD_FREE(rho, uint8_t, MLDSA_SEEDBYTES, context); MLD_FREE(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), context); return ret; } diff --git a/proofs/cbmc/unpack_hints/Makefile b/proofs/cbmc/sig_unpack_hints/Makefile similarity index 92% rename from proofs/cbmc/unpack_hints/Makefile rename to proofs/cbmc/sig_unpack_hints/Makefile index 49f7fe008..22b8cb1f7 100644 --- a/proofs/cbmc/unpack_hints/Makefile +++ b/proofs/cbmc/sig_unpack_hints/Makefile @@ -4,11 +4,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = unpack_hints_harness +HARNESS_FILE = sig_unpack_hints_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 = unpack_hints +PROOF_UID = sig_unpack_hints DEFINES += INCLUDES += @@ -18,7 +18,7 @@ REMOVE_FUNCTION_BODY += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c -CHECK_FUNCTION_CONTRACTS=mld_unpack_hints +CHECK_FUNCTION_CONTRACTS=mld_sig_unpack_hints USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = mld_unpack_hints +FUNCTION_NAME = mld_sig_unpack_hints # 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 diff --git a/proofs/cbmc/unpack_sig/unpack_sig_harness.c b/proofs/cbmc/sig_unpack_hints/sig_unpack_hints_harness.c similarity index 73% rename from proofs/cbmc/unpack_sig/unpack_sig_harness.c rename to proofs/cbmc/sig_unpack_hints/sig_unpack_hints_harness.c index 73adbe557..104785c55 100644 --- a/proofs/cbmc/unpack_sig/unpack_sig_harness.c +++ b/proofs/cbmc/sig_unpack_hints/sig_unpack_hints_harness.c @@ -3,13 +3,10 @@ #include "packing.h" - void harness(void) { - uint8_t *c; uint8_t *sig; mld_polyveck *h; - mld_polyvecl *z; int r; - r = mld_unpack_sig(c, z, h, sig); + r = mld_sig_unpack_hints(h, sig); } diff --git a/proofs/cbmc/sign_verify_internal/Makefile b/proofs/cbmc/sign_verify_internal/Makefile index f0873ea5e..de78960cf 100644 --- a/proofs/cbmc/sign_verify_internal/Makefile +++ b/proofs/cbmc/sign_verify_internal/Makefile @@ -20,8 +20,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c CHECK_FUNCTION_CONTRACTS=mld_verify_internal -USE_FUNCTION_CONTRACTS=mld_unpack_pk -USE_FUNCTION_CONTRACTS+=mld_unpack_sig +USE_FUNCTION_CONTRACTS=mld_unpack_pk_t1 +USE_FUNCTION_CONTRACTS+=mld_sig_unpack_hints +USE_FUNCTION_CONTRACTS+=mld_polyvecl_unpack_z USE_FUNCTION_CONTRACTS+=mld_polyvecl_chknorm USE_FUNCTION_CONTRACTS+=mld_H USE_FUNCTION_CONTRACTS+=mld_poly_challenge @@ -46,7 +47,7 @@ USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3 FUNCTION_NAME = sign_verify_internal diff --git a/proofs/cbmc/unpack_hints/unpack_hints_harness.c b/proofs/cbmc/unpack_hints/unpack_hints_harness.c deleted file mode 100644 index 9e10493e2..000000000 --- a/proofs/cbmc/unpack_hints/unpack_hints_harness.c +++ /dev/null @@ -1,15 +0,0 @@ -// Copyright (c) The mldsa-native project authors -// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -#include "packing.h" - -int mld_unpack_hints(mld_polyveck *h, - const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES]); - -void harness(void) -{ - uint8_t *sig; - mld_polyveck *h; - int r; - r = mld_unpack_hints(h, sig); -} diff --git a/proofs/cbmc/unpack_pk/Makefile b/proofs/cbmc/unpack_pk_t1/Makefile similarity index 90% rename from proofs/cbmc/unpack_pk/Makefile rename to proofs/cbmc/unpack_pk_t1/Makefile index 09cfb8a01..ddcb246fd 100644 --- a/proofs/cbmc/unpack_pk/Makefile +++ b/proofs/cbmc/unpack_pk_t1/Makefile @@ -4,22 +4,22 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = unpack_pk_harness +HARNESS_FILE = unpack_pk_t1_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 = unpack_pk +PROOF_UID = unpack_pk_t1 DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += mld_unpack_pk.0:8 # Largest value of MLDSA_K +UNWINDSET += mld_unpack_pk_t1.0:8 # Largest value of MLDSA_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c -CHECK_FUNCTION_CONTRACTS=mld_unpack_pk +CHECK_FUNCTION_CONTRACTS=mld_unpack_pk_t1 USE_FUNCTION_CONTRACTS=mld_polyt1_unpack APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = unpack_pk +FUNCTION_NAME = unpack_pk_t1 # 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 diff --git a/proofs/cbmc/unpack_pk/unpack_pk_harness.c b/proofs/cbmc/unpack_pk_t1/unpack_pk_t1_harness.c similarity index 70% rename from proofs/cbmc/unpack_pk/unpack_pk_harness.c rename to proofs/cbmc/unpack_pk_t1/unpack_pk_t1_harness.c index 49a088bea..e7f096159 100644 --- a/proofs/cbmc/unpack_pk/unpack_pk_harness.c +++ b/proofs/cbmc/unpack_pk_t1/unpack_pk_t1_harness.c @@ -6,7 +6,7 @@ void harness(void) { - uint8_t *a, *b; - mld_polyveck *c; - mld_unpack_pk(a, c, b); + uint8_t *pk; + mld_polyveck *t1; + mld_unpack_pk_t1(t1, pk); } diff --git a/proofs/cbmc/unpack_sig/Makefile b/proofs/cbmc/unpack_sig/Makefile deleted file mode 100644 index 3c5c350c8..000000000 --- a/proofs/cbmc/unpack_sig/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 = unpack_sig_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 = unpack_sig - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c - -CHECK_FUNCTION_CONTRACTS=mld_unpack_sig -USE_FUNCTION_CONTRACTS=mld_polyvecl_unpack_z -USE_FUNCTION_CONTRACTS+=mld_unpack_hints -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 = unpack_sig - -# 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