Skip to content

Commit ecedcd3

Browse files
mkannwischermkannwischer
committed
sign stack usage: compute z incrementally
This commit reduces the stack usage of signing by computing z = y + s1*cp incrementally (one polynomial at a time) allowing to eliminate the polyvecl z (at to cost of a single poly z). The computation of z is moved into a separate function (compute_pack_z) to vastly speed up the CBMC proofs. De-facto this saves L-1 KB irrespective of MLD_CONFIG_REDUCE_RAM. Practically, the same buffer was used early in the function too. Here we instead introduce a new polyvecl buffer tmp, but that can be placed in a union together with w1. Unfortuantely, with the current struct workaround for diffblue/cbmc#8813, this results in an increase in stack space by L KB. This gets eliminated when MLD_CONFIG_REDUCE_RAM is set. Hoisted out from #791 Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 75ab215 commit ecedcd3

File tree

21 files changed

+225
-525
lines changed

21 files changed

+225
-525
lines changed

‎mldsa/mldsa_native.S‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -223,7 +223,8 @@
223223
/* mldsa/src/packing.h */
224224
#undef MLD_PACKING_H
225225
#undef mld_pack_pk
226-
#undef mld_pack_sig
226+
#undef mld_pack_sig_c_h
227+
#undef mld_pack_sig_z
227228
#undef mld_pack_sk
228229
#undef mld_unpack_pk
229230
#undef mld_unpack_sig
@@ -298,15 +299,10 @@
298299
#undef mld_polyveck_unpack_t0
299300
#undef mld_polyveck_use_hint
300301
#undef mld_polyvecl
301-
#undef mld_polyvecl_add
302302
#undef mld_polyvecl_chknorm
303-
#undef mld_polyvecl_invntt_tomont
304303
#undef mld_polyvecl_ntt
305304
#undef mld_polyvecl_pack_eta
306-
#undef mld_polyvecl_pack_z
307305
#undef mld_polyvecl_pointwise_acc_montgomery
308-
#undef mld_polyvecl_pointwise_poly_montgomery
309-
#undef mld_polyvecl_reduce
310306
#undef mld_polyvecl_uniform_gamma1
311307
#undef mld_polyvecl_unpack_eta
312308
#undef mld_polyvecl_unpack_z

‎mldsa/mldsa_native.c‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -219,7 +219,8 @@
219219
/* mldsa/src/packing.h */
220220
#undef MLD_PACKING_H
221221
#undef mld_pack_pk
222-
#undef mld_pack_sig
222+
#undef mld_pack_sig_c_h
223+
#undef mld_pack_sig_z
223224
#undef mld_pack_sk
224225
#undef mld_unpack_pk
225226
#undef mld_unpack_sig
@@ -294,15 +295,10 @@
294295
#undef mld_polyveck_unpack_t0
295296
#undef mld_polyveck_use_hint
296297
#undef mld_polyvecl
297-
#undef mld_polyvecl_add
298298
#undef mld_polyvecl_chknorm
299-
#undef mld_polyvecl_invntt_tomont
300299
#undef mld_polyvecl_ntt
301300
#undef mld_polyvecl_pack_eta
302-
#undef mld_polyvecl_pack_z
303301
#undef mld_polyvecl_pointwise_acc_montgomery
304-
#undef mld_polyvecl_pointwise_poly_montgomery
305-
#undef mld_polyvecl_reduce
306302
#undef mld_polyvecl_uniform_gamma1
307303
#undef mld_polyvecl_unpack_eta
308304
#undef mld_polyvecl_unpack_z

‎mldsa/src/packing.c‎

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -99,16 +99,16 @@ void mld_unpack_sk(uint8_t rho[MLDSA_SEEDBYTES], uint8_t tr[MLDSA_TRBYTES],
9999
}
100100

101101
MLD_INTERNAL_API
102-
void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
103-
const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyvecl *z,
104-
const mld_polyveck *h, const unsigned int number_of_hints)
102+
void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES],
103+
const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,
104+
const unsigned int number_of_hints)
105105
{
106106
unsigned int i, j, k;
107107

108108
mld_memcpy(sig, c, MLDSA_CTILDEBYTES);
109109
sig += MLDSA_CTILDEBYTES;
110110

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

114114
/* Encode hints h */
@@ -168,6 +168,15 @@ void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
168168
}
169169
}
170170

171+
MLD_INTERNAL_API
172+
void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
173+
unsigned i)
174+
{
175+
sig += MLDSA_CTILDEBYTES;
176+
sig += i * MLDSA_POLYZ_PACKEDBYTES;
177+
mld_polyz_pack(sig, zi);
178+
}
179+
171180
/*************************************************
172181
* Name: mld_unpack_hints
173182
*

‎mldsa/src/packing.h‎

Lines changed: 31 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -69,16 +69,16 @@ __contract__(
6969
);
7070

7171

72-
#define mld_pack_sig MLD_NAMESPACE_KL(pack_sig)
72+
#define mld_pack_sig_c_h MLD_NAMESPACE_KL(pack_sig_c_h)
7373
/*************************************************
74-
* Name: mld_pack_sig
74+
* Name: mld_pack_sig_c_h
7575
*
76-
* Description: Bit-pack signature sig = (c, z, h).
76+
* Description: Bit-pack c and h component of sig = (c, z, h).
77+
* The z component is packed separately using mld_pack_sig_z.
7778
*
7879
* Arguments: - uint8_t sig[]: output byte array
7980
* - const uint8_t *c: pointer to challenge hash length
8081
* MLDSA_SEEDBYTES
81-
* - const mld_polyvecl *z: pointer to vector z
8282
* - const mld_polyveck *h: pointer to hint vector h
8383
* - const unsigned int number_of_hints: total
8484
* hints in *h
@@ -88,22 +88,43 @@ __contract__(
8888
* proof of type safety.
8989
**************************************************/
9090
MLD_INTERNAL_API
91-
void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
92-
const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyvecl *z,
93-
const mld_polyveck *h, const unsigned int number_of_hints)
91+
void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES],
92+
const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,
93+
const unsigned int number_of_hints)
9494
__contract__(
9595
requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
9696
requires(memory_no_alias(c, MLDSA_CTILDEBYTES))
97-
requires(memory_no_alias(z, sizeof(mld_polyvecl)))
9897
requires(memory_no_alias(h, sizeof(mld_polyveck)))
99-
requires(forall(k0, 0, MLDSA_L,
100-
array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
10198
requires(forall(k1, 0, MLDSA_K,
10299
array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
103100
requires(number_of_hints <= MLDSA_OMEGA)
104101
assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
105102
);
106103

104+
#define mld_pack_sig_z MLD_NAMESPACE_KL(pack_sig_z)
105+
/*************************************************
106+
* Name: mld_pack_sig_z
107+
*
108+
* Description: Bit-pack single polynomial of z component of sig = (c, z, h).
109+
* The c and h components are packed separately using
110+
* mld_pack_sig_c_h.
111+
*
112+
* Arguments: - uint8_t sig[]: output byte array
113+
* - const mld_poly *zi: pointer to a single polynomial in z
114+
* - const unsigned int i: index of zi in vector z
115+
*
116+
**************************************************/
117+
MLD_INTERNAL_API
118+
void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
119+
unsigned i)
120+
__contract__(
121+
requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
122+
requires(memory_no_alias(zi, sizeof(mld_poly)))
123+
requires(i < MLDSA_L)
124+
requires(array_bound(zi->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
125+
assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
126+
);
127+
107128
#define mld_unpack_pk MLD_NAMESPACE_KL(unpack_pk)
108129
/*************************************************
109130
* Name: mld_unpack_pk

‎mldsa/src/polyvec.c‎

Lines changed: 0 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -290,50 +290,6 @@ void mld_polyvecl_uniform_gamma1(mld_polyvecl *v,
290290
MLDSA_GAMMA1 + 1);
291291
}
292292

293-
MLD_INTERNAL_API
294-
void mld_polyvecl_reduce(mld_polyvecl *v)
295-
{
296-
unsigned int i;
297-
mld_assert_bound_2d(v->vec, MLDSA_L, MLDSA_N, INT32_MIN,
298-
MLD_REDUCE32_DOMAIN_MAX);
299-
300-
for (i = 0; i < MLDSA_L; ++i)
301-
__loop__(
302-
assigns(i, memory_slice(v, sizeof(mld_polyvecl)))
303-
invariant(i <= MLDSA_L)
304-
invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1])))
305-
invariant(forall(k2, 0, i,
306-
array_bound(v->vec[k2].coeffs, 0, MLDSA_N, -MLD_REDUCE32_RANGE_MAX, MLD_REDUCE32_RANGE_MAX))))
307-
{
308-
mld_poly_reduce(&v->vec[i]);
309-
}
310-
311-
mld_assert_bound_2d(v->vec, MLDSA_L, MLDSA_N, -MLD_REDUCE32_RANGE_MAX,
312-
MLD_REDUCE32_RANGE_MAX);
313-
}
314-
315-
/* Reference: We use destructive version (output=first input) to avoid
316-
* reasoning about aliasing in the CBMC specification */
317-
MLD_INTERNAL_API
318-
void mld_polyvecl_add(mld_polyvecl *u, const mld_polyvecl *v)
319-
{
320-
unsigned int i;
321-
322-
for (i = 0; i < MLDSA_L; ++i)
323-
__loop__(
324-
assigns(i, memory_slice(u, sizeof(mld_polyvecl)))
325-
invariant(i <= MLDSA_L)
326-
invariant(forall(k0, i, MLDSA_L,
327-
forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1])))
328-
invariant(forall(k6, 0, i, array_bound(u->vec[k6].coeffs, 0, MLDSA_N, INT32_MIN, MLD_REDUCE32_DOMAIN_MAX)))
329-
)
330-
{
331-
mld_poly_add(&u->vec[i], &v->vec[i]);
332-
}
333-
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, INT32_MIN,
334-
MLD_REDUCE32_DOMAIN_MAX);
335-
}
336-
337293
MLD_INTERNAL_API
338294
void mld_polyvecl_ntt(mld_polyvecl *v)
339295
{
@@ -353,46 +309,6 @@ void mld_polyvecl_ntt(mld_polyvecl *v)
353309
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
354310
}
355311

356-
MLD_INTERNAL_API
357-
void mld_polyvecl_invntt_tomont(mld_polyvecl *v)
358-
{
359-
unsigned int i;
360-
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLDSA_Q);
361-
362-
for (i = 0; i < MLDSA_L; ++i)
363-
__loop__(
364-
assigns(i, memory_slice(v, sizeof(mld_polyvecl)))
365-
invariant(i <= MLDSA_L)
366-
invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1])))
367-
invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, MLD_INTT_BOUND))))
368-
{
369-
mld_poly_invntt_tomont(&v->vec[i]);
370-
}
371-
372-
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_INTT_BOUND);
373-
}
374-
375-
MLD_INTERNAL_API
376-
void mld_polyvecl_pointwise_poly_montgomery(mld_polyvecl *r, const mld_poly *a,
377-
const mld_polyvecl *v)
378-
{
379-
unsigned int i;
380-
mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
381-
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
382-
383-
for (i = 0; i < MLDSA_L; ++i)
384-
__loop__(
385-
assigns(i, memory_slice(r, sizeof(mld_polyvecl)))
386-
invariant(i <= MLDSA_L)
387-
invariant(forall(k2, 0, i, array_abs_bound(r->vec[k2].coeffs, 0, MLDSA_N, MLDSA_Q)))
388-
)
389-
{
390-
mld_poly_pointwise_montgomery(&r->vec[i], a, &v->vec[i]);
391-
}
392-
393-
mld_assert_abs_bound_2d(r->vec, MLDSA_L, MLDSA_N, MLDSA_Q);
394-
}
395-
396312
MLD_STATIC_TESTABLE void mld_polyvecl_pointwise_acc_montgomery_c(
397313
mld_poly *w, const mld_polyvecl *u, const mld_polyvecl *v)
398314
__contract__(
@@ -858,23 +774,6 @@ void mld_polyvecl_pack_eta(uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES],
858774
}
859775
}
860776

861-
MLD_INTERNAL_API
862-
void mld_polyvecl_pack_z(uint8_t r[MLDSA_L * MLDSA_POLYZ_PACKEDBYTES],
863-
const mld_polyvecl *p)
864-
{
865-
unsigned int i;
866-
mld_assert_bound_2d(p->vec, MLDSA_L, MLDSA_N, -(MLDSA_GAMMA1 - 1),
867-
MLDSA_GAMMA1 + 1);
868-
for (i = 0; i < MLDSA_L; ++i)
869-
__loop__(
870-
assigns(i, memory_slice(r, MLDSA_L * MLDSA_POLYZ_PACKEDBYTES))
871-
invariant(i <= MLDSA_L)
872-
)
873-
{
874-
mld_polyz_pack(&r[i * MLDSA_POLYZ_PACKEDBYTES], &p->vec[i]);
875-
}
876-
}
877-
878777
MLD_INTERNAL_API
879778
void mld_polyveck_pack_t0(uint8_t r[MLDSA_K * MLDSA_POLYT0_PACKEDBYTES],
880779
const mld_polyveck *p)

0 commit comments

Comments
 (0)