diff --git a/dev/aarch64_clean/src/arith_native_aarch64.h b/dev/aarch64_clean/src/arith_native_aarch64.h
index 21faa5af5f..2a4cac451b 100644
--- a/dev/aarch64_clean/src/arith_native_aarch64.h
+++ b/dev/aarch64_clean/src/arith_native_aarch64.h
@@ -67,6 +67,7 @@ void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456,
  * in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: 8380417 == MLDSA_Q */
   requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
   requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456)
   requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78)
@@ -261,12 +262,14 @@ void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *a, const int32_t *b)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
-  /* check-magic: off */
-  requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
-  requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
+  /* Input bound MLD_NTT_BOUND = 9 * MLD_FQMUL_BOUND, the post-condition of
+   * the forward NTT. Hardcoded here to keep this header free of poly.h.
+   * Must be kept in sync with the HOL-Light precondition. */
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(array_abs_bound(a, 0, MLDSA_N, 94279698))
+  requires(array_abs_bound(b, 0, MLDSA_N, 94279698))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(a, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API || \
           MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */
@@ -283,12 +286,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm \
@@ -303,12 +305,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm \
@@ -323,12 +324,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */
diff --git a/dev/aarch64_opt/src/arith_native_aarch64.h b/dev/aarch64_opt/src/arith_native_aarch64.h
index 21faa5af5f..2a4cac451b 100644
--- a/dev/aarch64_opt/src/arith_native_aarch64.h
+++ b/dev/aarch64_opt/src/arith_native_aarch64.h
@@ -67,6 +67,7 @@ void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456,
  * in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: 8380417 == MLDSA_Q */
   requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
   requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456)
   requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78)
@@ -261,12 +262,14 @@ void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *a, const int32_t *b)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
-  /* check-magic: off */
-  requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
-  requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
+  /* Input bound MLD_NTT_BOUND = 9 * MLD_FQMUL_BOUND, the post-condition of
+   * the forward NTT. Hardcoded here to keep this header free of poly.h.
+   * Must be kept in sync with the HOL-Light precondition. */
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(array_abs_bound(a, 0, MLDSA_N, 94279698))
+  requires(array_abs_bound(b, 0, MLDSA_N, 94279698))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(a, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API || \
           MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */
@@ -283,12 +286,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm \
@@ -303,12 +305,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm \
@@ -323,12 +324,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */
diff --git a/dev/x86_64/src/arith_native_x86_64.h b/dev/x86_64/src/arith_native_x86_64.h
index 3173d0bf4b..e0ffcc1f2a 100644
--- a/dev/x86_64/src/arith_native_x86_64.h
+++ b/dev/x86_64/src/arith_native_x86_64.h
@@ -37,6 +37,7 @@ void mld_ntt_avx2_asm(int32_t *r, const int32_t *qdata)
  * in proofs/hol_light/x86_64/proofs/ntt_avx2_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: 8380417 == MLDSA_Q */
   requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
   requires(qdata == mld_qdata)
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
@@ -136,13 +137,15 @@ void mld_pointwise_avx2_asm(int32_t *a, const int32_t *b, const int32_t *qdata)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
-  /* check-magic: off */
-  requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
-  requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
+  /* Input bound MLD_NTT_BOUND = 9 * MLD_FQMUL_BOUND, the post-condition of
+   * the forward NTT. Hardcoded here to keep this header free of poly.h.
+   * Must be kept in sync with the HOL-Light precondition. */
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(array_abs_bound(a, 0, MLDSA_N, 94279698))
+  requires(array_abs_bound(b, 0, MLDSA_N, 94279698))
   requires(qdata == mld_qdata)
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(a, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_pointwise_acc_l4_avx2_asm MLD_NAMESPACE(pointwise_acc_l4_avx2_asm)
@@ -156,13 +159,12 @@ __contract__(
   requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   requires(qdata == mld_qdata)
   assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_pointwise_acc_l5_avx2_asm MLD_NAMESPACE(pointwise_acc_l5_avx2_asm)
@@ -176,13 +178,12 @@ __contract__(
   requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   requires(qdata == mld_qdata)
   assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_pointwise_acc_l7_avx2_asm MLD_NAMESPACE(pointwise_acc_l7_avx2_asm)
@@ -196,13 +197,12 @@ __contract__(
   requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   requires(qdata == mld_qdata)
   assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #endif /* !MLD_NATIVE_X86_64_SRC_ARITH_NATIVE_X86_64_H */
diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c
index 503d0753a5..8e0fce16b9 100644
--- a/mldsa/mldsa_native.c
+++ b/mldsa/mldsa_native.c
@@ -442,6 +442,7 @@
 #undef mld_debug_check_assert
 #undef mld_debug_check_bounds
 /* mldsa/src/poly.h */
+#undef MLD_FQMUL_BOUND
 #undef MLD_INTT_BOUND
 #undef MLD_NTT_BOUND
 #undef MLD_POLY_H
@@ -652,6 +653,7 @@
 #endif /* MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */
 #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH)
 /* mldsa/src/native/api.h */
+#undef MLD_FQMUL_BOUND
 #undef MLD_INTT_BOUND
 #undef MLD_NATIVE_API_H
 #undef MLD_NATIVE_FUNC_FALLBACK
diff --git a/mldsa/mldsa_native_asm.S b/mldsa/mldsa_native_asm.S
index 8873e0b6fa..fd7c72af6b 100644
--- a/mldsa/mldsa_native_asm.S
+++ b/mldsa/mldsa_native_asm.S
@@ -449,6 +449,7 @@
 #undef mld_debug_check_assert
 #undef mld_debug_check_bounds
 /* mldsa/src/poly.h */
+#undef MLD_FQMUL_BOUND
 #undef MLD_INTT_BOUND
 #undef MLD_NTT_BOUND
 #undef MLD_POLY_H
@@ -659,6 +660,7 @@
 #endif /* MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */
 #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH)
 /* mldsa/src/native/api.h */
+#undef MLD_FQMUL_BOUND
 #undef MLD_INTT_BOUND
 #undef MLD_NATIVE_API_H
 #undef MLD_NATIVE_FUNC_FALLBACK
diff --git a/mldsa/src/native/aarch64/src/arith_native_aarch64.h b/mldsa/src/native/aarch64/src/arith_native_aarch64.h
index 21faa5af5f..2a4cac451b 100644
--- a/mldsa/src/native/aarch64/src/arith_native_aarch64.h
+++ b/mldsa/src/native/aarch64/src/arith_native_aarch64.h
@@ -67,6 +67,7 @@ void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456,
  * in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: 8380417 == MLDSA_Q */
   requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
   requires(zetas_l123456 == mld_aarch64_ntt_zetas_layer123456)
   requires(zetas_l78 == mld_aarch64_ntt_zetas_layer78)
@@ -261,12 +262,14 @@ void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *a, const int32_t *b)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
-  /* check-magic: off */
-  requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
-  requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
+  /* Input bound MLD_NTT_BOUND = 9 * MLD_FQMUL_BOUND, the post-condition of
+   * the forward NTT. Hardcoded here to keep this header free of poly.h.
+   * Must be kept in sync with the HOL-Light precondition. */
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(array_abs_bound(a, 0, MLDSA_N, 94279698))
+  requires(array_abs_bound(b, 0, MLDSA_N, 94279698))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(a, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API || \
           MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */
@@ -283,12 +286,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm \
@@ -303,12 +305,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm \
@@ -323,12 +324,11 @@ __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */
diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h
index 2b603b387d..b7dca2e61b 100644
--- a/mldsa/src/native/api.h
+++ b/mldsa/src/native/api.h
@@ -37,11 +37,17 @@
  */
 #define MLD_NATIVE_FUNC_FALLBACK (-1)
 
+/* Absolute exclusive upper bound for the output of fqmul.
+ *
+ * NOTE: This is the same bound as in poly.h and has to be kept
+ * in sync. */
+#define MLD_FQMUL_BOUND ((5 * MLDSA_Q + 3) / 4)
+
 /* Bound on absolute value of coefficients after NTT.
  *
  * NOTE: This is the same bound as in poly.h and has to be kept
  * in sync. */
-#define MLD_NTT_BOUND (9 * MLDSA_Q)
+#define MLD_NTT_BOUND (9 * MLD_FQMUL_BOUND)
 
 /* Absolute exclusive upper bound for the output of the inverse NTT
  *
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 3173d0bf4b..e0ffcc1f2a 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
@@ -37,6 +37,7 @@ void mld_ntt_avx2_asm(int32_t *r, const int32_t *qdata)
  * in proofs/hol_light/x86_64/proofs/ntt_avx2_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: 8380417 == MLDSA_Q */
   requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
   requires(qdata == mld_qdata)
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
@@ -136,13 +137,15 @@ void mld_pointwise_avx2_asm(int32_t *a, const int32_t *b, const int32_t *qdata)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
-  /* check-magic: off */
-  requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
-  requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
+  /* Input bound MLD_NTT_BOUND = 9 * MLD_FQMUL_BOUND, the post-condition of
+   * the forward NTT. Hardcoded here to keep this header free of poly.h.
+   * Must be kept in sync with the HOL-Light precondition. */
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(array_abs_bound(a, 0, MLDSA_N, 94279698))
+  requires(array_abs_bound(b, 0, MLDSA_N, 94279698))
   requires(qdata == mld_qdata)
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(a, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_pointwise_acc_l4_avx2_asm MLD_NAMESPACE(pointwise_acc_l4_avx2_asm)
@@ -156,13 +159,12 @@ __contract__(
   requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   requires(qdata == mld_qdata)
   assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_pointwise_acc_l5_avx2_asm MLD_NAMESPACE(pointwise_acc_l5_avx2_asm)
@@ -176,13 +178,12 @@ __contract__(
   requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   requires(qdata == mld_qdata)
   assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #define mld_pointwise_acc_l7_avx2_asm MLD_NAMESPACE(pointwise_acc_l7_avx2_asm)
@@ -196,13 +197,12 @@ __contract__(
   requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
   requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
-  /* check-magic: off */
   requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
-  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
+  /* check-magic: 94279698 == 9 * ((5 * MLDSA_Q + 3) / 4) */
+  requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 94279698)))
   requires(qdata == mld_qdata)
   assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
   ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
-  /* check-magic: on */
 );
 
 #endif /* !MLD_NATIVE_X86_64_SRC_ARITH_NATIVE_X86_64_H */
diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c
index 09f3ab00bc..3408c41a02 100644
--- a/mldsa/src/poly.c
+++ b/mldsa/src/poly.c
@@ -167,16 +167,18 @@ void mld_poly_shiftl(mld_poly *a)
 static MLD_INLINE int32_t mld_fqmul(int32_t a, int32_t b)
 __contract__(
   requires(b > -MLDSA_Q_HALF && b < MLDSA_Q_HALF)
-  ensures(return_value > -MLDSA_Q && return_value < MLDSA_Q)
+  ensures(return_value > -MLD_FQMUL_BOUND && return_value < MLD_FQMUL_BOUND)
 )
 {
-  /* Bounds: We argue in mld_montgomery_reduce() that the reult
+  /* Bounds: We argue in mld_montgomery_reduce() that the result
    * of Montgomery reduction is < MLDSA_Q if the input is smaller
    * than 2^31 * MLDSA_Q in absolute value. Indeed, we have:
    *
    *    |a * b|   = |a| * |b|
    *              < 2^31 * MLDSA_Q_HALF
    *              < 2^31 * MLDSA_Q
+   *
+   * So the output is < MLDSA_Q < MLD_FQMUL_BOUND.
    */
   return mld_montgomery_reduce((int64_t)a * (int64_t)b);
 }
@@ -219,13 +221,13 @@ static MLD_INLINE void mld_ntt_butterfly_block(int32_t r[MLDSA_N],
 __contract__(
   requires(start < MLDSA_N)
   requires(1 <= len && len <= MLDSA_N / 2 && start + 2 * len <= MLDSA_N)
-  requires(0 <= bound && bound < INT32_MAX - MLDSA_Q)
+  requires(0 <= bound && bound < INT32_MAX - MLD_FQMUL_BOUND)
   requires(-MLDSA_Q_HALF < zeta && zeta < MLDSA_Q_HALF)
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
-  requires(array_abs_bound(r, 0, start, bound + MLDSA_Q))
+  requires(array_abs_bound(r, 0, start, bound + MLD_FQMUL_BOUND))
   requires(array_abs_bound(r, start, MLDSA_N, bound))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
-  ensures(array_abs_bound(r, 0, start + 2*len, bound + MLDSA_Q))
+  ensures(array_abs_bound(r, 0, start + 2*len, bound + MLD_FQMUL_BOUND))
   ensures(array_abs_bound(r, start + 2 * len, MLDSA_N, bound)))
 {
   /* `bound` is a ghost variable only needed in the CBMC specification */
@@ -238,9 +240,9 @@ __contract__(
      * Coefficients are updated in strided pairs, so the bounds for the
      * intermediate states alternate twice between the old and new bound
      */
-    invariant(array_abs_bound(r, 0,           j,           bound + MLDSA_Q))
+    invariant(array_abs_bound(r, 0,           j,           bound + MLD_FQMUL_BOUND))
     invariant(array_abs_bound(r, j,           start + len, bound))
-    invariant(array_abs_bound(r, start + len, j + len,     bound + MLDSA_Q))
+    invariant(array_abs_bound(r, start + len, j + len,     bound + MLD_FQMUL_BOUND))
     invariant(array_abs_bound(r, j + len,     MLDSA_N,     bound))
     decreases(start + len - j))
   {
@@ -265,9 +267,9 @@ static MLD_INLINE void mld_ntt_layer(int32_t r[MLDSA_N], const unsigned layer)
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
   requires(1 <= layer && layer <= 8)
-  requires(array_abs_bound(r, 0, MLDSA_N, layer * MLDSA_Q))
+  requires(array_abs_bound(r, 0, MLDSA_N, layer * MLD_FQMUL_BOUND))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
-  ensures(array_abs_bound(r, 0, MLDSA_N, (layer + 1) * MLDSA_Q)))
+  ensures(array_abs_bound(r, 0, MLDSA_N, (layer + 1) * MLD_FQMUL_BOUND)))
 {
   unsigned start, k, len;
   /* Twiddle factors for layer n are at indices 2^(n-1)..2^n-1. */
@@ -278,12 +280,12 @@ __contract__(
     invariant(start < MLDSA_N + 2 * len)
     invariant(k <= MLDSA_N)
     invariant(2 * len * k == start + MLDSA_N)
-    invariant(array_abs_bound(r, 0, start, layer * MLDSA_Q + MLDSA_Q))
-    invariant(array_abs_bound(r, start, MLDSA_N, layer * MLDSA_Q))
+    invariant(array_abs_bound(r, 0, start, layer * MLD_FQMUL_BOUND + MLD_FQMUL_BOUND))
+    invariant(array_abs_bound(r, start, MLDSA_N, layer * MLD_FQMUL_BOUND))
     decreases(MLDSA_N - start))
   {
     int32_t zeta = mld_zetas[k++];
-    mld_ntt_butterfly_block(r, zeta, start, len, layer * MLDSA_Q);
+    mld_ntt_butterfly_block(r, zeta, start, len, layer * MLD_FQMUL_BOUND);
   }
 }
 
@@ -305,7 +307,7 @@ __contract__(
   for (layer = 1; layer < 9; layer++)
   __loop__(
     invariant(1 <= layer && layer <= 9)
-    invariant(array_abs_bound(r, 0, MLDSA_N, layer * MLDSA_Q))
+    invariant(array_abs_bound(r, 0, MLDSA_N, layer * MLD_FQMUL_BOUND))
     decreases(9 - layer)
   )
   {
@@ -377,13 +379,18 @@ __contract__(
     unsigned j;
     int32_t zeta = -mld_zetas[k--];
 
+    /* The bound `(MLDSA_N >> (layer - 1)) * MLDSA_Q` is loose enough to
+     * cover both the input bound `(MLDSA_N >> layer) * MLDSA_Q`
+     * (for layers >= 1) and the fqmul output bound `MLD_FQMUL_BOUND`
+     * (which is < 2 * MLDSA_Q <= (MLDSA_N >> (layer - 1)) * MLDSA_Q). */
     for (j = start; j < start + len; j++)
     __loop__(
       invariant(start <= j && j <= start + len)
       invariant(array_abs_bound(r, 0, start, (MLDSA_N >> (layer - 1)) * MLDSA_Q))
       invariant(array_abs_bound(r, start, j, (MLDSA_N >> (layer - 1)) * MLDSA_Q))
       invariant(array_abs_bound(r, j, start + len, (MLDSA_N >> layer) * MLDSA_Q))
-      invariant(array_abs_bound(r, start + len, MLDSA_N, (MLDSA_N >> layer) * MLDSA_Q))
+      invariant(array_abs_bound(r, start + len, j + len, (MLDSA_N >> (layer - 1)) * MLDSA_Q))
+      invariant(array_abs_bound(r, j + len, MLDSA_N, (MLDSA_N >> layer) * MLDSA_Q))
       decreases(start + len - j))
     {
       int32_t t = r[j];
diff --git a/mldsa/src/poly.h b/mldsa/src/poly.h
index ddde0f0544..589e7874b1 100644
--- a/mldsa/src/poly.h
+++ b/mldsa/src/poly.h
@@ -10,8 +10,10 @@
 #include "reduce.h"
 #include "rounding.h"
 
+/* Absolute exclusive upper bound for the output of fqmul */
+#define MLD_FQMUL_BOUND ((5 * MLDSA_Q + 3) / 4)
 /* Absolute exclusive upper bound for the output of the forward NTT */
-#define MLD_NTT_BOUND (9 * MLDSA_Q)
+#define MLD_NTT_BOUND (9 * MLD_FQMUL_BOUND)
 /* Absolute exclusive upper bound for the output of the inverse NTT*/
 #define MLD_INTT_BOUND MLDSA_Q
 
diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c
index e02fc07dbf..58571973df 100644
--- a/mldsa/src/polyvec.c
+++ b/mldsa/src/polyvec.c
@@ -196,11 +196,11 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
           MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 &&   \
           MLD_CONFIG_PARAMETER_SET == 87 */
   /* The first input is bounded by [0, MLDSA_Q-1] inclusive.
-   * The second input is bounded by [-(9*MLDSA_Q-1), 9*MLDSA_Q-1] inclusive.
+   * The second input is bounded by [-(MLD_NTT_BOUND-1), MLD_NTT_BOUND-1].
    * Hence, we can safely accumulate in 64-bits without intermediate reductions
    * as MLDSA_L * (MLD_NTT_BOUND-1) * (MLDSA_Q-1) < INT64_MAX.
    *
-   * The worst case is ML-DSA-87: 7 * (9*MLDSA_Q-1) * (MLDSA_Q-1) < 2**52
+   * The worst case is ML-DSA-87: 7 * (MLD_NTT_BOUND-1) * (MLDSA_Q-1) < 2**53
    * (and likewise for negative values).
    */
   mld_polyvecl_pointwise_acc_montgomery_c(w, u, v);
diff --git a/proofs/cbmc/poly_ntt_c/Makefile b/proofs/cbmc/poly_ntt_c/Makefile
index 6139dee9cf..26fca0df98 100644
--- a/proofs/cbmc/poly_ntt_c/Makefile
+++ b/proofs/cbmc/poly_ntt_c/Makefile
@@ -37,7 +37,7 @@ FUNCTION_NAME = mld_poly_ntt_c
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 9
+CBMC_OBJECT_BITS = 10
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file
diff --git a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile
index 7eefed6331..388f2aa553 100644
--- a/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile
+++ b/proofs/cbmc/polyvecl_pointwise_acc_montgomery_c/Makefile
@@ -42,7 +42,13 @@ FUNCTION_NAME = mld_polyvecl_pointwise_acc_montgomery_c
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 12
+# Optimal CBMC_OBJECT_BITS depends on the parameter set; the values below
+# avoid SMT-solver timeouts for each L. See pq-code-package/mldsa-native#1131.
+ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
+CBMC_OBJECT_BITS = 10
+else
+CBMC_OBJECT_BITS = 11
+endif
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file
diff --git a/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml
index 39d1c81c6d..8eef919509 100644
--- a/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml
@@ -139,7 +139,7 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove
                read PC s = word pc /\
                C_ARGUMENTS [r; a; b] s /\
                (!i. i < 1024 ==> abs(ival(x i)) <= &8380416) /\
-               (!i. i < 1024 ==> abs(ival(y i)) <= &75423752) /\
+               (!i. i < 1024 ==> abs(ival(y i)) <= &94279697) /\
                (!i. i < 1024 ==>
                  read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                (!i. i < 1024 ==>
@@ -165,7 +165,7 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove
 
   (* Lift x bound to match y bound for product lemma *)
   SUBGOAL_THEN
-    `!i. i < 1024 ==> abs(ival((x:num->int32) i)) <= &75423752`
+    `!i. i < 1024 ==> abs(ival((x:num->int32) i)) <= &94279697`
     ASSUME_TAC THENL
   [GEN_TAC THEN DISCH_TAC THEN
    MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416:int` THEN
@@ -213,18 +213,18 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove
   (* Rewrite ARM montred to standard montred for CONGBOUND *)
   REWRITE_TAC[ARM_MLDSA_MONTRED_EQ] THEN
 
-  (* Product bounds (tight: 8380416 * 75423752 = 632082418040832) *)
+  (* Product bounds (tight: 8380416 * 94279697 = 790103081213952) *)
   SUBGOAL_THEN
    `!i. i < 1024 ==>
      abs(ival(word_mul (word_sx ((x:num->int32) i):int64)
-                       (word_sx ((y:num->int32) i):int64))) <= &632082418040832`
+                       (word_sx ((y:num->int32) i):int64))) <= &790103081213952`
    ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`(x:num->int32) i`; `(y:num->int32) i`] IVAL_WORD_MUL_SX32_64) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
    REWRITE_TAC[INT_ABS_MUL] THEN
-   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &75423752:int` THEN
+   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &94279697:int` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC INT_LE_MUL2 THEN REWRITE_TAC[INT_ABS_POS] THEN ASM_MESON_TAC[];
      CONV_TAC INT_REDUCE_CONV];
@@ -303,7 +303,7 @@ let MLDSA_POINTWISE_ACC_L4_SUBROUTINE_CORRECT = prove
                read X30 s = returnaddress /\
                C_ARGUMENTS [r; a; b] s /\
                (!i. i < 1024 ==> abs(ival(x i)) <= &8380416) /\
-               (!i. i < 1024 ==> abs(ival(y i)) <= &75423752) /\
+               (!i. i < 1024 ==> abs(ival(y i)) <= &94279697) /\
                (!i. i < 1024 ==>
                  read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                (!i. i < 1024 ==>
diff --git a/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml
index b3dec34fa2..e27664b1d7 100644
--- a/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml
@@ -155,7 +155,7 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove
                read PC s = word pc /\
                C_ARGUMENTS [r; a; b] s /\
                (!i. i < 1280 ==> abs(ival(x i)) <= &8380416) /\
-               (!i. i < 1280 ==> abs(ival(y i)) <= &75423752) /\
+               (!i. i < 1280 ==> abs(ival(y i)) <= &94279697) /\
                (!i. i < 1280 ==>
                  read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                (!i. i < 1280 ==>
@@ -181,7 +181,7 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove
 
   (* Lift x bound to match y bound for product lemma *)
   SUBGOAL_THEN
-    `!i. i < 1280 ==> abs(ival((x:num->int32) i)) <= &75423752`
+    `!i. i < 1280 ==> abs(ival((x:num->int32) i)) <= &94279697`
     ASSUME_TAC THENL
   [GEN_TAC THEN DISCH_TAC THEN
    MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416:int` THEN
@@ -239,18 +239,18 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove
   (* Rewrite ARM montred to standard montred for CONGBOUND *)
   REWRITE_TAC[ARM_MLDSA_MONTRED_EQ] THEN
 
-  (* Product bounds (tight: 8380416 * 75423752 = 632082418040832) *)
+  (* Product bounds (tight: 8380416 * 94279697 = 790103081213952) *)
   SUBGOAL_THEN
    `!i. i < 1280 ==>
      abs(ival(word_mul (word_sx ((x:num->int32) i):int64)
-                       (word_sx ((y:num->int32) i):int64))) <= &632082418040832`
+                       (word_sx ((y:num->int32) i):int64))) <= &790103081213952`
    ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`(x:num->int32) i`; `(y:num->int32) i`] IVAL_WORD_MUL_SX32_64) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
    REWRITE_TAC[INT_ABS_MUL] THEN
-   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &75423752:int` THEN
+   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &94279697:int` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC INT_LE_MUL2 THEN REWRITE_TAC[INT_ABS_POS] THEN ASM_MESON_TAC[];
      CONV_TAC INT_REDUCE_CONV];
@@ -329,7 +329,7 @@ let MLDSA_POINTWISE_ACC_L5_SUBROUTINE_CORRECT = prove
                read X30 s = returnaddress /\
                C_ARGUMENTS [r; a; b] s /\
                (!i. i < 1280 ==> abs(ival(x i)) <= &8380416) /\
-               (!i. i < 1280 ==> abs(ival(y i)) <= &75423752) /\
+               (!i. i < 1280 ==> abs(ival(y i)) <= &94279697) /\
                (!i. i < 1280 ==>
                  read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                (!i. i < 1280 ==>
diff --git a/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml
index 7853acd1ff..a689114b90 100644
--- a/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml
@@ -187,7 +187,7 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove
                read PC s = word pc /\
                C_ARGUMENTS [r; a; b] s /\
                (!i. i < 1792 ==> abs(ival(x i)) <= &8380416) /\
-               (!i. i < 1792 ==> abs(ival(y i)) <= &75423752) /\
+               (!i. i < 1792 ==> abs(ival(y i)) <= &94279697) /\
                (!i. i < 1792 ==>
                  read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                (!i. i < 1792 ==>
@@ -213,7 +213,7 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove
 
   (* Lift x bound to match y bound for product lemma *)
   SUBGOAL_THEN
-    `!i. i < 1792 ==> abs(ival((x:num->int32) i)) <= &75423752`
+    `!i. i < 1792 ==> abs(ival((x:num->int32) i)) <= &94279697`
     ASSUME_TAC THENL
   [GEN_TAC THEN DISCH_TAC THEN
    MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416:int` THEN
@@ -271,18 +271,18 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove
   (* Rewrite ARM montred to standard montred for CONGBOUND *)
   REWRITE_TAC[ARM_MLDSA_MONTRED_EQ] THEN
 
-  (* Product bounds (tight: 8380416 * 75423752 = 632082418040832) *)
+  (* Product bounds (tight: 8380416 * 94279697 = 790103081213952) *)
   SUBGOAL_THEN
    `!i. i < 1792 ==>
      abs(ival(word_mul (word_sx ((x:num->int32) i):int64)
-                       (word_sx ((y:num->int32) i):int64))) <= &632082418040832`
+                       (word_sx ((y:num->int32) i):int64))) <= &790103081213952`
    ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`(x:num->int32) i`; `(y:num->int32) i`] IVAL_WORD_MUL_SX32_64) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
    REWRITE_TAC[INT_ABS_MUL] THEN
-   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &75423752:int` THEN
+   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &94279697:int` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC INT_LE_MUL2 THEN REWRITE_TAC[INT_ABS_POS] THEN ASM_MESON_TAC[];
      CONV_TAC INT_REDUCE_CONV];
@@ -361,7 +361,7 @@ let MLDSA_POINTWISE_ACC_L7_SUBROUTINE_CORRECT = prove
                read X30 s = returnaddress /\
                C_ARGUMENTS [r; a; b] s /\
                (!i. i < 1792 ==> abs(ival(x i)) <= &8380416) /\
-               (!i. i < 1792 ==> abs(ival(y i)) <= &75423752) /\
+               (!i. i < 1792 ==> abs(ival(y i)) <= &94279697) /\
                (!i. i < 1792 ==>
                  read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                (!i. i < 1792 ==>
diff --git a/proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml
index 60beaff01c..4fe5d86b7e 100644
--- a/proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml
@@ -86,8 +86,8 @@ let MLDSA_POINTWISE_CORRECT = prove
           (\s. aligned_bytes_loaded s (word pc) mldsa_pointwise_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [a; b] s /\
-               (!i. i < 256 ==> abs(ival(x i)) <= &75423752) /\
-               (!i. i < 256 ==> abs(ival(y i)) <= &75423752) /\
+               (!i. i < 256 ==> abs(ival(x i)) <= &94279697) /\
+               (!i. i < 256 ==> abs(ival(y i)) <= &94279697) /\
                (!i. i < 256 ==>
                  read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                (!i. i < 256 ==>
@@ -151,14 +151,14 @@ let MLDSA_POINTWISE_CORRECT = prove
   SUBGOAL_THEN
    `!i. i < 256 ==>
      abs(ival(word_mul (word_sx ((x:num->int32) i):int64)
-                       (word_sx ((y:num->int32) i):int64))) <= &5688742365757504`
+                       (word_sx ((y:num->int32) i):int64))) <= &8888661266411809`
    ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`(x:num->int32) i`; `(y:num->int32) i`] IVAL_WORD_MUL_SX32_64) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
    REWRITE_TAC[INT_ABS_MUL] THEN
-   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&75423752 * &75423752:int` THEN
+   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&94279697 * &94279697:int` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC INT_LE_MUL2 THEN REWRITE_TAC[INT_ABS_POS] THEN ASM_MESON_TAC[];
      CONV_TAC INT_REDUCE_CONV];
@@ -218,8 +218,8 @@ let MLDSA_POINTWISE_SUBROUTINE_CORRECT = prove
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [a; b] s /\
-               (!i. i < 256 ==> abs(ival(x i)) <= &75423752) /\
-               (!i. i < 256 ==> abs(ival(y i)) <= &75423752) /\
+               (!i. i < 256 ==> abs(ival(x i)) <= &94279697) /\
+               (!i. i < 256 ==> abs(ival(y i)) <= &94279697) /\
                (!i. i < 256 ==>
                  read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                (!i. i < 256 ==>
diff --git a/proofs/hol_light/common/mldsa_specs.ml b/proofs/hol_light/common/mldsa_specs.ml
index ef88cef269..e22abdc6af 100644
--- a/proofs/hol_light/common/mldsa_specs.ml
+++ b/proofs/hol_light/common/mldsa_specs.ml
@@ -423,16 +423,16 @@ let ARM_MLDSA_MONTRED_EQ = prove(
 (* ival of sign-extended product equals integer product when bounded *)
 let IVAL_WORD_MUL_SX32_64 = prove(
  `!x:int32 y:int32.
-    abs(ival x) <= &75423752 /\ abs(ival y) <= &75423752
+    abs(ival x) <= &94279697 /\ abs(ival y) <= &94279697
     ==> ival(word_mul (word_sx x:int64) (word_sx y:int64)) = ival x * ival y`,
   REPEAT STRIP_TAC THEN
   REWRITE_TAC[WORD_RULE `word_mul a b:int64 = iword(ival a * ival b)`] THEN
   SIMP_TAC[IVAL_WORD_SX; DIMINDEX_32; DIMINDEX_64; ARITH] THEN
   MATCH_MP_TAC IVAL_IWORD THEN REWRITE_TAC[DIMINDEX_64] THEN
   CONV_TAC NUM_REDUCE_CONV THEN
-  SUBGOAL_THEN `abs(ival(x:int32) * ival(y:int32)) <= &5688742365757504` MP_TAC THENL
+  SUBGOAL_THEN `abs(ival(x:int32) * ival(y:int32)) <= &8888661266411809` MP_TAC THENL
    [REWRITE_TAC[INT_ABS_MUL] THEN
-    MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&75423752 * &75423752:int` THEN
+    MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&94279697 * &94279697:int` THEN
     CONJ_TAC THENL
      [MATCH_MP_TAC INT_LE_MUL2 THEN ASM_REWRITE_TAC[INT_ABS_POS];
       CONV_TAC INT_REDUCE_CONV];
diff --git a/proofs/hol_light/x86_64/proofs/pointwise_acc_l4_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/pointwise_acc_l4_avx2_asm.ml
index b6ac99a988..b1030a8a73 100644
--- a/proofs/hol_light/x86_64/proofs/pointwise_acc_l4_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/pointwise_acc_l4_avx2_asm.ml
@@ -207,7 +207,7 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1024 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1024 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1024 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1024 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1024 ==>
@@ -232,7 +232,7 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
   GLOBALIZE_PRECONDITION_TAC THEN
   SUBGOAL_THEN
-    `!i. i < 1024 ==> abs(ival((x:num->int32) i)) <= &75423752`
+    `!i. i < 1024 ==> abs(ival((x:num->int32) i)) <= &94279697`
     ASSUME_TAC THENL
   [GEN_TAC THEN DISCH_TAC THEN
    MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416:int` THEN
@@ -295,18 +295,18 @@ let MLDSA_POINTWISE_ACC_L4_CORRECT = prove
   CONV_TAC(LAND_CONV WORD_REDUCE_CONV) THEN
   STRIP_TAC THEN
 
-  (* Product bounds (tight: 8380416 * 75423752 = 632082418040832) *)
+  (* Product bounds (tight: 8380416 * 94279697 = 790103081213952) *)
   SUBGOAL_THEN
    `!i. i < 1024 ==>
      abs(ival(word_mul (word_sx ((x:num->int32) i):int64)
-                       (word_sx ((y:num->int32) i):int64))) <= &632082418040832`
+                       (word_sx ((y:num->int32) i):int64))) <= &790103081213952`
    ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`(x:num->int32) i`; `(y:num->int32) i`] IVAL_WORD_MUL_SX32_64) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
    REWRITE_TAC[INT_ABS_MUL] THEN
-   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &75423752:int` THEN
+   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &94279697:int` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC INT_LE_MUL2 THEN REWRITE_TAC[INT_ABS_POS] THEN ASM_MESON_TAC[];
      CONV_TAC INT_REDUCE_CONV];
@@ -417,7 +417,7 @@ let MLDSA_POINTWISE_ACC_L4_NOIBT_SUBROUTINE_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1024 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1024 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1024 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1024 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1024 ==>
@@ -465,7 +465,7 @@ let MLDSA_POINTWISE_ACC_L4_SUBROUTINE_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1024 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1024 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1024 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1024 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1024 ==>
diff --git a/proofs/hol_light/x86_64/proofs/pointwise_acc_l5_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/pointwise_acc_l5_avx2_asm.ml
index b53f7b4dec..9a94cc6a0a 100644
--- a/proofs/hol_light/x86_64/proofs/pointwise_acc_l5_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/pointwise_acc_l5_avx2_asm.ml
@@ -235,7 +235,7 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1280 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1280 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1280 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1280 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1280 ==>
@@ -260,7 +260,7 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
   GLOBALIZE_PRECONDITION_TAC THEN
   SUBGOAL_THEN
-    `!i. i < 1280 ==> abs(ival((x:num->int32) i)) <= &75423752`
+    `!i. i < 1280 ==> abs(ival((x:num->int32) i)) <= &94279697`
     ASSUME_TAC THENL
   [GEN_TAC THEN DISCH_TAC THEN
    MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416:int` THEN
@@ -326,14 +326,14 @@ let MLDSA_POINTWISE_ACC_L5_CORRECT = prove
   SUBGOAL_THEN
    `!i. i < 1280 ==>
      abs(ival(word_mul (word_sx ((x:num->int32) i):int64)
-                       (word_sx ((y:num->int32) i):int64))) <= &632082418040832`
+                       (word_sx ((y:num->int32) i):int64))) <= &790103081213952`
    ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`(x:num->int32) i`; `(y:num->int32) i`] IVAL_WORD_MUL_SX32_64) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
    REWRITE_TAC[INT_ABS_MUL] THEN
-   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &75423752:int` THEN
+   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &94279697:int` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC INT_LE_MUL2 THEN REWRITE_TAC[INT_ABS_POS] THEN ASM_MESON_TAC[];
      CONV_TAC INT_REDUCE_CONV];
@@ -444,7 +444,7 @@ let MLDSA_POINTWISE_ACC_L5_NOIBT_SUBROUTINE_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1280 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1280 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1280 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1280 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1280 ==>
@@ -492,7 +492,7 @@ let MLDSA_POINTWISE_ACC_L5_SUBROUTINE_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1280 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1280 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1280 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1280 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1280 ==>
diff --git a/proofs/hol_light/x86_64/proofs/pointwise_acc_l7_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/pointwise_acc_l7_avx2_asm.ml
index 3607d797de..229d418292 100644
--- a/proofs/hol_light/x86_64/proofs/pointwise_acc_l7_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/pointwise_acc_l7_avx2_asm.ml
@@ -291,7 +291,7 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1792 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1792 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1792 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1792 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1792 ==>
@@ -316,7 +316,7 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
   GLOBALIZE_PRECONDITION_TAC THEN
   SUBGOAL_THEN
-    `!i. i < 1792 ==> abs(ival((x:num->int32) i)) <= &75423752`
+    `!i. i < 1792 ==> abs(ival((x:num->int32) i)) <= &94279697`
     ASSUME_TAC THENL
   [GEN_TAC THEN DISCH_TAC THEN
    MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416:int` THEN
@@ -382,14 +382,14 @@ let MLDSA_POINTWISE_ACC_L7_CORRECT = prove
   SUBGOAL_THEN
    `!i. i < 1792 ==>
      abs(ival(word_mul (word_sx ((x:num->int32) i):int64)
-                       (word_sx ((y:num->int32) i):int64))) <= &632082418040832`
+                       (word_sx ((y:num->int32) i):int64))) <= &790103081213952`
    ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`(x:num->int32) i`; `(y:num->int32) i`] IVAL_WORD_MUL_SX32_64) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
    REWRITE_TAC[INT_ABS_MUL] THEN
-   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &75423752:int` THEN
+   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&8380416 * &94279697:int` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC INT_LE_MUL2 THEN REWRITE_TAC[INT_ABS_POS] THEN ASM_MESON_TAC[];
      CONV_TAC INT_REDUCE_CONV];
@@ -500,7 +500,7 @@ let MLDSA_POINTWISE_ACC_L7_NOIBT_SUBROUTINE_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1792 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1792 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1792 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1792 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1792 ==>
@@ -548,7 +548,7 @@ let MLDSA_POINTWISE_ACC_L7_SUBROUTINE_CORRECT = prove
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
               (!i. i < 1792 ==> abs(ival(x i)) <= &8380416) /\
-              (!i. i < 1792 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 1792 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 1792 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 1792 ==>
diff --git a/proofs/hol_light/x86_64/proofs/pointwise_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/pointwise_avx2_asm.ml
index 45b8f6f3d5..5a3c1f0edb 100644
--- a/proofs/hol_light/x86_64/proofs/pointwise_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/pointwise_avx2_asm.ml
@@ -200,8 +200,8 @@ let MLDSA_POINTWISE_CORRECT = prove
               C_ARGUMENTS [a; b; consts] s /\
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
-              (!i. i < 256 ==> abs(ival(x i)) <= &75423752) /\
-              (!i. i < 256 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 256 ==> abs(ival(x i)) <= &94279697) /\
+              (!i. i < 256 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 256 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 256 ==>
@@ -288,14 +288,14 @@ let MLDSA_POINTWISE_CORRECT = prove
   SUBGOAL_THEN
    `!i. i < 256 ==>
      abs(ival(word_mul (word_sx ((x:num->int32) i):int64)
-                       (word_sx ((y:num->int32) i):int64))) <= &5688742365757504`
+                       (word_sx ((y:num->int32) i):int64))) <= &8888661266411809`
    ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN
    MP_TAC(ISPECL [`(x:num->int32) i`; `(y:num->int32) i`] IVAL_WORD_MUL_SX32_64) THEN
    ANTS_TAC THENL
     [ASM_MESON_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
    REWRITE_TAC[INT_ABS_MUL] THEN
-   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&75423752 * &75423752:int` THEN
+   MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `&94279697 * &94279697:int` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC INT_LE_MUL2 THEN REWRITE_TAC[INT_ABS_POS] THEN ASM_MESON_TAC[];
      CONV_TAC INT_REDUCE_CONV];
@@ -391,8 +391,8 @@ let MLDSA_POINTWISE_NOIBT_SUBROUTINE_CORRECT = prove
               C_ARGUMENTS [a; b; consts] s /\
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
-              (!i. i < 256 ==> abs(ival(x i)) <= &75423752) /\
-              (!i. i < 256 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 256 ==> abs(ival(x i)) <= &94279697) /\
+              (!i. i < 256 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 256 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 256 ==>
@@ -433,8 +433,8 @@ let MLDSA_POINTWISE_SUBROUTINE_CORRECT = prove
               C_ARGUMENTS [a; b; consts] s /\
               wordlist_from_memory(consts,624) s =
                 MAP (iword: int -> 32 word) mldsa_complete_qdata /\
-              (!i. i < 256 ==> abs(ival(x i)) <= &75423752) /\
-              (!i. i < 256 ==> abs(ival(y i)) <= &75423752) /\
+              (!i. i < 256 ==> abs(ival(x i)) <= &94279697) /\
+              (!i. i < 256 ==> abs(ival(y i)) <= &94279697) /\
               (!i. i < 256 ==>
                 read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
               (!i. i < 256 ==>