Skip to content

Commit e7893df

Browse files
hanno-beckerhanno-becker
committed
Define mlk_polyvec[_mulcache] as typedef for array
This commit changes the definition of `mlk_polyvec` from a struct wrapper `struct { mlk_poly vec[MLKEM_K] }` to a typedef for `mlk_poly[MLKEM_K]`. This ensures that when working with polynomial matrices -- that is, arrays of `mlk_polyvec`s -- the polynomial entries are consecutive in memory. This needs to be assumed for the correctness of `gen_matrix()`. From all we know, is a theoretical concern that without this change, compilers would be free to introduce padding into `mlk_polyvec`, breaking `gen_matrix()`. Yet, the behaviour of `gen_matrix` is strictly speaking UB, so it is better to change it. A slight nuisance is that when passing `mlk_polyvec *ptr` to a function, we have to take care to use `(*ptr)[i]` to access the i-th polynomial in the vector. The tempting `ptr[i]` would instead represent the `i * MLKEM_K`-th polynomial. Signed-off-by: Hanno Becker <[email protected]>
1 parent cc6c398 commit e7893df

File tree

4 files changed

+50
-62
lines changed

4 files changed

+50
-62
lines changed

‎mlkem/indcpa.c

Lines changed: 21 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,7 @@ void mlk_gen_matrix(mlk_polyvec *a, const uint8_t seed[MLKEM_SYMBYTES],
228228
* This call writes across mlk_polyvec boundaries for K=2 and K=3.
229229
* This is intentional and safe.
230230
*/
231-
mlk_poly_rej_uniform_x4(&a[0].vec[0] + i, seed_ext);
231+
mlk_poly_rej_uniform_x4((mlk_poly *)a + i, seed_ext);
232232
}
233233

234234
/* For MLKEM_K == 3, sample the last entry individually. */
@@ -249,7 +249,7 @@ void mlk_gen_matrix(mlk_polyvec *a, const uint8_t seed[MLKEM_SYMBYTES],
249249
seed_ext[0][MLKEM_SYMBYTES + 1] = x;
250250
}
251251

252-
mlk_poly_rej_uniform(&a[0].vec[0] + i, seed_ext[0]);
252+
mlk_poly_rej_uniform((mlk_poly *)a + i, seed_ext[0]);
253253
i++;
254254
}
255255

@@ -263,7 +263,7 @@ void mlk_gen_matrix(mlk_polyvec *a, const uint8_t seed[MLKEM_SYMBYTES],
263263
{
264264
for (j = 0; j < MLKEM_K; j++)
265265
{
266-
mlk_poly_permute_bitrev_to_custom(a[i].vec[j].coeffs);
266+
mlk_poly_permute_bitrev_to_custom(a[i][j].coeffs);
267267
}
268268
}
269269

@@ -298,7 +298,7 @@ __contract__(
298298
requires(memory_no_alias(vc, sizeof(mlk_polyvec_mulcache)))
299299
requires(forall(k0, 0, MLKEM_K,
300300
forall(k1, 0, MLKEM_K,
301-
array_bound(a[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))))
301+
array_bound(a[k0][k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))))
302302
assigns(object_whole(out)))
303303
{
304304
unsigned i;
@@ -307,7 +307,7 @@ __contract__(
307307
assigns(i, object_whole(out))
308308
invariant(i <= MLKEM_K))
309309
{
310-
mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a[i], v, vc);
310+
mlk_polyvec_basemul_acc_montgomery_cached(&(*out)[i], &a[i], v, vc);
311311
}
312312
}
313313

@@ -348,25 +348,23 @@ void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
348348
mlk_gen_matrix(a, publicseed, 0 /* no transpose */);
349349

350350
#if MLKEM_K == 2
351-
mlk_poly_getnoise_eta1_4x(skpv.vec + 0, skpv.vec + 1, e.vec + 0, e.vec + 1,
352-
noiseseed, 0, 1, 2, 3);
351+
mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &e[0], &e[1], noiseseed, 0, 1,
352+
2, 3);
353353
#elif MLKEM_K == 3
354354
/*
355355
* Only the first three output buffers are needed.
356356
* The laster parameter is a dummy that's overwritten later.
357357
*/
358-
mlk_poly_getnoise_eta1_4x(skpv.vec + 0, skpv.vec + 1, skpv.vec + 2,
359-
pkpv.vec + 0 /* irrelevant */, noiseseed, 0, 1, 2,
358+
mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2],
359+
&pkpv[0] /* irrelevant */, noiseseed, 0, 1, 2,
360360
0xFF /* irrelevant */);
361361
/* Same here */
362-
mlk_poly_getnoise_eta1_4x(e.vec + 0, e.vec + 1, e.vec + 2,
363-
pkpv.vec + 0 /* irrelevant */, noiseseed, 3, 4, 5,
364-
0xFF /* irrelevant */);
362+
mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &pkpv[0] /* irrelevant */,
363+
noiseseed, 3, 4, 5, 0xFF /* irrelevant */);
365364
#elif MLKEM_K == 4
366-
mlk_poly_getnoise_eta1_4x(skpv.vec + 0, skpv.vec + 1, skpv.vec + 2,
367-
skpv.vec + 3, noiseseed, 0, 1, 2, 3);
368-
mlk_poly_getnoise_eta1_4x(e.vec + 0, e.vec + 1, e.vec + 2, e.vec + 3,
369-
noiseseed, 4, 5, 6, 7);
365+
mlk_poly_getnoise_eta1_4x(&skpv[0], &skpv[1], &skpv[2], &skpv[3], noiseseed,
366+
0, 1, 2, 3);
367+
mlk_poly_getnoise_eta1_4x(&e[0], &e[1], &e[2], &e[3], noiseseed, 4, 5, 6, 7);
370368
#endif
371369

372370
mlk_polyvec_ntt(&skpv);
@@ -426,24 +424,21 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES],
426424
mlk_gen_matrix(at, seed, 1 /* transpose */);
427425

428426
#if MLKEM_K == 2
429-
mlk_poly_getnoise_eta1122_4x(sp.vec + 0, sp.vec + 1, ep.vec + 0, ep.vec + 1,
430-
coins, 0, 1, 2, 3);
427+
mlk_poly_getnoise_eta1122_4x(&sp[0], &sp[1], &ep[0], &ep[1], coins, 0, 1, 2,
428+
3);
431429
mlk_poly_getnoise_eta2(&epp, coins, 4);
432430
#elif MLKEM_K == 3
433431
/*
434432
* In this call, only the first three output buffers are needed.
435433
* The last parameter is a dummy that's overwritten later.
436434
*/
437-
mlk_poly_getnoise_eta1_4x(sp.vec + 0, sp.vec + 1, sp.vec + 2, &b.vec[0],
438-
coins, 0, 1, 2, 0xFF);
435+
mlk_poly_getnoise_eta1_4x(&sp[0], &sp[1], &sp[2], &b[0], coins, 0, 1, 2,
436+
0xFF);
439437
/* The fourth output buffer in this call _is_ used. */
440-
mlk_poly_getnoise_eta2_4x(ep.vec + 0, ep.vec + 1, ep.vec + 2, &epp, coins, 3,
441-
4, 5, 6);
438+
mlk_poly_getnoise_eta2_4x(&ep[0], &ep[1], &ep[2], &epp, coins, 3, 4, 5, 6);
442439
#elif MLKEM_K == 4
443-
mlk_poly_getnoise_eta1_4x(sp.vec + 0, sp.vec + 1, sp.vec + 2, sp.vec + 3,
444-
coins, 0, 1, 2, 3);
445-
mlk_poly_getnoise_eta2_4x(ep.vec + 0, ep.vec + 1, ep.vec + 2, ep.vec + 3,
446-
coins, 4, 5, 6, 7);
440+
mlk_poly_getnoise_eta1_4x(&sp[0], &sp[1], &sp[2], &sp[3], coins, 0, 1, 2, 3);
441+
mlk_poly_getnoise_eta2_4x(&ep[0], &ep[1], &ep[2], &ep[3], coins, 4, 5, 6, 7);
447442
mlk_poly_getnoise_eta2(&epp, coins, 8);
448443
#endif
449444

‎mlkem/indcpa.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ __contract__(
3737
requires(transposed == 0 || transposed == 1)
3838
assigns(object_whole(a))
3939
ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
40-
array_bound(a[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))));
40+
array_bound(a[x][y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))));
4141
);
4242

4343
#define mlk_indcpa_keypair_derand MLK_NAMESPACE_K(indcpa_keypair_derand)

‎mlkem/poly_k.c

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ void mlk_polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU],
3333

3434
for (i = 0; i < MLKEM_K; i++)
3535
{
36-
mlk_poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &a->vec[i]);
36+
mlk_poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &(*a)[i]);
3737
}
3838
}
3939

@@ -45,7 +45,7 @@ void mlk_polyvec_decompress_du(mlk_polyvec *r,
4545
unsigned i;
4646
for (i = 0; i < MLKEM_K; i++)
4747
{
48-
mlk_poly_decompress_du(&r->vec[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU);
48+
mlk_poly_decompress_du(&(*r)[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU);
4949
}
5050

5151
mlk_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
@@ -64,7 +64,7 @@ void mlk_polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const mlk_polyvec *a)
6464

6565
for (i = 0; i < MLKEM_K; i++)
6666
{
67-
mlk_poly_tobytes(r + i * MLKEM_POLYBYTES, &a->vec[i]);
67+
mlk_poly_tobytes(r + i * MLKEM_POLYBYTES, &(*a)[i]);
6868
}
6969
}
7070

@@ -75,7 +75,7 @@ void mlk_polyvec_frombytes(mlk_polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES])
7575
unsigned i;
7676
for (i = 0; i < MLKEM_K; i++)
7777
{
78-
mlk_poly_frombytes(&r->vec[i], a + i * MLKEM_POLYBYTES);
78+
mlk_poly_frombytes(&(*r)[i], a + i * MLKEM_POLYBYTES);
7979
}
8080

8181
mlk_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT);
@@ -88,7 +88,7 @@ void mlk_polyvec_ntt(mlk_polyvec *r)
8888
unsigned i;
8989
for (i = 0; i < MLKEM_K; i++)
9090
{
91-
mlk_poly_ntt(&r->vec[i]);
91+
mlk_poly_ntt(&(*r)[i]);
9292
}
9393

9494
mlk_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, MLK_NTT_BOUND);
@@ -105,7 +105,7 @@ void mlk_polyvec_invntt_tomont(mlk_polyvec *r)
105105
unsigned i;
106106
for (i = 0; i < MLKEM_K; i++)
107107
{
108-
mlk_poly_invntt_tomont(&r->vec[i]);
108+
mlk_poly_invntt_tomont(&(*r)[i]);
109109
}
110110

111111
mlk_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, MLK_INVNTT_BOUND);
@@ -143,10 +143,10 @@ void mlk_polyvec_basemul_acc_montgomery_cached(
143143
t[1] <= ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) &&
144144
t[1] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768)))
145145
{
146-
t[0] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i];
147-
t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i];
148-
t[1] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1];
149-
t[1] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i];
146+
t[0] += (int32_t)(*a)[k].coeffs[2 * i + 1] * (*b_cache)[k].coeffs[i];
147+
t[0] += (int32_t)(*a)[k].coeffs[2 * i] * (*b)[k].coeffs[2 * i];
148+
t[1] += (int32_t)(*a)[k].coeffs[2 * i] * (*b)[k].coeffs[2 * i + 1];
149+
t[1] += (int32_t)(*a)[k].coeffs[2 * i + 1] * (*b)[k].coeffs[2 * i];
150150
}
151151
r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]);
152152
r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]);
@@ -190,7 +190,7 @@ void mlk_polyvec_mulcache_compute(mlk_polyvec_mulcache *x, const mlk_polyvec *a)
190190
unsigned i;
191191
for (i = 0; i < MLKEM_K; i++)
192192
{
193-
mlk_poly_mulcache_compute(&x->vec[i], &a->vec[i]);
193+
mlk_poly_mulcache_compute(&(*x)[i], &(*a)[i]);
194194
}
195195
}
196196

@@ -207,7 +207,7 @@ void mlk_polyvec_reduce(mlk_polyvec *r)
207207
unsigned i;
208208
for (i = 0; i < MLKEM_K; i++)
209209
{
210-
mlk_poly_reduce(&r->vec[i]);
210+
mlk_poly_reduce(&(*r)[i]);
211211
}
212212

213213
mlk_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
@@ -222,7 +222,7 @@ void mlk_polyvec_add(mlk_polyvec *r, const mlk_polyvec *b)
222222
unsigned i;
223223
for (i = 0; i < MLKEM_K; i++)
224224
{
225-
mlk_poly_add(&r->vec[i], &b->vec[i]);
225+
mlk_poly_add(&(*r)[i], &(*b)[i]);
226226
}
227227
}
228228

@@ -233,7 +233,7 @@ void mlk_polyvec_tomont(mlk_polyvec *r)
233233
unsigned i;
234234
for (i = 0; i < MLKEM_K; i++)
235235
{
236-
mlk_poly_tomont(&r->vec[i]);
236+
mlk_poly_tomont(&(*r)[i]);
237237
}
238238

239239
mlk_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, MLKEM_Q);

‎mlkem/poly_k.h

Lines changed: 14 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -18,15 +18,8 @@
1818
#define mlk_polyvec_mulcache MLK_ADD_LEVEL(mlk_polyvec_mulcache)
1919
/* End of level namespacing */
2020

21-
typedef struct
22-
{
23-
mlk_poly vec[MLKEM_K];
24-
} MLK_ALIGN mlk_polyvec;
25-
26-
typedef struct
27-
{
28-
mlk_poly_mulcache vec[MLKEM_K];
29-
} mlk_polyvec_mulcache;
21+
typedef mlk_poly mlk_polyvec[MLKEM_K];
22+
typedef mlk_poly_mulcache mlk_polyvec_mulcache[MLKEM_K];
3023

3124
#define mlk_poly_compress_du MLK_NAMESPACE_K(poly_compress_du)
3225
/*************************************************
@@ -200,7 +193,7 @@ __contract__(
200193
requires(memory_no_alias(r, MLKEM_POLYVECCOMPRESSEDBYTES_DU))
201194
requires(memory_no_alias(a, sizeof(mlk_polyvec)))
202195
requires(forall(k0, 0, MLKEM_K,
203-
array_bound(a->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
196+
array_bound((*a)[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
204197
assigns(object_whole(r))
205198
);
206199

@@ -230,7 +223,7 @@ __contract__(
230223
requires(memory_no_alias(r, sizeof(mlk_polyvec)))
231224
assigns(object_whole(r))
232225
ensures(forall(k0, 0, MLKEM_K,
233-
array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
226+
array_bound((*r)[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
234227
);
235228

236229
#define mlk_polyvec_tobytes MLK_NAMESPACE_K(polyvec_tobytes)
@@ -256,7 +249,7 @@ __contract__(
256249
requires(memory_no_alias(a, sizeof(mlk_polyvec)))
257250
requires(memory_no_alias(r, MLKEM_POLYVECBYTES))
258251
requires(forall(k0, 0, MLKEM_K,
259-
array_bound(a->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
252+
array_bound((*a)[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
260253
assigns(object_whole(r))
261254
);
262255

@@ -285,7 +278,7 @@ __contract__(
285278
requires(memory_no_alias(a, MLKEM_POLYVECBYTES))
286279
assigns(object_whole(r))
287280
ensures(forall(k0, 0, MLKEM_K,
288-
array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
281+
array_bound((*r)[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
289282
);
290283

291284
#define mlk_polyvec_ntt MLK_NAMESPACE_K(polyvec_ntt)
@@ -312,10 +305,10 @@ void mlk_polyvec_ntt(mlk_polyvec *r)
312305
__contract__(
313306
requires(memory_no_alias(r, sizeof(mlk_polyvec)))
314307
requires(forall(j, 0, MLKEM_K,
315-
array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q)))
308+
array_abs_bound((*r)[j].coeffs, 0, MLKEM_N, MLKEM_Q)))
316309
assigns(object_whole(r))
317310
ensures(forall(j, 0, MLKEM_K,
318-
array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
311+
array_abs_bound((*r)[j].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
319312
);
320313

321314
#define mlk_polyvec_invntt_tomont MLK_NAMESPACE_K(polyvec_invntt_tomont)
@@ -344,7 +337,7 @@ __contract__(
344337
requires(memory_no_alias(r, sizeof(mlk_polyvec)))
345338
assigns(object_whole(r))
346339
ensures(forall(j, 0, MLKEM_K,
347-
array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND)))
340+
array_abs_bound((*r)[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND)))
348341
);
349342

350343
#define mlk_polyvec_basemul_acc_montgomery_cached \
@@ -383,7 +376,7 @@ __contract__(
383376
requires(memory_no_alias(b, sizeof(mlk_polyvec)))
384377
requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache)))
385378
requires(forall(k1, 0, MLKEM_K,
386-
array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
379+
array_bound((*a)[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
387380
assigns(object_whole(r))
388381
);
389382

@@ -453,7 +446,7 @@ __contract__(
453446
requires(memory_no_alias(r, sizeof(mlk_polyvec)))
454447
assigns(object_whole(r))
455448
ensures(forall(k0, 0, MLKEM_K,
456-
array_bound(r->vec[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
449+
array_bound((*r)[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
457450
);
458451

459452
#define mlk_polyvec_add MLK_NAMESPACE_K(polyvec_add)
@@ -486,10 +479,10 @@ __contract__(
486479
requires(memory_no_alias(b, sizeof(mlk_polyvec)))
487480
requires(forall(j0, 0, MLKEM_K,
488481
forall(k0, 0, MLKEM_N,
489-
(int32_t)r->vec[j0].coeffs[k0] + b->vec[j0].coeffs[k0] <= INT16_MAX)))
482+
(int32_t)(*r)[j0].coeffs[k0] + (*b)[j0].coeffs[k0] <= INT16_MAX)))
490483
requires(forall(j1, 0, MLKEM_K,
491484
forall(k1, 0, MLKEM_N,
492-
(int32_t)r->vec[j1].coeffs[k1] + b->vec[j1].coeffs[k1] >= INT16_MIN)))
485+
(int32_t)(*r)[j1].coeffs[k1] + (*b)[j1].coeffs[k1] >= INT16_MIN)))
493486
assigns(object_whole(r))
494487
);
495488

@@ -515,7 +508,7 @@ __contract__(
515508
assigns(memory_slice(r, sizeof(mlk_polyvec)))
516509
assigns(object_whole(r))
517510
ensures(forall(j, 0, MLKEM_K,
518-
array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLKEM_Q)))
511+
array_abs_bound((*r)[j].coeffs, 0, MLKEM_N, MLKEM_Q)))
519512
);
520513

521514
#define mlk_poly_getnoise_eta1_4x MLK_NAMESPACE_K(poly_getnoise_eta1_4x)

0 commit comments

Comments
 (0)