Skip to content

Commit 85979ed

Browse files
jakemasmkannwischer
jakemas
authored and
mkannwischer
committed
x86_64: Replace poly_decompose AVX2 intrinsics with hand-written assembly
Mirror the AArch64 conversion in poly_decompose_{32,88}_aarch64_asm: replace the C intrinsics with fully-unrolled AVX2 routines, add HOL-Light correctness and memory-safety proofs, and CBMC contracts. Helper lemmas common to both variants are shared via the x86-only mldsa_utils.ml. - Resolves #420 - Resolves #914 Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent f6a6793 commit 85979ed

35 files changed

Lines changed: 5407 additions & 654 deletions

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -205,6 +205,10 @@ jobs:
205205
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
206206
- name: poly_chknorm_avx2_asm
207207
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
208+
- name: poly_decompose_32_avx2_asm
209+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
210+
- name: poly_decompose_88_avx2_asm
211+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
208212
- name: polyz_unpack_17_avx2_asm
209213
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
210214
- name: polyz_unpack_19_avx2_asm

‎BIBLIOGRAPHY.md‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -302,8 +302,8 @@ source code and documentation.
302302
- [dev/x86_64/src/pointwise_avx2_asm.S](dev/x86_64/src/pointwise_avx2_asm.S)
303303
- [dev/x86_64/src/poly_caddq_avx2_asm.S](dev/x86_64/src/poly_caddq_avx2_asm.S)
304304
- [dev/x86_64/src/poly_chknorm_avx2_asm.S](dev/x86_64/src/poly_chknorm_avx2_asm.S)
305-
- [dev/x86_64/src/poly_decompose_32_avx2.c](dev/x86_64/src/poly_decompose_32_avx2.c)
306-
- [dev/x86_64/src/poly_decompose_88_avx2.c](dev/x86_64/src/poly_decompose_88_avx2.c)
305+
- [dev/x86_64/src/poly_decompose_32_avx2_asm.S](dev/x86_64/src/poly_decompose_32_avx2_asm.S)
306+
- [dev/x86_64/src/poly_decompose_88_avx2_asm.S](dev/x86_64/src/poly_decompose_88_avx2_asm.S)
307307
- [dev/x86_64/src/poly_use_hint_32_avx2.c](dev/x86_64/src/poly_use_hint_32_avx2.c)
308308
- [dev/x86_64/src/poly_use_hint_88_avx2.c](dev/x86_64/src/poly_use_hint_88_avx2.c)
309309
- [dev/x86_64/src/polyz_unpack_17_avx2_asm.S](dev/x86_64/src/polyz_unpack_17_avx2_asm.S)
@@ -320,8 +320,8 @@ source code and documentation.
320320
- [mldsa/src/native/x86_64/src/pointwise_avx2_asm.S](mldsa/src/native/x86_64/src/pointwise_avx2_asm.S)
321321
- [mldsa/src/native/x86_64/src/poly_caddq_avx2_asm.S](mldsa/src/native/x86_64/src/poly_caddq_avx2_asm.S)
322322
- [mldsa/src/native/x86_64/src/poly_chknorm_avx2_asm.S](mldsa/src/native/x86_64/src/poly_chknorm_avx2_asm.S)
323-
- [mldsa/src/native/x86_64/src/poly_decompose_32_avx2.c](mldsa/src/native/x86_64/src/poly_decompose_32_avx2.c)
324-
- [mldsa/src/native/x86_64/src/poly_decompose_88_avx2.c](mldsa/src/native/x86_64/src/poly_decompose_88_avx2.c)
323+
- [mldsa/src/native/x86_64/src/poly_decompose_32_avx2_asm.S](mldsa/src/native/x86_64/src/poly_decompose_32_avx2_asm.S)
324+
- [mldsa/src/native/x86_64/src/poly_decompose_88_avx2_asm.S](mldsa/src/native/x86_64/src/poly_decompose_88_avx2_asm.S)
325325
- [mldsa/src/native/x86_64/src/poly_use_hint_32_avx2.c](mldsa/src/native/x86_64/src/poly_use_hint_32_avx2.c)
326326
- [mldsa/src/native/x86_64/src/poly_use_hint_88_avx2.c](mldsa/src/native/x86_64/src/poly_use_hint_88_avx2.c)
327327
- [mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S](mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S)
@@ -338,6 +338,8 @@ source code and documentation.
338338
- [proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S)
339339
- [proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S)
340340
- [proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S)
341+
- [proofs/hol_light/x86_64/mldsa/poly_decompose_32_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_decompose_32_avx2_asm.S)
342+
- [proofs/hol_light/x86_64/mldsa/poly_decompose_88_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_decompose_88_avx2_asm.S)
341343
- [proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S)
342344
- [proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S)
343345

‎dev/x86_64/meta.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,7 @@ static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0)
153153
{
154154
return MLD_NATIVE_FUNC_FALLBACK;
155155
}
156-
mld_poly_decompose_32_avx2(a1, a0);
156+
mld_poly_decompose_32_avx2_asm(a1, a0);
157157
return MLD_NATIVE_FUNC_SUCCESS;
158158
}
159159
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
@@ -167,7 +167,7 @@ static MLD_INLINE int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0)
167167
{
168168
return MLD_NATIVE_FUNC_FALLBACK;
169169
}
170-
mld_poly_decompose_88_avx2(a1, a0);
170+
mld_poly_decompose_88_avx2_asm(a1, a0);
171171
return MLD_NATIVE_FUNC_SUCCESS;
172172
}
173173
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 32 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -95,11 +95,39 @@ unsigned mld_rej_uniform_eta4_avx2(
9595
#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
9696

9797
#if !defined(MLD_CONFIG_NO_SIGN_API)
98-
#define mld_poly_decompose_32_avx2 MLD_NAMESPACE(mld_poly_decompose_32_avx2)
99-
void mld_poly_decompose_32_avx2(int32_t *a1, int32_t *a0);
98+
#define mld_poly_decompose_32_avx2_asm MLD_NAMESPACE(poly_decompose_32_avx2_asm)
99+
MLD_SYSV_ABI
100+
void mld_poly_decompose_32_avx2_asm(int32_t *a1, int32_t *a0)
101+
/* This must be kept in sync with the HOL-Light specification
102+
* in proofs/hol_light/x86_64/proofs/poly_decompose_32_avx2_asm.ml */
103+
__contract__(
104+
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
105+
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
106+
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
107+
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
108+
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
109+
/* check-magic: 16 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 32)) */
110+
ensures(array_bound(a1, 0, MLDSA_N, 0, 16))
111+
/* check-magic: 261889 == (MLDSA_Q - 1) / 32 + 1 */
112+
ensures(array_abs_bound(a0, 0, MLDSA_N, 261889))
113+
);
100114

101-
#define mld_poly_decompose_88_avx2 MLD_NAMESPACE(mld_poly_decompose_88_avx2)
102-
void mld_poly_decompose_88_avx2(int32_t *a1, int32_t *a0);
115+
#define mld_poly_decompose_88_avx2_asm MLD_NAMESPACE(poly_decompose_88_avx2_asm)
116+
MLD_SYSV_ABI
117+
void mld_poly_decompose_88_avx2_asm(int32_t *a1, int32_t *a0)
118+
/* This must be kept in sync with the HOL-Light specification
119+
* in proofs/hol_light/x86_64/proofs/poly_decompose_88_avx2_asm.ml */
120+
__contract__(
121+
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
122+
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
123+
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
124+
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
125+
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
126+
/* check-magic: 44 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 88)) */
127+
ensures(array_bound(a1, 0, MLDSA_N, 0, 44))
128+
/* check-magic: 95233 == (MLDSA_Q - 1) / 88 + 1 */
129+
ensures(array_abs_bound(a0, 0, MLDSA_N, 95233))
130+
);
103131
#endif /* !MLD_CONFIG_NO_SIGN_API */
104132

105133
#define mld_poly_caddq_avx2_asm MLD_NAMESPACE(poly_caddq_avx2_asm)

‎dev/x86_64/src/poly_decompose_32_avx2.c‎

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

0 commit comments

Comments
 (0)