From 926bbe1e352eda32cf8c7e1995df30b9340087ce Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 7 Apr 2026 14:16:07 +0800 Subject: [PATCH] lowmem: Unpack z lazily in verification Introduce mld_zvec (eager / lazy, dispatched by MLD_CONFIG_REDUCE_RAM): - mld_zvec_init: eager unpacks the full polyvecl, runs the polyvecl-wide norm check, and NTTs in place; lazy stores a pointer. - mld_zvec_get_poly: eager copies one poly from the precomputed vector; lazy unpacks one poly, norm-checks it, and NTTs into the caller's buf. The norm check moves out of mld_sign_verify_internal into the accessors. Add a fused mld_polyvec_matrix_pointwise_montgomery_zvec helper used by verify: eager is a thin wrapper around the standard matrix-vector multiply (z is already NTT'd); lazy streams z via mld_zvec_get_poly_lazy and samples the matrix column-by-column. In REDUCE_RAM mode this avoids holding the full unpacked polyvecl z, reducing verify allocation by 2-5 KiB per parameter set. Signed-off-by: Matthias J. Kannwischer --- integration/opentitan/reduce_alloc.patch | 6 +- mldsa/mldsa_native.c | 12 + mldsa/mldsa_native.h | 18 +- mldsa/mldsa_native_asm.S | 12 + mldsa/src/polyvec.c | 22 +- mldsa/src/polyvec.h | 23 +- mldsa/src/polyvec_lazy.c | 104 ++++++++- mldsa/src/polyvec_lazy.h | 209 +++++++++++++++++- mldsa/src/sign.c | 40 ++-- proofs/cbmc/Makefile.common | 3 + .../Makefile | 64 ++++++ ...matrix_pointwise_montgomery_zvec_harness.c | 13 ++ proofs/cbmc/polyvecl_unpack_z/Makefile | 5 + .../polyvecl_unpack_z_harness.c | 2 + proofs/cbmc/sign_verify_internal/Makefile | 6 +- proofs/cbmc/zvec_get_poly/Makefile | 59 +++++ .../zvec_get_poly/zvec_get_poly_harness.c | 14 ++ proofs/cbmc/zvec_init/Makefile | 59 +++++ proofs/cbmc/zvec_init/zvec_init_harness.c | 13 ++ test/src/test_unit.c | 80 ++++++- 20 files changed, 699 insertions(+), 65 deletions(-) create mode 100644 proofs/cbmc/polyvec_matrix_pointwise_montgomery_zvec/Makefile create mode 100644 proofs/cbmc/polyvec_matrix_pointwise_montgomery_zvec/polyvec_matrix_pointwise_montgomery_zvec_harness.c create mode 100644 proofs/cbmc/zvec_get_poly/Makefile create mode 100644 proofs/cbmc/zvec_get_poly/zvec_get_poly_harness.c create mode 100644 proofs/cbmc/zvec_init/Makefile create mode 100644 proofs/cbmc/zvec_init/zvec_init_harness.c diff --git a/integration/opentitan/reduce_alloc.patch b/integration/opentitan/reduce_alloc.patch index f017e07b1..1f7295572 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 = 13184 / sizeof(uint32_t), ++ kOtcryptoMldsa44WorkBufferVerifyWords = 11168 / 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 = 18368 / sizeof(uint32_t), ++ kOtcryptoMldsa65WorkBufferVerifyWords = 15328 / 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 = 24768 / sizeof(uint32_t), ++ kOtcryptoMldsa87WorkBufferVerifyWords = 19680 / sizeof(uint32_t), }; diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 2c645d411..efec75499 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -355,6 +355,9 @@ #undef mld_polyvec_matrix_pointwise_montgomery_yvec #undef mld_polyvec_matrix_pointwise_montgomery_yvec_eager #undef mld_polyvec_matrix_pointwise_montgomery_yvec_lazy +#undef mld_polyvec_matrix_pointwise_montgomery_zvec +#undef mld_polyvec_matrix_pointwise_montgomery_zvec_eager +#undef mld_polyvec_matrix_pointwise_montgomery_zvec_lazy #undef mld_sk_s1hat #undef mld_sk_s1hat_eager #undef mld_sk_s1hat_get_poly @@ -391,6 +394,15 @@ #undef mld_yvec_init_eager #undef mld_yvec_init_lazy #undef mld_yvec_lazy +#undef mld_zvec +#undef mld_zvec_eager +#undef mld_zvec_get_poly +#undef mld_zvec_get_poly_eager +#undef mld_zvec_get_poly_lazy +#undef mld_zvec_init +#undef mld_zvec_init_eager +#undef mld_zvec_init_lazy +#undef mld_zvec_lazy /* mldsa/src/rounding.h */ #undef MLD_2_POW_D #undef MLD_ROUNDING_H diff --git a/mldsa/mldsa_native.h b/mldsa/mldsa_native.h index 94e32c2b2..119d85ae8 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 25472 +#define MLD_TOTAL_ALLOC_44_VERIFY 26496 #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 42944 +#define MLD_TOTAL_ALLOC_65_VERIFY 43968 #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 73920 +#define MLD_TOTAL_ALLOC_87_VERIFY 74944 #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 16928 +#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 16864 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 21728 #define MLD_TOTAL_ALLOC_44_SIGN 13120 -#define MLD_TOTAL_ALLOC_44_VERIFY 13184 +#define MLD_TOTAL_ALLOC_44_VERIFY 11168 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 19744 -#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 23648 +#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 22528 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 30944 #define MLD_TOTAL_ALLOC_65_SIGN 17248 -#define MLD_TOTAL_ALLOC_65_VERIFY 18368 +#define MLD_TOTAL_ALLOC_65_VERIFY 15328 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 25888 -#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 32000 +#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 28576 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 41184 #define MLD_TOTAL_ALLOC_87_SIGN 21344 -#define MLD_TOTAL_ALLOC_87_VERIFY 24768 +#define MLD_TOTAL_ALLOC_87_VERIFY 19680 #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 ef1173058..a37890283 100644 --- a/mldsa/mldsa_native_asm.S +++ b/mldsa/mldsa_native_asm.S @@ -360,6 +360,9 @@ #undef mld_polyvec_matrix_pointwise_montgomery_yvec #undef mld_polyvec_matrix_pointwise_montgomery_yvec_eager #undef mld_polyvec_matrix_pointwise_montgomery_yvec_lazy +#undef mld_polyvec_matrix_pointwise_montgomery_zvec +#undef mld_polyvec_matrix_pointwise_montgomery_zvec_eager +#undef mld_polyvec_matrix_pointwise_montgomery_zvec_lazy #undef mld_sk_s1hat #undef mld_sk_s1hat_eager #undef mld_sk_s1hat_get_poly @@ -396,6 +399,15 @@ #undef mld_yvec_init_eager #undef mld_yvec_init_lazy #undef mld_yvec_lazy +#undef mld_zvec +#undef mld_zvec_eager +#undef mld_zvec_get_poly +#undef mld_zvec_get_poly_eager +#undef mld_zvec_get_poly_lazy +#undef mld_zvec_init +#undef mld_zvec_init_eager +#undef mld_zvec_init_lazy +#undef mld_zvec_lazy /* mldsa/src/rounding.h */ #undef MLD_2_POW_D #undef MLD_ROUNDING_H diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c index f0ecc2f4e..51227d864 100644 --- a/mldsa/src/polyvec.c +++ b/mldsa/src/polyvec.c @@ -73,8 +73,8 @@ void mld_polyvecl_uniform_gamma1(mld_polyvecl *v, */ #if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \ - !defined(MLD_CONFIG_NO_VERIFY_API) || \ - (!defined(MLD_CONFIG_NO_SIGN_API) && \ + ((!defined(MLD_CONFIG_NO_SIGN_API) || \ + !defined(MLD_CONFIG_NO_VERIFY_API)) && \ (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST))) MLD_INTERNAL_API void mld_polyvecl_ntt(mld_polyvecl *v) @@ -95,8 +95,8 @@ void mld_polyvecl_ntt(mld_polyvecl *v) mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND); } -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API || \ - (!MLD_CONFIG_NO_SIGN_API && (!MLD_CONFIG_REDUCE_RAM || \ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API || ((!MLD_CONFIG_NO_SIGN_API || \ + !MLD_CONFIG_NO_VERIFY_API) && (!MLD_CONFIG_REDUCE_RAM || \ MLD_UNIT_TEST)) */ #if !defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST) @@ -207,7 +207,9 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u, } #endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */ -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) || \ +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \ + (!defined(MLD_CONFIG_NO_VERIFY_API) && \ + (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST))) || \ defined(MLD_UNIT_TEST) MLD_INTERNAL_API uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound) @@ -233,8 +235,8 @@ uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound) } return t; } -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API || \ - MLD_UNIT_TEST */ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API || (!MLD_CONFIG_NO_VERIFY_API && \ + (!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST)) || MLD_UNIT_TEST */ /**************************************************************/ /************ Vectors of polynomials of length MLDSA_K **************/ @@ -633,7 +635,8 @@ void mld_polyvecl_unpack_eta( #endif /* !MLD_CONFIG_NO_KEYPAIR_API || (!MLD_CONFIG_NO_SIGN_API && \ (!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST)) */ -#if !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_VERIFY_API) && \ + (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST)) MLD_INTERNAL_API void mld_polyvecl_unpack_z(mld_polyvecl *z, const uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES]) @@ -647,7 +650,8 @@ void mld_polyvecl_unpack_z(mld_polyvecl *z, mld_assert_bound_2d(z->vec, MLDSA_L, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1); } -#endif /* !MLD_CONFIG_NO_VERIFY_API */ +#endif /* !MLD_CONFIG_NO_VERIFY_API && (!MLD_CONFIG_REDUCE_RAM || \ + MLD_UNIT_TEST) */ #if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \ (!defined(MLD_CONFIG_NO_SIGN_API) && \ diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h index 6caba054d..02a791620 100644 --- a/mldsa/src/polyvec.h +++ b/mldsa/src/polyvec.h @@ -55,9 +55,9 @@ __contract__( #endif /* !MLD_CONFIG_NO_SIGN_API && (!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST) \ */ -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \ - !defined(MLD_CONFIG_NO_VERIFY_API) || \ - (!defined(MLD_CONFIG_NO_SIGN_API) && \ +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \ + ((!defined(MLD_CONFIG_NO_SIGN_API) || \ + !defined(MLD_CONFIG_NO_VERIFY_API)) && \ (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST))) #define mld_polyvecl_ntt MLD_NAMESPACE_KL(polyvecl_ntt) /************************************************* @@ -76,8 +76,8 @@ __contract__( assigns(memory_slice(v, sizeof(mld_polyvecl))) ensures(forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) ); -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API || \ - (!MLD_CONFIG_NO_SIGN_API && (!MLD_CONFIG_REDUCE_RAM || \ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API || ((!MLD_CONFIG_NO_SIGN_API || \ + !MLD_CONFIG_NO_VERIFY_API) && (!MLD_CONFIG_REDUCE_RAM || \ MLD_UNIT_TEST)) */ #if !defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST) @@ -120,7 +120,9 @@ __contract__( ); #endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */ -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \ + (!defined(MLD_CONFIG_NO_VERIFY_API) && \ + (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST))) #define mld_polyvecl_chknorm MLD_NAMESPACE_KL(polyvecl_chknorm) /************************************************* * Name: mld_polyvecl_chknorm @@ -145,7 +147,8 @@ __contract__( ensures(return_value == 0 || return_value == 0xFFFFFFFF) ensures((return_value == 0) == forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, B))) ); -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API || (!MLD_CONFIG_NO_VERIFY_API && \ + (!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST)) */ /* Vectors of polynomials of length MLDSA_K */ typedef struct @@ -584,7 +587,8 @@ __contract__( #endif /* !MLD_CONFIG_NO_KEYPAIR_API || (!MLD_CONFIG_NO_SIGN_API && \ (!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST)) */ -#if !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_VERIFY_API) && \ + (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST)) #define mld_polyvecl_unpack_z MLD_NAMESPACE_KL(polyvecl_unpack_z) /************************************************* * Name: mld_polyvecl_unpack_z @@ -606,7 +610,8 @@ __contract__( ensures(forall(k1, 0, MLDSA_L, array_bound(z->vec[k1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))) ); -#endif /* !MLD_CONFIG_NO_VERIFY_API */ +#endif /* !MLD_CONFIG_NO_VERIFY_API && (!MLD_CONFIG_REDUCE_RAM || \ + MLD_UNIT_TEST) */ #if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \ (!defined(MLD_CONFIG_NO_SIGN_API) && \ diff --git a/mldsa/src/polyvec_lazy.c b/mldsa/src/polyvec_lazy.c index 04ffdb6b8..4056f66e9 100644 --- a/mldsa/src/polyvec_lazy.c +++ b/mldsa/src/polyvec_lazy.c @@ -184,6 +184,31 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_eager(mld_polyveck *w, } #endif /* !MLD_CONFIG_NO_SIGN_API */ +#if !defined(MLD_CONFIG_NO_VERIFY_API) +MLD_INTERNAL_API +int mld_polyvec_matrix_pointwise_montgomery_zvec_eager(mld_polyveck *w, + mld_polymat_eager *mat, + mld_zvec_eager *z) +{ + unsigned int i; + + for (i = 0; i < MLDSA_K; ++i) + __loop__( + assigns(i, memory_slice(w, sizeof(mld_polyveck))) + invariant(i <= MLDSA_K) + invariant(forall(k0, 0, i, + array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) + decreases(MLDSA_K - i) + ) + { + mld_polyvec_matrix_pointwise_montgomery_row_eager(&w->vec[i], mat, &z->vec, + i); + } + + return 0; +} +#endif /* !MLD_CONFIG_NO_VERIFY_API */ + #endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */ #if defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST) @@ -195,7 +220,7 @@ void mld_polyvec_matrix_expand_lazy(mld_polymat_lazy *mat, mld_memcpy(mat->rho, rho, MLDSA_SEEDBYTES); } -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) MLD_INTERNAL_API void mld_polyvec_matrix_pointwise_montgomery_row_lazy(mld_poly *t_row, mld_polymat_lazy *mat, @@ -228,7 +253,7 @@ void mld_polyvec_matrix_pointwise_montgomery_row_lazy(mld_poly *t_row, /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ mld_zeroize(seed_ext, sizeof(seed_ext)); } -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API */ #if !defined(MLD_CONFIG_NO_SIGN_API) MLD_INTERNAL_API @@ -305,9 +330,80 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w, } #endif /* !MLD_CONFIG_NO_SIGN_API */ +#if !defined(MLD_CONFIG_NO_VERIFY_API) +MLD_INTERNAL_API +int mld_polyvec_matrix_pointwise_montgomery_zvec_lazy(mld_polyveck *w, + mld_polymat_lazy *mat, + mld_zvec_lazy *z) +{ + unsigned int k, l; + MLD_ALIGN uint8_t seed_ext[MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)]; + + mld_memcpy(seed_ext, mat->rho, MLDSA_SEEDBYTES); + + for (l = 0; l < MLDSA_L; l++) + __loop__( + assigns(k, l, object_whole(seed_ext), + memory_slice(w, sizeof(mld_polyveck)), + memory_slice(mat, sizeof(mld_polymat_lazy)), + memory_slice(&z->scratch, sizeof(mld_poly))) + invariant(l <= MLDSA_L) + invariant(l == 0 || + forall(k0, 0, MLDSA_K, + array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, + (int)l * MLDSA_Q))) + decreases(MLDSA_L - l) + ) + { + if (mld_zvec_get_poly_lazy(&z->scratch, z, l)) + { + mld_zeroize(seed_ext, sizeof(seed_ext)); + return MLD_ERR_FAIL; + } + for (k = 0; k < MLDSA_K; k++) + __loop__( + assigns(k, object_whole(seed_ext), + memory_slice(w, sizeof(mld_polyveck)), + memory_slice(mat, sizeof(mld_polymat_lazy))) + invariant(k <= MLDSA_K) + invariant(l != 0 || + forall(k1, 0, k, + array_abs_bound(w->vec[k1].coeffs, 0, MLDSA_N, MLDSA_Q))) + invariant(l == 0 || + forall(k2, 0, k, + array_abs_bound(w->vec[k2].coeffs, 0, MLDSA_N, + ((int)l + 1) * MLDSA_Q))) + invariant(l == 0 || + forall(k3, k, MLDSA_K, + array_abs_bound(w->vec[k3].coeffs, 0, MLDSA_N, + (int)l * MLDSA_Q))) + decreases(MLDSA_K - k) + ) + { + if (l == 0) + { + mld_polymat_expand_entry(&w->vec[k], seed_ext, 0, (uint8_t)k); + mld_poly_pointwise_montgomery(&w->vec[k], &z->scratch); + } + else + { + mld_polymat_expand_entry(&mat->cur, seed_ext, (uint8_t)l, (uint8_t)k); + mld_poly_pointwise_montgomery(&mat->cur, &z->scratch); + mld_poly_add(&w->vec[k], &mat->cur); + } + } + } + + /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ + mld_zeroize(seed_ext, sizeof(seed_ext)); + mld_polyveck_reduce(w); + return 0; +} +#endif /* !MLD_CONFIG_NO_VERIFY_API */ + #endif /* MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */ -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) MLD_INTERNAL_API void mld_polyvec_matrix_pointwise_montgomery(mld_polyveck *t, mld_polymat *mat, const mld_polyvecl *v) @@ -329,7 +425,7 @@ void mld_polyvec_matrix_pointwise_montgomery(mld_polyveck *t, mld_polymat *mat, mld_polyvec_matrix_pointwise_montgomery_row(&t->vec[i], mat, v, i); } } -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API */ /* To facilitate single-compilation-unit (SCU) builds, undefine all macros. * Don't modify by hand -- this is auto-generated by scripts/autogen. */ diff --git a/mldsa/src/polyvec_lazy.h b/mldsa/src/polyvec_lazy.h index 4db4185ab..b04447890 100644 --- a/mldsa/src/polyvec_lazy.h +++ b/mldsa/src/polyvec_lazy.h @@ -57,6 +57,13 @@ #define mld_sk_t0hat_get_poly_eager \ MLD_ADD_PARAM_SET(mld_sk_t0hat_get_poly_eager) #define mld_sk_t0hat_get_poly_lazy MLD_ADD_PARAM_SET(mld_sk_t0hat_get_poly_lazy) +#define mld_zvec_eager MLD_ADD_PARAM_SET(mld_zvec_eager) +#define mld_zvec_lazy MLD_ADD_PARAM_SET(mld_zvec_lazy) +#define mld_zvec MLD_ADD_PARAM_SET(mld_zvec) +#define mld_zvec_init_eager MLD_ADD_PARAM_SET(mld_zvec_init_eager) +#define mld_zvec_init_lazy MLD_ADD_PARAM_SET(mld_zvec_init_lazy) +#define mld_zvec_get_poly_eager MLD_ADD_PARAM_SET(mld_zvec_get_poly_eager) +#define mld_zvec_get_poly_lazy MLD_ADD_PARAM_SET(mld_zvec_get_poly_lazy) #define mld_polymat MLD_ADD_PARAM_SET(mld_polymat) #define mld_polymat_eager MLD_ADD_PARAM_SET(mld_polymat_eager) #define mld_polymat_lazy MLD_ADD_PARAM_SET(mld_polymat_lazy) @@ -76,6 +83,10 @@ MLD_NAMESPACE_KL(polyvec_matrix_pointwise_montgomery_yvec_eager) #define mld_polyvec_matrix_pointwise_montgomery_yvec_lazy \ MLD_NAMESPACE_KL(polyvec_matrix_pointwise_montgomery_yvec_lazy) +#define mld_polyvec_matrix_pointwise_montgomery_zvec_eager \ + MLD_NAMESPACE_KL(polyvec_matrix_pointwise_montgomery_zvec_eager) +#define mld_polyvec_matrix_pointwise_montgomery_zvec_lazy \ + MLD_NAMESPACE_KL(polyvec_matrix_pointwise_montgomery_zvec_lazy) #define mld_yvec_eager MLD_ADD_PARAM_SET(mld_yvec_eager) #define mld_yvec_lazy MLD_ADD_PARAM_SET(mld_yvec_lazy) #define mld_yvec MLD_ADD_PARAM_SET(mld_yvec) @@ -385,6 +396,115 @@ __contract__( #endif /* !MLD_CONFIG_NO_SIGN_API && (MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST) \ */ +/* zvec: z polynomial vector from a signature. + * + * The infinity-norm bound check on z and the (in-place) NTT of z are + * performed at the boundary between unpack and use: + * - In eager mode, both happen in mld_zvec_init (the full vector is + * already in memory at that point). + * - In lazy mode, both happen in mld_zvec_get_poly per polynomial. + * + * Either may fail with MLD_ERR_FAIL if the norm bound is violated, so the + * matrix-vector multiplication helpers below need not repeat the check. */ + +/* Eager: precompute and store the full unpacked vector */ +typedef struct +{ + mld_polyvecl vec; +} mld_zvec_eager; + +/* Lazy: borrow packed data, unpack one polynomial on demand */ +typedef struct +{ + const uint8_t *packed; + mld_poly scratch; +} mld_zvec_lazy; + +#if !defined(MLD_CONFIG_NO_VERIFY_API) && \ + (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST)) +MLD_MUST_CHECK_RETURN_VALUE +static MLD_INLINE int mld_zvec_init_eager( + mld_zvec_eager *z, + const uint8_t packed_z[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES]) +__contract__( + requires(memory_no_alias(z, sizeof(mld_zvec_eager))) + requires(memory_no_alias(packed_z, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) + assigns(memory_slice(z, sizeof(mld_zvec_eager))) + ensures(return_value == 0 || return_value == MLD_ERR_FAIL) + ensures(return_value == 0 ==> + forall(k0, 0, MLDSA_L, + array_abs_bound(z->vec.vec[k0].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) +) +{ + mld_polyvecl_unpack_z(&z->vec, packed_z); + if (mld_polyvecl_chknorm(&z->vec, MLDSA_GAMMA1 - MLDSA_BETA)) + { + return MLD_ERR_FAIL; + } + mld_polyvecl_ntt(&z->vec); + return 0; +} + +MLD_MUST_CHECK_RETURN_VALUE +static MLD_INLINE int mld_zvec_get_poly_eager(mld_poly *buf, + const mld_zvec_eager *z, + unsigned int i) +__contract__( + requires(memory_no_alias(buf, sizeof(mld_poly))) + requires(memory_no_alias(z, sizeof(mld_zvec_eager))) + requires(i < MLDSA_L) + requires(array_abs_bound(z->vec.vec[i].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) + assigns(memory_slice(buf, sizeof(mld_poly))) + ensures(return_value == 0) + ensures(array_abs_bound(buf->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) +) +{ + *buf = z->vec.vec[i]; + return 0; +} +#endif /* !MLD_CONFIG_NO_VERIFY_API && (!MLD_CONFIG_REDUCE_RAM || \ + MLD_UNIT_TEST) */ +#if !defined(MLD_CONFIG_NO_VERIFY_API) && \ + (defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST)) +MLD_MUST_CHECK_RETURN_VALUE +static MLD_INLINE int mld_zvec_init_lazy( + mld_zvec_lazy *z, const uint8_t packed_z[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES]) +__contract__( + requires(memory_no_alias(z, sizeof(mld_zvec_lazy))) + assigns(memory_slice(z, sizeof(mld_zvec_lazy))) + ensures(z->packed == old(packed_z)) + ensures(return_value == 0) +) +{ + z->packed = packed_z; + return 0; +} + +MLD_MUST_CHECK_RETURN_VALUE +static MLD_INLINE int mld_zvec_get_poly_lazy(mld_poly *buf, mld_zvec_lazy *z, + unsigned int i) +__contract__( + requires(memory_no_alias(z, sizeof(mld_zvec_lazy))) + requires(buf == &z->scratch) + requires(i < MLDSA_L) + requires(memory_no_alias(z->packed, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) + assigns(memory_slice(buf, sizeof(mld_poly))) + ensures(return_value == 0 || return_value == MLD_ERR_FAIL) + ensures(return_value == 0 ==> + array_abs_bound(buf->coeffs, 0, MLDSA_N, MLD_NTT_BOUND)) +) +{ + mld_polyz_unpack(buf, z->packed + i * MLDSA_POLYZ_PACKEDBYTES); + if (mld_poly_chknorm(buf, MLDSA_GAMMA1 - MLDSA_BETA)) + { + return MLD_ERR_FAIL; + } + mld_poly_ntt(buf); + return 0; +} +#endif /* !MLD_CONFIG_NO_VERIFY_API && (MLD_CONFIG_REDUCE_RAM || \ + MLD_UNIT_TEST) */ + /* polymat */ #if !defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST) @@ -508,6 +628,40 @@ __contract__( array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) ); #endif /* !MLD_CONFIG_NO_SIGN_API */ + +#if !defined(MLD_CONFIG_NO_VERIFY_API) +/************************************************* + * Name: mld_polyvec_matrix_pointwise_montgomery_zvec_eager + * + * Description: Verify-side matrix-vector multiplication for the z + * polynomial vector. In eager mode, z is already NTT'd by + * mld_zvec_init_eager, so this delegates to the standard + * matrix-vector multiplication w = A * z (no invNTT). + * Always returns 0. + * + * Arguments: - mld_polyveck *w: pointer to output vector + * - mld_polymat_eager *mat: pointer to input matrix + * - mld_zvec_eager *z: NTT'd z vector + **************************************************/ +MLD_INTERNAL_API +MLD_MUST_CHECK_RETURN_VALUE +int mld_polyvec_matrix_pointwise_montgomery_zvec_eager(mld_polyveck *w, + mld_polymat_eager *mat, + mld_zvec_eager *z) +__contract__( + requires(memory_no_alias(w, sizeof(mld_polyveck))) + requires(memory_no_alias(mat, sizeof(mld_polymat_eager))) + requires(memory_no_alias(z, sizeof(mld_zvec_eager))) + requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L, + array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))) + requires(forall(l2, 0, MLDSA_L, + array_abs_bound(z->vec.vec[l2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND))) + assigns(memory_slice(w, sizeof(mld_polyveck))) + ensures(return_value == 0) + ensures(forall(k0, 0, MLDSA_K, + array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) +); +#endif /* !MLD_CONFIG_NO_VERIFY_API */ #endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */ #if defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST) @@ -520,7 +674,7 @@ __contract__( assigns(memory_slice(mat, sizeof(mld_polymat_lazy))) ); -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) /************************************************* * Name: mld_polyvec_matrix_pointwise_montgomery_row_lazy * @@ -553,7 +707,7 @@ __contract__( assigns(memory_slice(mat, sizeof(mld_polymat_lazy))) ensures(array_abs_bound(t_row->coeffs, 0, MLDSA_N, MLDSA_Q)) ); -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API */ #if !defined(MLD_CONFIG_NO_SIGN_API) /************************************************* @@ -592,6 +746,43 @@ __contract__( array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))) ); #endif /* !MLD_CONFIG_NO_SIGN_API */ + +#if !defined(MLD_CONFIG_NO_VERIFY_API) +/************************************************* + * Name: mld_polyvec_matrix_pointwise_montgomery_zvec_lazy + * + * Description: Verify-side matrix-vector multiplication for the z + * polynomial vector. Streams z one polynomial at a time + * into z->scratch (with norm check + NTT) and accumulates + * A[*,l] * NTT(z[l]) into w column-by-column. Matrix + * elements are sampled on demand via mat. + * + * Returns MLD_ERR_FAIL if any norm check on z[l] fails, + * 0 on success. + * + * Arguments: - mld_polyveck *w: pointer to output vector + * - mld_polymat_lazy *mat: pointer to (lazy) input matrix + * - mld_zvec_lazy *z: lazy z vector to be unpacked + **************************************************/ +MLD_INTERNAL_API +MLD_MUST_CHECK_RETURN_VALUE +int mld_polyvec_matrix_pointwise_montgomery_zvec_lazy(mld_polyveck *w, + mld_polymat_lazy *mat, + mld_zvec_lazy *z) +__contract__( + requires(memory_no_alias(w, sizeof(mld_polyveck))) + requires(memory_no_alias(mat, sizeof(mld_polymat_lazy))) + requires(memory_no_alias(z, sizeof(mld_zvec_lazy))) + requires(memory_no_alias(z->packed, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES)) + assigns(memory_slice(w, sizeof(mld_polyveck))) + assigns(memory_slice(mat, sizeof(mld_polymat_lazy))) + assigns(memory_slice(&z->scratch, sizeof(mld_poly))) + ensures(return_value == 0 || return_value == MLD_ERR_FAIL) + ensures(return_value == 0 ==> + forall(k0, 0, MLDSA_K, + array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) +); +#endif /* !MLD_CONFIG_NO_VERIFY_API */ #endif /* MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */ /* Dispatch: typedef and define based on MLD_CONFIG_REDUCE_RAM */ @@ -599,6 +790,7 @@ __contract__( typedef mld_sk_s1hat_lazy mld_sk_s1hat; typedef mld_sk_s2hat_lazy mld_sk_s2hat; typedef mld_sk_t0hat_lazy mld_sk_t0hat; +typedef mld_zvec_lazy mld_zvec; typedef mld_polymat_lazy mld_polymat; typedef mld_yvec_lazy mld_yvec; #define mld_unpack_sk_s1hat mld_unpack_sk_s1hat_lazy @@ -616,10 +808,15 @@ typedef mld_yvec_lazy mld_yvec; #define mld_yvec_get_poly mld_yvec_get_poly_lazy #define mld_polyvec_matrix_pointwise_montgomery_yvec \ mld_polyvec_matrix_pointwise_montgomery_yvec_lazy +#define mld_zvec_init mld_zvec_init_lazy +#define mld_zvec_get_poly mld_zvec_get_poly_lazy +#define mld_polyvec_matrix_pointwise_montgomery_zvec \ + mld_polyvec_matrix_pointwise_montgomery_zvec_lazy #else /* MLD_CONFIG_REDUCE_RAM */ typedef mld_sk_s1hat_eager mld_sk_s1hat; typedef mld_sk_s2hat_eager mld_sk_s2hat; typedef mld_sk_t0hat_eager mld_sk_t0hat; +typedef mld_zvec_eager mld_zvec; typedef mld_polymat_eager mld_polymat; typedef mld_yvec_eager mld_yvec; #define mld_unpack_sk_s1hat mld_unpack_sk_s1hat_eager @@ -637,9 +834,13 @@ typedef mld_yvec_eager mld_yvec; #define mld_yvec_get_poly mld_yvec_get_poly_eager #define mld_polyvec_matrix_pointwise_montgomery_yvec \ mld_polyvec_matrix_pointwise_montgomery_yvec_eager +#define mld_zvec_init mld_zvec_init_eager +#define mld_zvec_get_poly mld_zvec_get_poly_eager +#define mld_polyvec_matrix_pointwise_montgomery_zvec \ + mld_polyvec_matrix_pointwise_montgomery_zvec_eager #endif /* !MLD_CONFIG_REDUCE_RAM */ -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) /************************************************* * Name: mld_polyvec_matrix_pointwise_montgomery * @@ -676,7 +877,7 @@ __contract__( ensures(forall(k0, 0, MLDSA_K, array_abs_bound(t->vec[k0].coeffs, 0, MLDSA_N, MLDSA_Q))) ); -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API */ #endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_SIGN_API || \ !MLD_CONFIG_NO_VERIFY_API */ diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 797313a75..cbe381a60 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -1051,14 +1051,6 @@ 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; @@ -1073,18 +1065,17 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, 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(zcp, zcp_u, 1, context); + MLD_ALLOC(z, mld_zvec, 1, context); + MLD_ALLOC(cp, mld_poly, 1, context); MLD_ALLOC(w1, mld_polyveck, 1, context); MLD_ALLOC(reuse, reuse_u, 1, context); - if (buf == NULL || mu == NULL || c == NULL || c2 == NULL || zcp == NULL || - w1 == NULL || reuse == NULL) + if (buf == NULL || mu == NULL || c == NULL || c2 == NULL || z == NULL || + cp == 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; @@ -1096,11 +1087,13 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, } mld_memcpy(c, sig, MLDSA_CTILDEBYTES); - mld_polyvecl_unpack_z(z, sig + MLDSA_CTILDEBYTES); - /* mld_polyvecl_chknorm signals failure through a single non-zero error code + /* Eager: unpack z, norm-check it, and NTT in place (failure reported here). + * Lazy: just store the packed pointer; per-poly norm check is deferred + * to the matrix-vector multiplication helper. + * mld_zvec_init signals norm-check failure through a 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)) + if (mld_zvec_init(z, sig + MLDSA_CTILDEBYTES)) { ret = MLD_ERR_FAIL; goto cleanup; @@ -1123,10 +1116,16 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, mld_memcpy(mu, m, MLDSA_CRHBYTES); } - /* Matrix-vector multiplication; compute Az - c2^dt1 */ - mld_polyvecl_ntt(z); + /* Matrix-vector multiplication; compute Az - c2^dt1. + * In lazy mode, mld_polyvec_matrix_pointwise_montgomery_zvec performs the + * per-poly norm check on z and signals failure through a non-zero error + * code that's not yet aligned with MLD_ERR_XXX. Map it to MLD_ERR_FAIL. */ mld_polyvec_matrix_expand(mat, pk); - mld_polyvec_matrix_pointwise_montgomery(w1, mat, z); + if (mld_polyvec_matrix_pointwise_montgomery_zvec(w1, mat, z)) + { + ret = MLD_ERR_FAIL; + goto cleanup; + } mld_poly_challenge(cp, c); mld_poly_ntt(cp); @@ -1165,7 +1164,8 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen, /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ MLD_FREE(reuse, reuse_u, 1, context); MLD_FREE(w1, mld_polyveck, 1, context); - MLD_FREE(zcp, zcp_u, 1, context); + MLD_FREE(cp, mld_poly, 1, context); + MLD_FREE(z, mld_zvec, 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); diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common index a8acb5bf4..ea4a08bbc 100644 --- a/proofs/cbmc/Makefile.common +++ b/proofs/cbmc/Makefile.common @@ -462,12 +462,15 @@ USE_FUNCTION_CONTRACTS ?= LAZY_EAGER_FUNCTIONS = \ mld_polyvec_matrix_pointwise_montgomery_row \ mld_polyvec_matrix_pointwise_montgomery_yvec \ + mld_polyvec_matrix_pointwise_montgomery_zvec \ mld_polyvec_matrix_expand \ mld_sk_s1hat_get_poly \ mld_sk_s2hat_get_poly \ mld_sk_t0hat_get_poly \ mld_yvec_get_poly \ mld_yvec_init \ + mld_zvec_get_poly \ + mld_zvec_init \ mld_unpack_sk_s1hat \ mld_unpack_sk_s2hat \ mld_unpack_sk_t0hat diff --git a/proofs/cbmc/polyvec_matrix_pointwise_montgomery_zvec/Makefile b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_zvec/Makefile new file mode 100644 index 000000000..6f1beda5f --- /dev/null +++ b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_zvec/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 = polyvec_matrix_pointwise_montgomery_zvec_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 = polyvec_matrix_pointwise_montgomery_zvec + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec_lazy.c + +CHECK_FUNCTION_CONTRACTS=mld_polyvec_matrix_pointwise_montgomery_zvec +ifdef MLD_CONFIG_REDUCE_RAM +USE_FUNCTION_CONTRACTS=mld_zvec_get_poly +USE_FUNCTION_CONTRACTS+=mld_poly_pointwise_montgomery +USE_FUNCTION_CONTRACTS+=mld_polymat_expand_entry +USE_FUNCTION_CONTRACTS+=mld_poly_add +USE_FUNCTION_CONTRACTS+=mld_polyveck_reduce +USE_FUNCTION_CONTRACTS+=mld_zeroize +else +USE_FUNCTION_CONTRACTS=mld_polyvec_matrix_pointwise_montgomery_row +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 --arrays-uf-always + +FUNCTION_NAME = polyvec_matrix_pointwise_montgomery_zvec + +# 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/polyvec_matrix_pointwise_montgomery_zvec/polyvec_matrix_pointwise_montgomery_zvec_harness.c b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_zvec/polyvec_matrix_pointwise_montgomery_zvec_harness.c new file mode 100644 index 000000000..810c368dc --- /dev/null +++ b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_zvec/polyvec_matrix_pointwise_montgomery_zvec_harness.c @@ -0,0 +1,13 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "polyvec_lazy.h" + +void harness(void) +{ + mld_polyveck *w; + mld_polymat *mat; + mld_zvec *z; + int r; + r = mld_polyvec_matrix_pointwise_montgomery_zvec(w, mat, z); +} diff --git a/proofs/cbmc/polyvecl_unpack_z/Makefile b/proofs/cbmc/polyvecl_unpack_z/Makefile index e7b8fc85c..4fbd01d01 100644 --- a/proofs/cbmc/polyvecl_unpack_z/Makefile +++ b/proofs/cbmc/polyvecl_unpack_z/Makefile @@ -19,8 +19,13 @@ UNWINDSET += mld_polyvecl_unpack_z.0:7 # Largest value of MLDSA_L PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c +ifdef MLD_CONFIG_REDUCE_RAM +CHECK_FUNCTION_CONTRACTS= +USE_FUNCTION_CONTRACTS= +else CHECK_FUNCTION_CONTRACTS=mld_polyvecl_unpack_z USE_FUNCTION_CONTRACTS=mld_polyz_unpack +endif APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/proofs/cbmc/polyvecl_unpack_z/polyvecl_unpack_z_harness.c b/proofs/cbmc/polyvecl_unpack_z/polyvecl_unpack_z_harness.c index 4eede80ac..7715b4447 100644 --- a/proofs/cbmc/polyvecl_unpack_z/polyvecl_unpack_z_harness.c +++ b/proofs/cbmc/polyvecl_unpack_z/polyvecl_unpack_z_harness.c @@ -5,7 +5,9 @@ void harness(void) { +#if !defined(MLD_CONFIG_REDUCE_RAM) mld_polyvecl *a; uint8_t *b; mld_polyvecl_unpack_z(a, b); +#endif } diff --git a/proofs/cbmc/sign_verify_internal/Makefile b/proofs/cbmc/sign_verify_internal/Makefile index de78960cf..f37e9cbcd 100644 --- a/proofs/cbmc/sign_verify_internal/Makefile +++ b/proofs/cbmc/sign_verify_internal/Makefile @@ -22,13 +22,11 @@ PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c CHECK_FUNCTION_CONTRACTS=mld_verify_internal 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 USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_expand -USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_pointwise_montgomery -USE_FUNCTION_CONTRACTS+=mld_polyvecl_ntt +USE_FUNCTION_CONTRACTS+=mld_zvec_init +USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_pointwise_montgomery_zvec USE_FUNCTION_CONTRACTS+=mld_poly_ntt USE_FUNCTION_CONTRACTS+=mld_polyveck_shiftl USE_FUNCTION_CONTRACTS+=mld_polyveck_ntt diff --git a/proofs/cbmc/zvec_get_poly/Makefile b/proofs/cbmc/zvec_get_poly/Makefile new file mode 100644 index 000000000..ec121b5ee --- /dev/null +++ b/proofs/cbmc/zvec_get_poly/Makefile @@ -0,0 +1,59 @@ +# 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 = zvec_get_poly_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 = zvec_get_poly + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec_lazy.c + +CHECK_FUNCTION_CONTRACTS=mld_zvec_get_poly +ifdef MLD_CONFIG_REDUCE_RAM +USE_FUNCTION_CONTRACTS=mld_polyz_unpack +USE_FUNCTION_CONTRACTS+=mld_poly_chknorm +USE_FUNCTION_CONTRACTS+=mld_poly_ntt +else +USE_FUNCTION_CONTRACTS= +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 = zvec_get_poly + +# 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 = 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/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/zvec_get_poly/zvec_get_poly_harness.c b/proofs/cbmc/zvec_get_poly/zvec_get_poly_harness.c new file mode 100644 index 000000000..bea011c34 --- /dev/null +++ b/proofs/cbmc/zvec_get_poly/zvec_get_poly_harness.c @@ -0,0 +1,14 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "polyvec_lazy.h" + +void harness(void) +{ + mld_poly *buf; + mld_zvec *z; + unsigned int i; + int r; + + r = mld_zvec_get_poly(buf, z, i); +} diff --git a/proofs/cbmc/zvec_init/Makefile b/proofs/cbmc/zvec_init/Makefile new file mode 100644 index 000000000..0f2c35b6b --- /dev/null +++ b/proofs/cbmc/zvec_init/Makefile @@ -0,0 +1,59 @@ +# 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 = zvec_init_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 = zvec_init + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec_lazy.c + +CHECK_FUNCTION_CONTRACTS=mld_zvec_init +ifdef MLD_CONFIG_REDUCE_RAM +USE_FUNCTION_CONTRACTS= +else +USE_FUNCTION_CONTRACTS=mld_polyvecl_unpack_z +USE_FUNCTION_CONTRACTS+=mld_polyvecl_chknorm +USE_FUNCTION_CONTRACTS+=mld_polyvecl_ntt +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 = zvec_init + +# 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 = 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/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/zvec_init/zvec_init_harness.c b/proofs/cbmc/zvec_init/zvec_init_harness.c new file mode 100644 index 000000000..44a13475d --- /dev/null +++ b/proofs/cbmc/zvec_init/zvec_init_harness.c @@ -0,0 +1,13 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "polyvec_lazy.h" + +void harness(void) +{ + mld_zvec *z; + uint8_t *packed_z; + int r; + + r = mld_zvec_init(z, packed_z); +} diff --git a/test/src/test_unit.c b/test/src/test_unit.c index 484082808..c94dcd714 100644 --- a/test/src/test_unit.c +++ b/test/src/test_unit.c @@ -786,6 +786,34 @@ static int test_backend_units(void) MLD_USE_FIPS202_X1_NATIVE || MLD_USE_FIPS202_X4_NATIVE */ #if !defined(MLD_CONFIG_NO_SIGN_API) +#if !defined(MLD_CONFIG_NO_VERIFY_API) +/* Generate a random polyvecl with all coefficients in + * [-(MLDSA_GAMMA1 - MLDSA_BETA - 1), MLDSA_GAMMA1 - MLDSA_BETA - 1] + * and bit-pack it into MLDSA_L * MLDSA_POLYZ_PACKEDBYTES, so that the + * encoded data passes the chknorm bound used by mld_zvec_init/get_poly. */ +static void random_valid_packed_z( + uint8_t packed[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES]) +{ + unsigned int i, j; + mld_polyvecl z; + const int32_t bound = MLDSA_GAMMA1 - MLDSA_BETA; + const int32_t modulus = 2 * bound - 1; + randombytes((uint8_t *)&z, sizeof(z)); + for (i = 0; i < MLDSA_L; i++) + { + for (j = 0; j < MLDSA_N; j++) + { + int32_t c = z.vec[i].coeffs[j]; + /* Map to [-(bound - 1), bound - 1] */ + c = ((c % modulus) + modulus) % modulus - (bound - 1); + z.vec[i].coeffs[j] = c; + } + mld_polyz_pack(packed + i * MLDSA_POLYZ_PACKEDBYTES, &z.vec[i]); + } +} +#endif /* !MLD_CONFIG_NO_VERIFY_API */ + + /* Test that eager and lazy polyvec init+get produce the same results */ static int test_polyvec_lazy_eager(void) { @@ -793,6 +821,11 @@ static int test_polyvec_lazy_eager(void) uint8_t packed_s1[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES]; uint8_t packed_s2[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES]; uint8_t packed_t0[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES]; +#if !defined(MLD_CONFIG_NO_VERIFY_API) + uint8_t packed_z[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES]; + mld_zvec_eager z_eager; + mld_zvec_lazy z_lazy; +#endif uint8_t rho[MLDSA_SEEDBYTES]; uint8_t rhoprime[MLDSA_CRHBYTES]; mld_sk_s1hat_eager s1_eager; @@ -806,7 +839,7 @@ static int test_polyvec_lazy_eager(void) mld_poly poly_eager, poly_lazy; mld_polymat_eager mat_eager; mld_polymat_lazy mat_lazy; -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) unsigned int j; mld_polyvecl v; #endif @@ -850,9 +883,23 @@ static int test_polyvec_lazy_eager(void) mld_sk_t0hat_get_poly_lazy(&poly_lazy, &t0_lazy, i); CHECK(memcmp(&poly_eager, &poly_lazy, sizeof(mld_poly)) == 0); } + +#if !defined(MLD_CONFIG_NO_VERIFY_API) + /* Test zvec: eager vs lazy */ + random_valid_packed_z(packed_z); + CHECK(mld_zvec_init_eager(&z_eager, packed_z) == 0); + CHECK(mld_zvec_init_lazy(&z_lazy, packed_z) == 0); + + for (i = 0; i < MLDSA_L; i++) + { + CHECK(mld_zvec_get_poly_eager(&poly_eager, &z_eager, i) == 0); + CHECK(mld_zvec_get_poly_lazy(&z_lazy.scratch, &z_lazy, i) == 0); + CHECK(memcmp(&poly_eager, &z_lazy.scratch, sizeof(mld_poly)) == 0); + } +#endif /* !MLD_CONFIG_NO_VERIFY_API */ } -#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) +#if !defined(MLD_CONFIG_NO_KEYPAIR_API) /* Test row helpers: eager vs lazy. Both compute one row of A * v in * Montgomery (NTT domain), reduced mod q, but with different storage * strategies for A. */ @@ -883,7 +930,7 @@ static int test_polyvec_lazy_eager(void) CHECK(memcmp(&poly_eager, &poly_lazy, sizeof(mld_poly)) == 0); } } -#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */ +#endif /* !MLD_CONFIG_NO_KEYPAIR_API */ /* Test yvec: eager vs lazy. Verify that mld_yvec_get_poly_eager and * mld_yvec_get_poly_lazy produce the same y[i], and that the matrix-vector @@ -919,6 +966,33 @@ static int test_polyvec_lazy_eager(void) CHECK(memcmp(&w_eager, &w_lazy, sizeof(mld_polyveck)) == 0); } +#if !defined(MLD_CONFIG_NO_VERIFY_API) + /* Test the fused matrix-vector multiplication helper for z: + * eager and lazy variants must agree on w = A * NTT(z). */ + for (t = 0; t < NUM_RANDOM_TESTS_SLOW; t++) + { + randombytes(rho, sizeof(rho)); + mld_polyvec_matrix_expand_eager(&mat_eager, rho); + mld_polyvec_matrix_expand_lazy(&mat_lazy, rho); + + random_valid_packed_z(packed_z); + CHECK(mld_zvec_init_eager(&z_eager, packed_z) == 0); + CHECK(mld_zvec_init_lazy(&z_lazy, packed_z) == 0); + + CHECK(mld_polyvec_matrix_pointwise_montgomery_zvec_eager( + &w_eager, &mat_eager, &z_eager) == 0); + CHECK(mld_polyvec_matrix_pointwise_montgomery_zvec_lazy(&w_lazy, &mat_lazy, + &z_lazy) == 0); + + /* Compare mod q */ + mld_polyveck_reduce(&w_eager); + mld_polyveck_reduce(&w_lazy); + mld_polyveck_caddq(&w_eager); + mld_polyveck_caddq(&w_lazy); + CHECK(memcmp(&w_eager, &w_lazy, sizeof(mld_polyveck)) == 0); + } +#endif /* !MLD_CONFIG_NO_VERIFY_API */ + return 0; } #endif /* !MLD_CONFIG_NO_SIGN_API */