Skip to content

Commit f2b5fe9

Browse files
mkannwischermkannwischer
committed
HOL-Light: Add HOL Light proof for aarch64 polyz_unpack_{17,19}
Add functional correctness proofs for polyz_unpack_17 and polyz_unpack_19. Closely following the decompress proofs from mlkem-native: pq-code-package/mlkem-native#1543 Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent bb07ee8 commit f2b5fe9

File tree

12 files changed

+1377
-5
lines changed

12 files changed

+1377
-5
lines changed

‎.github/workflows/hol_light.yml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ on:
1212
- 'proofs/hol_light/aarch64/Makefile'
1313
- 'proofs/hol_light/aarch64/**/*.S'
1414
- 'proofs/hol_light/aarch64/**/*.ml'
15+
- 'proofs/hol_light/common/**/*.ml'
1516
- 'proofs/hol_light/x86_64/Makefile'
1617
- 'proofs/hol_light/x86_64/**/*.S'
1718
- 'proofs/hol_light/x86_64/**/*.ml'
@@ -26,6 +27,7 @@ on:
2627
- 'proofs/hol_light/aarch64/Makefile'
2728
- 'proofs/hol_light/aarch64/**/*.S'
2829
- 'proofs/hol_light/aarch64/**/*.ml'
30+
- 'proofs/hol_light/common/**/*.ml'
2931
- 'proofs/hol_light/x86_64/Makefile'
3032
- 'proofs/hol_light/x86_64/**/*.S'
3133
- 'proofs/hol_light/x86_64/**/*.ml'
@@ -83,6 +85,10 @@ jobs:
8385
needs: ["aarch64_utils.ml"]
8486
- name: mldsa_poly_chknorm
8587
needs: ["aarch64_utils.ml"]
88+
- name: mldsa_polyz_unpack_17
89+
needs: ["aarch64_utils.ml", "mldsa_polyz_unpack_consts.ml", "mldsa_specs.ml"]
90+
- name: mldsa_polyz_unpack_19
91+
needs: ["aarch64_utils.ml", "mldsa_polyz_unpack_consts.ml", "mldsa_specs.ml"]
8692
name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
8793
runs-on: pqcp-arm64
8894
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

‎nix/s2n_bignum/default.nix‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@
44
{ stdenv, fetchFromGitHub, writeText, ... }:
55
stdenv.mkDerivation rec {
66
pname = "s2n_bignum";
7-
version = "3bfe68deb9fbdaf23be0a927c362a87a799adc28";
7+
version = "1d6cb3dc9ac7648e99b9718b8c532be44f25970a";
88
src = fetchFromGitHub {
9-
owner = "awslabs";
9+
owner = "mkannwischer";
1010
repo = "s2n-bignum";
1111
rev = "${version}";
12-
hash = "sha256-C3SdYZ/PhfTmHefz3klO3l/lbEgtA8Hq9wjDmjd+Fek=";
12+
hash = "sha256-haOO4xW5ZHfJQo/HMrnmg6Qmf4FgzYOnEQgDjPhC27M=";
1313
};
1414
setupHook = writeText "setup-hook.sh" ''
1515
export S2N_BIGNUM_DIR="$1"

‎proofs/hol_light/aarch64/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,9 @@ endif
5454
SPLIT=tr ';' '\n'
5555

5656
OBJ = mldsa/mldsa_poly_caddq.o \
57-
mldsa/mldsa_poly_chknorm.o
57+
mldsa/mldsa_poly_chknorm.o \
58+
mldsa/mldsa_polyz_unpack_17.o \
59+
mldsa/mldsa_polyz_unpack_19.o
5860

5961
# According to
6062
# https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms,

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

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
/*
2+
* Copyright (c) The mldsa-native project authors
3+
* Copyright (c) The mlkem-native project authors
4+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
5+
*/
6+
7+
8+
/*
9+
* WARNING: This file is auto-derived from the mldsa-native source file
10+
* dev/aarch64_opt/src/polyz_unpack_17_asm.S using scripts/simpasm. Do not modify it directly.
11+
*/
12+
13+
#if defined(__ELF__)
14+
.section .note.GNU-stack,"",@progbits
15+
#endif
16+
17+
.text
18+
.balign 4
19+
#ifdef __APPLE__
20+
.global _PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_asm
21+
_PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_asm:
22+
#else
23+
.global PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_asm
24+
PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_asm:
25+
#endif
26+
27+
.cfi_startproc
28+
ldr q24, [x2]
29+
ldr q25, [x2, #0x10]
30+
ldr q26, [x2, #0x20]
31+
ldr q27, [x2, #0x30]
32+
mov x3, #0xfe00000000 // =1090921693184
33+
mov v28.d[0], x3
34+
mov x3, #0xfc // =252
35+
movk x3, #0xfa, lsl #32
36+
mov v28.d[1], x3
37+
movi v29.4s, #0x3, msl #16
38+
movi v30.4s, #0x2, lsl #16
39+
mov x9, #0x10 // =16
40+
41+
Lpolyz_unpack_17_loop:
42+
ld1 { v0.16b, v1.16b }, [x1]
43+
add x1, x1, #0x14
44+
ld1 { v2.16b }, [x1], #16
45+
tbl v4.16b, { v0.16b }, v24.16b
46+
tbl v5.16b, { v0.16b, v1.16b }, v25.16b
47+
tbl v6.16b, { v1.16b }, v26.16b
48+
tbl v7.16b, { v1.16b, v2.16b }, v27.16b
49+
ushl v4.4s, v4.4s, v28.4s
50+
and v4.16b, v4.16b, v29.16b
51+
sub v4.4s, v30.4s, v4.4s
52+
ushl v5.4s, v5.4s, v28.4s
53+
and v5.16b, v5.16b, v29.16b
54+
sub v5.4s, v30.4s, v5.4s
55+
ushl v6.4s, v6.4s, v28.4s
56+
and v6.16b, v6.16b, v29.16b
57+
sub v6.4s, v30.4s, v6.4s
58+
ushl v7.4s, v7.4s, v28.4s
59+
and v7.16b, v7.16b, v29.16b
60+
sub v7.4s, v30.4s, v7.4s
61+
str q5, [x0, #0x10]
62+
str q6, [x0, #0x20]
63+
str q7, [x0, #0x30]
64+
str q4, [x0], #0x40
65+
subs x9, x9, #0x1
66+
b.ne Lpolyz_unpack_17_loop
67+
ret
68+
.cfi_endproc

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

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
/*
2+
* Copyright (c) The mldsa-native project authors
3+
* Copyright (c) The mlkem-native project authors
4+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
5+
*/
6+
7+
8+
/*
9+
* WARNING: This file is auto-derived from the mldsa-native source file
10+
* dev/aarch64_opt/src/polyz_unpack_19_asm.S using scripts/simpasm. Do not modify it directly.
11+
*/
12+
13+
#if defined(__ELF__)
14+
.section .note.GNU-stack,"",@progbits
15+
#endif
16+
17+
.text
18+
.balign 4
19+
#ifdef __APPLE__
20+
.global _PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_19_asm
21+
_PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_19_asm:
22+
#else
23+
.global PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_19_asm
24+
PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_19_asm:
25+
#endif
26+
27+
.cfi_startproc
28+
ldr q24, [x2]
29+
ldr q25, [x2, #0x10]
30+
ldr q26, [x2, #0x20]
31+
ldr q27, [x2, #0x30]
32+
mov x3, #0xfc00000000 // =1082331758592
33+
dup v28.2d, x3
34+
movi v29.4s, #0xf, msl #16
35+
movi v30.4s, #0x8, lsl #16
36+
mov x9, #0x10 // =16
37+
38+
Lpolyz_unpack_19_loop:
39+
ld1 { v0.16b, v1.16b }, [x1]
40+
add x1, x1, #0x18
41+
ld1 { v2.16b }, [x1], #16
42+
tbl v4.16b, { v0.16b }, v24.16b
43+
tbl v5.16b, { v0.16b, v1.16b }, v25.16b
44+
tbl v6.16b, { v1.16b }, v26.16b
45+
tbl v7.16b, { v1.16b, v2.16b }, v27.16b
46+
ushl v4.4s, v4.4s, v28.4s
47+
and v4.16b, v4.16b, v29.16b
48+
sub v4.4s, v30.4s, v4.4s
49+
ushl v5.4s, v5.4s, v28.4s
50+
and v5.16b, v5.16b, v29.16b
51+
sub v5.4s, v30.4s, v5.4s
52+
ushl v6.4s, v6.4s, v28.4s
53+
and v6.16b, v6.16b, v29.16b
54+
sub v6.4s, v30.4s, v6.4s
55+
ushl v7.4s, v7.4s, v28.4s
56+
and v7.16b, v7.16b, v29.16b
57+
sub v7.4s, v30.4s, v7.4s
58+
str q5, [x0, #0x10]
59+
str q6, [x0, #0x20]
60+
str q7, [x0, #0x30]
61+
str q4, [x0], #0x40
62+
subs x9, x9, #0x1
63+
b.ne Lpolyz_unpack_19_loop
64+
ret
65+
.cfi_endproc

0 commit comments

Comments
 (0)