Skip to content

x86_64 + HOL-Light: Replace poly_decompose AVX2 intrinsics with hand-written assembly and HOL-Light proofs #1181

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
jakemas wants to merge 1 commit into
base: main
Choose a base branch
from
Open

x86_64 + HOL-Light: Replace poly_decompose AVX2 intrinsics with hand-written assembly and HOL-Light proofs #1181

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
4 changes: 4 additions & 0 deletions .github/workflows/hol_light.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,10 @@ jobs:
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
- name: poly_chknorm_avx2_asm
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
- name: poly_decompose_32_avx2_asm
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
- name: poly_decompose_88_avx2_asm
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
- name: polyz_unpack_17_avx2_asm
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "subroutine_signatures.ml"]
- name: polyz_unpack_19_avx2_asm
Expand Down
10 changes: 6 additions & 4 deletions BIBLIOGRAPHY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -272,8 +272,8 @@ source code and documentation.
- [dev/x86_64/src/pointwise_avx2_asm.S](dev/x86_64/src/pointwise_avx2_asm.S)
- [dev/x86_64/src/poly_caddq_avx2_asm.S](dev/x86_64/src/poly_caddq_avx2_asm.S)
- [dev/x86_64/src/poly_chknorm_avx2_asm.S](dev/x86_64/src/poly_chknorm_avx2_asm.S)
- [dev/x86_64/src/poly_decompose_32_avx2.c](dev/x86_64/src/poly_decompose_32_avx2.c)
- [dev/x86_64/src/poly_decompose_88_avx2.c](dev/x86_64/src/poly_decompose_88_avx2.c)
- [dev/x86_64/src/poly_decompose_32_avx2_asm.S](dev/x86_64/src/poly_decompose_32_avx2_asm.S)
- [dev/x86_64/src/poly_decompose_88_avx2_asm.S](dev/x86_64/src/poly_decompose_88_avx2_asm.S)
- [dev/x86_64/src/poly_use_hint_32_avx2.c](dev/x86_64/src/poly_use_hint_32_avx2.c)
- [dev/x86_64/src/poly_use_hint_88_avx2.c](dev/x86_64/src/poly_use_hint_88_avx2.c)
- [dev/x86_64/src/polyz_unpack_17_avx2_asm.S](dev/x86_64/src/polyz_unpack_17_avx2_asm.S)
Expand All @@ -290,8 +290,8 @@ source code and documentation.
- [mldsa/src/native/x86_64/src/pointwise_avx2_asm.S](mldsa/src/native/x86_64/src/pointwise_avx2_asm.S)
- [mldsa/src/native/x86_64/src/poly_caddq_avx2_asm.S](mldsa/src/native/x86_64/src/poly_caddq_avx2_asm.S)
- [mldsa/src/native/x86_64/src/poly_chknorm_avx2_asm.S](mldsa/src/native/x86_64/src/poly_chknorm_avx2_asm.S)
- [mldsa/src/native/x86_64/src/poly_decompose_32_avx2.c](mldsa/src/native/x86_64/src/poly_decompose_32_avx2.c)
- [mldsa/src/native/x86_64/src/poly_decompose_88_avx2.c](mldsa/src/native/x86_64/src/poly_decompose_88_avx2.c)
- [mldsa/src/native/x86_64/src/poly_decompose_32_avx2_asm.S](mldsa/src/native/x86_64/src/poly_decompose_32_avx2_asm.S)
- [mldsa/src/native/x86_64/src/poly_decompose_88_avx2_asm.S](mldsa/src/native/x86_64/src/poly_decompose_88_avx2_asm.S)
- [mldsa/src/native/x86_64/src/poly_use_hint_32_avx2.c](mldsa/src/native/x86_64/src/poly_use_hint_32_avx2.c)
- [mldsa/src/native/x86_64/src/poly_use_hint_88_avx2.c](mldsa/src/native/x86_64/src/poly_use_hint_88_avx2.c)
- [mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S](mldsa/src/native/x86_64/src/polyz_unpack_17_avx2_asm.S)
Expand All @@ -308,6 +308,8 @@ source code and documentation.
- [proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S)
- [proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_caddq_avx2_asm.S)
- [proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_chknorm_avx2_asm.S)
- [proofs/hol_light/x86_64/mldsa/poly_decompose_32_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_decompose_32_avx2_asm.S)
- [proofs/hol_light/x86_64/mldsa/poly_decompose_88_avx2_asm.S](proofs/hol_light/x86_64/mldsa/poly_decompose_88_avx2_asm.S)
- [proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_17_avx2_asm.S)
- [proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S](proofs/hol_light/x86_64/mldsa/polyz_unpack_19_avx2_asm.S)

Expand Down
4 changes: 2 additions & 2 deletions dev/x86_64/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,7 @@ static MLD_INLINE int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0)
{
return MLD_NATIVE_FUNC_FALLBACK;
}
mld_poly_decompose_32_avx2(a1, a0);
mld_poly_decompose_32_avx2_asm(a1, a0);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
Expand All @@ -167,7 +167,7 @@ static MLD_INLINE int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0)
{
return MLD_NATIVE_FUNC_FALLBACK;
}
mld_poly_decompose_88_avx2(a1, a0);
mld_poly_decompose_88_avx2_asm(a1, a0);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
Expand Down
36 changes: 32 additions & 4 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 @@ -95,11 +95,39 @@ unsigned mld_rej_uniform_eta4_avx2(
#endif /* !MLD_CONFIG_NO_KEYPAIR_API */

#if !defined(MLD_CONFIG_NO_SIGN_API)
#define mld_poly_decompose_32_avx2 MLD_NAMESPACE(mld_poly_decompose_32_avx2)
void mld_poly_decompose_32_avx2(int32_t *a1, int32_t *a0);
#define mld_poly_decompose_32_avx2_asm MLD_NAMESPACE(poly_decompose_32_avx2_asm)
MLD_SYSV_ABI
void mld_poly_decompose_32_avx2_asm(int32_t *a1, int32_t *a0)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/poly_decompose_32_avx2_asm.ml */
__contract__(
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
/* check-magic: 16 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 32)) */
ensures(array_bound(a1, 0, MLDSA_N, 0, 16))
/* check-magic: 261889 == (MLDSA_Q - 1) / 32 + 1 */
ensures(array_abs_bound(a0, 0, MLDSA_N, 261889))
);

#define mld_poly_decompose_88_avx2 MLD_NAMESPACE(mld_poly_decompose_88_avx2)
void mld_poly_decompose_88_avx2(int32_t *a1, int32_t *a0);
#define mld_poly_decompose_88_avx2_asm MLD_NAMESPACE(poly_decompose_88_avx2_asm)
MLD_SYSV_ABI
void mld_poly_decompose_88_avx2_asm(int32_t *a1, int32_t *a0)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/poly_decompose_88_avx2_asm.ml */
__contract__(
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
/* check-magic: 44 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 88)) */
ensures(array_bound(a1, 0, MLDSA_N, 0, 44))
/* check-magic: 95233 == (MLDSA_Q - 1) / 88 + 1 */
ensures(array_abs_bound(a0, 0, MLDSA_N, 95233))
);
#endif /* !MLD_CONFIG_NO_SIGN_API */

#define mld_poly_caddq_avx2_asm MLD_NAMESPACE(poly_caddq_avx2_asm)
Expand Down
157 changes: 0 additions & 157 deletions dev/x86_64/src/poly_decompose_32_avx2.c
View file
Open in desktop

This file was deleted.

Loading
Loading