Skip to content

Enforce ML-DSA x86 native assumptions #1244

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tob-joe wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Enforce ML-DSA x86 native assumptions #1244

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
76ced79
Enforce ML-DSA x86 native assumptions
tob-joe Jun 25, 2026
fe9c7ce
Fix ML-DSA x86 qdata guard autogen
tob-joe Jun 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions dev/x86_64/src/arith_native_x86_64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

@mkannwischer mkannwischer Jun 30, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unfortunately, this doesn't work. There is no way to guarantee alignment with CBMC iirc.

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))
Expand All @@ -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))
Expand All @@ -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))
Expand Down Expand Up @@ -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))
Expand All @@ -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))
Expand Down
21 changes: 20 additions & 1 deletion dev/x86_64/src/intt_avx2_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
21 changes: 20 additions & 1 deletion dev/x86_64/src/ntt_avx2_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
21 changes: 14 additions & 7 deletions mldsa/src/native/api.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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))
Expand All @@ -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))
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down
7 changes: 7 additions & 0 deletions mldsa/src/native/x86_64/src/arith_native_x86_64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand All @@ -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))
Expand All @@ -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))
Expand Down Expand Up @@ -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))
Expand All @@ -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))
Expand Down
2 changes: 2 additions & 0 deletions mldsa/src/native/x86_64/src/intt_avx2_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions mldsa/src/native/x86_64/src/ntt_avx2_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
1 change: 1 addition & 0 deletions proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading