From 76ced7985789ca4d56307fce3b0101e6c8f1250c Mon Sep 17 00:00:00 2001 From: Joe Doyle Date: Thu, 25 Jun 2026 15:57:51 -0400 Subject: [PATCH 1/2] Enforce ML-DSA x86 native assumptions Add assembly-time guards for AVX2 qdata offsets and make the x86 native entry contracts require the alignment assumed by the assembly implementations. This keeps the public native wrappers, implementation declarations, and proof-facing assumptions aligned for the affected x86 routines. Verification: - ./scripts/tests cbmc -kl ALL -p poly_use_hint_native --single-step -j1 - ./scripts/tests cbmc -kl ALL -p poly_caddq_native_x86_64 --single-step -j1 - ./scripts/tests cbmc -kl 44 -p polyz_unpack_native_x86_64 --single-step -j1 - ./scripts/tests cbmc -kl 65 -p polyz_unpack_native_x86_64 --single-step -j1 - ./scripts/tests cbmc -kl 87 -p polyz_unpack_native_x86_64 --single-step -j1 - ./scripts/tests cbmc -kl ALL -p polyz_unpack_native --single-step -j1 Co-authored-by: Codex Signed-off-by: Joe Doyle --- dev/x86_64/src/arith_native_x86_64.h | 7 ++++++ dev/x86_64/src/intt_avx2_asm.S | 23 +++++++++++++++++-- dev/x86_64/src/ntt_avx2_asm.S | 23 +++++++++++++++++-- mldsa/src/native/api.h | 21 +++++++++++------ .../native/x86_64/src/arith_native_x86_64.h | 7 ++++++ mldsa/src/native/x86_64/src/intt_avx2_asm.S | 21 +++++++++++++++++ mldsa/src/native/x86_64/src/ntt_avx2_asm.S | 21 +++++++++++++++++ 7 files changed, 112 insertions(+), 11 deletions(-) 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..b730a06585 100644 --- a/dev/x86_64/src/intt_avx2_asm.S +++ b/dev/x86_64/src/intt_avx2_asm.S @@ -43,10 +43,29 @@ #include "../../../common.h" #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \ !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) -/* 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 + +/* simpasm: header-end */ + .macro shuffle8 r0, r1, r2, r3 vperm2i128 $0x20,%ymm\r1,%ymm\r0,%ymm\r2 vperm2i128 $0x31,%ymm\r1,%ymm\r0,%ymm\r3 diff --git a/dev/x86_64/src/ntt_avx2_asm.S b/dev/x86_64/src/ntt_avx2_asm.S index 07eabf42fa..abf46e8884 100644 --- a/dev/x86_64/src/ntt_avx2_asm.S +++ b/dev/x86_64/src/ntt_avx2_asm.S @@ -43,10 +43,29 @@ #include "../../../common.h" #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \ !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) -/* 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 + +/* simpasm: header-end */ + .macro shuffle8 r0, r1, r2, r3 vperm2i128 $0x20,%ymm\r1,%ymm\r0,%ymm\r2 vperm2i128 $0x31,%ymm\r1,%ymm\r0,%ymm\r3 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..d9b8c6eb1f 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,27 @@ #include "../../../common.h" #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \ !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) +#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 + /* * 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..87ed5bc7ae 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,27 @@ #include "../../../common.h" #if defined(MLD_ARITH_BACKEND_X86_64_DEFAULT) && \ !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) +#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 + /* * WARNING: This file is auto-derived from the mldsa-native source file From fe9c7cefef5b937baff74744e9db5e9d9a20d2ae Mon Sep 17 00:00:00 2001 From: Joe Doyle Date: Tue, 30 Jun 2026 12:41:41 -0400 Subject: [PATCH 2/2] Fix ML-DSA x86 qdata guard autogen Move the AVX2 qdata layout assertions out of the simpasm header region. The assertions still check the dev assembly source against consts.h, but simpasm no longer carries them into the generated assembly it reassembles without that macro context. Regenerate the affected x86_64 native and HOL-Light assembly copies so lint and the x86_64 Intel-syntax autogen job can run past assembly generation. Co-authored-by: Codex Signed-off-by: Joe Doyle --- dev/x86_64/src/intt_avx2_asm.S | 4 ++-- dev/x86_64/src/ntt_avx2_asm.S | 4 ++-- mldsa/src/native/x86_64/src/intt_avx2_asm.S | 19 ------------------- mldsa/src/native/x86_64/src/ntt_avx2_asm.S | 19 ------------------- proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S | 1 + proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S | 1 + 6 files changed, 6 insertions(+), 42 deletions(-) diff --git a/dev/x86_64/src/intt_avx2_asm.S b/dev/x86_64/src/intt_avx2_asm.S index b730a06585..3e26ff4b54 100644 --- a/dev/x86_64/src/intt_avx2_asm.S +++ b/dev/x86_64/src/intt_avx2_asm.S @@ -45,6 +45,8 @@ !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) #include "consts.h" +/* simpasm: header-end */ + .if MLD_AVX2_BACKEND_DATA_OFFSET_8XQ != 0 .error "Update intt_avx2_asm.S qdata displacements for 8XQ" .endif @@ -64,8 +66,6 @@ .error "Update intt_avx2_asm.S qdata displacements for ZETAS" .endif -/* simpasm: header-end */ - .macro shuffle8 r0, r1, r2, r3 vperm2i128 $0x20,%ymm\r1,%ymm\r0,%ymm\r2 vperm2i128 $0x31,%ymm\r1,%ymm\r0,%ymm\r3 diff --git a/dev/x86_64/src/ntt_avx2_asm.S b/dev/x86_64/src/ntt_avx2_asm.S index abf46e8884..13366dd08e 100644 --- a/dev/x86_64/src/ntt_avx2_asm.S +++ b/dev/x86_64/src/ntt_avx2_asm.S @@ -45,6 +45,8 @@ !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) #include "consts.h" +/* simpasm: header-end */ + .if MLD_AVX2_BACKEND_DATA_OFFSET_8XQ != 0 .error "Update ntt_avx2_asm.S qdata displacements for 8XQ" .endif @@ -64,8 +66,6 @@ .error "Update ntt_avx2_asm.S qdata displacements for ZETAS" .endif -/* simpasm: header-end */ - .macro shuffle8 r0, r1, r2, r3 vperm2i128 $0x20,%ymm\r1,%ymm\r0,%ymm\r2 vperm2i128 $0x31,%ymm\r1,%ymm\r0,%ymm\r3 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 d9b8c6eb1f..52a8579ce0 100644 --- a/mldsa/src/native/x86_64/src/intt_avx2_asm.S +++ b/mldsa/src/native/x86_64/src/intt_avx2_asm.S @@ -45,25 +45,6 @@ !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) #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 - /* * 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 87ed5bc7ae..0299a1bff5 100644 --- a/mldsa/src/native/x86_64/src/ntt_avx2_asm.S +++ b/mldsa/src/native/x86_64/src/ntt_avx2_asm.S @@ -45,25 +45,6 @@ !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED) #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 - /* * 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.