diff --git a/dev/aarch64_clean/meta.h b/dev/aarch64_clean/meta.h
index dec3f5d57..6d26b56ef 100644
--- a/dev/aarch64_clean/meta.h
+++ b/dev/aarch64_clean/meta.h
@@ -156,10 +156,9 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
     (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
 {
-  mld_poly_use_hint_32_asm(b, a, h);
+  mld_poly_use_hint_32_asm(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
@@ -167,10 +166,9 @@ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
 
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
 {
-  mld_poly_use_hint_88_asm(b, a, h);
+  mld_poly_use_hint_88_asm(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
diff --git a/dev/aarch64_clean/src/arith_native_aarch64.h b/dev/aarch64_clean/src/arith_native_aarch64.h
index 11cf75223..181a78a3f 100644
--- a/dev/aarch64_clean/src/arith_native_aarch64.h
+++ b/dev/aarch64_clean/src/arith_native_aarch64.h
@@ -117,31 +117,29 @@ __contract__(
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
-void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
+void mld_poly_use_hint_32_asm(int32_t *a, const int32_t *h)
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */
 __contract__(
-  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
-  ensures(array_bound(b, 0, MLDSA_N, 0, 16))
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(a, 0, MLDSA_N, 0, 16))
 );
 
 #define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
-void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
+void mld_poly_use_hint_88_asm(int32_t *a, const int32_t *h)
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */
 __contract__(
-  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
-  ensures(array_bound(b, 0, MLDSA_N, 0, 44))
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(a, 0, MLDSA_N, 0, 44))
 );
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
diff --git a/dev/aarch64_clean/src/poly_use_hint_32_asm.S b/dev/aarch64_clean/src/poly_use_hint_32_asm.S
index d5d5d5894..a7ebfafb8 100644
--- a/dev/aarch64_clean/src/poly_use_hint_32_asm.S
+++ b/dev/aarch64_clean/src/poly_use_hint_32_asm.S
@@ -46,9 +46,8 @@
 .endm
 
         /* Parameters */
-        b_ptr           .req x0     // Output polynomial
-        a_ptr           .req x1     // Input polynomial
-        h_ptr           .req x2     // Input hints
+        a_ptr           .req x0     // In/out: input on entry, result on exit
+        h_ptr           .req x1     // Input hints
 
         count           .req x3
 
@@ -88,7 +87,7 @@ poly_use_hint_32_loop:
         ldr q1, [a_ptr, #1*16]
         ldr q2, [a_ptr, #2*16]
         ldr q3, [a_ptr, #3*16]
-        ldr q0, [a_ptr], #4*16
+        ldr q0, [a_ptr, #0*16]
 
         ldr q5, [h_ptr, #1*16]
         ldr q6, [h_ptr, #2*16]
@@ -100,17 +99,16 @@ poly_use_hint_32_loop:
         use_hint32 v19, v3, v7, v25
         use_hint32 v16, v0, v4, v25
 
-        str q17, [b_ptr, #1*16]
-        str q18, [b_ptr, #2*16]
-        str q19, [b_ptr, #3*16]
-        str q16, [b_ptr], #4*16
+        str q17, [a_ptr, #1*16]
+        str q18, [a_ptr, #2*16]
+        str q19, [a_ptr, #3*16]
+        str q16, [a_ptr], #4*16
 
         subs count, count, #1
         bne poly_use_hint_32_loop
 
         ret
 
-        .unreq b_ptr
         .unreq a_ptr
         .unreq h_ptr
         .unreq count
diff --git a/dev/aarch64_clean/src/poly_use_hint_88_asm.S b/dev/aarch64_clean/src/poly_use_hint_88_asm.S
index 93c37b06b..66ae66c86 100644
--- a/dev/aarch64_clean/src/poly_use_hint_88_asm.S
+++ b/dev/aarch64_clean/src/poly_use_hint_88_asm.S
@@ -48,9 +48,8 @@
 .endm
 
         /* Parameters */
-        b_ptr           .req x0     // Output polynomial
-        a_ptr           .req x1     // Input polynomial
-        h_ptr           .req x2     // Input hints
+        a_ptr           .req x0     // In/out: input on entry, result on exit
+        h_ptr           .req x1     // Input hints
 
         count           .req x3
 
@@ -90,7 +89,7 @@ poly_use_hint_88_loop:
         ldr q1, [a_ptr, #1*16]
         ldr q2, [a_ptr, #2*16]
         ldr q3, [a_ptr, #3*16]
-        ldr q0, [a_ptr], #4*16
+        ldr q0, [a_ptr, #0*16]
 
         ldr q5, [h_ptr, #1*16]
         ldr q6, [h_ptr, #2*16]
@@ -102,17 +101,16 @@ poly_use_hint_88_loop:
         use_hint88 v19, v3, v7, v25
         use_hint88 v16, v0, v4, v25
 
-        str q17, [b_ptr, #1*16]
-        str q18, [b_ptr, #2*16]
-        str q19, [b_ptr, #3*16]
-        str q16, [b_ptr], #4*16
+        str q17, [a_ptr, #1*16]
+        str q18, [a_ptr, #2*16]
+        str q19, [a_ptr, #3*16]
+        str q16, [a_ptr], #4*16
 
         subs count, count, #1
         bne poly_use_hint_88_loop
 
         ret
 
-        .unreq b_ptr
         .unreq a_ptr
         .unreq h_ptr
         .unreq count
diff --git a/dev/aarch64_opt/meta.h b/dev/aarch64_opt/meta.h
index dec3f5d57..6d26b56ef 100644
--- a/dev/aarch64_opt/meta.h
+++ b/dev/aarch64_opt/meta.h
@@ -156,10 +156,9 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
     (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
 {
-  mld_poly_use_hint_32_asm(b, a, h);
+  mld_poly_use_hint_32_asm(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
@@ -167,10 +166,9 @@ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
 
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
 {
-  mld_poly_use_hint_88_asm(b, a, h);
+  mld_poly_use_hint_88_asm(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
diff --git a/dev/aarch64_opt/src/arith_native_aarch64.h b/dev/aarch64_opt/src/arith_native_aarch64.h
index 11cf75223..181a78a3f 100644
--- a/dev/aarch64_opt/src/arith_native_aarch64.h
+++ b/dev/aarch64_opt/src/arith_native_aarch64.h
@@ -117,31 +117,29 @@ __contract__(
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
-void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
+void mld_poly_use_hint_32_asm(int32_t *a, const int32_t *h)
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */
 __contract__(
-  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
-  ensures(array_bound(b, 0, MLDSA_N, 0, 16))
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(a, 0, MLDSA_N, 0, 16))
 );
 
 #define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
-void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
+void mld_poly_use_hint_88_asm(int32_t *a, const int32_t *h)
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */
 __contract__(
-  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
-  ensures(array_bound(b, 0, MLDSA_N, 0, 44))
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(a, 0, MLDSA_N, 0, 44))
 );
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
diff --git a/dev/aarch64_opt/src/poly_use_hint_32_asm.S b/dev/aarch64_opt/src/poly_use_hint_32_asm.S
index d5d5d5894..a7ebfafb8 100644
--- a/dev/aarch64_opt/src/poly_use_hint_32_asm.S
+++ b/dev/aarch64_opt/src/poly_use_hint_32_asm.S
@@ -46,9 +46,8 @@
 .endm
 
         /* Parameters */
-        b_ptr           .req x0     // Output polynomial
-        a_ptr           .req x1     // Input polynomial
-        h_ptr           .req x2     // Input hints
+        a_ptr           .req x0     // In/out: input on entry, result on exit
+        h_ptr           .req x1     // Input hints
 
         count           .req x3
 
@@ -88,7 +87,7 @@ poly_use_hint_32_loop:
         ldr q1, [a_ptr, #1*16]
         ldr q2, [a_ptr, #2*16]
         ldr q3, [a_ptr, #3*16]
-        ldr q0, [a_ptr], #4*16
+        ldr q0, [a_ptr, #0*16]
 
         ldr q5, [h_ptr, #1*16]
         ldr q6, [h_ptr, #2*16]
@@ -100,17 +99,16 @@ poly_use_hint_32_loop:
         use_hint32 v19, v3, v7, v25
         use_hint32 v16, v0, v4, v25
 
-        str q17, [b_ptr, #1*16]
-        str q18, [b_ptr, #2*16]
-        str q19, [b_ptr, #3*16]
-        str q16, [b_ptr], #4*16
+        str q17, [a_ptr, #1*16]
+        str q18, [a_ptr, #2*16]
+        str q19, [a_ptr, #3*16]
+        str q16, [a_ptr], #4*16
 
         subs count, count, #1
         bne poly_use_hint_32_loop
 
         ret
 
-        .unreq b_ptr
         .unreq a_ptr
         .unreq h_ptr
         .unreq count
diff --git a/dev/aarch64_opt/src/poly_use_hint_88_asm.S b/dev/aarch64_opt/src/poly_use_hint_88_asm.S
index 93c37b06b..66ae66c86 100644
--- a/dev/aarch64_opt/src/poly_use_hint_88_asm.S
+++ b/dev/aarch64_opt/src/poly_use_hint_88_asm.S
@@ -48,9 +48,8 @@
 .endm
 
         /* Parameters */
-        b_ptr           .req x0     // Output polynomial
-        a_ptr           .req x1     // Input polynomial
-        h_ptr           .req x2     // Input hints
+        a_ptr           .req x0     // In/out: input on entry, result on exit
+        h_ptr           .req x1     // Input hints
 
         count           .req x3
 
@@ -90,7 +89,7 @@ poly_use_hint_88_loop:
         ldr q1, [a_ptr, #1*16]
         ldr q2, [a_ptr, #2*16]
         ldr q3, [a_ptr, #3*16]
-        ldr q0, [a_ptr], #4*16
+        ldr q0, [a_ptr, #0*16]
 
         ldr q5, [h_ptr, #1*16]
         ldr q6, [h_ptr, #2*16]
@@ -102,17 +101,16 @@ poly_use_hint_88_loop:
         use_hint88 v19, v3, v7, v25
         use_hint88 v16, v0, v4, v25
 
-        str q17, [b_ptr, #1*16]
-        str q18, [b_ptr, #2*16]
-        str q19, [b_ptr, #3*16]
-        str q16, [b_ptr], #4*16
+        str q17, [a_ptr, #1*16]
+        str q18, [a_ptr, #2*16]
+        str q19, [a_ptr, #3*16]
+        str q16, [a_ptr], #4*16
 
         subs count, count, #1
         bne poly_use_hint_88_loop
 
         ret
 
-        .unreq b_ptr
         .unreq a_ptr
         .unreq h_ptr
         .unreq count
diff --git a/dev/x86_64/meta.h b/dev/x86_64/meta.h
index 23600f9d5..6fba6ef36 100644
--- a/dev/x86_64/meta.h
+++ b/dev/x86_64/meta.h
@@ -189,14 +189,13 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
     (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
 {
   if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2))
   {
     return MLD_NATIVE_FUNC_FALLBACK;
   }
-  mld_poly_use_hint_32_avx2(b, a, h);
+  mld_poly_use_hint_32_avx2(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
@@ -204,14 +203,13 @@ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
 
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
 {
   if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2))
   {
     return MLD_NATIVE_FUNC_FALLBACK;
   }
-  mld_poly_use_hint_88_avx2(b, a, h);
+  mld_poly_use_hint_88_avx2(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
diff --git a/dev/x86_64/src/arith_native_x86_64.h b/dev/x86_64/src/arith_native_x86_64.h
index b5fd4e9b8..bcbfd6cfa 100644
--- a/dev/x86_64/src/arith_native_x86_64.h
+++ b/dev/x86_64/src/arith_native_x86_64.h
@@ -103,10 +103,10 @@ void mld_poly_caddq_avx2(int32_t *r);
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_avx2 MLD_NAMESPACE(mld_poly_use_hint_32_avx2)
-void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_32_avx2(int32_t *a, const int32_t *h);
 
 #define mld_poly_use_hint_88_avx2 MLD_NAMESPACE(mld_poly_use_hint_88_avx2)
-void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_88_avx2(int32_t *a, const int32_t *h);
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
 #define mld_poly_chknorm_avx2 MLD_NAMESPACE(mld_poly_chknorm_avx2)
diff --git a/dev/x86_64/src/poly_use_hint_32_avx2.c b/dev/x86_64/src/poly_use_hint_32_avx2.c
index b2702f01a..9a9edfa53 100644
--- a/dev/x86_64/src/poly_use_hint_32_avx2.c
+++ b/dev/x86_64/src/poly_use_hint_32_avx2.c
@@ -34,8 +34,7 @@
                                        _mm256_castsi256_ps(b), \
                                        _mm256_castsi256_ps(mask)))
 
-void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a,
-                               const int32_t *hint)
+void mld_poly_use_hint_32_avx2(int32_t *a, const int32_t *hint)
 {
   unsigned int i;
   __m256i f, f0, f1, h, t;
@@ -83,7 +82,7 @@ void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a,
     f1 = _mm256_add_epi32(f1, h);
     f1 = _mm256_and_si256(f1, mask);
 
-    _mm256_store_si256((__m256i *)&b[8 * i], f1);
+    _mm256_store_si256((__m256i *)&a[8 * i], f1);
   }
 }
 
diff --git a/dev/x86_64/src/poly_use_hint_88_avx2.c b/dev/x86_64/src/poly_use_hint_88_avx2.c
index 01c17bb54..41112a2a3 100644
--- a/dev/x86_64/src/poly_use_hint_88_avx2.c
+++ b/dev/x86_64/src/poly_use_hint_88_avx2.c
@@ -34,8 +34,7 @@
                                        _mm256_castsi256_ps(b), \
                                        _mm256_castsi256_ps(mask)))
 
-void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a,
-                               const int32_t *hint)
+void mld_poly_use_hint_88_avx2(int32_t *a, const int32_t *hint)
 {
   unsigned int i;
   __m256i f, f0, f1, h, t;
@@ -85,7 +84,7 @@ void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a,
     f = _mm256_cmpgt_epi32(f1, max);
     f1 = MLD_MM256_BLENDV_EPI32(f1, zero, f);
 
-    _mm256_store_si256((__m256i *)&b[8 * i], f1);
+    _mm256_store_si256((__m256i *)&a[8 * i], f1);
   }
 }
 
diff --git a/mldsa/src/native/aarch64/meta.h b/mldsa/src/native/aarch64/meta.h
index dec3f5d57..6d26b56ef 100644
--- a/mldsa/src/native/aarch64/meta.h
+++ b/mldsa/src/native/aarch64/meta.h
@@ -156,10 +156,9 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
     (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
 {
-  mld_poly_use_hint_32_asm(b, a, h);
+  mld_poly_use_hint_32_asm(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
@@ -167,10 +166,9 @@ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
 
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
 {
-  mld_poly_use_hint_88_asm(b, a, h);
+  mld_poly_use_hint_88_asm(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
diff --git a/mldsa/src/native/aarch64/src/arith_native_aarch64.h b/mldsa/src/native/aarch64/src/arith_native_aarch64.h
index 11cf75223..181a78a3f 100644
--- a/mldsa/src/native/aarch64/src/arith_native_aarch64.h
+++ b/mldsa/src/native/aarch64/src/arith_native_aarch64.h
@@ -117,31 +117,29 @@ __contract__(
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
-void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
+void mld_poly_use_hint_32_asm(int32_t *a, const int32_t *h)
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */
 __contract__(
-  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
-  ensures(array_bound(b, 0, MLDSA_N, 0, 16))
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(a, 0, MLDSA_N, 0, 16))
 );
 
 #define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
-void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
+void mld_poly_use_hint_88_asm(int32_t *a, const int32_t *h)
 /* This must be kept in sync with the HOL-Light specification
  * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */
 __contract__(
-  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
-  ensures(array_bound(b, 0, MLDSA_N, 0, 44))
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(a, 0, MLDSA_N, 0, 44))
 );
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
diff --git a/mldsa/src/native/aarch64/src/poly_use_hint_32_asm.S b/mldsa/src/native/aarch64/src/poly_use_hint_32_asm.S
index f0d6a4fa4..27f43afed 100644
--- a/mldsa/src/native/aarch64/src/poly_use_hint_32_asm.S
+++ b/mldsa/src/native/aarch64/src/poly_use_hint_32_asm.S
@@ -34,14 +34,14 @@ MLD_ASM_FN_SYMBOL(poly_use_hint_32_asm)
         mov x3, #0x10               // =16
 
 Lpoly_use_hint_32_loop:
-        ldr q1, [x1, #0x10]
-        ldr q2, [x1, #0x20]
-        ldr q3, [x1, #0x30]
-        ldr q0, [x1], #0x40
-        ldr q5, [x2, #0x10]
-        ldr q6, [x2, #0x20]
-        ldr q7, [x2, #0x30]
-        ldr q4, [x2], #0x40
+        ldr q1, [x0, #0x10]
+        ldr q2, [x0, #0x20]
+        ldr q3, [x0, #0x30]
+        ldr q0, [x0]
+        ldr q5, [x1, #0x10]
+        ldr q6, [x1, #0x20]
+        ldr q7, [x1, #0x30]
+        ldr q4, [x1], #0x40
         sqdmulh v17.4s, v1.4s, v23.4s
         srshr v17.4s, v17.4s, #0x12
         cmgt v25.4s, v1.4s, v21.4s
diff --git a/mldsa/src/native/aarch64/src/poly_use_hint_88_asm.S b/mldsa/src/native/aarch64/src/poly_use_hint_88_asm.S
index 70aa80d4f..a21f56b61 100644
--- a/mldsa/src/native/aarch64/src/poly_use_hint_88_asm.S
+++ b/mldsa/src/native/aarch64/src/poly_use_hint_88_asm.S
@@ -34,14 +34,14 @@ MLD_ASM_FN_SYMBOL(poly_use_hint_88_asm)
         mov x3, #0x10               // =16
 
 Lpoly_use_hint_88_loop:
-        ldr q1, [x1, #0x10]
-        ldr q2, [x1, #0x20]
-        ldr q3, [x1, #0x30]
-        ldr q0, [x1], #0x40
-        ldr q5, [x2, #0x10]
-        ldr q6, [x2, #0x20]
-        ldr q7, [x2, #0x30]
-        ldr q4, [x2], #0x40
+        ldr q1, [x0, #0x10]
+        ldr q2, [x0, #0x20]
+        ldr q3, [x0, #0x30]
+        ldr q0, [x0]
+        ldr q5, [x1, #0x10]
+        ldr q6, [x1, #0x20]
+        ldr q7, [x1, #0x30]
+        ldr q4, [x1], #0x40
         sqdmulh v17.4s, v1.4s, v23.4s
         srshr v17.4s, v17.4s, #0x11
         cmgt v25.4s, v1.4s, v21.4s
diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h
index efc8e057d..9081d3097 100644
--- a/mldsa/src/native/api.h
+++ b/mldsa/src/native/api.h
@@ -370,26 +370,22 @@ __contract__(
  * Name:        mld_poly_use_hint_32_native
  *
  * Description: Native implementation of poly_use_hint for GAMMA2 = (Q-1)/32.
- *              Use hint polynomial to correct the high bits of a polynomial.
+ *              Use hint h to correct the high bits of a in-place.
  *
- * Arguments:   - int32_t *b: pointer to output polynomial with corrected high
- *                            bits
- *              - const int32_t *a: pointer to input polynomial
- *              - const int32_t *h: pointer to input hint polynomial
+ * Arguments:   - int32_t *a: input/output polynomial
+ *              - const int32_t *h: hint polynomial
  **************************************************/
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
-  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
   ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
-  ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(b, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
-  ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(b, MLDSA_N))
+  ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+  ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N))
 );
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
           || MLD_CONFIG_PARAMETER_SET == 87 */
@@ -401,26 +397,22 @@ __contract__(
  * Name:        mld_poly_use_hint_88_native
  *
  * Description: Native implementation of poly_use_hint for GAMMA2 = (Q-1)/88.
- *              Use hint polynomial to correct the high bits of a polynomial.
+ *              Use hint h to correct the high bits of a in-place.
  *
- * Arguments:   - int32_t *b: pointer to output polynomial with corrected high
- *                            bits
- *              - const int32_t *a: pointer to input polynomial
- *              - const int32_t *h: pointer to input hint polynomial
+ * Arguments:   - int32_t *a: input/output polynomial
+ *              - const int32_t *h: hint polynomial
  **************************************************/
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
-  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
   ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
-  ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(b, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
-  ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(b, MLDSA_N))
+  ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_bound(a, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+  ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(a, MLDSA_N))
 );
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
         */
diff --git a/mldsa/src/native/x86_64/meta.h b/mldsa/src/native/x86_64/meta.h
index 23600f9d5..6fba6ef36 100644
--- a/mldsa/src/native/x86_64/meta.h
+++ b/mldsa/src/native/x86_64/meta.h
@@ -189,14 +189,13 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
     (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
 {
   if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2))
   {
     return MLD_NATIVE_FUNC_FALLBACK;
   }
-  mld_poly_use_hint_32_avx2(b, a, h);
+  mld_poly_use_hint_32_avx2(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
@@ -204,14 +203,13 @@ static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
 
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
 MLD_MUST_CHECK_RETURN_VALUE
-static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
-                                                  const int32_t *h)
+static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
 {
   if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2))
   {
     return MLD_NATIVE_FUNC_FALLBACK;
   }
-  mld_poly_use_hint_88_avx2(b, a, h);
+  mld_poly_use_hint_88_avx2(a, h);
   return MLD_NATIVE_FUNC_SUCCESS;
 }
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
diff --git a/mldsa/src/native/x86_64/src/arith_native_x86_64.h b/mldsa/src/native/x86_64/src/arith_native_x86_64.h
index b5fd4e9b8..bcbfd6cfa 100644
--- a/mldsa/src/native/x86_64/src/arith_native_x86_64.h
+++ b/mldsa/src/native/x86_64/src/arith_native_x86_64.h
@@ -103,10 +103,10 @@ void mld_poly_caddq_avx2(int32_t *r);
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_avx2 MLD_NAMESPACE(mld_poly_use_hint_32_avx2)
-void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_32_avx2(int32_t *a, const int32_t *h);
 
 #define mld_poly_use_hint_88_avx2 MLD_NAMESPACE(mld_poly_use_hint_88_avx2)
-void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_88_avx2(int32_t *a, const int32_t *h);
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
 #define mld_poly_chknorm_avx2 MLD_NAMESPACE(mld_poly_chknorm_avx2)
diff --git a/mldsa/src/native/x86_64/src/poly_use_hint_32_avx2.c b/mldsa/src/native/x86_64/src/poly_use_hint_32_avx2.c
index b2702f01a..9a9edfa53 100644
--- a/mldsa/src/native/x86_64/src/poly_use_hint_32_avx2.c
+++ b/mldsa/src/native/x86_64/src/poly_use_hint_32_avx2.c
@@ -34,8 +34,7 @@
                                        _mm256_castsi256_ps(b), \
                                        _mm256_castsi256_ps(mask)))
 
-void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a,
-                               const int32_t *hint)
+void mld_poly_use_hint_32_avx2(int32_t *a, const int32_t *hint)
 {
   unsigned int i;
   __m256i f, f0, f1, h, t;
@@ -83,7 +82,7 @@ void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a,
     f1 = _mm256_add_epi32(f1, h);
     f1 = _mm256_and_si256(f1, mask);
 
-    _mm256_store_si256((__m256i *)&b[8 * i], f1);
+    _mm256_store_si256((__m256i *)&a[8 * i], f1);
   }
 }
 
diff --git a/mldsa/src/native/x86_64/src/poly_use_hint_88_avx2.c b/mldsa/src/native/x86_64/src/poly_use_hint_88_avx2.c
index 01c17bb54..41112a2a3 100644
--- a/mldsa/src/native/x86_64/src/poly_use_hint_88_avx2.c
+++ b/mldsa/src/native/x86_64/src/poly_use_hint_88_avx2.c
@@ -34,8 +34,7 @@
                                        _mm256_castsi256_ps(b), \
                                        _mm256_castsi256_ps(mask)))
 
-void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a,
-                               const int32_t *hint)
+void mld_poly_use_hint_88_avx2(int32_t *a, const int32_t *hint)
 {
   unsigned int i;
   __m256i f, f0, f1, h, t;
@@ -85,7 +84,7 @@ void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a,
     f = _mm256_cmpgt_epi32(f1, max);
     f1 = MLD_MM256_BLENDV_EPI32(f1, zero, f);
 
-    _mm256_store_si256((__m256i *)&b[8 * i], f1);
+    _mm256_store_si256((__m256i *)&a[8 * i], f1);
   }
 }
 
diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c
index b92eaafce..58616e10f 100644
--- a/mldsa/src/poly_kl.c
+++ b/mldsa/src/poly_kl.c
@@ -127,16 +127,14 @@ unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0,
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
-MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *b, const mld_poly *a,
-                                             const mld_poly *h)
+MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *a, const mld_poly *h)
 __contract__(
-  requires(memory_no_alias(a,  sizeof(mld_poly)))
-  requires(memory_no_alias(b, sizeof(mld_poly)))
+  requires(memory_no_alias(a, sizeof(mld_poly)))
   requires(memory_no_alias(h, sizeof(mld_poly)))
   requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(mld_poly)))
-  ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+  assigns(memory_slice(a, sizeof(mld_poly)))
+  ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
 )
 {
   unsigned int i;
@@ -146,26 +144,27 @@ __contract__(
   for (i = 0; i < MLDSA_N; ++i)
   __loop__(
     invariant(i <= MLDSA_N)
-    invariant(array_bound(b->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+    invariant(array_bound(a->coeffs, 0, i, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+    invariant(array_bound(a->coeffs, i, MLDSA_N, 0, MLDSA_Q))
     decreases(MLDSA_N - i)
   )
   {
-    b->coeffs[i] = mld_use_hint(a->coeffs[i], h->coeffs[i]);
+    a->coeffs[i] = mld_use_hint(a->coeffs[i], h->coeffs[i]);
   }
-  mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
+  mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
 }
 
 MLD_INTERNAL_API
-void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
+void mld_poly_use_hint(mld_poly *a, const mld_poly *h)
 {
 #if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) && MLD_CONFIG_PARAMETER_SET == 44
   int ret;
   mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
   mld_assert_bound(h->coeffs, MLDSA_N, 0, 2);
-  ret = mld_poly_use_hint_88_native(b->coeffs, a->coeffs, h->coeffs);
+  ret = mld_poly_use_hint_88_native(a->coeffs, h->coeffs);
   if (ret == MLD_NATIVE_FUNC_SUCCESS)
   {
-    mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
+    mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
     return;
   }
 #elif defined(MLD_USE_NATIVE_POLY_USE_HINT_32) && \
@@ -173,16 +172,16 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
   int ret;
   mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
   mld_assert_bound(h->coeffs, MLDSA_N, 0, 2);
-  ret = mld_poly_use_hint_32_native(b->coeffs, a->coeffs, h->coeffs);
+  ret = mld_poly_use_hint_32_native(a->coeffs, h->coeffs);
   if (ret == MLD_NATIVE_FUNC_SUCCESS)
   {
-    mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
+    mld_assert_bound(a->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
     return;
   }
 #endif /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \
           && MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET ==   \
           65 || MLD_CONFIG_PARAMETER_SET == 87) */
-  mld_poly_use_hint_c(b, a, h);
+  mld_poly_use_hint_c(a, h);
 }
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h
index 99c31129e..bcf9c8e72 100644
--- a/mldsa/src/poly_kl.h
+++ b/mldsa/src/poly_kl.h
@@ -77,23 +77,20 @@ __contract__(
 /*************************************************
  * Name:        mld_poly_use_hint
  *
- * Description: Use hint polynomial to correct the high bits of a polynomial.
+ * Description: Use hint polynomial h to correct the high bits of a in-place.
  *
- * Arguments:   - mld_poly *b: pointer to output polynomial with corrected high
- *bits
- *              - const mld_poly *a: pointer to input polynomial
- *              - const mld_poly *h: pointer to input hint polynomial
+ * Arguments:   - mld_poly *a: input/output polynomial
+ *              - const mld_poly *h: hint polynomial
  **************************************************/
 MLD_INTERNAL_API
-void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
+void mld_poly_use_hint(mld_poly *a, const mld_poly *h)
 __contract__(
-  requires(memory_no_alias(a,  sizeof(mld_poly)))
-  requires(memory_no_alias(b, sizeof(mld_poly)))
+  requires(memory_no_alias(a, sizeof(mld_poly)))
   requires(memory_no_alias(h, sizeof(mld_poly)))
   requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(mld_poly)))
-  ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+  assigns(memory_slice(a, sizeof(mld_poly)))
+  ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
 );
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c
index 53fc8303c..f0ecc2f4e 100644
--- a/mldsa/src/polyvec.c
+++ b/mldsa/src/polyvec.c
@@ -513,8 +513,7 @@ void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0)
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 MLD_INTERNAL_API
-void mld_polyveck_use_hint(mld_polyveck *w, const mld_polyveck *u,
-                           const mld_polyveck *h)
+void mld_polyveck_use_hint(mld_polyveck *u, const mld_polyveck *h)
 {
   unsigned int i;
   mld_assert_bound_2d(u->vec, MLDSA_K, MLDSA_N, 0, MLDSA_Q);
@@ -522,18 +521,20 @@ void mld_polyveck_use_hint(mld_polyveck *w, const mld_polyveck *u,
 
   for (i = 0; i < MLDSA_K; ++i)
   __loop__(
-    assigns(i, memory_slice(w, sizeof(mld_polyveck)))
+    assigns(i, memory_slice(u, sizeof(mld_polyveck)))
     invariant(i <= MLDSA_K)
     invariant(forall(k2, 0, i,
-                     array_bound(w->vec[k2].coeffs, 0, MLDSA_N, 0,
+                     array_bound(u->vec[k2].coeffs, 0, MLDSA_N, 0,
                                  (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2))))
+    invariant(forall(k3, i, MLDSA_K,
+                     array_bound(u->vec[k3].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
     decreases(MLDSA_K - i)
   )
   {
-    mld_poly_use_hint(&w->vec[i], &u->vec[i], &h->vec[i]);
+    mld_poly_use_hint(&u->vec[i], &h->vec[i]);
   }
 
-  mld_assert_bound_2d(w->vec, MLDSA_K, MLDSA_N, 0,
+  mld_assert_bound_2d(u->vec, MLDSA_K, MLDSA_N, 0,
                       (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
 }
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h
index 025ff0edb..6caba054d 100644
--- a/mldsa/src/polyvec.h
+++ b/mldsa/src/polyvec.h
@@ -444,27 +444,23 @@ __contract__(
 /*************************************************
  * Name:        mld_polyveck_use_hint
  *
- * Description: Use hint vector to correct the high bits of input vector.
+ * Description: Use hint vector h to correct the high bits of u in-place.
  *
- * Arguments:   - mld_polyveck *w: pointer to output vector of polynomials with
- *                             corrected high bits
- *              - const mld_polyveck *u: pointer to input vector
- *              - const mld_polyveck *h: pointer to input hint vector
+ * Arguments:   - mld_polyveck *u: input/output vector
+ *              - const mld_polyveck *h: hint vector
  **************************************************/
 MLD_INTERNAL_API
-void mld_polyveck_use_hint(mld_polyveck *w, const mld_polyveck *v,
-                           const mld_polyveck *h)
+void mld_polyveck_use_hint(mld_polyveck *u, const mld_polyveck *h)
 __contract__(
-  requires(memory_no_alias(w,  sizeof(mld_polyveck)))
-  requires(memory_no_alias(v, sizeof(mld_polyveck)))
+  requires(memory_no_alias(u, sizeof(mld_polyveck)))
   requires(memory_no_alias(h, sizeof(mld_polyveck)))
   requires(forall(k0, 0, MLDSA_K,
-    array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
+    array_bound(u->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
   requires(forall(k1, 0, MLDSA_K,
     array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
-  assigns(memory_slice(w, sizeof(mld_polyveck)))
+  assigns(memory_slice(u, sizeof(mld_polyveck)))
   ensures(forall(k2, 0, MLDSA_K,
-    array_bound(w->vec[k2].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))))
+    array_bound(u->vec[k2].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))))
 );
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
index 43f0b86dc..3d59ce5cd 100644
--- a/mldsa/src/sign.c
+++ b/mldsa/src/sign.c
@@ -1051,14 +1051,6 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
 {
   int ret, cmp;
 
-  typedef union
-  {
-    mld_polyveck t1;
-    mld_polyveck w1;
-  } t1w1_u;
-  mld_polyveck *t1;
-  mld_polyveck *w1;
-
   MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), context);
   MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES, context);
   MLD_ALLOC(mu, uint8_t, MLDSA_CRHBYTES, context);
@@ -1067,19 +1059,17 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
   MLD_ALLOC(cp, mld_poly, 1, context);
   MLD_ALLOC(mat, mld_polymat, 1, context);
   MLD_ALLOC(z, mld_polyvecl, 1, context);
-  MLD_ALLOC(t1w1, t1w1_u, 1, context);
+  MLD_ALLOC(t1, mld_polyveck, 1, context);
   MLD_ALLOC(tmp, mld_polyveck, 1, context);
   MLD_ALLOC(h, mld_polyveck, 1, context);
 
   if (buf == NULL || rho == NULL || mu == NULL || c == NULL || c2 == NULL ||
-      cp == NULL || mat == NULL || z == NULL || t1w1 == NULL || tmp == NULL ||
+      cp == NULL || mat == NULL || z == NULL || t1 == NULL || tmp == NULL ||
       h == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
-  t1 = &t1w1->t1;
-  w1 = &t1w1->w1;
 
   if (siglen != MLDSA_CRYPTO_BYTES)
   {
@@ -1136,8 +1126,8 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
 
   /* Reconstruct w1 */
   mld_polyveck_caddq(tmp);
-  mld_polyveck_use_hint(w1, tmp, h);
-  mld_polyveck_pack_w1(buf, w1);
+  mld_polyveck_use_hint(tmp, h);
+  mld_polyveck_pack_w1(buf, tmp);
   /* Call random oracle and verify challenge */
   mld_H(c2, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, buf,
         MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
@@ -1153,7 +1143,7 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
   MLD_FREE(h, mld_polyveck, 1, context);
   MLD_FREE(tmp, mld_polyveck, 1, context);
-  MLD_FREE(t1w1, t1w1_u, 1, context);
+  MLD_FREE(t1, mld_polyveck, 1, context);
   MLD_FREE(z, mld_polyvecl, 1, context);
   MLD_FREE(mat, mld_polymat, 1, context);
   MLD_FREE(cp, mld_poly, 1, context);
diff --git a/proofs/cbmc/poly_use_hint/poly_use_hint_harness.c b/proofs/cbmc/poly_use_hint/poly_use_hint_harness.c
index 360de6d3f..bf3e43b4f 100644
--- a/proofs/cbmc/poly_use_hint/poly_use_hint_harness.c
+++ b/proofs/cbmc/poly_use_hint/poly_use_hint_harness.c
@@ -6,6 +6,6 @@
 
 void harness(void)
 {
-  mld_poly *a, *b, *h;
-  mld_poly_use_hint(b, a, h);
+  mld_poly *a, *h;
+  mld_poly_use_hint(a, h);
 }
diff --git a/proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c b/proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c
index 0b17ee2be..e358e2aab 100644
--- a/proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c
+++ b/proofs/cbmc/poly_use_hint_c/poly_use_hint_c_harness.c
@@ -5,11 +5,11 @@
 
 // Prototype for the function under test
 #define mld_poly_use_hint_c MLD_ADD_PARAM_SET(mld_poly_use_hint_c)
-void mld_poly_use_hint_c(mld_poly *b, mld_poly *a, mld_poly *h);
+void mld_poly_use_hint_c(mld_poly *a, mld_poly *h);
 
 
 void harness(void)
 {
-  mld_poly *a, *b, *h;
-  mld_poly_use_hint_c(b, a, h);
+  mld_poly *a, *h;
+  mld_poly_use_hint_c(a, h);
 }
diff --git a/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c b/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c
index 360de6d3f..bf3e43b4f 100644
--- a/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c
+++ b/proofs/cbmc/poly_use_hint_native/poly_use_hint_native_harness.c
@@ -6,6 +6,6 @@
 
 void harness(void)
 {
-  mld_poly *a, *b, *h;
-  mld_poly_use_hint(b, a, h);
+  mld_poly *a, *h;
+  mld_poly_use_hint(a, h);
 }
diff --git a/proofs/cbmc/poly_use_hint_native_aarch64/poly_use_hint_native_aarch64_harness.c b/proofs/cbmc/poly_use_hint_native_aarch64/poly_use_hint_native_aarch64_harness.c
index 3b0e943dd..bae3059b6 100644
--- a/proofs/cbmc/poly_use_hint_native_aarch64/poly_use_hint_native_aarch64_harness.c
+++ b/proofs/cbmc/poly_use_hint_native_aarch64/poly_use_hint_native_aarch64_harness.c
@@ -6,19 +6,19 @@
 #include "params.h"
 
 #if MLDSA_GAMMA2 == ((MLDSA_Q - 1) / 88)
-int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a, const int32_t *h);
+int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h);
 #else
-int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a, const int32_t *h);
+int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h);
 #endif
 
 void harness(void)
 {
-  int32_t *b, *a, *h;
+  int32_t *a, *h;
   int t;
 
 #if MLDSA_GAMMA2 == ((MLDSA_Q - 1) / 88)
-  t = mld_poly_use_hint_88_native(b, a, h);
+  t = mld_poly_use_hint_88_native(a, h);
 #else
-  t = mld_poly_use_hint_32_native(b, a, h);
+  t = mld_poly_use_hint_32_native(a, h);
 #endif
 }
diff --git a/proofs/cbmc/polyveck_use_hint/polyveck_use_hint_harness.c b/proofs/cbmc/polyveck_use_hint/polyveck_use_hint_harness.c
index 99924a89e..c01f2c000 100644
--- a/proofs/cbmc/polyveck_use_hint/polyveck_use_hint_harness.c
+++ b/proofs/cbmc/polyveck_use_hint/polyveck_use_hint_harness.c
@@ -5,6 +5,6 @@
 
 void harness(void)
 {
-  mld_polyveck *a, *b, *c;
-  mld_polyveck_use_hint(a, b, c);
+  mld_polyveck *a, *h;
+  mld_polyveck_use_hint(a, h);
 }
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
index 3d788eeef..c2f8d27c5 100644
--- 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
@@ -36,14 +36,14 @@ PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm:
         mov x3, #0x10               // =16
 
 Lpoly_use_hint_32_loop:
-        ldr q1, [x1, #0x10]
-        ldr q2, [x1, #0x20]
-        ldr q3, [x1, #0x30]
-        ldr q0, [x1], #0x40
-        ldr q5, [x2, #0x10]
-        ldr q6, [x2, #0x20]
-        ldr q7, [x2, #0x30]
-        ldr q4, [x2], #0x40
+        ldr q1, [x0, #0x10]
+        ldr q2, [x0, #0x20]
+        ldr q3, [x0, #0x30]
+        ldr q0, [x0]
+        ldr q5, [x1, #0x10]
+        ldr q6, [x1, #0x20]
+        ldr q7, [x1, #0x30]
+        ldr q4, [x1], #0x40
         sqdmulh v17.4s, v1.4s, v23.4s
         srshr v17.4s, v17.4s, #0x12
         cmgt v25.4s, v1.4s, v21.4s
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
index d40d410dd..ef03935f9 100644
--- 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
@@ -36,14 +36,14 @@ PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_88_asm:
         mov x3, #0x10               // =16
 
 Lpoly_use_hint_88_loop:
-        ldr q1, [x1, #0x10]
-        ldr q2, [x1, #0x20]
-        ldr q3, [x1, #0x30]
-        ldr q0, [x1], #0x40
-        ldr q5, [x2, #0x10]
-        ldr q6, [x2, #0x20]
-        ldr q7, [x2, #0x30]
-        ldr q4, [x2], #0x40
+        ldr q1, [x0, #0x10]
+        ldr q2, [x0, #0x20]
+        ldr q3, [x0, #0x30]
+        ldr q0, [x0]
+        ldr q5, [x1, #0x10]
+        ldr q6, [x1, #0x20]
+        ldr q7, [x1, #0x30]
+        ldr q4, [x1], #0x40
         sqdmulh v17.4s, v1.4s, v23.4s
         srshr v17.4s, v17.4s, #0x11
         cmgt v25.4s, v1.4s, v21.4s
diff --git a/proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml
index 8273007e3..d9eaf46f0 100644
--- a/proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml
@@ -34,14 +34,14 @@ let poly_use_hint_32_aarch64_asm_mc = define_assert_from_elf
   0x4e040d77;       (* arm_DUP_GEN Q23 X11 32 128 *)
   0x4f0005f8;       (* arm_MOVI Q24 (word 64424509455) *)
   0xd2800203;       (* arm_MOV X3 (rvalue (word 16)) *)
-  0x3dc00421;       (* arm_LDR Q1 X1 (Immediate_Offset (word 16)) *)
-  0x3dc00822;       (* arm_LDR Q2 X1 (Immediate_Offset (word 32)) *)
-  0x3dc00c23;       (* arm_LDR Q3 X1 (Immediate_Offset (word 48)) *)
-  0x3cc40420;       (* arm_LDR Q0 X1 (Postimmediate_Offset (word 64)) *)
-  0x3dc00445;       (* arm_LDR Q5 X2 (Immediate_Offset (word 16)) *)
-  0x3dc00846;       (* arm_LDR Q6 X2 (Immediate_Offset (word 32)) *)
-  0x3dc00c47;       (* arm_LDR Q7 X2 (Immediate_Offset (word 48)) *)
-  0x3cc40444;       (* arm_LDR Q4 X2 (Postimmediate_Offset (word 64)) *)
+  0x3dc00401;       (* arm_LDR Q1 X0 (Immediate_Offset (word 16)) *)
+  0x3dc00802;       (* arm_LDR Q2 X0 (Immediate_Offset (word 32)) *)
+  0x3dc00c03;       (* arm_LDR Q3 X0 (Immediate_Offset (word 48)) *)
+  0x3dc00000;       (* arm_LDR Q0 X0 (Immediate_Offset (word 0)) *)
+  0x3dc00425;       (* arm_LDR Q5 X1 (Immediate_Offset (word 16)) *)
+  0x3dc00826;       (* arm_LDR Q6 X1 (Immediate_Offset (word 32)) *)
+  0x3dc00c27;       (* arm_LDR Q7 X1 (Immediate_Offset (word 48)) *)
+  0x3cc40424;       (* arm_LDR Q4 X1 (Postimmediate_Offset (word 64)) *)
   0x4eb7b431;       (* arm_SQDMULH_VEC Q17 Q1 Q23 32 128 *)
   0x4f2e2631;       (* arm_SRSHR_VEC Q17 Q17 18 32 128 *)
   0x4eb53439;       (* arm_CMGT_VEC Q25 Q1 Q21 32 128 *)
@@ -404,14 +404,13 @@ let ELEMENT_CORRECT_WORD = prove(
 (* ========================================================================= *)
 
 let POLY_USE_HINT_32_AARCH64_ASM_CORRECT_CODE = prove
- (`!b a h x y pc.
-    nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (b, 1024) /\
-    nonoverlapping (b, 1024) (a, 1024) /\
-    nonoverlapping (b, 1024) (h, 1024)
+ (`!a h x y pc.
+    nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (a, 1024) /\
+    nonoverlapping (a, 1024) (h, 1024)
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) poly_use_hint_32_aarch64_asm_mc /\
                read PC s = word pc /\
-               C_ARGUMENTS [b; a; h] s /\
+               C_ARGUMENTS [a; h] s /\
                (!i. i < 256 ==> val(x i) < 8380417) /\
                (!i. i < 256 ==> val(y i) <= 1) /\
                (!i. i < 256 ==>
@@ -420,14 +419,14 @@ let POLY_USE_HINT_32_AARCH64_ASM_CORRECT_CODE = prove
                  read(memory :> bytes32(word_add h (word(4 * i)))) s = y i))
           (\s. read PC s = word(pc + LENGTH poly_use_hint_32_aarch64_asm_mc - 4) /\
                (!i. i < 256 ==>
-                 read(memory :> bytes32(word_add b (word(4 * i)))) s =
+                 read(memory :> bytes32(word_add a (word(4 * i)))) s =
                  word(mldsa_use_hint_32_code (val(x i)) (val(y i)))))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
-           MAYCHANGE [memory :> bytes(b, 1024)])`,
+           MAYCHANGE [memory :> bytes(a, 1024)])`,
 
   (* Setup *)
   MAP_EVERY X_GEN_TAC
-    [`b:int64`; `a:int64`; `h:int64`;
+    [`a:int64`; `h:int64`;
      `x:num->int32`; `y:num->int32`; `pc:num`] THEN
   REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
               NONOVERLAPPING_CLAUSES; ALL;
@@ -496,14 +495,13 @@ let POLY_USE_HINT_32_AARCH64_ASM_CORRECT_CODE = prove
 (* ========================================================================= *)
 
 let POLY_USE_HINT_32_AARCH64_ASM_CORRECT_BOUND_CODE = prove
- (`!b a h x y pc.
-    nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (b, 1024) /\
-    nonoverlapping (b, 1024) (a, 1024) /\
-    nonoverlapping (b, 1024) (h, 1024)
+ (`!a h x y pc.
+    nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (a, 1024) /\
+    nonoverlapping (a, 1024) (h, 1024)
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) poly_use_hint_32_aarch64_asm_mc /\
                read PC s = word pc /\
-               C_ARGUMENTS [b; a; h] s /\
+               C_ARGUMENTS [a; h] s /\
                (!i. i < 256 ==> val(x i) < 8380417) /\
                (!i. i < 256 ==> val(y i) <= 1) /\
                (!i. i < 256 ==>
@@ -512,18 +510,18 @@ let POLY_USE_HINT_32_AARCH64_ASM_CORRECT_BOUND_CODE = prove
                  read(memory :> bytes32(word_add h (word(4 * i)))) s = y i))
           (\s. read PC s = word(pc + LENGTH poly_use_hint_32_aarch64_asm_mc - 4) /\
                (!i. i < 256 ==>
-                 read(memory :> bytes32(word_add b (word(4 * i)))) s =
+                 read(memory :> bytes32(word_add a (word(4 * i)))) s =
                    word(mldsa_use_hint_32_code (val(x i)) (val(y i)))) /\
                (!i. i < 256 ==>
-                 val(read(memory :> bytes32(word_add b (word(4 * i)))) s) < 16))
+                 val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 16))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
-           MAYCHANGE [memory :> bytes(b, 1024)])`,
+           MAYCHANGE [memory :> bytes(a, 1024)])`,
   REPEAT GEN_TAC THEN DISCH_TAC THEN
   MATCH_MP_TAC ENSURES_STRENGTHEN_POST THEN
   EXISTS_TAC
    `\s. read PC s = word(pc + LENGTH poly_use_hint_32_aarch64_asm_mc - 4) /\
         (!i. i < 256 ==>
-          read(memory :> bytes32(word_add b (word(4 * i)))) s =
+          read(memory :> bytes32(word_add a (word(4 * i)))) s =
             word(mldsa_use_hint_32_code (val(x i:int32)) (val(y i:int32))))` THEN
   CONJ_TAC THENL
   [MATCH_MP_TAC POLY_USE_HINT_32_AARCH64_ASM_CORRECT_CODE THEN ASM_REWRITE_TAC[];
@@ -540,15 +538,14 @@ let POLY_USE_HINT_32_AARCH64_ASM_CORRECT_BOUND_CODE = prove
    Bridged to the public FIPS 204-aligned theorem below via
    MLDSA_USE_HINT_32_EQUIV. *)
 let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT_CODE = prove
- (`!b a h x y pc returnaddress.
-    nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (b, 1024) /\
-    nonoverlapping (b, 1024) (a, 1024) /\
-    nonoverlapping (b, 1024) (h, 1024)
+ (`!a h x y pc returnaddress.
+    nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (a, 1024) /\
+    nonoverlapping (a, 1024) (h, 1024)
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) poly_use_hint_32_aarch64_asm_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
-               C_ARGUMENTS [b; a; h] s /\
+               C_ARGUMENTS [a; h] s /\
                (!i. i < 256 ==> val(x i) < 8380417) /\
                (!i. i < 256 ==> val(y i) <= 1) /\
                (!i. i < 256 ==>
@@ -557,12 +554,12 @@ let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT_CODE = prove
                  read(memory :> bytes32(word_add h (word(4 * i)))) s = y i))
           (\s. read PC s = returnaddress /\
                (!i. i < 256 ==>
-                 read(memory :> bytes32(word_add b (word(4 * i)))) s =
+                 read(memory :> bytes32(word_add a (word(4 * i)))) s =
                    word(mldsa_use_hint_32_code (val(x i)) (val(y i)))) /\
                (!i. i < 256 ==>
-                 val(read(memory :> bytes32(word_add b (word(4 * i)))) s) < 16))
+                 val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 16))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
-           MAYCHANGE [memory :> bytes(b, 1024)])`,
+           MAYCHANGE [memory :> bytes(a, 1024)])`,
   REWRITE_TAC[fst POLY_USE_HINT_32_AARCH64_ASM_EXEC] THEN
   CONV_TAC NUM_REDUCE_CONV THEN
   ARM_ADD_RETURN_NOSTACK_TAC POLY_USE_HINT_32_AARCH64_ASM_EXEC
@@ -872,17 +869,16 @@ let MLDSA_USE_HINT_32_EQUIV = prove(
    rewriting mldsa_use_hint_32_code -> mldsa_use_hint_32 via
    MLDSA_USE_HINT_32_EQUIV. *)
 let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT = prove
- (`!b a h x y pc returnaddress.
-    nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (b, 1024) /\
-    nonoverlapping (b, 1024) (a, 1024) /\
-    nonoverlapping (b, 1024) (h, 1024) /\
+ (`!a h x y pc returnaddress.
+    nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (a, 1024) /\
+    nonoverlapping (a, 1024) (h, 1024) /\
     (!i. i < 256 ==> val((x:num->int32) i) < 8380417) /\
     (!i. i < 256 ==> val((y:num->int32) i) <= 1)
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) poly_use_hint_32_aarch64_asm_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
-               C_ARGUMENTS [b; a; h] s /\
+               C_ARGUMENTS [a; h] s /\
                (!i. i < 256 ==> val(x i) < 8380417) /\
                (!i. i < 256 ==> val(y i) <= 1) /\
                (!i. i < 256 ==>
@@ -891,12 +887,12 @@ let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT = prove
                  read(memory :> bytes32(word_add h (word(4 * i)))) s = y i))
           (\s. read PC s = returnaddress /\
                (!i. i < 256 ==>
-                 read(memory :> bytes32(word_add b (word(4 * i)))) s =
+                 read(memory :> bytes32(word_add a (word(4 * i)))) s =
                    word(mldsa_use_hint_32 (val(y i)) (val(x i)))) /\
                (!i. i < 256 ==>
-                 val(read(memory :> bytes32(word_add b (word(4 * i)))) s) < 16))
+                 val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 16))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
-           MAYCHANGE [memory :> bytes(b, 1024)])`,
+           MAYCHANGE [memory :> bytes(a, 1024)])`,
   REPEAT GEN_TAC THEN
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
   SUBGOAL_THEN
@@ -926,25 +922,24 @@ let full_spec,public_vars = mk_safety_spec
 
 let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_SAFE = time prove
  (`exists f_events.
-       forall e b a h pc returnaddress.
-           nonoverlapping (word pc,LENGTH poly_use_hint_32_aarch64_asm_mc) (b,1024) /\
-           nonoverlapping (b,1024) (a,1024) /\
-           nonoverlapping (b,1024) (h,1024)
+       forall e a h pc returnaddress.
+           nonoverlapping (word pc,LENGTH poly_use_hint_32_aarch64_asm_mc) (a,1024) /\
+           nonoverlapping (a,1024) (h,1024)
            ==> ensures arm
                (\s.
                     aligned_bytes_loaded s (word pc)
                     poly_use_hint_32_aarch64_asm_mc /\
                     read PC s = word pc /\
                     read X30 s = returnaddress /\
-                    C_ARGUMENTS [b; a; h] s /\
+                    C_ARGUMENTS [a; h] s /\
                     read events s = e)
                (\s.
                     read PC s = returnaddress /\
                     (exists e2.
                          read events s = APPEND e2 e /\
-                         e2 = f_events a h b pc returnaddress /\
-                         memaccess_inbounds e2 [a,1024; h,1024; b,1024]
-                         [b,1024]))
+                         e2 = f_events h a pc returnaddress /\
+                         memaccess_inbounds e2 [a,1024; h,1024]
+                         [a,1024]))
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars POLY_USE_HINT_32_AARCH64_ASM_EXEC);;
diff --git a/proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml
index f2ed72dca..20ab36769 100644
--- a/proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml
@@ -34,14 +34,14 @@ let poly_use_hint_88_aarch64_asm_mc = define_assert_from_elf
   0x4e040d77;       (* arm_DUP_GEN Q23 X11 32 128 *)
   0x4f010578;       (* arm_MOVI Q24 (word 184683593771) *)
   0xd2800203;       (* arm_MOV X3 (rvalue (word 16)) *)
-  0x3dc00421;       (* arm_LDR Q1 X1 (Immediate_Offset (word 16)) *)
-  0x3dc00822;       (* arm_LDR Q2 X1 (Immediate_Offset (word 32)) *)
-  0x3dc00c23;       (* arm_LDR Q3 X1 (Immediate_Offset (word 48)) *)
-  0x3cc40420;       (* arm_LDR Q0 X1 (Postimmediate_Offset (word 64)) *)
-  0x3dc00445;       (* arm_LDR Q5 X2 (Immediate_Offset (word 16)) *)
-  0x3dc00846;       (* arm_LDR Q6 X2 (Immediate_Offset (word 32)) *)
-  0x3dc00c47;       (* arm_LDR Q7 X2 (Immediate_Offset (word 48)) *)
-  0x3cc40444;       (* arm_LDR Q4 X2 (Postimmediate_Offset (word 64)) *)
+  0x3dc00401;       (* arm_LDR Q1 X0 (Immediate_Offset (word 16)) *)
+  0x3dc00802;       (* arm_LDR Q2 X0 (Immediate_Offset (word 32)) *)
+  0x3dc00c03;       (* arm_LDR Q3 X0 (Immediate_Offset (word 48)) *)
+  0x3dc00000;       (* arm_LDR Q0 X0 (Immediate_Offset (word 0)) *)
+  0x3dc00425;       (* arm_LDR Q5 X1 (Immediate_Offset (word 16)) *)
+  0x3dc00826;       (* arm_LDR Q6 X1 (Immediate_Offset (word 32)) *)
+  0x3dc00c27;       (* arm_LDR Q7 X1 (Immediate_Offset (word 48)) *)
+  0x3cc40424;       (* arm_LDR Q4 X1 (Postimmediate_Offset (word 64)) *)
   0x4eb7b431;       (* arm_SQDMULH_VEC Q17 Q1 Q23 32 128 *)
   0x4f2f2631;       (* arm_SRSHR_VEC Q17 Q17 17 32 128 *)
   0x4eb53439;       (* arm_CMGT_VEC Q25 Q1 Q21 32 128 *)
@@ -451,14 +451,13 @@ let ELEMENT_CORRECT_WORD_88 = prove(
 (* ========================================================================= *)
 
 let POLY_USE_HINT_88_AARCH64_ASM_CORRECT_CODE = prove
- (`!b a h x y pc.
-    nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (b, 1024) /\
-    nonoverlapping (b, 1024) (a, 1024) /\
-    nonoverlapping (b, 1024) (h, 1024)
+ (`!a h x y pc.
+    nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (a, 1024) /\
+    nonoverlapping (a, 1024) (h, 1024)
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) poly_use_hint_88_aarch64_asm_mc /\
                read PC s = word pc /\
-               C_ARGUMENTS [b; a; h] s /\
+               C_ARGUMENTS [a; h] s /\
                (!i. i < 256 ==> val(x i) < 8380417) /\
                (!i. i < 256 ==> val(y i) <= 1) /\
                (!i. i < 256 ==>
@@ -467,13 +466,13 @@ let POLY_USE_HINT_88_AARCH64_ASM_CORRECT_CODE = prove
                  read(memory :> bytes32(word_add h (word(4 * i)))) s = y i))
           (\s. read PC s = word(pc + LENGTH poly_use_hint_88_aarch64_asm_mc - 4) /\
                (!i. i < 256 ==>
-                 read(memory :> bytes32(word_add b (word(4 * i)))) s =
+                 read(memory :> bytes32(word_add a (word(4 * i)))) s =
                    word(mldsa_use_hint_88_code (val(x i)) (val(y i)))))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
-           MAYCHANGE [memory :> bytes(b, 1024)])`,
+           MAYCHANGE [memory :> bytes(a, 1024)])`,
 
   MAP_EVERY X_GEN_TAC
-    [`b:int64`; `a:int64`; `h:int64`;
+    [`a:int64`; `h:int64`;
      `x:num->int32`; `y:num->int32`; `pc:num`] THEN
   REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
               NONOVERLAPPING_CLAUSES; ALL;
@@ -534,14 +533,13 @@ let POLY_USE_HINT_88_AARCH64_ASM_CORRECT_CODE = prove
 (* ========================================================================= *)
 
 let POLY_USE_HINT_88_AARCH64_ASM_CORRECT_BOUND_CODE = prove
- (`!b a h x y pc.
-    nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (b, 1024) /\
-    nonoverlapping (b, 1024) (a, 1024) /\
-    nonoverlapping (b, 1024) (h, 1024)
+ (`!a h x y pc.
+    nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (a, 1024) /\
+    nonoverlapping (a, 1024) (h, 1024)
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) poly_use_hint_88_aarch64_asm_mc /\
                read PC s = word pc /\
-               C_ARGUMENTS [b; a; h] s /\
+               C_ARGUMENTS [a; h] s /\
                (!i. i < 256 ==> val(x i) < 8380417) /\
                (!i. i < 256 ==> val(y i) <= 1) /\
                (!i. i < 256 ==>
@@ -550,18 +548,18 @@ let POLY_USE_HINT_88_AARCH64_ASM_CORRECT_BOUND_CODE = prove
                  read(memory :> bytes32(word_add h (word(4 * i)))) s = y i))
           (\s. read PC s = word(pc + LENGTH poly_use_hint_88_aarch64_asm_mc - 4) /\
                (!i. i < 256 ==>
-                 read(memory :> bytes32(word_add b (word(4 * i)))) s =
+                 read(memory :> bytes32(word_add a (word(4 * i)))) s =
                    word(mldsa_use_hint_88_code (val(x i)) (val(y i)))) /\
                (!i. i < 256 ==>
-                 val(read(memory :> bytes32(word_add b (word(4 * i)))) s) < 44))
+                 val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 44))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
-           MAYCHANGE [memory :> bytes(b, 1024)])`,
+           MAYCHANGE [memory :> bytes(a, 1024)])`,
   REPEAT GEN_TAC THEN DISCH_TAC THEN
   MATCH_MP_TAC ENSURES_STRENGTHEN_POST THEN
   EXISTS_TAC
    `\s. read PC s = word(pc + LENGTH poly_use_hint_88_aarch64_asm_mc - 4) /\
         (!i. i < 256 ==>
-          read(memory :> bytes32(word_add b (word(4 * i)))) s =
+          read(memory :> bytes32(word_add a (word(4 * i)))) s =
             word(mldsa_use_hint_88_code (val(x i:int32)) (val(y i:int32))))` THEN
   CONJ_TAC THENL
   [MATCH_MP_TAC POLY_USE_HINT_88_AARCH64_ASM_CORRECT_CODE THEN ASM_REWRITE_TAC[];
@@ -578,15 +576,14 @@ let POLY_USE_HINT_88_AARCH64_ASM_CORRECT_BOUND_CODE = prove
    Bridged to the public FIPS 204-aligned theorem below via
    MLDSA_USE_HINT_88_EQUIV. *)
 let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_CORRECT_CODE = prove
- (`!b a h x y pc returnaddress.
-    nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (b, 1024) /\
-    nonoverlapping (b, 1024) (a, 1024) /\
-    nonoverlapping (b, 1024) (h, 1024)
+ (`!a h x y pc returnaddress.
+    nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (a, 1024) /\
+    nonoverlapping (a, 1024) (h, 1024)
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) poly_use_hint_88_aarch64_asm_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
-               C_ARGUMENTS [b; a; h] s /\
+               C_ARGUMENTS [a; h] s /\
                (!i. i < 256 ==> val(x i) < 8380417) /\
                (!i. i < 256 ==> val(y i) <= 1) /\
                (!i. i < 256 ==>
@@ -595,12 +592,12 @@ let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_CORRECT_CODE = prove
                  read(memory :> bytes32(word_add h (word(4 * i)))) s = y i))
           (\s. read PC s = returnaddress /\
                (!i. i < 256 ==>
-                 read(memory :> bytes32(word_add b (word(4 * i)))) s =
+                 read(memory :> bytes32(word_add a (word(4 * i)))) s =
                    word(mldsa_use_hint_88_code (val(x i)) (val(y i)))) /\
                (!i. i < 256 ==>
-                 val(read(memory :> bytes32(word_add b (word(4 * i)))) s) < 44))
+                 val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 44))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
-           MAYCHANGE [memory :> bytes(b, 1024)])`,
+           MAYCHANGE [memory :> bytes(a, 1024)])`,
   REWRITE_TAC[fst POLY_USE_HINT_88_AARCH64_ASM_EXEC] THEN
   CONV_TAC NUM_REDUCE_CONV THEN
   ARM_ADD_RETURN_NOSTACK_TAC POLY_USE_HINT_88_AARCH64_ASM_EXEC
@@ -942,17 +939,16 @@ let MLDSA_USE_HINT_88_EQUIV = prove(
    rewriting mldsa_use_hint_88_code -> mldsa_use_hint_88 via
    MLDSA_USE_HINT_88_EQUIV. *)
 let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_CORRECT = prove
- (`!b a h x y pc returnaddress.
-    nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (b, 1024) /\
-    nonoverlapping (b, 1024) (a, 1024) /\
-    nonoverlapping (b, 1024) (h, 1024) /\
+ (`!a h x y pc returnaddress.
+    nonoverlapping (word pc, LENGTH poly_use_hint_88_aarch64_asm_mc) (a, 1024) /\
+    nonoverlapping (a, 1024) (h, 1024) /\
     (!i. i < 256 ==> val((x:num->int32) i) < 8380417) /\
     (!i. i < 256 ==> val((y:num->int32) i) <= 1)
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) poly_use_hint_88_aarch64_asm_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
-               C_ARGUMENTS [b; a; h] s /\
+               C_ARGUMENTS [a; h] s /\
                (!i. i < 256 ==> val(x i) < 8380417) /\
                (!i. i < 256 ==> val(y i) <= 1) /\
                (!i. i < 256 ==>
@@ -961,12 +957,12 @@ let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_CORRECT = prove
                  read(memory :> bytes32(word_add h (word(4 * i)))) s = y i))
           (\s. read PC s = returnaddress /\
                (!i. i < 256 ==>
-                 read(memory :> bytes32(word_add b (word(4 * i)))) s =
+                 read(memory :> bytes32(word_add a (word(4 * i)))) s =
                    word(mldsa_use_hint_88 (val(y i)) (val(x i)))) /\
                (!i. i < 256 ==>
-                 val(read(memory :> bytes32(word_add b (word(4 * i)))) s) < 44))
+                 val(read(memory :> bytes32(word_add a (word(4 * i)))) s) < 44))
           (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
-           MAYCHANGE [memory :> bytes(b, 1024)])`,
+           MAYCHANGE [memory :> bytes(a, 1024)])`,
   REPEAT GEN_TAC THEN
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
   SUBGOAL_THEN
@@ -996,25 +992,24 @@ let full_spec,public_vars = mk_safety_spec
 
 let POLY_USE_HINT_88_AARCH64_ASM_SUBROUTINE_SAFE = time prove
  (`exists f_events.
-       forall e b a h pc returnaddress.
-           nonoverlapping (word pc,LENGTH poly_use_hint_88_aarch64_asm_mc) (b,1024) /\
-           nonoverlapping (b,1024) (a,1024) /\
-           nonoverlapping (b,1024) (h,1024)
+       forall e a h pc returnaddress.
+           nonoverlapping (word pc,LENGTH poly_use_hint_88_aarch64_asm_mc) (a,1024) /\
+           nonoverlapping (a,1024) (h,1024)
            ==> ensures arm
                (\s.
                     aligned_bytes_loaded s (word pc)
                     poly_use_hint_88_aarch64_asm_mc /\
                     read PC s = word pc /\
                     read X30 s = returnaddress /\
-                    C_ARGUMENTS [b; a; h] s /\
+                    C_ARGUMENTS [a; h] s /\
                     read events s = e)
                (\s.
                     read PC s = returnaddress /\
                     (exists e2.
                          read events s = APPEND e2 e /\
-                         e2 = f_events a h b pc returnaddress /\
-                         memaccess_inbounds e2 [a,1024; h,1024; b,1024]
-                         [b,1024]))
+                         e2 = f_events h a pc returnaddress /\
+                         memaccess_inbounds e2 [a,1024; h,1024]
+                         [a,1024]))
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars POLY_USE_HINT_88_AARCH64_ASM_EXEC);;
diff --git a/proofs/hol_light/aarch64/proofs/subroutine_signatures.ml b/proofs/hol_light/aarch64/proofs/subroutine_signatures.ml
index 41e54856d..940a287d4 100644
--- a/proofs/hol_light/aarch64/proofs/subroutine_signatures.ml
+++ b/proofs/hol_light/aarch64/proofs/subroutine_signatures.ml
@@ -83,8 +83,7 @@ let subroutine_signatures = [
 
 ("poly_use_hint_32_aarch64_asm",
   ([(*args*)
-     ("b", "int32_t[static 256]", (*is const?*)"false");
-     ("a", "int32_t[static 256]", (*is const?*)"true");
+     ("a", "int32_t[static 256]", (*is const?*)"false");
      ("h", "int32_t[static 256]", (*is const?*)"true");
    ],
    "void",
@@ -93,7 +92,7 @@ let subroutine_signatures = [
     ("h", "256"(* num elems *), 4(* elem bytesize *));
    ],
    [(* output buffers *)
-    ("b", "256"(* num elems *), 4(* elem bytesize *));
+    ("a", "256"(* num elems *), 4(* elem bytesize *));
    ],
    [(* temporary buffers *)
    ])
@@ -101,8 +100,7 @@ let subroutine_signatures = [
 
 ("poly_use_hint_88_aarch64_asm",
   ([(*args*)
-     ("b", "int32_t[static 256]", (*is const?*)"false");
-     ("a", "int32_t[static 256]", (*is const?*)"true");
+     ("a", "int32_t[static 256]", (*is const?*)"false");
      ("h", "int32_t[static 256]", (*is const?*)"true");
    ],
    "void",
@@ -111,7 +109,7 @@ let subroutine_signatures = [
     ("h", "256"(* num elems *), 4(* elem bytesize *));
    ],
    [(* output buffers *)
-    ("b", "256"(* num elems *), 4(* elem bytesize *));
+    ("a", "256"(* num elems *), 4(* elem bytesize *));
    ],
    [(* temporary buffers *)
    ])
diff --git a/test/src/test_unit.c b/test/src/test_unit.c
index b3f531153..484082808 100644
--- a/test/src/test_unit.c
+++ b/test/src/test_unit.c
@@ -44,7 +44,7 @@ void mld_poly_caddq_c(mld_poly *a);
 void mld_poly_decompose_c(mld_poly *a1, mld_poly *a0);
 #endif
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
-void mld_poly_use_hint_c(mld_poly *b, const mld_poly *a, const mld_poly *h);
+void mld_poly_use_hint_c(mld_poly *a, const mld_poly *h);
 #endif
 uint32_t mld_poly_chknorm_c(const mld_poly *a, int32_t B);
 #if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
@@ -455,12 +455,14 @@ static int test_poly_use_hint_core(const mld_poly *poly_a,
                                    const mld_poly *poly_h,
                                    const char *test_name)
 {
-  mld_poly test_b, ref_b;
+  mld_poly test_a, ref_a;
 
-  mld_poly_use_hint(&test_b, poly_a, poly_h);
-  mld_poly_use_hint_c(&ref_b, poly_a, poly_h);
+  test_a = *poly_a;
+  ref_a = *poly_a;
+  mld_poly_use_hint(&test_a, poly_h);
+  mld_poly_use_hint_c(&ref_a, poly_h);
 
-  CHECK(compare_i32_arrays(test_b.coeffs, ref_b.coeffs, MLDSA_N, test_name,
+  CHECK(compare_i32_arrays(test_a.coeffs, ref_a.coeffs, MLDSA_N, test_name,
                            poly_a->coeffs));
   return 0;
 }