Skip to content

Commit ebe4c51

Browse files
mkannwischermkannwischer
committed
HOL-Light: Add AArch64 poly_decompose_{32,88} correctness proofs
Add functional correctness proofs for the AArch64 assembly implementations of poly_decompose for both GAMMA2 variants: - poly_decompose_32 (GAMMA2 = (Q-1)/32 = 261888, used in ML-DSA-65/87) - poly_decompose_88 (GAMMA2 = (Q-1)/88 = 95232, used in ML-DSA-44) Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent 35ca99c commit ebe4c51

11 files changed

Lines changed: 1775 additions & 0 deletions

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,10 @@ jobs:
115115
needs: ["aarch64_utils.ml", "mldsa_polyz_unpack_consts.ml", "mldsa_specs.ml", "subroutine_signatures.ml"]
116116
- name: mldsa_polyz_unpack_19
117117
needs: ["aarch64_utils.ml", "mldsa_polyz_unpack_consts.ml", "mldsa_specs.ml", "subroutine_signatures.ml"]
118+
- name: poly_decompose_32_aarch64_asm
119+
needs: ["aarch64_utils.ml", "mldsa_specs.ml", "subroutine_signatures.ml"]
120+
- name: poly_decompose_88_aarch64_asm
121+
needs: ["aarch64_utils.ml", "mldsa_specs.ml", "subroutine_signatures.ml"]
118122
name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
119123
runs-on: pqcp-arm64
120124
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

‎proofs/hol_light/README.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,8 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
5757
* AArch64 poly_chknorm: [mldsa_poly_chknorm.S](aarch64/mldsa/mldsa_poly_chknorm.S)
5858
* AArch64 poly_use_hint (l=5,7): [poly_use_hint_32_aarch64_asm.S](aarch64/mldsa/poly_use_hint_32_aarch64_asm.S)
5959
* AArch64 poly_use_hint (l=4): [poly_use_hint_88_aarch64_asm.S](aarch64/mldsa/poly_use_hint_88_aarch64_asm.S)
60+
* AArch64 poly_decompose (l=5,7): [poly_decompose_32_aarch64_asm.S](aarch64/mldsa/poly_decompose_32_aarch64_asm.S)
61+
* AArch64 poly_decompose (l=4): [poly_decompose_88_aarch64_asm.S](aarch64/mldsa/poly_decompose_88_aarch64_asm.S)
6062
* AArch64 pointwise multiplication: [mldsa_pointwise.S](aarch64/mldsa/mldsa_pointwise.S)
6163
* AArch64 pointwise multiplication-accumulation (l=4): [mldsa_pointwise_acc_l4.S](aarch64/mldsa/mldsa_pointwise_acc_l4.S)
6264
* AArch64 pointwise multiplication-accumulation (l=5): [mldsa_pointwise_acc_l5.S](aarch64/mldsa/mldsa_pointwise_acc_l5.S)

‎proofs/hol_light/aarch64/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,8 @@ OBJ = mldsa/mldsa_ntt.o \
5757
mldsa/mldsa_pointwise.o \
5858
mldsa/mldsa_poly_caddq.o \
5959
mldsa/mldsa_poly_chknorm.o \
60+
mldsa/poly_decompose_32_aarch64_asm.o \
61+
mldsa/poly_decompose_88_aarch64_asm.o \
6062
mldsa/mldsa_pointwise_acc_l4.o \
6163
mldsa/mldsa_pointwise_acc_l5.o \
6264
mldsa/mldsa_pointwise_acc_l7.o \

‎proofs/hol_light/aarch64/mldsa/poly_decompose_32_aarch64_asm.S‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
/*
2+
* Copyright (c) The mldsa-native project authors
3+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
*/
5+
6+
7+
/*
8+
* WARNING: This file is auto-derived from the mldsa-native source file
9+
* dev/aarch64_opt/src/poly_decompose_32_asm.S using scripts/simpasm. Do not modify it directly.
10+
*/
11+
12+
.text
13+
.balign 4
14+
#ifdef __APPLE__
15+
.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_32_asm
16+
_PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_32_asm:
17+
#else
18+
.global PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_32_asm
19+
PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_32_asm:
20+
#endif
21+
22+
.cfi_startproc
23+
mov w4, #0xe001 // =57345
24+
movk w4, #0x7f, lsl #16
25+
dup v20.4s, w4
26+
mov w5, #0xe100 // =57600
27+
movk w5, #0x7b, lsl #16
28+
dup v21.4s, w5
29+
mov w7, #0xfe00 // =65024
30+
movk w7, #0x7, lsl #16
31+
dup v22.4s, w7
32+
mov w11, #0x401 // =1025
33+
movk w11, #0x4010, lsl #16
34+
dup v23.4s, w11
35+
mov x3, #0x10 // =16
36+
37+
Lpoly_decompose_32_loop:
38+
ldr q0, [x1]
39+
ldr q1, [x1, #0x10]
40+
ldr q2, [x1, #0x20]
41+
ldr q3, [x1, #0x30]
42+
sqdmulh v5.4s, v1.4s, v23.4s
43+
srshr v5.4s, v5.4s, #0x12
44+
cmgt v24.4s, v1.4s, v21.4s
45+
mls v1.4s, v5.4s, v22.4s
46+
bic v5.16b, v5.16b, v24.16b
47+
add v1.4s, v1.4s, v24.4s
48+
sqdmulh v6.4s, v2.4s, v23.4s
49+
srshr v6.4s, v6.4s, #0x12
50+
cmgt v24.4s, v2.4s, v21.4s
51+
mls v2.4s, v6.4s, v22.4s
52+
bic v6.16b, v6.16b, v24.16b
53+
add v2.4s, v2.4s, v24.4s
54+
sqdmulh v7.4s, v3.4s, v23.4s
55+
srshr v7.4s, v7.4s, #0x12
56+
cmgt v24.4s, v3.4s, v21.4s
57+
mls v3.4s, v7.4s, v22.4s
58+
bic v7.16b, v7.16b, v24.16b
59+
add v3.4s, v3.4s, v24.4s
60+
sqdmulh v4.4s, v0.4s, v23.4s
61+
srshr v4.4s, v4.4s, #0x12
62+
cmgt v24.4s, v0.4s, v21.4s
63+
mls v0.4s, v4.4s, v22.4s
64+
bic v4.16b, v4.16b, v24.16b
65+
add v0.4s, v0.4s, v24.4s
66+
str q5, [x0, #0x10]
67+
str q6, [x0, #0x20]
68+
str q7, [x0, #0x30]
69+
str q4, [x0], #0x40
70+
str q1, [x1, #0x10]
71+
str q2, [x1, #0x20]
72+
str q3, [x1, #0x30]
73+
str q0, [x1], #0x40
74+
subs x3, x3, #0x1
75+
b.ne Lpoly_decompose_32_loop
76+
ret
77+
.cfi_endproc
78+
79+
#if defined(__ELF__)
80+
.section .note.GNU-stack,"",%progbits
81+
#endif

‎proofs/hol_light/aarch64/mldsa/poly_decompose_88_aarch64_asm.S‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
/*
2+
* Copyright (c) The mldsa-native project authors
3+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
*/
5+
6+
7+
/*
8+
* WARNING: This file is auto-derived from the mldsa-native source file
9+
* dev/aarch64_opt/src/poly_decompose_88_asm.S using scripts/simpasm. Do not modify it directly.
10+
*/
11+
12+
.text
13+
.balign 4
14+
#ifdef __APPLE__
15+
.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_88_asm
16+
_PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_88_asm:
17+
#else
18+
.global PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_88_asm
19+
PQCP_MLDSA_NATIVE_MLDSA44_poly_decompose_88_asm:
20+
#endif
21+
22+
.cfi_startproc
23+
mov w4, #0xe001 // =57345
24+
movk w4, #0x7f, lsl #16
25+
dup v20.4s, w4
26+
mov w5, #0x6c00 // =27648
27+
movk w5, #0x7e, lsl #16
28+
dup v21.4s, w5
29+
mov w7, #0xe800 // =59392
30+
movk w7, #0x2, lsl #16
31+
dup v22.4s, w7
32+
mov w11, #0x581 // =1409
33+
movk w11, #0x5816, lsl #16
34+
dup v23.4s, w11
35+
mov x3, #0x10 // =16
36+
37+
Lpoly_decompose_88_loop:
38+
ldr q0, [x1]
39+
ldr q1, [x1, #0x10]
40+
ldr q2, [x1, #0x20]
41+
ldr q3, [x1, #0x30]
42+
sqdmulh v5.4s, v1.4s, v23.4s
43+
srshr v5.4s, v5.4s, #0x11
44+
cmgt v24.4s, v1.4s, v21.4s
45+
mls v1.4s, v5.4s, v22.4s
46+
bic v5.16b, v5.16b, v24.16b
47+
add v1.4s, v1.4s, v24.4s
48+
sqdmulh v6.4s, v2.4s, v23.4s
49+
srshr v6.4s, v6.4s, #0x11
50+
cmgt v24.4s, v2.4s, v21.4s
51+
mls v2.4s, v6.4s, v22.4s
52+
bic v6.16b, v6.16b, v24.16b
53+
add v2.4s, v2.4s, v24.4s
54+
sqdmulh v7.4s, v3.4s, v23.4s
55+
srshr v7.4s, v7.4s, #0x11
56+
cmgt v24.4s, v3.4s, v21.4s
57+
mls v3.4s, v7.4s, v22.4s
58+
bic v7.16b, v7.16b, v24.16b
59+
add v3.4s, v3.4s, v24.4s
60+
sqdmulh v4.4s, v0.4s, v23.4s
61+
srshr v4.4s, v4.4s, #0x11
62+
cmgt v24.4s, v0.4s, v21.4s
63+
mls v0.4s, v4.4s, v22.4s
64+
bic v4.16b, v4.16b, v24.16b
65+
add v0.4s, v0.4s, v24.4s
66+
str q5, [x0, #0x10]
67+
str q6, [x0, #0x20]
68+
str q7, [x0, #0x30]
69+
str q4, [x0], #0x40
70+
str q1, [x1, #0x10]
71+
str q2, [x1, #0x20]
72+
str q3, [x1, #0x30]
73+
str q0, [x1], #0x40
74+
subs x3, x3, #0x1
75+
b.ne Lpoly_decompose_88_loop
76+
ret
77+
.cfi_endproc
78+
79+
#if defined(__ELF__)
80+
.section .note.GNU-stack,"",%progbits
81+
#endif

‎proofs/hol_light/aarch64/proofs/dump_bytecode.ml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,14 @@ print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_chknorm.o ===\n";;
4242
print_literal_from_elf "aarch64/mldsa/mldsa_poly_chknorm.o";;
4343
print_string "==== bytecode end =====================================\n\n";;
4444

45+
print_string "=== bytecode start: aarch64/mldsa/poly_decompose_32_aarch64_asm.o ===\n";;
46+
print_literal_from_elf "aarch64/mldsa/poly_decompose_32_aarch64_asm.o";;
47+
print_string "==== bytecode end =====================================\n\n";;
48+
49+
print_string "=== bytecode start: aarch64/mldsa/poly_decompose_88_aarch64_asm.o ===\n";;
50+
print_literal_from_elf "aarch64/mldsa/poly_decompose_88_aarch64_asm.o";;
51+
print_string "==== bytecode end =====================================\n\n";;
52+
4553
print_string "=== bytecode start: aarch64/mldsa/mldsa_polyz_unpack_17.o ===\n";;
4654
print_literal_from_elf "aarch64/mldsa/mldsa_polyz_unpack_17.o";;
4755
print_string "==== bytecode end =====================================\n\n";;

0 commit comments

Comments
 (0)