Skip to content

sign stack usage: compute z incrementally #825

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mkannwischer wants to merge 3 commits into
base: main
Choose a base branch
from
Open

sign stack usage: compute z incrementally #825

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
478a80b
sign stack usage: compute z incrementally
mkannwischer Dec 30, 2025
e2d613e
CBMC: Correct called contracts in verify_pre_hash_internal
mkannwischer Dec 31, 2025
5ecdabc
[SQUASH ME] Address review feedback
mkannwischer Jan 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 2 additions & 6 deletions mldsa/mldsa_native.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,8 @@
/* mldsa/src/packing.h */
#undef MLD_PACKING_H
#undef mld_pack_pk
#undef mld_pack_sig
#undef mld_pack_sig_c_h
#undef mld_pack_sig_z
#undef mld_pack_sk
#undef mld_unpack_pk
#undef mld_unpack_sig
Expand Down Expand Up @@ -298,15 +299,10 @@
#undef mld_polyveck_unpack_t0
#undef mld_polyveck_use_hint
#undef mld_polyvecl
#undef mld_polyvecl_add
#undef mld_polyvecl_chknorm
#undef mld_polyvecl_invntt_tomont
#undef mld_polyvecl_ntt
#undef mld_polyvecl_pack_eta
#undef mld_polyvecl_pack_z
#undef mld_polyvecl_pointwise_acc_montgomery
#undef mld_polyvecl_pointwise_poly_montgomery
#undef mld_polyvecl_reduce
#undef mld_polyvecl_uniform_gamma1
#undef mld_polyvecl_unpack_eta
#undef mld_polyvecl_unpack_z
Expand Down
8 changes: 2 additions & 6 deletions mldsa/mldsa_native.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -219,7 +219,8 @@
/* mldsa/src/packing.h */
#undef MLD_PACKING_H
#undef mld_pack_pk
#undef mld_pack_sig
#undef mld_pack_sig_c_h
#undef mld_pack_sig_z
#undef mld_pack_sk
#undef mld_unpack_pk
#undef mld_unpack_sig
Expand Down Expand Up @@ -294,15 +295,10 @@
#undef mld_polyveck_unpack_t0
#undef mld_polyveck_use_hint
#undef mld_polyvecl
#undef mld_polyvecl_add
#undef mld_polyvecl_chknorm
#undef mld_polyvecl_invntt_tomont
#undef mld_polyvecl_ntt
#undef mld_polyvecl_pack_eta
#undef mld_polyvecl_pack_z
#undef mld_polyvecl_pointwise_acc_montgomery
#undef mld_polyvecl_pointwise_poly_montgomery
#undef mld_polyvecl_reduce
#undef mld_polyvecl_uniform_gamma1
#undef mld_polyvecl_unpack_eta
#undef mld_polyvecl_unpack_z
Expand Down
17 changes: 13 additions & 4 deletions mldsa/src/packing.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,16 +99,16 @@ void mld_unpack_sk(uint8_t rho[MLDSA_SEEDBYTES], uint8_t tr[MLDSA_TRBYTES],
}

MLD_INTERNAL_API
void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyvecl *z,
const mld_polyveck *h, const unsigned int number_of_hints)
void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES],
const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,
const unsigned int number_of_hints)
{
unsigned int i, j, k;

mld_memcpy(sig, c, MLDSA_CTILDEBYTES);
sig += MLDSA_CTILDEBYTES;

mld_polyvecl_pack_z(sig, z);
/* skip z component - packed via mld_pack_sig_z */
sig += MLDSA_L * MLDSA_POLYZ_PACKEDBYTES;

/* Encode hints h */
Expand Down Expand Up @@ -168,6 +168,15 @@ void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
}
}

MLD_INTERNAL_API
void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
unsigned i)
{
sig += MLDSA_CTILDEBYTES;
sig += i * MLDSA_POLYZ_PACKEDBYTES;
mld_polyz_pack(sig, zi);
}

/*************************************************
* Name: mld_unpack_hints
*
Expand Down
41 changes: 31 additions & 10 deletions mldsa/src/packing.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,16 +69,16 @@ __contract__(
);


#define mld_pack_sig MLD_NAMESPACE_KL(pack_sig)
#define mld_pack_sig_c_h MLD_NAMESPACE_KL(pack_sig_c_h)
/*************************************************
* Name: mld_pack_sig
* Name: mld_pack_sig_c_h
*
* Description: Bit-pack signature sig = (c, z, h).
* Description: Bit-pack c and h component of sig = (c, z, h).
* The z component is packed separately using mld_pack_sig_z.
*
* Arguments: - uint8_t sig[]: output byte array
* - const uint8_t *c: pointer to challenge hash length
* MLDSA_SEEDBYTES
* - const mld_polyvecl *z: pointer to vector z
* - const mld_polyveck *h: pointer to hint vector h
* - const unsigned int number_of_hints: total
* hints in *h
Expand All @@ -88,22 +88,43 @@ __contract__(
* proof of type safety.
**************************************************/
MLD_INTERNAL_API
void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyvecl *z,
const mld_polyveck *h, const unsigned int number_of_hints)
void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES],
const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,
const unsigned int number_of_hints)
__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)))
requires(forall(k0, 0, MLDSA_L,
array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
requires(forall(k1, 0, MLDSA_K,
array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
requires(number_of_hints <= MLDSA_OMEGA)
assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
);

#define mld_pack_sig_z MLD_NAMESPACE_KL(pack_sig_z)
/*************************************************
* Name: mld_pack_sig_z
*
* Description: Bit-pack single polynomial of z component of sig = (c, z, h).
* The c and h components are packed separately using
* mld_pack_sig_c_h.
*
* Arguments: - uint8_t sig[]: output byte array
* - const mld_poly *zi: pointer to a single polynomial in z
* - const unsigned int i: index of zi in vector z
*
**************************************************/
MLD_INTERNAL_API
void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
unsigned i)
__contract__(
requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
requires(memory_no_alias(zi, sizeof(mld_poly)))
requires(i < MLDSA_L)
requires(array_bound(zi->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
);

#define mld_unpack_pk MLD_NAMESPACE_KL(unpack_pk)
/*************************************************
* Name: mld_unpack_pk
Expand Down
101 changes: 0 additions & 101 deletions mldsa/src/polyvec.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,50 +290,6 @@ void mld_polyvecl_uniform_gamma1(mld_polyvecl *v,
MLDSA_GAMMA1 + 1);
}

MLD_INTERNAL_API
void mld_polyvecl_reduce(mld_polyvecl *v)
{
unsigned int i;
mld_assert_bound_2d(v->vec, MLDSA_L, MLDSA_N, INT32_MIN,
MLD_REDUCE32_DOMAIN_MAX);

for (i = 0; i < MLDSA_L; ++i)
__loop__(
assigns(i, memory_slice(v, sizeof(mld_polyvecl)))
invariant(i <= MLDSA_L)
invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1])))
invariant(forall(k2, 0, i,
array_bound(v->vec[k2].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))))
{
mld_poly_reduce(&v->vec[i]);
}

mld_assert_bound_2d(v->vec, MLDSA_L, MLDSA_N, -MLD_REDUCE32_RANGE_MAX,
MLD_REDUCE32_RANGE_MAX);
}

/* Reference: We use destructive version (output=first input) to avoid
* reasoning about aliasing in the CBMC specification */
MLD_INTERNAL_API
void mld_polyvecl_add(mld_polyvecl *u, const mld_polyvecl *v)
{
unsigned int i;

for (i = 0; i < MLDSA_L; ++i)
__loop__(
assigns(i, memory_slice(u, sizeof(mld_polyvecl)))
invariant(i <= MLDSA_L)
invariant(forall(k0, i, MLDSA_L,
forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1])))
invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX)))
)
{
mld_poly_add(&u->vec[i], &v->vec[i]);
}
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, INT32_MIN,
MLD_REDUCE32_DOMAIN_MAX);
}

MLD_INTERNAL_API
void mld_polyvecl_ntt(mld_polyvecl *v)
{
Expand All @@ -353,46 +309,6 @@ void mld_polyvecl_ntt(mld_polyvecl *v)
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
}

MLD_INTERNAL_API
void mld_polyvecl_invntt_tomont(mld_polyvecl *v)
{
unsigned int i;
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLDSA_Q);

for (i = 0; i < MLDSA_L; ++i)
__loop__(
assigns(i, memory_slice(v, sizeof(mld_polyvecl)))
invariant(i <= MLDSA_L)
invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1])))
invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))))
{
mld_poly_invntt_tomont(&v->vec[i]);
}

mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_INTT_BOUND);
}

MLD_INTERNAL_API
void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a,
const mld_polyvecl *v)
{
unsigned int i;
mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);

for (i = 0; i < MLDSA_L; ++i)
__loop__(
assigns(i, memory_slice(r, sizeof(mld_polyvecl)))
invariant(i <= MLDSA_L)
invariant(forall(k2, 0, i, array_abs_bound(r->vec[k2].coeffs, 0, MLDSA_N, MLDSA_Q)))
)
{
mld_poly_pointwise_montgomery(&r->vec[i], a, &v->vec[i]);
}

mld_assert_abs_bound_2d(r->vec, MLDSA_L, MLDSA_N, MLDSA_Q);
}

MLD_STATIC_TESTABLE void mld_polyvecl_pointwise_acc_montgomery_c(
mld_poly *w, const mld_polyvecl *u, const mld_polyvecl *v)
__contract__(
Expand Down Expand Up @@ -858,23 +774,6 @@ void mld_polyvecl_pack_eta(uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES],
}
}

MLD_INTERNAL_API
void mld_polyvecl_pack_z(uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES],
const mld_polyvecl *p)
{
unsigned int i;
mld_assert_bound_2d(p->vec, MLDSA_L, MLDSA_N, -(MLDSA_GAMMA1 - 1),
MLDSA_GAMMA1 + 1);
for (i = 0; i < MLDSA_L; ++i)
__loop__(
assigns(i, memory_slice(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES))
invariant(i <= MLDSA_L)
)
{
mld_polyz_pack(&r[i * MLDSA_POLYZ_PACKEDBYTES], &p->vec[i]);
}
}

MLD_INTERNAL_API
void mld_polyveck_pack_t0(uint8_t r[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES],
const mld_polyveck *p)
Expand Down
Loading