HOL-Light: Switch to mld_ namespace

mkannwischer · hanno-becker · commit d417b6bb6052 · 2026-06-11T16:47:29.000+01:00
Previously, the HOL-Light assembly kernels used the default PQCP namespace. This namespace is both overly verbose and prefixed with the ML-DSA parameter set, which in the context of parameter-set independent assembly is confusing. This commit switches the namespace used in the HOL-Light assembly to `mld_`. Ports pq-code-package/mlkem-native#1739. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
diff --git a/proofs/hol_light/aarch64/mldsa/intt_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/intt_aarch64_asm.S
@@ -31,11 +31,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_intt_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_intt_aarch64_asm:
+.global _mld_intt_aarch64_asm
+_mld_intt_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_intt_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_intt_aarch64_asm:
+.global mld_intt_aarch64_asm
+mld_intt_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S
@@ -40,11 +40,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x1_scalar_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x1_scalar_aarch64_asm:
+.global _mld_keccak_f1600_x1_scalar_aarch64_asm
+_mld_keccak_f1600_x1_scalar_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x1_scalar_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x1_scalar_aarch64_asm:
+.global mld_keccak_f1600_x1_scalar_aarch64_asm
+mld_keccak_f1600_x1_scalar_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.S
@@ -56,11 +56,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x1_v84a_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x1_v84a_aarch64_asm:
+.global _mld_keccak_f1600_x1_v84a_aarch64_asm
+_mld_keccak_f1600_x1_v84a_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x1_v84a_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x1_v84a_aarch64_asm:
+.global mld_keccak_f1600_x1_v84a_aarch64_asm
+mld_keccak_f1600_x1_v84a_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x2_v84a_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x2_v84a_aarch64_asm.S
@@ -56,11 +56,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x2_v84a_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x2_v84a_aarch64_asm:
+.global _mld_keccak_f1600_x2_v84a_aarch64_asm
+_mld_keccak_f1600_x2_v84a_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x2_v84a_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x2_v84a_aarch64_asm:
+.global mld_keccak_f1600_x2_v84a_aarch64_asm
+mld_keccak_f1600_x2_v84a_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.S
@@ -40,11 +40,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm:
+.global _mld_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
+_mld_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm:
+.global mld_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
+mld_keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.S
@@ -41,11 +41,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm:
+.global _mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm
+_mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm:
+.global mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm
+mld_keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.S
@@ -11,11 +11,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm:
+.global _mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm
+_mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm:
+.global mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm
+mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S
@@ -11,11 +11,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm:
+.global _mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm
+_mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm:
+.global mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm
+mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S
@@ -11,11 +11,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm:
+.global _mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm
+_mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm:
+.global mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm
+mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/ntt_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/ntt_aarch64_asm.S
@@ -31,11 +31,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_ntt_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_ntt_aarch64_asm:
+.global _mld_ntt_aarch64_asm
+_mld_ntt_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_ntt_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_ntt_aarch64_asm:
+.global mld_ntt_aarch64_asm
+mld_ntt_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/pointwise_montgomery_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/pointwise_montgomery_aarch64_asm.S
@@ -11,11 +11,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_pointwise_montgomery_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_poly_pointwise_montgomery_aarch64_asm:
+.global _mld_poly_pointwise_montgomery_aarch64_asm
+_mld_poly_pointwise_montgomery_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_poly_pointwise_montgomery_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_poly_pointwise_montgomery_aarch64_asm:
+.global mld_poly_pointwise_montgomery_aarch64_asm
+mld_poly_pointwise_montgomery_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/poly_caddq_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/poly_caddq_aarch64_asm.S
@@ -12,11 +12,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_caddq_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_poly_caddq_aarch64_asm:
+.global _mld_poly_caddq_aarch64_asm
+_mld_poly_caddq_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_poly_caddq_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_poly_caddq_aarch64_asm:
+.global mld_poly_caddq_aarch64_asm
+mld_poly_caddq_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/poly_chknorm_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/poly_chknorm_aarch64_asm.S
@@ -12,11 +12,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_chknorm_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_poly_chknorm_aarch64_asm:
+.global _mld_poly_chknorm_aarch64_asm
+_mld_poly_chknorm_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_poly_chknorm_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_poly_chknorm_aarch64_asm:
+.global mld_poly_chknorm_aarch64_asm
+mld_poly_chknorm_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/poly_decompose_32_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/poly_decompose_32_aarch64_asm.S
@@ -12,11 +12,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_32_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_32_aarch64_asm:
+.global _mld_poly_decompose_32_aarch64_asm
+_mld_poly_decompose_32_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_32_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_32_aarch64_asm:
+.global mld_poly_decompose_32_aarch64_asm
+mld_poly_decompose_32_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/poly_decompose_88_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/poly_decompose_88_aarch64_asm.S
@@ -12,11 +12,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_88_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_88_aarch64_asm:
+.global _mld_poly_decompose_88_aarch64_asm
+_mld_poly_decompose_88_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_88_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_88_aarch64_asm:
+.global mld_poly_decompose_88_aarch64_asm
+mld_poly_decompose_88_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/poly_use_hint_32_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/poly_use_hint_32_aarch64_asm.S
@@ -12,11 +12,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_aarch64_asm:
+.global _mld_poly_use_hint_32_aarch64_asm
+_mld_poly_use_hint_32_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_aarch64_asm:
+.global mld_poly_use_hint_32_aarch64_asm
+mld_poly_use_hint_32_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/poly_use_hint_88_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/poly_use_hint_88_aarch64_asm.S
@@ -12,11 +12,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_aarch64_asm:
+.global _mld_poly_use_hint_88_aarch64_asm
+_mld_poly_use_hint_88_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_aarch64_asm:
+.global mld_poly_use_hint_88_aarch64_asm
+mld_poly_use_hint_88_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/polyz_unpack_17_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/polyz_unpack_17_aarch64_asm.S
@@ -13,11 +13,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_aarch64_asm:
+.global _mld_polyz_unpack_17_aarch64_asm
+_mld_polyz_unpack_17_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_aarch64_asm:
+.global mld_polyz_unpack_17_aarch64_asm
+mld_polyz_unpack_17_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/polyz_unpack_19_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/polyz_unpack_19_aarch64_asm.S
@@ -13,11 +13,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_19_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_19_aarch64_asm:
+.global _mld_polyz_unpack_19_aarch64_asm
+_mld_polyz_unpack_19_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_19_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_19_aarch64_asm:
+.global mld_polyz_unpack_19_aarch64_asm
+mld_polyz_unpack_19_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/rej_uniform_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/rej_uniform_aarch64_asm.S
@@ -13,11 +13,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_aarch64_asm:
+.global _mld_rej_uniform_aarch64_asm
+_mld_rej_uniform_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_aarch64_asm:
+.global mld_rej_uniform_aarch64_asm
+mld_rej_uniform_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/rej_uniform_eta2_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/rej_uniform_eta2_aarch64_asm.S
@@ -13,11 +13,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta2_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta2_aarch64_asm:
+.global _mld_rej_uniform_eta2_aarch64_asm
+_mld_rej_uniform_eta2_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta2_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta2_aarch64_asm:
+.global mld_rej_uniform_eta2_aarch64_asm
+mld_rej_uniform_eta2_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/aarch64/mldsa/rej_uniform_eta4_aarch64_asm.S b/proofs/hol_light/aarch64/mldsa/rej_uniform_eta4_aarch64_asm.S
@@ -13,11 +13,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta4_aarch64_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta4_aarch64_asm:
+.global _mld_rej_uniform_eta4_aarch64_asm
+_mld_rej_uniform_eta4_aarch64_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta4_aarch64_asm
-PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta4_aarch64_asm:
+.global mld_rej_uniform_eta4_aarch64_asm
+mld_rej_uniform_eta4_aarch64_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S
@@ -27,11 +27,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_invntt_avx2_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_invntt_avx2_asm:
+.global _mld_invntt_avx2_asm
+_mld_invntt_avx2_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_invntt_avx2_asm
-PQCP_MLDSA_NATIVE_MLDSA44_invntt_avx2_asm:
+.global mld_invntt_avx2_asm
+mld_invntt_avx2_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/x86_64/mldsa/keccak_f1600_x4_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/keccak_f1600_x4_avx2_asm.S
@@ -13,11 +13,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_avx2_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_avx2_asm:
+.global _mld_keccak_f1600_x4_avx2_asm
+_mld_keccak_f1600_x4_avx2_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_avx2_asm
-PQCP_MLDSA_NATIVE_MLDSA44_keccak_f1600_x4_avx2_asm:
+.global mld_keccak_f1600_x4_avx2_asm
+mld_keccak_f1600_x4_avx2_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S
@@ -27,11 +27,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2_asm
-_PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2_asm:
+.global _mld_ntt_avx2_asm
+_mld_ntt_avx2_asm:
 #else
-.global PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2_asm
-PQCP_MLDSA_NATIVE_MLDSA44_ntt_avx2_asm:
+.global mld_ntt_avx2_asm
+mld_ntt_avx2_asm:
 #endif
 
         .cfi_startproc
diff --git a/proofs/hol_light/x86_64/mldsa/nttunpack_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/nttunpack_avx2_asm.S
diff --git a/proofs/hol_light/x86_64/mldsa/pointwise_acc_l4_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/pointwise_acc_l4_avx2_asm.S
diff --git a/proofs/hol_light/x86_64/mldsa/pointwise_acc_l5_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/pointwise_acc_l5_avx2_asm.S
diff --git a/proofs/hol_light/x86_64/mldsa/pointwise_acc_l7_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/pointwise_acc_l7_avx2_asm.S
diff --git a/proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S
diff --git a/proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S
diff --git a/proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S
diff --git a/scripts/autogen b/scripts/autogen
