diff --git a/dev/x86_64/src/arith_native_x86_64.h b/dev/x86_64/src/arith_native_x86_64.h
index 3af2af4921..4ae051ff47 100644
--- a/dev/x86_64/src/arith_native_x86_64.h
+++ b/dev/x86_64/src/arith_native_x86_64.h
@@ -137,6 +137,7 @@ void mld_poly_caddq_avx2_asm(int32_t *r)
  * in proofs/hol_light/x86_64/proofs/poly_caddq_avx2_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)
   requires(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_bound(r, 0, MLDSA_N, 0, MLDSA_Q))
@@ -151,6 +152,8 @@ void mld_poly_use_hint_32_avx2_asm(int32_t *a, const int32_t *h)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)a % MLD_DEFAULT_ALIGN) == 0)
+  requires(((uintptr_t)h % MLD_DEFAULT_ALIGN) == 0)
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
@@ -166,6 +169,8 @@ void mld_poly_use_hint_88_avx2_asm(int32_t *a, const int32_t *h)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)a % MLD_DEFAULT_ALIGN) == 0)
+  requires(((uintptr_t)h % MLD_DEFAULT_ALIGN) == 0)
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
@@ -197,6 +202,7 @@ void mld_polyz_unpack_17_avx2_asm(int32_t *r, const uint8_t *a)
  * in proofs/hol_light/x86_64/proofs/polyz_unpack_17_avx2_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)
   requires(memory_no_alias(a, 576))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_bound(r, 0, MLDSA_N, -((1 << 17) - 1), (1 << 17) + 1))
@@ -209,6 +215,7 @@ void mld_polyz_unpack_19_avx2_asm(int32_t *r, const uint8_t *a)
  * in proofs/hol_light/x86_64/proofs/polyz_unpack_19_avx2_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)
   requires(memory_no_alias(a, 640))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_bound(r, 0, MLDSA_N, -((1 << 19) - 1), (1 << 19) + 1))
diff --git a/dev/x86_64/src/intt_avx2_asm.S b/dev/x86_64/src/intt_avx2_asm.S
index 115f33accf..3e26ff4b54 100644
--- a/dev/x86_64/src/intt_avx2_asm.S
+++ b/dev/x86_64/src/intt_avx2_asm.S
@@ -43,9 +43,28 @@
 #include "../../../common.h"
 #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \
     !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
+#include "consts.h"
+
 /* simpasm: header-end */
 
-#include "consts.h"
+.if MLD_AVX2_BACKEND_DATA_OFFSET_8XQ != 0
+.error "Update intt_avx2_asm.S qdata displacements for 8XQ"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_8XQINV != 8
+.error "Update intt_avx2_asm.S qdata displacements for 8XQINV"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_8XDIV_QINV != 16
+.error "Update intt_avx2_asm.S qdata displacements for 8XDIV_QINV"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_8XDIV != 24
+.error "Update intt_avx2_asm.S qdata displacements for 8XDIV"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_ZETAS_QINV != 32
+.error "Update intt_avx2_asm.S qdata displacements for ZETAS_QINV"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_ZETAS != 328
+.error "Update intt_avx2_asm.S qdata displacements for ZETAS"
+.endif
 
 .macro shuffle8 r0, r1, r2, r3
 vperm2i128 $0x20,%ymm\r1,%ymm\r0,%ymm\r2
diff --git a/dev/x86_64/src/ntt_avx2_asm.S b/dev/x86_64/src/ntt_avx2_asm.S
index 07eabf42fa..13366dd08e 100644
--- a/dev/x86_64/src/ntt_avx2_asm.S
+++ b/dev/x86_64/src/ntt_avx2_asm.S
@@ -43,9 +43,28 @@
 #include "../../../common.h"
 #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \
     !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
+#include "consts.h"
+
 /* simpasm: header-end */
 
-#include "consts.h"
+.if MLD_AVX2_BACKEND_DATA_OFFSET_8XQ != 0
+.error "Update ntt_avx2_asm.S qdata displacements for 8XQ"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_8XQINV != 8
+.error "Update ntt_avx2_asm.S qdata displacements for 8XQINV"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_8XDIV_QINV != 16
+.error "Update ntt_avx2_asm.S qdata displacements for 8XDIV_QINV"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_8XDIV != 24
+.error "Update ntt_avx2_asm.S qdata displacements for 8XDIV"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_ZETAS_QINV != 32
+.error "Update ntt_avx2_asm.S qdata displacements for ZETAS_QINV"
+.endif
+.if MLD_AVX2_BACKEND_DATA_OFFSET_ZETAS != 328
+.error "Update ntt_avx2_asm.S qdata displacements for ZETAS"
+.endif
 
 .macro shuffle8 r0, r1, r2, r3
 vperm2i128 $0x20,%ymm\r1,%ymm\r0,%ymm\r2
diff --git a/mldsa/src/native/api.h b/mldsa/src/native/api.h
index 8c72c31d03..3f0fc0ccab 100644
--- a/mldsa/src/native/api.h
+++ b/mldsa/src/native/api.h
@@ -334,12 +334,13 @@ __contract__(
 /**
  * For all coefficients of in/out polynomial add Q if coefficient is negative.
  *
- * @param[in,out] a Pointer to input/output polynomial.
+ * @param[in,out] a Pointer to 32-byte-aligned input/output polynomial.
  */
 MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)a % MLD_DEFAULT_ALIGN) == 0)
   requires(array_abs_bound(a, 0, MLDSA_N, MLDSA_Q))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
   ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
@@ -358,14 +359,16 @@ __contract__(
  *
  * Use hint h to correct the high bits of a in-place.
  *
- * @param[in,out] a Input/output polynomial.
- * @param[in]     h Hint polynomial.
+ * @param[in,out] a 32-byte-aligned input/output polynomial.
+ * @param[in]     h 32-byte-aligned hint polynomial.
  */
 MLD_MUST_CHECK_RETURN_VALUE
 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(h, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)a % MLD_DEFAULT_ALIGN) == 0)
+  requires(((uintptr_t)h % MLD_DEFAULT_ALIGN) == 0)
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
@@ -384,14 +387,16 @@ __contract__(
  *
  * Use hint h to correct the high bits of a in-place.
  *
- * @param[in,out] a Input/output polynomial.
- * @param[in]     h Hint polynomial.
+ * @param[in,out] a 32-byte-aligned input/output polynomial.
+ * @param[in]     h 32-byte-aligned hint polynomial.
  */
 MLD_MUST_CHECK_RETURN_VALUE
 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(h, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)a % MLD_DEFAULT_ALIGN) == 0)
+  requires(((uintptr_t)h % MLD_DEFAULT_ALIGN) == 0)
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
@@ -441,13 +446,14 @@ __contract__(
  * Unpack polynomial z with coefficients in
  * [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1].
  *
- * @param[out] r Pointer to output polynomial.
+ * @param[out] r Pointer to 32-byte-aligned output polynomial.
  * @param[in]  a Byte array with bit-packed polynomial.
  */
 MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a)
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)
   requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
@@ -467,13 +473,14 @@ __contract__(
  * Unpack polynomial z with coefficients in
  * [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1].
  *
- * @param[out] r Pointer to output polynomial.
+ * @param[out] r Pointer to 32-byte-aligned output polynomial.
  * @param[in]  a Byte array with bit-packed polynomial.
  */
 MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int mld_polyz_unpack_19_native(int32_t *r, const uint8_t *a)
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)
   requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
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 3af2af4921..4ae051ff47 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
@@ -137,6 +137,7 @@ void mld_poly_caddq_avx2_asm(int32_t *r)
  * in proofs/hol_light/x86_64/proofs/poly_caddq_avx2_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)
   requires(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_bound(r, 0, MLDSA_N, 0, MLDSA_Q))
@@ -151,6 +152,8 @@ void mld_poly_use_hint_32_avx2_asm(int32_t *a, const int32_t *h)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)a % MLD_DEFAULT_ALIGN) == 0)
+  requires(((uintptr_t)h % MLD_DEFAULT_ALIGN) == 0)
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
@@ -166,6 +169,8 @@ void mld_poly_use_hint_88_avx2_asm(int32_t *a, const int32_t *h)
 __contract__(
   requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
   requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)a % MLD_DEFAULT_ALIGN) == 0)
+  requires(((uintptr_t)h % MLD_DEFAULT_ALIGN) == 0)
   requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
   requires(array_bound(h, 0, MLDSA_N, 0, 2))
   assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
@@ -197,6 +202,7 @@ void mld_polyz_unpack_17_avx2_asm(int32_t *r, const uint8_t *a)
  * in proofs/hol_light/x86_64/proofs/polyz_unpack_17_avx2_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)
   requires(memory_no_alias(a, 576))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_bound(r, 0, MLDSA_N, -((1 << 17) - 1), (1 << 17) + 1))
@@ -209,6 +215,7 @@ void mld_polyz_unpack_19_avx2_asm(int32_t *r, const uint8_t *a)
  * in proofs/hol_light/x86_64/proofs/polyz_unpack_19_avx2_asm.ml */
 __contract__(
   requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)
   requires(memory_no_alias(a, 640))
   assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
   ensures(array_bound(r, 0, MLDSA_N, -((1 << 19) - 1), (1 << 19) + 1))
diff --git a/mldsa/src/native/x86_64/src/intt_avx2_asm.S b/mldsa/src/native/x86_64/src/intt_avx2_asm.S
index ef1b1765c5..52a8579ce0 100644
--- a/mldsa/src/native/x86_64/src/intt_avx2_asm.S
+++ b/mldsa/src/native/x86_64/src/intt_avx2_asm.S
@@ -43,6 +43,8 @@
 #include "../../../common.h"
 #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \
     !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
+#include "consts.h"
+
 
 /*
  * WARNING: This file is auto-derived from the mldsa-native source file
diff --git a/mldsa/src/native/x86_64/src/ntt_avx2_asm.S b/mldsa/src/native/x86_64/src/ntt_avx2_asm.S
index bfc3ce8e27..0299a1bff5 100644
--- a/mldsa/src/native/x86_64/src/ntt_avx2_asm.S
+++ b/mldsa/src/native/x86_64/src/ntt_avx2_asm.S
@@ -43,6 +43,8 @@
 #include "../../../common.h"
 #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \
     !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
+#include "consts.h"
+
 
 /*
  * WARNING: This file is auto-derived from the mldsa-native source file
diff --git a/proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S
index d3172ba85a..eb186f3790 100644
--- a/proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S
+++ b/proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S
@@ -41,6 +41,7 @@
 */
 
 
+
 /*
  * WARNING: This file is auto-derived from the mldsa-native source file
  *   dev/x86_64/src/intt_avx2_asm.S using scripts/simpasm. Do not modify it directly.
diff --git a/proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S b/proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S
index dfc91107fa..bcf1642251 100644
--- a/proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S
+++ b/proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S
@@ -41,6 +41,7 @@
 */
 
 
+
 /*
  * WARNING: This file is auto-derived from the mldsa-native source file
  *   dev/x86_64/src/ntt_avx2_asm.S using scripts/simpasm. Do not modify it directly.