@@ -70,44 +70,44 @@ jobs:
7070 gh_token : ${{ secrets.GITHUB_TOKEN }}
7171 nix-shell : ' hol_light'
7272 script : |
73- make -C proofs/hol_light/aarch64 mlkem/mlkem_poly_tobytes .o
74- echo 'needs "aarch64/proofs/mlkem_poly_tobytes .ml";;' | hol.sh
73+ make -C proofs/hol_light/aarch64 mlkem/poly_tobytes_aarch64_asm .o
74+ echo 'needs "aarch64/proofs/poly_tobytes_aarch64_asm .ml";;' | hol.sh
7575hol_light_proofs :
7676 needs : [ hol_light_bytecode ]
7777 strategy :
7878 fail-fast : false
7979 matrix :
8080 proof :
8181 # Dependencies on {name}.{S,ml} are implicit
82- - name : mlkem_ntt
82+ - name : ntt_aarch64_asm
8383 needs : ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
84- - name : mlkem_intt
84+ - name : intt_aarch64_asm
8585 needs : ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
86- - name : mlkem_poly_tomont
86+ - name : poly_tomont_aarch64_asm
8787 needs : ["mlkem_specs.ml", "mlkem_utils.ml"]
88- - name : mlkem_poly_mulcache_compute
88+ - name : poly_mulcache_compute_aarch64_asm
8989 needs : ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
90- - name : mlkem_poly_reduce
90+ - name : poly_reduce_aarch64_asm
9191 needs : ["mlkem_specs.ml", "mlkem_utils.ml"]
92- - name : mlkem_poly_basemul_acc_montgomery_cached_k2
92+ - name : polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm
9393 needs : ["mlkem_specs.ml", "mlkem_utils.ml"]
94- - name : mlkem_poly_basemul_acc_montgomery_cached_k3
94+ - name : polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm
9595 needs : ["mlkem_specs.ml", "mlkem_utils.ml"]
96- - name : mlkem_poly_basemul_acc_montgomery_cached_k4
96+ - name : polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm
9797 needs : ["mlkem_specs.ml", "mlkem_utils.ml"]
98- - name : mlkem_poly_tobytes
98+ - name : poly_tobytes_aarch64_asm
9999 needs : ["mlkem_specs.ml", "mlkem_utils.ml" ]
100- - name : mlkem_rej_uniform
100+ - name : rej_uniform_aarch64_asm
101101 needs : ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_rej_uniform_table.ml"]
102- - name : keccak_f1600_x1_scalar
102+ - name : keccak_f1600_x1_scalar_aarch64_asm
103103 needs : ["keccak_specs.ml"]
104- - name : keccak_f1600_x1_v84a
104+ - name : keccak_f1600_x1_v84a_aarch64_asm
105105 needs : ["keccak_specs.ml"]
106- - name : keccak_f1600_x2_v84a
106+ - name : keccak_f1600_x2_v84a_aarch64_asm
107107 needs : ["keccak_specs.ml"]
108- - name : keccak_f1600_x4_v8a_v84a_scalar
108+ - name : keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm
109109 needs : ["keccak_specs.ml"]
110- - name : keccak_f1600_x4_v8a_scalar
110+ - name : keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
111111 needs : ["keccak_specs.ml"]
112112 name : AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
113113 runs-on : pqcp-arm64
@@ -178,56 +178,56 @@ jobs:
178178 gh_token : ${{ secrets.GITHUB_TOKEN }}
179179 nix-shell : ' hol_light'
180180 script : |
181- make -C proofs/hol_light/x86_64 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2 .o
182- echo 'needs "x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2 .ml";;' | hol.sh
181+ make -C proofs/hol_light/x86_64 mlkem/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm .o
182+ echo 'needs "x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm .ml";;' | hol.sh
183183hol_light_proofs_x86_64 :
184184 needs : [ hol_light_bytecode_x86_64 ]
185185 strategy :
186186 fail-fast : false
187187 matrix :
188188 proof :
189189 # Dependencies on {name}.{S,ml} are implicit
190- - name : mlkem_ntt
190+ - name : ntt_avx2_asm
191191 needs : ["mlkem_specs.ml", "mlkem_zetas.ml"]
192- - name : mlkem_intt
192+ - name : intt_avx2_asm
193193 needs : ["mlkem_specs.ml", "mlkem_zetas.ml"]
194- - name : mlkem_poly_basemul_acc_montgomery_cached_k2
194+ - name : polyvec_basemul_acc_montgomery_cached_k2_avx2_asm
195195 needs : ["mlkem_specs.ml"]
196- - name : mlkem_poly_basemul_acc_montgomery_cached_k3
196+ - name : polyvec_basemul_acc_montgomery_cached_k3_avx2_asm
197197 needs : ["mlkem_specs.ml"]
198- - name : mlkem_poly_basemul_acc_montgomery_cached_k4
198+ - name : polyvec_basemul_acc_montgomery_cached_k4_avx2_asm
199199 needs : ["mlkem_specs.ml"]
200- - name : mlkem_reduce
200+ - name : reduce_avx2_asm
201201 needs : ["mlkem_specs.ml"]
202- - name : mlkem_tobytes
202+ - name : ntttobytes_avx2_asm
203203 needs : ["mlkem_specs.ml"]
204- - name : mlkem_rej_uniform
204+ - name : rej_uniform_avx2_asm
205205 needs : ["mlkem_specs.ml", "mlkem_rej_uniform_table.ml"]
206- - name : mlkem_frombytes
206+ - name : nttfrombytes_avx2_asm
207207 needs : ["mlkem_specs.ml"]
208- - name : mlkem_tomont
208+ - name : tomont_avx2_asm
209209 needs : ["mlkem_specs.ml"]
210- - name : mlkem_unpack
210+ - name : nttunpack_avx2_asm
211211 needs : ["mlkem_specs.ml"]
212- - name : mlkem_mulcache_compute
212+ - name : poly_mulcache_compute_avx2_asm
213213 needs : ["mlkem_specs.ml", "mlkem_zetas.ml"]
214- - name : mlkem_poly_compress_d4
214+ - name : poly_compress_d4_avx2_asm
215215 needs : ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
216- - name : mlkem_poly_decompress_d4
216+ - name : poly_decompress_d4_avx2_asm
217217 needs : ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
218- - name : mlkem_poly_compress_d5
218+ - name : poly_compress_d5_avx2_asm
219219 needs : ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
220- - name : mlkem_poly_decompress_d5
220+ - name : poly_decompress_d5_avx2_asm
221221 needs : ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
222- - name : mlkem_poly_compress_d10
222+ - name : poly_compress_d10_avx2_asm
223223 needs : ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
224- - name : mlkem_poly_decompress_d10
224+ - name : poly_decompress_d10_avx2_asm
225225 needs : ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
226- - name : mlkem_poly_compress_d11
226+ - name : poly_compress_d11_avx2_asm
227227 needs : ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
228- - name : mlkem_poly_decompress_d11
228+ - name : poly_decompress_d11_avx2_asm
229229 needs : ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
230- - name : keccak_f1600_x4_avx2
230+ - name : keccak_f1600_x4_avx2_asm
231231 needs : ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"]
232232 name : x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
233233 runs-on : pqcp-x64
0 commit comments