@@ -368,13 +368,13 @@ __contract__(
368368 for (i = 0 ; i < MLKEM_K ; i ++ )
369369 __loop__ (
370370 assigns (i , object_whole (out ))
371- invariant (i <= MLKEM_K ))
371+ invariant (i <= MLKEM_K )
372372 invariant (forall (k , 0 , i ,
373- array_abs_bound (out [k ].coeffs , 0 , MLKEM_N , INT16_MAX /2 ))))
374- {
375- mlk_polyvec_basemul_acc_montgomery_cached ( & out -> vec [ i ], & a -> vec [ i ], v ,
376- vc );
377- }
373+ array_abs_bound (out [k ].coeffs , 0 , MLKEM_N , INT16_MAX /2 )))
374+ )
375+ {
376+ mlk_polyvec_basemul_acc_montgomery_cached ( & out -> vec [ i ], & a -> vec [ i ], v , vc );
377+ }
378378}
379379
380380/* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF].
@@ -425,7 +425,7 @@ int mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
425425 */
426426 MLK_CT_TESTING_DECLASSIFY (publicseed , MLKEM_SYMBYTES );
427427
428- mlk_gen_matrix (& a , publicseed , 0 /* no transpose */ );
428+ mlk_gen_matrix (a , publicseed , 0 /* no transpose */ );
429429
430430#if MLKEM_K == 2
431431 mlk_poly_getnoise_eta1_4x (& skpv -> vec [0 ], & skpv -> vec [1 ], & e -> vec [0 ],
@@ -449,19 +449,19 @@ int mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
449449 noiseseed , 4 , 5 , 6 , 7 );
450450#endif /* MLKEM_K == 4 */
451451
452- mlk_polyvec_ntt (& skpv );
453- mlk_polyvec_ntt (& e );
452+ mlk_polyvec_ntt (skpv );
453+ mlk_polyvec_ntt (e );
454454
455- mlk_polyvec_mulcache_compute (& skpv_cache , & skpv );
456- mlk_matvec_mul (& pkpv , & a , & skpv , & skpv_cache );
457- mlk_polyvec_tomont (& pkpv );
455+ mlk_polyvec_mulcache_compute (skpv_cache , skpv );
456+ mlk_matvec_mul (pkpv , a , skpv , skpv_cache );
457+ mlk_polyvec_tomont (pkpv );
458458
459- mlk_polyvec_add (& pkpv , & e );
460- mlk_polyvec_reduce (& pkpv );
461- mlk_polyvec_reduce (& skpv );
459+ mlk_polyvec_add (pkpv , e );
460+ mlk_polyvec_reduce (pkpv );
461+ mlk_polyvec_reduce (skpv );
462462
463- mlk_pack_sk (sk , & skpv );
464- mlk_pack_pk (pk , & pkpv , publicseed );
463+ mlk_pack_sk (sk , skpv );
464+ mlk_pack_pk (pk , pkpv , publicseed );
465465
466466cleanup :
467467 /* Specification: Partially implements
@@ -520,7 +520,7 @@ int mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES],
520520 */
521521 MLK_CT_TESTING_DECLASSIFY (seed , MLKEM_SYMBYTES );
522522
523- mlk_gen_matrix (& at , seed , 1 /* transpose */ );
523+ mlk_gen_matrix (at , seed , 1 /* transpose */ );
524524
525525#if MLKEM_K == 2
526526 mlk_poly_getnoise_eta1122_4x (& sp -> vec [0 ], & sp -> vec [1 ], & ep -> vec [0 ],
@@ -544,7 +544,7 @@ int mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES],
544544 mlk_poly_getnoise_eta2 (epp , coins , 8 );
545545#endif /* MLKEM_K == 4 */
546546
547- mlk_polyvec_ntt (& sp );
547+ mlk_polyvec_ntt (sp );
548548
549549 mlk_polyvec_mulcache_compute (sp_cache , sp );
550550 mlk_matvec_mul (b , at , sp , sp_cache );
0 commit comments