Skip to content

Make poly_use_hint destructive #1070

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

Merged
mkannwischer merged 1 commit into from
May 2, 2026
Merged

Make poly_use_hint destructive #1070

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
10 changes: 4 additions & 6 deletions dev/aarch64_clean/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,21 +156,19 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
(MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
MLD_MUST_CHECK_RETURN_VALUE
static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
const int32_t *h)
static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
{
mld_poly_use_hint_32_asm(b, a, h);
mld_poly_use_hint_32_asm(a, h);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
|| MLD_CONFIG_PARAMETER_SET == 87 */

#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
MLD_MUST_CHECK_RETURN_VALUE
static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
const int32_t *h)
static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
{
mld_poly_use_hint_88_asm(b, a, h);
mld_poly_use_hint_88_asm(a, h);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
Expand Down
14 changes: 6 additions & 8 deletions dev/aarch64_clean/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,31 +117,29 @@ __contract__(

#if !defined(MLD_CONFIG_NO_VERIFY_API)
#define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
void mld_poly_use_hint_32_asm(int32_t *a, const int32_t *h)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */
__contract__(
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
requires(array_bound(h, 0, MLDSA_N, 0, 2))
assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
ensures(array_bound(b, 0, MLDSA_N, 0, 16))
assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
ensures(array_bound(a, 0, MLDSA_N, 0, 16))
);

#define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
void mld_poly_use_hint_88_asm(int32_t *a, const int32_t *h)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */
__contract__(
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
requires(array_bound(h, 0, MLDSA_N, 0, 2))
assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
ensures(array_bound(b, 0, MLDSA_N, 0, 44))
assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
ensures(array_bound(a, 0, MLDSA_N, 0, 44))
);
#endif /* !MLD_CONFIG_NO_VERIFY_API */

Expand Down
16 changes: 7 additions & 9 deletions dev/aarch64_clean/src/poly_use_hint_32_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,8 @@
.endm

/* Parameters */
b_ptr .req x0 // Output polynomial
a_ptr .req x1 // Input polynomial
h_ptr .req x2 // Input hints
a_ptr .req x0 // In/out: input on entry, result on exit
h_ptr .req x1 // Input hints

count .req x3

Expand Down Expand Up @@ -88,7 +87,7 @@ poly_use_hint_32_loop:
ldr q1, [a_ptr, #1*16]
ldr q2, [a_ptr, #2*16]
ldr q3, [a_ptr, #3*16]
ldr q0, [a_ptr], #4*16
ldr q0, [a_ptr, #0*16]

ldr q5, [h_ptr, #1*16]
ldr q6, [h_ptr, #2*16]
Expand All @@ -100,17 +99,16 @@ poly_use_hint_32_loop:
use_hint32 v19, v3, v7, v25
use_hint32 v16, v0, v4, v25

str q17, [b_ptr, #1*16]
str q18, [b_ptr, #2*16]
str q19, [b_ptr, #3*16]
str q16, [b_ptr], #4*16
str q17, [a_ptr, #1*16]
str q18, [a_ptr, #2*16]
str q19, [a_ptr, #3*16]
str q16, [a_ptr], #4*16

subs count, count, #1
bne poly_use_hint_32_loop

ret

.unreq b_ptr
.unreq a_ptr
.unreq h_ptr
.unreq count
Expand Down
16 changes: 7 additions & 9 deletions dev/aarch64_clean/src/poly_use_hint_88_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,8 @@
.endm

/* Parameters */
b_ptr .req x0 // Output polynomial
a_ptr .req x1 // Input polynomial
h_ptr .req x2 // Input hints
a_ptr .req x0 // In/out: input on entry, result on exit
h_ptr .req x1 // Input hints

count .req x3

Expand Down Expand Up @@ -90,7 +89,7 @@ poly_use_hint_88_loop:
ldr q1, [a_ptr, #1*16]
ldr q2, [a_ptr, #2*16]
ldr q3, [a_ptr, #3*16]
ldr q0, [a_ptr], #4*16
ldr q0, [a_ptr, #0*16]

ldr q5, [h_ptr, #1*16]
ldr q6, [h_ptr, #2*16]
Expand All @@ -102,17 +101,16 @@ poly_use_hint_88_loop:
use_hint88 v19, v3, v7, v25
use_hint88 v16, v0, v4, v25

str q17, [b_ptr, #1*16]
str q18, [b_ptr, #2*16]
str q19, [b_ptr, #3*16]
str q16, [b_ptr], #4*16
str q17, [a_ptr, #1*16]
str q18, [a_ptr, #2*16]
str q19, [a_ptr, #3*16]
str q16, [a_ptr], #4*16

subs count, count, #1
bne poly_use_hint_88_loop

ret

.unreq b_ptr
.unreq a_ptr
.unreq h_ptr
.unreq count
Expand Down
10 changes: 4 additions & 6 deletions dev/aarch64_opt/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,21 +156,19 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
(MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
MLD_MUST_CHECK_RETURN_VALUE
static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
const int32_t *h)
static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
{
mld_poly_use_hint_32_asm(b, a, h);
mld_poly_use_hint_32_asm(a, h);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
|| MLD_CONFIG_PARAMETER_SET == 87 */

#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
MLD_MUST_CHECK_RETURN_VALUE
static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
const int32_t *h)
static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
{
mld_poly_use_hint_88_asm(b, a, h);
mld_poly_use_hint_88_asm(a, h);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
Expand Down
14 changes: 6 additions & 8 deletions dev/aarch64_opt/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,31 +117,29 @@ __contract__(

#if !defined(MLD_CONFIG_NO_VERIFY_API)
#define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
void mld_poly_use_hint_32_asm(int32_t *a, const int32_t *h)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */
__contract__(
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
requires(array_bound(h, 0, MLDSA_N, 0, 2))
assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
ensures(array_bound(b, 0, MLDSA_N, 0, 16))
assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
ensures(array_bound(a, 0, MLDSA_N, 0, 16))
);

#define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
void mld_poly_use_hint_88_asm(int32_t *a, const int32_t *h)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */
__contract__(
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
requires(array_bound(h, 0, MLDSA_N, 0, 2))
assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
ensures(array_bound(b, 0, MLDSA_N, 0, 44))
assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
ensures(array_bound(a, 0, MLDSA_N, 0, 44))
);
#endif /* !MLD_CONFIG_NO_VERIFY_API */

Expand Down
16 changes: 7 additions & 9 deletions dev/aarch64_opt/src/poly_use_hint_32_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,8 @@
.endm

/* Parameters */
b_ptr .req x0 // Output polynomial
a_ptr .req x1 // Input polynomial
h_ptr .req x2 // Input hints
a_ptr .req x0 // In/out: input on entry, result on exit
h_ptr .req x1 // Input hints

count .req x3

Expand Down Expand Up @@ -88,7 +87,7 @@ poly_use_hint_32_loop:
ldr q1, [a_ptr, #1*16]
ldr q2, [a_ptr, #2*16]
ldr q3, [a_ptr, #3*16]
ldr q0, [a_ptr], #4*16
ldr q0, [a_ptr, #0*16]

ldr q5, [h_ptr, #1*16]
ldr q6, [h_ptr, #2*16]
Expand All @@ -100,17 +99,16 @@ poly_use_hint_32_loop:
use_hint32 v19, v3, v7, v25
use_hint32 v16, v0, v4, v25

str q17, [b_ptr, #1*16]
str q18, [b_ptr, #2*16]
str q19, [b_ptr, #3*16]
str q16, [b_ptr], #4*16
str q17, [a_ptr, #1*16]
str q18, [a_ptr, #2*16]
str q19, [a_ptr, #3*16]
str q16, [a_ptr], #4*16

subs count, count, #1
bne poly_use_hint_32_loop

ret

.unreq b_ptr
.unreq a_ptr
.unreq h_ptr
.unreq count
Expand Down
16 changes: 7 additions & 9 deletions dev/aarch64_opt/src/poly_use_hint_88_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,8 @@
.endm

/* Parameters */
b_ptr .req x0 // Output polynomial
a_ptr .req x1 // Input polynomial
h_ptr .req x2 // Input hints
a_ptr .req x0 // In/out: input on entry, result on exit
h_ptr .req x1 // Input hints

count .req x3

Expand Down Expand Up @@ -90,7 +89,7 @@ poly_use_hint_88_loop:
ldr q1, [a_ptr, #1*16]
ldr q2, [a_ptr, #2*16]
ldr q3, [a_ptr, #3*16]
ldr q0, [a_ptr], #4*16
ldr q0, [a_ptr, #0*16]

ldr q5, [h_ptr, #1*16]
ldr q6, [h_ptr, #2*16]
Expand All @@ -102,17 +101,16 @@ poly_use_hint_88_loop:
use_hint88 v19, v3, v7, v25
use_hint88 v16, v0, v4, v25

str q17, [b_ptr, #1*16]
str q18, [b_ptr, #2*16]
str q19, [b_ptr, #3*16]
str q16, [b_ptr], #4*16
str q17, [a_ptr, #1*16]
str q18, [a_ptr, #2*16]
str q19, [a_ptr, #3*16]
str q16, [a_ptr], #4*16

subs count, count, #1
bne poly_use_hint_88_loop

ret

.unreq b_ptr
.unreq a_ptr
.unreq h_ptr
.unreq count
Expand Down
10 changes: 4 additions & 6 deletions dev/x86_64/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,29 +189,27 @@ static MLD_INLINE int mld_poly_caddq_native(int32_t a[MLDSA_N])
#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
(MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
MLD_MUST_CHECK_RETURN_VALUE
static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a,
const int32_t *h)
static MLD_INLINE int mld_poly_use_hint_32_native(int32_t *a, const int32_t *h)
{
if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2))
{
return MLD_NATIVE_FUNC_FALLBACK;
}
mld_poly_use_hint_32_avx2(b, a, h);
mld_poly_use_hint_32_avx2(a, h);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
|| MLD_CONFIG_PARAMETER_SET == 87 */

#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
MLD_MUST_CHECK_RETURN_VALUE
static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
const int32_t *h)
static MLD_INLINE int mld_poly_use_hint_88_native(int32_t *a, const int32_t *h)
{
if (!mld_sys_check_capability(MLD_SYS_CAP_AVX2))
{
return MLD_NATIVE_FUNC_FALLBACK;
}
mld_poly_use_hint_88_avx2(b, a, h);
mld_poly_use_hint_88_avx2(a, h);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
Expand Down
4 changes: 2 additions & 2 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 @@ -103,10 +103,10 @@ void mld_poly_caddq_avx2(int32_t *r);

#if !defined(MLD_CONFIG_NO_VERIFY_API)
#define mld_poly_use_hint_32_avx2 MLD_NAMESPACE(mld_poly_use_hint_32_avx2)
void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a, const int32_t *h);
void mld_poly_use_hint_32_avx2(int32_t *a, const int32_t *h);

#define mld_poly_use_hint_88_avx2 MLD_NAMESPACE(mld_poly_use_hint_88_avx2)
void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a, const int32_t *h);
void mld_poly_use_hint_88_avx2(int32_t *a, const int32_t *h);
#endif /* !MLD_CONFIG_NO_VERIFY_API */

#define mld_poly_chknorm_avx2 MLD_NAMESPACE(mld_poly_chknorm_avx2)
Expand Down
5 changes: 2 additions & 3 deletions dev/x86_64/src/poly_use_hint_32_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,7 @@
_mm256_castsi256_ps(b), \
_mm256_castsi256_ps(mask)))

void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a,
const int32_t *hint)
void mld_poly_use_hint_32_avx2(int32_t *a, const int32_t *hint)
{
unsigned int i;
__m256i f, f0, f1, h, t;
Expand Down Expand Up @@ -83,7 +82,7 @@ void mld_poly_use_hint_32_avx2(int32_t *b, const int32_t *a,
f1 = _mm256_add_epi32(f1, h);
f1 = _mm256_and_si256(f1, mask);

_mm256_store_si256((__m256i *)&b[8 * i], f1);
_mm256_store_si256((__m256i *)&a[8 * i], f1);
}
}

Expand Down
5 changes: 2 additions & 3 deletions dev/x86_64/src/poly_use_hint_88_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,7 @@
_mm256_castsi256_ps(b), \
_mm256_castsi256_ps(mask)))

void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a,
const int32_t *hint)
void mld_poly_use_hint_88_avx2(int32_t *a, const int32_t *hint)
{
unsigned int i;
__m256i f, f0, f1, h, t;
Expand Down Expand Up @@ -85,7 +84,7 @@ void mld_poly_use_hint_88_avx2(int32_t *b, const int32_t *a,
f = _mm256_cmpgt_epi32(f1, max);
f1 = MLD_MM256_BLENDV_EPI32(f1, zero, f);

_mm256_store_si256((__m256i *)&b[8 * i], f1);
_mm256_store_si256((__m256i *)&a[8 * i], f1);
}
}

Expand Down
Loading
Loading