@@ -34,9 +34,9 @@ MLK_INTERNAL_DATA_DECLARATION const int16_t
3434 mlk_aarch64_zetas_mulcache_twisted_native [128 ];
3535MLK_INTERNAL_DATA_DECLARATION const uint8_t mlk_rej_uniform_table [4096 ];
3636
37- #define mlk_ntt_asm MLK_NAMESPACE(ntt_asm )
38- void mlk_ntt_asm (int16_t p [256 ], const int16_t twiddles12345 [80 ],
39- const int16_t twiddles56 [384 ])
37+ #define mlk_ntt_aarch64_asm MLK_NAMESPACE(ntt_aarch64_asm )
38+ void mlk_ntt_aarch64_asm (int16_t p [256 ], const int16_t twiddles12345 [80 ],
39+ const int16_t twiddles56 [384 ])
4040/* This must be kept in sync with the HOL-Light specification
4141 * in proofs/hol_light/aarch64/proofs/mlkem_ntt.ml */
4242__contract__ (
@@ -50,9 +50,9 @@ __contract__(
5050 /* check-magic: on */
5151);
5252
53- #define mlk_intt_asm MLK_NAMESPACE(intt_asm )
54- void mlk_intt_asm (int16_t p [256 ], const int16_t twiddles12345 [80 ],
55- const int16_t twiddles56 [384 ])
53+ #define mlk_intt_aarch64_asm MLK_NAMESPACE(intt_aarch64_asm )
54+ void mlk_intt_aarch64_asm (int16_t p [256 ], const int16_t twiddles12345 [80 ],
55+ const int16_t twiddles56 [384 ])
5656/* This must be kept in sync with the HOL-Light specification
5757 * in proofs/hol_light/aarch64/proofs/mlkem_intt.ml */
5858__contract__ (
@@ -65,8 +65,8 @@ __contract__(
6565 /* check-magic: on */
6666);
6767
68- #define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm )
69- void mlk_poly_reduce_asm (int16_t p [256 ])
68+ #define mlk_poly_reduce_aarch64_asm MLK_NAMESPACE(poly_reduce_aarch64_asm )
69+ void mlk_poly_reduce_aarch64_asm (int16_t p [256 ])
7070/* This must be kept in sync with the HOL-Light specification
7171 * in proofs/hol_light/aarch64/proofs/mlkem_poly_reduce.ml */
7272__contract__ (
@@ -75,8 +75,8 @@ __contract__(
7575 ensures (array_bound (p , 0 , MLKEM_N , 0 , MLKEM_Q ))
7676);
7777
78- #define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm )
79- void mlk_poly_tomont_asm (int16_t p [256 ])
78+ #define mlk_poly_tomont_aarch64_asm MLK_NAMESPACE(poly_tomont_aarch64_asm )
79+ void mlk_poly_tomont_aarch64_asm (int16_t p [256 ])
8080/* This must be kept in sync with the HOL-Light specification
8181 * in proofs/hol_light/aarch64/proofs/mlkem_poly_tomont.ml */
8282__contract__ (
@@ -85,11 +85,12 @@ __contract__(
8585 ensures (array_abs_bound (p , 0 , MLKEM_N , MLKEM_Q ))
8686);
8787
88- #define mlk_poly_mulcache_compute_asm MLK_NAMESPACE(poly_mulcache_compute_asm)
89- void mlk_poly_mulcache_compute_asm (int16_t cache [128 ],
90- const int16_t mlk_poly [256 ],
91- const int16_t zetas [128 ],
92- const int16_t zetas_twisted [128 ])
88+ #define mlk_poly_mulcache_compute_aarch64_asm \
89+ MLK_NAMESPACE(poly_mulcache_compute_aarch64_asm)
90+ void mlk_poly_mulcache_compute_aarch64_asm (int16_t cache [128 ],
91+ const int16_t mlk_poly [256 ],
92+ const int16_t zetas [128 ],
93+ const int16_t zetas_twisted [128 ])
9394/* This must be kept in sync with the HOL-Light specification
9495 * in proofs/hol_light/aarch64/proofs/mlkem_poly_mulcache_compute.ml */
9596__contract__ (
@@ -101,8 +102,8 @@ __contract__(
101102 ensures (array_abs_bound (cache , 0 , MLKEM_N /2 , MLKEM_Q ))
102103);
103104
104- #define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm )
105- void mlk_poly_tobytes_asm (uint8_t r [384 ], const int16_t a [256 ])
105+ #define mlk_poly_tobytes_aarch64_asm MLK_NAMESPACE(poly_tobytes_aarch64_asm )
106+ void mlk_poly_tobytes_aarch64_asm (uint8_t r [384 ], const int16_t a [256 ])
106107/* This must be kept in sync with the HOL-Light specification
107108 * in proofs/hol_light/aarch64/proofs/mlkem_poly_tobytes.ml */
108109__contract__ (
@@ -112,9 +113,9 @@ __contract__(
112113 assigns (memory_slice (r , MLKEM_POLYBYTES ))
113114);
114115
115- #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
116- MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2 )
117- void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 (
116+ #define mlk_polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm \
117+ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm )
118+ void mlk_polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm (
118119 int16_t r [256 ], const int16_t a [512 ], const int16_t b [512 ],
119120 const int16_t b_cache [256 ])
120121/* This must be kept in sync with the HOL-Light specification in
@@ -129,9 +130,9 @@ __contract__(
129130 assigns (memory_slice (r , sizeof (int16_t ) * MLKEM_N ))
130131);
131132
132- #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
133- MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3 )
134- void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 (
133+ #define mlk_polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm \
134+ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm )
135+ void mlk_polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm (
135136 int16_t r [256 ], const int16_t a [768 ], const int16_t b [768 ],
136137 const int16_t b_cache [384 ])
137138/* This must be kept in sync with the HOL-Light specification in
@@ -146,9 +147,9 @@ __contract__(
146147 assigns (memory_slice (r , sizeof (int16_t ) * MLKEM_N ))
147148);
148149
149- #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
150- MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4 )
151- void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 (
150+ #define mlk_polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm \
151+ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm )
152+ void mlk_polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm (
152153 int16_t r [256 ], const int16_t a [1024 ], const int16_t b [1024 ],
153154 const int16_t b_cache [512 ])
154155/* This must be kept in sync with the HOL-Light specification in
@@ -163,10 +164,10 @@ __contract__(
163164 assigns (memory_slice (r , sizeof (int16_t ) * MLKEM_N ))
164165);
165166
166- #define mlk_rej_uniform_asm MLK_NAMESPACE (rej_uniform_asm )
167+ #define mlk_rej_uniform_aarch64_asm MLK_NAMESPACE (rej_uniform_aarch64_asm )
167168MLK_MUST_CHECK_RETURN_VALUE
168- uint64_t mlk_rej_uniform_asm (int16_t r [256 ], const uint8_t * buf ,
169- unsigned buflen , const uint8_t table [4096 ])
169+ uint64_t mlk_rej_uniform_aarch64_asm (int16_t r [256 ], const uint8_t * buf ,
170+ unsigned buflen , const uint8_t table [4096 ])
170171/* This must be kept in sync with the HOL-Light specification
171172 * in proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml. */
172173__contract__ (
0 commit comments