Skip to content

Commit f789e8d

Browse files
jakemasjakemas
committed
x86_64: Replace rej_uniform_eta2/eta4 intrinsics with hand-written assembly
Add hand-written x86_64 AVX2 assembly for rej_uniform_eta2 and rej_uniform_eta4 and remove the AVX2 intrinsics implementations they replace, following the rej_uniform approach in #1014: the table is passed as a parameter and all constants are built from immediates (no .rodata), enabling future HOL-Light verification. Both eta2 and eta4 are wired to the new asm in meta.h, with contracts in arith_native_x86_64.h, bytecode dump targets in autogen and the Makefile, and a poly_uniform_eta_4x component benchmark. The eta2 vector path applies the centered mod-5 reduction to (2 - nibble) directly (matching the reference), rather than reducing the raw nibble and subtracting afterwards; the two are not equivalent because vpmulhrsw rounds to nearest. Verified against the ACVP keyGen vectors for all parameter sets. Signed-off-by: jake massimo <jakemas@amazon.com>
1 parent 70fdba0 commit f789e8d

20 files changed

Lines changed: 1255 additions & 625 deletions

‎BIBLIOGRAPHY.md‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -279,8 +279,8 @@ source code and documentation.
279279
- [dev/x86_64/src/polyz_unpack_17_avx2_asm.S](dev/x86_64/src/polyz_unpack_17_avx2_asm.S)
280280
- [dev/x86_64/src/polyz_unpack_19_avx2_asm.S](dev/x86_64/src/polyz_unpack_19_avx2_asm.S)
281281
- [dev/x86_64/src/rej_uniform_avx2.c](dev/x86_64/src/rej_uniform_avx2.c)
282-
- [dev/x86_64/src/rej_uniform_eta2_avx2.c](dev/x86_64/src/rej_uniform_eta2_avx2.c)
283-
- [dev/x86_64/src/rej_uniform_eta4_avx2.c](dev/x86_64/src/rej_uniform_eta4_avx2.c)
282+
- [dev/x86_64/src/rej_uniform_eta2_avx2_asm.S](dev/x86_64/src/rej_uniform_eta2_avx2_asm.S)
283+
- [dev/x86_64/src/rej_uniform_eta4_avx2_asm.S](dev/x86_64/src/rej_uniform_eta4_avx2_asm.S)
284284
- [mldsa/src/native/x86_64/src/intt_avx2_asm.S](mldsa/src/native/x86_64/src/intt_avx2_asm.S)
285285
- [mldsa/src/native/x86_64/src/ntt_avx2_asm.S](mldsa/src/native/x86_64/src/ntt_avx2_asm.S)
286286
- [mldsa/src/native/x86_64/src/nttunpack_avx2_asm.S](mldsa/src/native/x86_64/src/nttunpack_avx2_asm.S)
@@ -297,8 +297,8 @@ source code and documentation.
297297
- [mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S](mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S)
298298
- [mldsa/src/native/x86_64/src/polyz_unpack_19_avx2_asm.S](mldsa/src/native/x86_64/src/polyz_unpack_19_avx2_asm.S)
299299
- [mldsa/src/native/x86_64/src/rej_uniform_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_avx2.c)
300-
- [mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c)
301-
- [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c)
300+
- [mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2_asm.S](mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2_asm.S)
301+
- [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2_asm.S](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2_asm.S)
302302
- [proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S](proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S)
303303
- [proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S](proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S)
304304
- [proofs/hol_light/x86_64/mldsa/nttunpack_avx2_asm.S](proofs/hol_light/x86_64/mldsa/nttunpack_avx2_asm.S)
@@ -310,6 +310,8 @@ source code and documentation.
310310
- [proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S)
311311
- [proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S)
312312
- [proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S)
313+
- [proofs/hol_light/x86_64/mldsa/rej_uniform_eta2_avx2_asm.S](proofs/hol_light/x86_64/mldsa/rej_uniform_eta2_avx2_asm.S)
314+
- [proofs/hol_light/x86_64/mldsa/rej_uniform_eta4_avx2_asm.S](proofs/hol_light/x86_64/mldsa/rej_uniform_eta4_avx2_asm.S)
313315

314316
### `Round3_Spec`
315317

‎dev/x86_64/meta.h‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,8 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
106106
* We declassify prior the input data and mark the outputs as secret.
107107
*/
108108
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
109-
outlen = mld_rej_uniform_eta2_avx2(r, buf);
109+
outlen = mld_rej_uniform_eta2_avx2_asm(
110+
r, buf, (const uint8_t *)mld_rej_uniform_table);
110111
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
111112
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
112113
return (int)outlen;
@@ -135,7 +136,8 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
135136
* We declassify prior the input data and mark the outputs as secret.
136137
*/
137138
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
138-
outlen = mld_rej_uniform_eta4_avx2(r, buf);
139+
outlen = mld_rej_uniform_eta4_avx2_asm(
140+
r, buf, (const uint8_t *)mld_rej_uniform_table);
139141
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
140142
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
141143
return (int)outlen;

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 28 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -83,15 +83,37 @@ unsigned mld_rej_uniform_avx2(int32_t *r,
8383
const uint8_t buf[MLD_AVX2_REJ_UNIFORM_BUFLEN]);
8484

8585
#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
86-
#define mld_rej_uniform_eta2_avx2 MLD_NAMESPACE(mld_rej_uniform_eta2_avx2)
86+
#define mld_rej_uniform_eta2_avx2_asm MLD_NAMESPACE(rej_uniform_eta2_avx2_asm)
87+
/* This contract must be kept in sync with the HOL-Light specification
88+
* in proofs/hol_light/x86_64/proofs/rej_uniform_eta2_avx2_asm.ml */
8789
MLD_MUST_CHECK_RETURN_VALUE
88-
unsigned mld_rej_uniform_eta2_avx2(
89-
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN]);
90+
unsigned mld_rej_uniform_eta2_avx2_asm(
91+
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN],
92+
const uint8_t *table)
93+
__contract__(
94+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
95+
requires(memory_no_alias(buf, MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN))
96+
requires(table == mld_rej_uniform_table)
97+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
98+
ensures(return_value <= MLDSA_N)
99+
ensures(array_bound(r, 0, return_value, -2, 2))
100+
);
90101

91-
#define mld_rej_uniform_eta4_avx2 MLD_NAMESPACE(mld_rej_uniform_eta4_avx2)
102+
#define mld_rej_uniform_eta4_avx2_asm MLD_NAMESPACE(rej_uniform_eta4_avx2_asm)
103+
/* This contract must be kept in sync with the HOL-Light specification
104+
* in proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml */
92105
MLD_MUST_CHECK_RETURN_VALUE
93-
unsigned mld_rej_uniform_eta4_avx2(
94-
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN]);
106+
unsigned mld_rej_uniform_eta4_avx2_asm(
107+
int32_t *r, const uint8_t buf[MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN],
108+
const uint8_t *table)
109+
__contract__(
110+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
111+
requires(memory_no_alias(buf, MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN))
112+
requires(table == mld_rej_uniform_table)
113+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
114+
ensures(return_value <= MLDSA_N)
115+
ensures(array_bound(r, 0, return_value, -4, 4))
116+
);
95117
#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
96118

97119
#if !defined(MLD_CONFIG_NO_SIGN_API)

‎dev/x86_64/src/rej_uniform_eta2_avx2.c‎

Lines changed: 0 additions & 157 deletions
This file was deleted.

0 commit comments

Comments
 (0)