36
36
* and the public seed used to generate the matrix A.
37
37
*
38
38
* Arguments: uint8_t *r: pointer to the output serialized public key
39
- * mlk_polyvec * pk: pointer to the input public-key mlk_polyvec.
39
+ * mlk_polyvec pk: pointer to the input public-key mlk_polyvec.
40
40
* Must have coefficients within [0,..,q-1].
41
41
* const uint8_t *seed: pointer to the input public seed
42
42
*
43
43
* Specification:
44
44
* Implements [FIPS 203, Algorithm 13 (K-PKE.KeyGen), L19]
45
45
*
46
46
**************************************************/
47
- static void mlk_pack_pk (uint8_t r [MLKEM_INDCPA_PUBLICKEYBYTES ], mlk_polyvec * pk ,
47
+ static void mlk_pack_pk (uint8_t r [MLKEM_INDCPA_PUBLICKEYBYTES ], mlk_polyvec pk ,
48
48
const uint8_t seed [MLKEM_SYMBYTES ])
49
49
{
50
50
mlk_assert_bound_2d (pk , MLKEM_K , MLKEM_N , 0 , MLKEM_Q );
@@ -58,7 +58,7 @@ static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], mlk_polyvec *pk,
58
58
* Description: De-serialize public key from a byte array;
59
59
* approximate inverse of mlk_pack_pk
60
60
*
61
- * Arguments: - mlk_polyvec * pk: pointer to output public-key polynomial
61
+ * Arguments: - mlk_polyvec pk: pointer to output public-key polynomial
62
62
* vector Coefficients will be normalized to [0,..,q-1].
63
63
* - uint8_t *seed: pointer to output seed to generate matrix A
64
64
* - const uint8_t *packedpk: pointer to input serialized public
@@ -68,7 +68,7 @@ static void mlk_pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], mlk_polyvec *pk,
68
68
* Implements [FIPS 203, Algorithm 14 (K-PKE.Encrypt), L2-3]
69
69
*
70
70
**************************************************/
71
- static void mlk_unpack_pk (mlk_polyvec * pk , uint8_t seed [MLKEM_SYMBYTES ],
71
+ static void mlk_unpack_pk (mlk_polyvec pk , uint8_t seed [MLKEM_SYMBYTES ],
72
72
const uint8_t packedpk [MLKEM_INDCPA_PUBLICKEYBYTES ])
73
73
{
74
74
mlk_polyvec_frombytes (pk , packedpk );
@@ -86,14 +86,14 @@ static void mlk_unpack_pk(mlk_polyvec *pk, uint8_t seed[MLKEM_SYMBYTES],
86
86
* Description: Serialize the secret key
87
87
*
88
88
* Arguments: - uint8_t *r: pointer to output serialized secret key
89
- * - mlk_polyvec * sk: pointer to input vector of polynomials
89
+ * - mlk_polyvec sk: pointer to input vector of polynomials
90
90
* (secret key)
91
91
*
92
92
* Specification:
93
93
* Implements [FIPS 203, Algorithm 13 (K-PKE.KeyGen), L20]
94
94
*
95
95
**************************************************/
96
- static void mlk_pack_sk (uint8_t r [MLKEM_INDCPA_SECRETKEYBYTES ], mlk_polyvec * sk )
96
+ static void mlk_pack_sk (uint8_t r [MLKEM_INDCPA_SECRETKEYBYTES ], mlk_polyvec sk )
97
97
{
98
98
mlk_assert_bound_2d (sk , MLKEM_K , MLKEM_N , 0 , MLKEM_Q );
99
99
mlk_polyvec_tobytes (r , sk );
@@ -104,7 +104,7 @@ static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], mlk_polyvec *sk)
104
104
*
105
105
* Description: De-serialize the secret key; inverse of mlk_pack_sk
106
106
*
107
- * Arguments: - mlk_polyvec * sk: pointer to output vector of polynomials
107
+ * Arguments: - mlk_polyvec sk: pointer to output vector of polynomials
108
108
* (secret key)
109
109
* - const uint8_t *packedsk: pointer to input serialized secret
110
110
* key
@@ -113,7 +113,7 @@ static void mlk_pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], mlk_polyvec *sk)
113
113
* Implements [FIPS 203, Algorithm 15 (K-PKE.Decrypt), L5]
114
114
*
115
115
**************************************************/
116
- static void mlk_unpack_sk (mlk_polyvec * sk ,
116
+ static void mlk_unpack_sk (mlk_polyvec sk ,
117
117
const uint8_t packedsk [MLKEM_INDCPA_SECRETKEYBYTES ])
118
118
{
119
119
mlk_polyvec_frombytes (sk , packedsk );
@@ -134,7 +134,7 @@ static void mlk_unpack_sk(mlk_polyvec *sk,
134
134
* Implements [FIPS 203, Algorithm 14 (K-PKE.Encrypt), L22-23]
135
135
*
136
136
**************************************************/
137
- static void mlk_pack_ciphertext (uint8_t r [MLKEM_INDCPA_BYTES ], mlk_polyvec * b ,
137
+ static void mlk_pack_ciphertext (uint8_t r [MLKEM_INDCPA_BYTES ], mlk_polyvec b ,
138
138
mlk_poly * v )
139
139
{
140
140
mlk_polyvec_compress_du (r , b );
@@ -147,15 +147,15 @@ static void mlk_pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], mlk_polyvec *b,
147
147
* Description: De-serialize and decompress ciphertext from a byte array;
148
148
* approximate inverse of mlk_pack_ciphertext
149
149
*
150
- * Arguments: - mlk_polyvec * b: pointer to the output vector of polynomials b
150
+ * Arguments: - mlk_polyvec b: pointer to the output vector of polynomials b
151
151
* - mlk_poly *v: pointer to the output polynomial v
152
152
* - const uint8_t *c: pointer to the input serialized ciphertext
153
153
*
154
154
* Specification:
155
155
* Implements [FIPS 203, Algorithm 15 (K-PKE.Decrypt), L1-4]
156
156
*
157
157
**************************************************/
158
- static void mlk_unpack_ciphertext (mlk_polyvec * b , mlk_poly * v ,
158
+ static void mlk_unpack_ciphertext (mlk_polyvec b , mlk_poly * v ,
159
159
const uint8_t c [MLKEM_INDCPA_BYTES ])
160
160
{
161
161
mlk_polyvec_decompress_du (b , c );
@@ -186,7 +186,7 @@ __contract__(
186
186
*
187
187
* Not static for benchmarking */
188
188
MLK_INTERNAL_API
189
- void mlk_gen_matrix (mlk_polyvec * a , const uint8_t seed [MLKEM_SYMBYTES ],
189
+ void mlk_gen_matrix (mlk_polymat a , const uint8_t seed [MLKEM_SYMBYTES ],
190
190
int transposed )
191
191
{
192
192
unsigned i , j ;
@@ -228,7 +228,7 @@ void mlk_gen_matrix(mlk_polyvec *a, const uint8_t seed[MLKEM_SYMBYTES],
228
228
* This call writes across mlk_polyvec boundaries for K=2 and K=3.
229
229
* This is intentional and safe.
230
230
*/
231
- mlk_poly_rej_uniform_x4 (& a [0 ]. vec [ 0 ] + i , seed_ext );
231
+ mlk_poly_rej_uniform_x4 (& a [i ] , seed_ext );
232
232
}
233
233
234
234
/* 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],
249
249
seed_ext [0 ][MLKEM_SYMBYTES + 1 ] = x ;
250
250
}
251
251
252
- mlk_poly_rej_uniform (& a [0 ]. vec [ 0 ] + i , seed_ext [0 ]);
252
+ mlk_poly_rej_uniform (& a [i ] , seed_ext [0 ]);
253
253
i ++ ;
254
254
}
255
255
@@ -259,12 +259,9 @@ void mlk_gen_matrix(mlk_polyvec *a, const uint8_t seed[MLKEM_SYMBYTES],
259
259
* The public matrix is generated in NTT domain. If the native backend
260
260
* uses a custom order in NTT domain, permute A accordingly.
261
261
*/
262
- for (i = 0 ; i < MLKEM_K ; i ++ )
262
+ for (i = 0 ; i < MLKEM_K * MLKEM_K ; i ++ )
263
263
{
264
- for (j = 0 ; j < MLKEM_K ; j ++ )
265
- {
266
- mlk_poly_permute_bitrev_to_custom (a [i ].vec [j ].coeffs );
267
- }
264
+ mlk_poly_permute_bitrev_to_custom (a [i ].coeffs );
268
265
}
269
266
270
267
/* Specification: Partially implements
@@ -278,27 +275,26 @@ void mlk_gen_matrix(mlk_polyvec *a, const uint8_t seed[MLKEM_SYMBYTES],
278
275
* Description: Computes matrix-vector product in NTT domain,
279
276
* via Montgomery multiplication.
280
277
*
281
- * Arguments: - mlk_polyvec * out: Pointer to output polynomial vector
282
- * - mlk_polyvec a[MLKEM_K] : Input matrix. Must be in NTT domain
278
+ * Arguments: - mlk_polyvec out: Pointer to output polynomial vector
279
+ * - mlk_polymat a : Input matrix. Must be in NTT domain
283
280
* and have coefficients of absolute value < 4096.
284
- * - mlk_polyvec * v: Input polynomial vector. Must be in NTT
281
+ * - mlk_polyvec v: Input polynomial vector. Must be in NTT
285
282
* domain.
286
- * - mlk_polyvec * vc: Mulcache for v, computed via
283
+ * - mlk_polyvec vc: Mulcache for v, computed via
287
284
* mlk_polyvec_mulcache_compute().
288
285
*
289
286
* Specification: Implements [FIPS 203, Section 2.4.7, Eq (2.12), (2.13)]
290
287
*
291
288
**************************************************/
292
- static void mlk_matvec_mul (mlk_polyvec * out , const mlk_polyvec a [ MLKEM_K ] ,
293
- const mlk_polyvec * v , const mlk_polyvec_mulcache * vc )
289
+ static void mlk_matvec_mul (mlk_polyvec out , const mlk_polymat a ,
290
+ const mlk_polyvec v , const mlk_polyvec_mulcache vc )
294
291
__contract__ (
295
292
requires (memory_no_alias (out , sizeof (mlk_polyvec )))
296
- requires (memory_no_alias (a , sizeof (mlk_polyvec ) * MLKEM_K ))
293
+ requires (memory_no_alias (a , sizeof (mlk_polymat ) ))
297
294
requires (memory_no_alias (v , sizeof (mlk_polyvec )))
298
295
requires (memory_no_alias (vc , sizeof (mlk_polyvec_mulcache )))
299
- requires (forall (k0 , 0 , MLKEM_K ,
300
- forall (k1 , 0 , MLKEM_K ,
301
- array_bound (a [k0 ].vec [k1 ].coeffs , 0 , MLKEM_N , 0 , MLKEM_UINT12_LIMIT ))))
296
+ requires (forall (k0 , 0 , MLKEM_K * MLKEM_K ,
297
+ array_bound (a [k0 ].coeffs , 0 , MLKEM_N , 0 , MLKEM_UINT12_LIMIT )))
302
298
assigns (object_whole (out )))
303
299
{
304
300
unsigned i ;
@@ -307,7 +303,7 @@ __contract__(
307
303
assigns (i , object_whole (out ))
308
304
invariant (i <= MLKEM_K ))
309
305
{
310
- mlk_polyvec_basemul_acc_montgomery_cached (& out -> vec [i ], & a [i ], v , vc );
306
+ mlk_polyvec_basemul_acc_montgomery_cached (& out [i ], & a [MLKEM_K * i ], v , vc );
311
307
}
312
308
}
313
309
@@ -327,7 +323,8 @@ void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
327
323
MLK_ALIGN uint8_t buf [2 * MLKEM_SYMBYTES ];
328
324
const uint8_t * publicseed = buf ;
329
325
const uint8_t * noiseseed = buf + MLKEM_SYMBYTES ;
330
- mlk_polyvec a [MLKEM_K ], e , pkpv , skpv ;
326
+ mlk_polymat a ;
327
+ mlk_polyvec e , pkpv , skpv ;
331
328
mlk_polyvec_mulcache skpv_cache ;
332
329
333
330
MLK_ALIGN uint8_t coins_with_domain_separator [MLKEM_SYMBYTES + 1 ];
@@ -348,40 +345,38 @@ void mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
348
345
mlk_gen_matrix (a , publicseed , 0 /* no transpose */ );
349
346
350
347
#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 );
348
+ mlk_poly_getnoise_eta1_4x (& skpv [ 0 ], & skpv [ 1 ], & e [ 0 ], & e [ 1 ], noiseseed , 0 , 1 ,
349
+ 2 , 3 );
353
350
#elif MLKEM_K == 3
354
351
/*
355
352
* Only the first three output buffers are needed.
356
353
* The laster parameter is a dummy that's overwritten later.
357
354
*/
358
- mlk_poly_getnoise_eta1_4x (skpv . vec + 0 , skpv . vec + 1 , skpv . vec + 2 ,
359
- pkpv . vec + 0 /* irrelevant */ , noiseseed , 0 , 1 , 2 ,
355
+ mlk_poly_getnoise_eta1_4x (& skpv [ 0 ], & skpv [ 1 ], & skpv [ 2 ] ,
356
+ & pkpv [ 0 ] /* irrelevant */ , noiseseed , 0 , 1 , 2 ,
360
357
0xFF /* irrelevant */ );
361
358
/* 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 */ );
359
+ mlk_poly_getnoise_eta1_4x (& e [0 ], & e [1 ], & e [2 ], & pkpv [0 ] /* irrelevant */ ,
360
+ noiseseed , 3 , 4 , 5 , 0xFF /* irrelevant */ );
365
361
#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 );
362
+ mlk_poly_getnoise_eta1_4x (& skpv [0 ], & skpv [1 ], & skpv [2 ], & skpv [3 ], noiseseed ,
363
+ 0 , 1 , 2 , 3 );
364
+ mlk_poly_getnoise_eta1_4x (& e [0 ], & e [1 ], & e [2 ], & e [3 ], noiseseed , 4 , 5 , 6 , 7 );
370
365
#endif
371
366
372
- mlk_polyvec_ntt (& skpv );
373
- mlk_polyvec_ntt (& e );
367
+ mlk_polyvec_ntt (skpv );
368
+ mlk_polyvec_ntt (e );
374
369
375
- mlk_polyvec_mulcache_compute (& skpv_cache , & skpv );
376
- mlk_matvec_mul (& pkpv , a , & skpv , & skpv_cache );
377
- mlk_polyvec_tomont (& pkpv );
370
+ mlk_polyvec_mulcache_compute (skpv_cache , skpv );
371
+ mlk_matvec_mul (pkpv , a , skpv , skpv_cache );
372
+ mlk_polyvec_tomont (pkpv );
378
373
379
- mlk_polyvec_add (& pkpv , & e );
380
- mlk_polyvec_reduce (& pkpv );
381
- mlk_polyvec_reduce (& skpv );
374
+ mlk_polyvec_add (pkpv , e );
375
+ mlk_polyvec_reduce (pkpv );
376
+ mlk_polyvec_reduce (skpv );
382
377
383
- mlk_pack_sk (sk , & skpv );
384
- mlk_pack_pk (pk , & pkpv , publicseed );
378
+ mlk_pack_sk (sk , skpv );
379
+ mlk_pack_pk (pk , pkpv , publicseed );
385
380
386
381
/* Specification: Partially implements
387
382
* [FIPS 203, Section 3.3, Destruction of intermediate values] */
@@ -408,11 +403,12 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES],
408
403
const uint8_t coins [MLKEM_SYMBYTES ])
409
404
{
410
405
MLK_ALIGN uint8_t seed [MLKEM_SYMBYTES ];
411
- mlk_polyvec sp , pkpv , ep , at [MLKEM_K ], b ;
406
+ mlk_polymat at ;
407
+ mlk_polyvec sp , pkpv , ep , b ;
412
408
mlk_poly v , k , epp ;
413
409
mlk_polyvec_mulcache sp_cache ;
414
410
415
- mlk_unpack_pk (& pkpv , seed , pk );
411
+ mlk_unpack_pk (pkpv , seed , pk );
416
412
mlk_poly_frommsg (& k , m );
417
413
418
414
/*
@@ -426,44 +422,41 @@ void mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES],
426
422
mlk_gen_matrix (at , seed , 1 /* transpose */ );
427
423
428
424
#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 );
425
+ mlk_poly_getnoise_eta1122_4x (& sp [ 0 ], & sp [ 1 ], & ep [ 0 ], & ep [ 1 ], coins , 0 , 1 , 2 ,
426
+ 3 );
431
427
mlk_poly_getnoise_eta2 (& epp , coins , 4 );
432
428
#elif MLKEM_K == 3
433
429
/*
434
430
* In this call, only the first three output buffers are needed.
435
431
* The last parameter is a dummy that's overwritten later.
436
432
*/
437
- mlk_poly_getnoise_eta1_4x (sp . vec + 0 , sp . vec + 1 , sp . vec + 2 , & b . vec [0 ],
438
- coins , 0 , 1 , 2 , 0xFF );
433
+ mlk_poly_getnoise_eta1_4x (& sp [ 0 ], & sp [ 1 ], & sp [ 2 ] , & b [0 ], coins , 0 , 1 , 2 ,
434
+ 0xFF );
439
435
/* 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 );
436
+ mlk_poly_getnoise_eta2_4x (& ep [0 ], & ep [1 ], & ep [2 ], & epp , coins , 3 , 4 , 5 , 6 );
442
437
#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 );
438
+ mlk_poly_getnoise_eta1_4x (& sp [0 ], & sp [1 ], & sp [2 ], & sp [3 ], coins , 0 , 1 , 2 , 3 );
439
+ mlk_poly_getnoise_eta2_4x (& ep [0 ], & ep [1 ], & ep [2 ], & ep [3 ], coins , 4 , 5 , 6 , 7 );
447
440
mlk_poly_getnoise_eta2 (& epp , coins , 8 );
448
441
#endif
449
442
450
- mlk_polyvec_ntt (& sp );
443
+ mlk_polyvec_ntt (sp );
451
444
452
- mlk_polyvec_mulcache_compute (& sp_cache , & sp );
453
- mlk_matvec_mul (& b , at , & sp , & sp_cache );
454
- mlk_polyvec_basemul_acc_montgomery_cached (& v , & pkpv , & sp , & sp_cache );
445
+ mlk_polyvec_mulcache_compute (sp_cache , sp );
446
+ mlk_matvec_mul (b , at , sp , sp_cache );
447
+ mlk_polyvec_basemul_acc_montgomery_cached (& v , pkpv , sp , sp_cache );
455
448
456
- mlk_polyvec_invntt_tomont (& b );
449
+ mlk_polyvec_invntt_tomont (b );
457
450
mlk_poly_invntt_tomont (& v );
458
451
459
- mlk_polyvec_add (& b , & ep );
452
+ mlk_polyvec_add (b , ep );
460
453
mlk_poly_add (& v , & epp );
461
454
mlk_poly_add (& v , & k );
462
455
463
- mlk_polyvec_reduce (& b );
456
+ mlk_polyvec_reduce (b );
464
457
mlk_poly_reduce (& v );
465
458
466
- mlk_pack_ciphertext (c , & b , & v );
459
+ mlk_pack_ciphertext (c , b , & v );
467
460
468
461
/* Specification: Partially implements
469
462
* [FIPS 203, Section 3.3, Destruction of intermediate values] */
@@ -490,12 +483,12 @@ void mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES],
490
483
mlk_poly v , sb ;
491
484
mlk_polyvec_mulcache b_cache ;
492
485
493
- mlk_unpack_ciphertext (& b , & v , c );
494
- mlk_unpack_sk (& skpv , sk );
486
+ mlk_unpack_ciphertext (b , & v , c );
487
+ mlk_unpack_sk (skpv , sk );
495
488
496
- mlk_polyvec_ntt (& b );
497
- mlk_polyvec_mulcache_compute (& b_cache , & b );
498
- mlk_polyvec_basemul_acc_montgomery_cached (& sb , & skpv , & b , & b_cache );
489
+ mlk_polyvec_ntt (b );
490
+ mlk_polyvec_mulcache_compute (b_cache , b );
491
+ mlk_polyvec_basemul_acc_montgomery_cached (& sb , skpv , b , b_cache );
499
492
mlk_poly_invntt_tomont (& sb );
500
493
501
494
mlk_poly_sub (& v , & sb );
0 commit comments