Skip to content

Commit 6fca70f

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 db65535 commit 6fca70f

12 files changed

Lines changed: 1369 additions & 5 deletions

File tree

‎.github/workflows/hol_light.yml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ on:
1313
- 'proofs/hol_light/aarch64/Makefile'
1414
- 'proofs/hol_light/aarch64/**/*.S'
1515
- 'proofs/hol_light/aarch64/**/*.ml'
16+
- 'proofs/hol_light/common/**/*.ml'
1617
- 'proofs/hol_light/x86_64/Makefile'
1718
- 'proofs/hol_light/x86_64/**/*.S'
1819
- 'proofs/hol_light/x86_64/**/*.ml'
@@ -28,6 +29,7 @@ on:
2829
- 'proofs/hol_light/aarch64/Makefile'
2930
- 'proofs/hol_light/aarch64/**/*.S'
3031
- 'proofs/hol_light/aarch64/**/*.ml'
32+
- 'proofs/hol_light/common/**/*.ml'
3133
- 'proofs/hol_light/x86_64/Makefile'
3234
- 'proofs/hol_light/x86_64/**/*.S'
3335
- 'proofs/hol_light/x86_64/**/*.ml'
@@ -87,6 +89,10 @@ jobs:
8789
needs: ["aarch64_utils.ml"]
8890
- name: mldsa_poly_chknorm
8991
needs: ["aarch64_utils.ml"]
92+
- name: mldsa_polyz_unpack_17
93+
needs: ["aarch64_utils.ml", "mldsa_polyz_unpack_consts.ml", "mldsa_specs.ml"]
94+
- name: mldsa_polyz_unpack_19
95+
needs: ["aarch64_utils.ml", "mldsa_polyz_unpack_consts.ml", "mldsa_specs.ml"]
9096
name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
9197
runs-on: pqcp-arm64
9298
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 = "553d5d39a1dd364235d1e3798d02f99c44be6008";
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-ktBmHimwc3qe/cvjDeDR+wTh8vMcv4bXv+BYETCc/wc=";
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
@@ -55,7 +55,9 @@ SPLIT=tr ';' '\n'
5555

5656
OBJ = mldsa/mldsa_ntt.o \
5757
mldsa/mldsa_poly_caddq.o \
58-
mldsa/mldsa_poly_chknorm.o
58+
mldsa/mldsa_poly_chknorm.o \
59+
mldsa/mldsa_polyz_unpack_17.o \
60+
mldsa/mldsa_polyz_unpack_19.o
5961

6062
# According to
6163
# 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)