hol_light: Unify asm and proof filenames with exported symbols

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Author: mkannwischer

.github/workflows/hol_light.yml

@@ -70,44 +70,44 @@ jobs:
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           nix-shell: 'hol_light'
           script: |
-            make -C proofs/hol_light/aarch64 mlkem/mlkem_poly_tobytes.o
-            echo 'needs "aarch64/proofs/mlkem_poly_tobytes.ml";;' | hol.sh
+            make -C proofs/hol_light/aarch64 mlkem/poly_tobytes_aarch64_asm.o
+            echo 'needs "aarch64/proofs/poly_tobytes_aarch64_asm.ml";;' | hol.sh
   hol_light_proofs:
     needs: [ hol_light_bytecode ]
     strategy:
       fail-fast: false
       matrix:
         proof:
           # Dependencies on {name}.{S,ml} are implicit
-          - name: mlkem_ntt
+          - name: ntt_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
-          - name: mlkem_intt
+          - name: intt_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
-          - name: mlkem_poly_tomont
+          - name: poly_tomont_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
-          - name: mlkem_poly_mulcache_compute
+          - name: poly_mulcache_compute_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
-          - name: mlkem_poly_reduce
+          - name: poly_reduce_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
-          - name: mlkem_poly_basemul_acc_montgomery_cached_k2
+          - name: polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
-          - name: mlkem_poly_basemul_acc_montgomery_cached_k3
+          - name: polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
-          - name: mlkem_poly_basemul_acc_montgomery_cached_k4
+          - name: polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
-          - name: mlkem_poly_tobytes
+          - name: poly_tobytes_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml" ]
-          - name: mlkem_rej_uniform
+          - name: rej_uniform_aarch64_asm
             needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_rej_uniform_table.ml"]
-          - name: keccak_f1600_x1_scalar
+          - name: keccak_f1600_x1_scalar_aarch64_asm
             needs: ["keccak_specs.ml"]
-          - name: keccak_f1600_x1_v84a
+          - name: keccak_f1600_x1_v84a_aarch64_asm
             needs: ["keccak_specs.ml"]
-          - name: keccak_f1600_x2_v84a
+          - name: keccak_f1600_x2_v84a_aarch64_asm
             needs: ["keccak_specs.ml"]
-          - name: keccak_f1600_x4_v8a_v84a_scalar
+          - name: keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm
             needs: ["keccak_specs.ml"]
-          - name: keccak_f1600_x4_v8a_scalar
+          - name: keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
             needs: ["keccak_specs.ml"]
     name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
     runs-on: pqcp-arm64
@@ -178,56 +178,56 @@ jobs:
           gh_token: ${{ secrets.GITHUB_TOKEN }}
           nix-shell: 'hol_light'
           script: |
-            make -C proofs/hol_light/x86_64 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
-            echo 'needs "x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
+            make -C proofs/hol_light/x86_64 mlkem/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.o
+            echo 'needs "x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.ml";;' | hol.sh
   hol_light_proofs_x86_64:
     needs: [ hol_light_bytecode_x86_64 ]
     strategy:
       fail-fast: false
       matrix:
         proof:
           # Dependencies on {name}.{S,ml} are implicit
-          - name: mlkem_ntt
+          - name: ntt_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_zetas.ml"]
-          - name: mlkem_intt
+          - name: intt_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_zetas.ml"]
-          - name: mlkem_poly_basemul_acc_montgomery_cached_k2
+          - name: polyvec_basemul_acc_montgomery_cached_k2_avx2_asm
             needs: ["mlkem_specs.ml"]
-          - name: mlkem_poly_basemul_acc_montgomery_cached_k3
+          - name: polyvec_basemul_acc_montgomery_cached_k3_avx2_asm
             needs: ["mlkem_specs.ml"]
-          - name: mlkem_poly_basemul_acc_montgomery_cached_k4
+          - name: polyvec_basemul_acc_montgomery_cached_k4_avx2_asm
             needs: ["mlkem_specs.ml"]
-          - name: mlkem_reduce
+          - name: reduce_avx2_asm
             needs: ["mlkem_specs.ml"]
-          - name: mlkem_tobytes
+          - name: ntttobytes_avx2_asm
             needs: ["mlkem_specs.ml"]
-          - name: mlkem_rej_uniform
+          - name: rej_uniform_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_rej_uniform_table.ml"]
-          - name: mlkem_frombytes
+          - name: nttfrombytes_avx2_asm
             needs: ["mlkem_specs.ml"]
-          - name: mlkem_tomont
+          - name: tomont_avx2_asm
             needs: ["mlkem_specs.ml"]
-          - name: mlkem_unpack
+          - name: nttunpack_avx2_asm
             needs: ["mlkem_specs.ml"]
-          - name: mlkem_mulcache_compute
+          - name: poly_mulcache_compute_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_zetas.ml"]
-          - name: mlkem_poly_compress_d4
+          - name: poly_compress_d4_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
-          - name: mlkem_poly_decompress_d4
+          - name: poly_decompress_d4_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
-          - name: mlkem_poly_compress_d5
+          - name: poly_compress_d5_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
-          - name: mlkem_poly_decompress_d5
+          - name: poly_decompress_d5_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
-          - name: mlkem_poly_compress_d10
+          - name: poly_compress_d10_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
-          - name: mlkem_poly_decompress_d10
+          - name: poly_decompress_d10_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
-          - name: mlkem_poly_compress_d11
+          - name: poly_compress_d11_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
-          - name: mlkem_poly_decompress_d11
+          - name: poly_decompress_d11_avx2_asm
             needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
-          - name: keccak_f1600_x4_avx2
+          - name: keccak_f1600_x4_avx2_asm
             needs: ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"]
     name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
     runs-on: pqcp-x64

BIBLIOGRAPHY.md

@@ -27,8 +27,8 @@ source code and documentation.
   - [dev/x86_64/src/ntt_avx2_asm.S](dev/x86_64/src/ntt_avx2_asm.S)
   - [mlkem/src/native/x86_64/src/intt_avx2_asm.S](mlkem/src/native/x86_64/src/intt_avx2_asm.S)
   - [mlkem/src/native/x86_64/src/ntt_avx2_asm.S](mlkem/src/native/x86_64/src/ntt_avx2_asm.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_intt.S](proofs/hol_light/x86_64/mlkem/mlkem_intt.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_ntt.S](proofs/hol_light/x86_64/mlkem/mlkem_ntt.S)
+  - [proofs/hol_light/x86_64/mlkem/intt_avx2_asm.S](proofs/hol_light/x86_64/mlkem/intt_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/ntt_avx2_asm.S](proofs/hol_light/x86_64/mlkem/ntt_avx2_asm.S)
 
 ### `CBMC`
 
@@ -188,8 +188,8 @@ source code and documentation.
   - [mlkem/src/fips202/native/aarch64/src/keccak_f1600_x1_v84a_aarch64_asm.S](mlkem/src/fips202/native/aarch64/src/keccak_f1600_x1_v84a_aarch64_asm.S)
   - [mlkem/src/fips202/native/aarch64/src/keccak_f1600_x2_v84a_aarch64_asm.S](mlkem/src/fips202/native/aarch64/src/keccak_f1600_x2_v84a_aarch64_asm.S)
   - [proofs/hol_light/README.md](proofs/hol_light/README.md)
-  - [proofs/hol_light/aarch64/mlkem/keccak_f1600_x1_v84a.S](proofs/hol_light/aarch64/mlkem/keccak_f1600_x1_v84a.S)
-  - [proofs/hol_light/aarch64/mlkem/keccak_f1600_x2_v84a.S](proofs/hol_light/aarch64/mlkem/keccak_f1600_x2_v84a.S)
+  - [proofs/hol_light/aarch64/mlkem/keccak_f1600_x1_v84a_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/keccak_f1600_x1_v84a_aarch64_asm.S)
+  - [proofs/hol_light/aarch64/mlkem/keccak_f1600_x2_v84a_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/keccak_f1600_x2_v84a_aarch64_asm.S)
 
 ### `KyberSlash`
 
@@ -241,11 +241,11 @@ source code and documentation.
   - [mlkem/src/native/aarch64/src/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.S](mlkem/src/native/aarch64/src/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.S)
   - [mlkem/src/poly.c](mlkem/src/poly.c)
   - [mlkem/src/poly_k.c](mlkem/src/poly_k.c)
-  - [proofs/hol_light/aarch64/mlkem/mlkem_intt.S](proofs/hol_light/aarch64/mlkem/mlkem_intt.S)
-  - [proofs/hol_light/aarch64/mlkem/mlkem_ntt.S](proofs/hol_light/aarch64/mlkem/mlkem_ntt.S)
-  - [proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S](proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S)
-  - [proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S](proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S)
-  - [proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S](proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
+  - [proofs/hol_light/aarch64/mlkem/intt_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/intt_aarch64_asm.S)
+  - [proofs/hol_light/aarch64/mlkem/ntt_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/ntt_aarch64_asm.S)
+  - [proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.S)
+  - [proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.S)
+  - [proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.S)
 
 ### `REF`
 
@@ -320,21 +320,21 @@ source code and documentation.
   - [mlkem/src/native/x86_64/src/poly_decompress_d5_avx2_asm.S](mlkem/src/native/x86_64/src/poly_decompress_d5_avx2_asm.S)
   - [mlkem/src/native/x86_64/src/reduce_avx2_asm.S](mlkem/src/native/x86_64/src/reduce_avx2_asm.S)
   - [mlkem/src/native/x86_64/src/tomont_avx2_asm.S](mlkem/src/native/x86_64/src/tomont_avx2_asm.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_frombytes.S](proofs/hol_light/x86_64/mlkem/mlkem_frombytes.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_intt.S](proofs/hol_light/x86_64/mlkem/mlkem_intt.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_ntt.S](proofs/hol_light/x86_64/mlkem/mlkem_ntt.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_poly_compress_d10.S](proofs/hol_light/x86_64/mlkem/mlkem_poly_compress_d10.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_poly_compress_d11.S](proofs/hol_light/x86_64/mlkem/mlkem_poly_compress_d11.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_poly_compress_d4.S](proofs/hol_light/x86_64/mlkem/mlkem_poly_compress_d4.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_poly_compress_d5.S](proofs/hol_light/x86_64/mlkem/mlkem_poly_compress_d5.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_poly_decompress_d10.S](proofs/hol_light/x86_64/mlkem/mlkem_poly_decompress_d10.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_poly_decompress_d11.S](proofs/hol_light/x86_64/mlkem/mlkem_poly_decompress_d11.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_poly_decompress_d4.S](proofs/hol_light/x86_64/mlkem/mlkem_poly_decompress_d4.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_poly_decompress_d5.S](proofs/hol_light/x86_64/mlkem/mlkem_poly_decompress_d5.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_reduce.S](proofs/hol_light/x86_64/mlkem/mlkem_reduce.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_tobytes.S](proofs/hol_light/x86_64/mlkem/mlkem_tobytes.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_tomont.S](proofs/hol_light/x86_64/mlkem/mlkem_tomont.S)
-  - [proofs/hol_light/x86_64/mlkem/mlkem_unpack.S](proofs/hol_light/x86_64/mlkem/mlkem_unpack.S)
+  - [proofs/hol_light/x86_64/mlkem/intt_avx2_asm.S](proofs/hol_light/x86_64/mlkem/intt_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/ntt_avx2_asm.S](proofs/hol_light/x86_64/mlkem/ntt_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/nttfrombytes_avx2_asm.S](proofs/hol_light/x86_64/mlkem/nttfrombytes_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/ntttobytes_avx2_asm.S](proofs/hol_light/x86_64/mlkem/ntttobytes_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/nttunpack_avx2_asm.S](proofs/hol_light/x86_64/mlkem/nttunpack_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/poly_compress_d10_avx2_asm.S](proofs/hol_light/x86_64/mlkem/poly_compress_d10_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/poly_compress_d11_avx2_asm.S](proofs/hol_light/x86_64/mlkem/poly_compress_d11_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/poly_compress_d4_avx2_asm.S](proofs/hol_light/x86_64/mlkem/poly_compress_d4_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/poly_compress_d5_avx2_asm.S](proofs/hol_light/x86_64/mlkem/poly_compress_d5_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/poly_decompress_d10_avx2_asm.S](proofs/hol_light/x86_64/mlkem/poly_decompress_d10_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/poly_decompress_d11_avx2_asm.S](proofs/hol_light/x86_64/mlkem/poly_decompress_d11_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/poly_decompress_d4_avx2_asm.S](proofs/hol_light/x86_64/mlkem/poly_decompress_d4_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/poly_decompress_d5_avx2_asm.S](proofs/hol_light/x86_64/mlkem/poly_decompress_d5_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/reduce_avx2_asm.S](proofs/hol_light/x86_64/mlkem/reduce_avx2_asm.S)
+  - [proofs/hol_light/x86_64/mlkem/tomont_avx2_asm.S](proofs/hol_light/x86_64/mlkem/tomont_avx2_asm.S)
 
 ### `SLOTHY`
 
@@ -370,8 +370,8 @@ source code and documentation.
   - [mlkem/src/native/aarch64/README.md](mlkem/src/native/aarch64/README.md)
   - [mlkem/src/native/aarch64/src/intt_aarch64_asm.S](mlkem/src/native/aarch64/src/intt_aarch64_asm.S)
   - [mlkem/src/native/aarch64/src/ntt_aarch64_asm.S](mlkem/src/native/aarch64/src/ntt_aarch64_asm.S)
-  - [proofs/hol_light/aarch64/mlkem/mlkem_intt.S](proofs/hol_light/aarch64/mlkem/mlkem_intt.S)
-  - [proofs/hol_light/aarch64/mlkem/mlkem_ntt.S](proofs/hol_light/aarch64/mlkem/mlkem_ntt.S)
+  - [proofs/hol_light/aarch64/mlkem/intt_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/intt_aarch64_asm.S)
+  - [proofs/hol_light/aarch64/mlkem/ntt_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/ntt_aarch64_asm.S)
 
 ### `clangover`
 

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -38,7 +38,7 @@ MLK_INTERNAL_DATA_DECLARATION const uint8_t mlk_rej_uniform_table[4096];
 void mlk_ntt_aarch64_asm(int16_t p[256], const int16_t twiddles12345[80],
                          const int16_t twiddles56[384])
 /* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/aarch64/proofs/mlkem_ntt.ml */
+ * in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
   requires(array_abs_bound(p, 0, MLKEM_N, 8192))
@@ -54,7 +54,7 @@ __contract__(
 void mlk_intt_aarch64_asm(int16_t p[256], const int16_t twiddles12345[80],
                           const int16_t twiddles56[384])
 /* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/aarch64/proofs/mlkem_intt.ml */
+ * in proofs/hol_light/aarch64/proofs/intt_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
   requires(twiddles12345 == mlk_aarch64_invntt_zetas_layer12345)
@@ -68,7 +68,7 @@ __contract__(
 #define mlk_poly_reduce_aarch64_asm MLK_NAMESPACE(poly_reduce_aarch64_asm)
 void mlk_poly_reduce_aarch64_asm(int16_t p[256])
 /* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/aarch64/proofs/mlkem_poly_reduce.ml */
+ * in proofs/hol_light/aarch64/proofs/poly_reduce_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
   assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
@@ -78,7 +78,7 @@ __contract__(
 #define mlk_poly_tomont_aarch64_asm MLK_NAMESPACE(poly_tomont_aarch64_asm)
 void mlk_poly_tomont_aarch64_asm(int16_t p[256])
 /* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/aarch64/proofs/mlkem_poly_tomont.ml */
+ * in proofs/hol_light/aarch64/proofs/poly_tomont_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
   assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
@@ -92,7 +92,7 @@ void mlk_poly_mulcache_compute_aarch64_asm(int16_t cache[128],
                                            const int16_t zetas[128],
                                            const int16_t zetas_twisted[128])
 /* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/aarch64/proofs/mlkem_poly_mulcache_compute.ml */
+ * in proofs/hol_light/aarch64/proofs/poly_mulcache_compute_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
   requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
@@ -105,7 +105,7 @@ __contract__(
 #define mlk_poly_tobytes_aarch64_asm MLK_NAMESPACE(poly_tobytes_aarch64_asm)
 void mlk_poly_tobytes_aarch64_asm(uint8_t r[384], const int16_t a[256])
 /* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/aarch64/proofs/mlkem_poly_tobytes.ml */
+ * in proofs/hol_light/aarch64/proofs/poly_tobytes_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(r, MLKEM_POLYBYTES))
   requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
@@ -119,7 +119,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm(
     int16_t r[256], const int16_t a[512], const int16_t b[512],
     const int16_t b_cache[256])
 /* This must be kept in sync with the HOL-Light specification in
- * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
+ * proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.ml.
  */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -136,7 +136,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm(
     int16_t r[256], const int16_t a[768], const int16_t b[768],
     const int16_t b_cache[384])
 /* This must be kept in sync with the HOL-Light specification in
- * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
+ * proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.ml.
  */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -153,7 +153,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm(
     int16_t r[256], const int16_t a[1024], const int16_t b[1024],
     const int16_t b_cache[512])
 /* This must be kept in sync with the HOL-Light specification in
- * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
+ * proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.ml.
  */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -169,7 +169,7 @@ MLK_MUST_CHECK_RETURN_VALUE
 uint64_t mlk_rej_uniform_aarch64_asm(int16_t r[256], const uint8_t *buf,
                                      unsigned buflen, const uint8_t table[4096])
 /* This must be kept in sync with the HOL-Light specification
- * in proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml. */
+ * in proofs/hol_light/aarch64/proofs/rej_uniform_aarch64_asm.ml. */
 __contract__(
     requires(buflen % 24 == 0)
     requires(memory_no_alias(buf, buflen))