Skip to content

Commit cbc80f6

Browse files
dkosticmkannwischer
dkostic
authored and
mkannwischer
committed
AArch64: Add rejection sampling HOL Light proofs and CBMC contract
- HOL Light correctness proof - HOL Light subroutine proof - HOL Light memory-safety proof - CBMC contract Signed-off-by: dkostic <dkostic@amazon.com>
1 parent 0591fe0 commit cbc80f6

14 files changed

Lines changed: 3479 additions & 4 deletions

File tree

‎.github/workflows/hol_light.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,8 @@ jobs:
121121
needs: ["aarch64_utils.ml", "mldsa_specs.ml", "subroutine_signatures.ml"]
122122
- name: poly_decompose_88_aarch64_asm
123123
needs: ["aarch64_utils.ml", "mldsa_specs.ml", "subroutine_signatures.ml"]
124+
- name: rej_uniform_aarch64_asm
125+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_table.ml"]
124126
name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
125127
runs-on: pqcp-arm64
126128
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,18 @@ __contract__(
9595
#define mld_rej_uniform_aarch64_asm MLD_NAMESPACE(rej_uniform_aarch64_asm)
9696
MLD_MUST_CHECK_RETURN_VALUE
9797
uint64_t mld_rej_uniform_aarch64_asm(int32_t *r, const uint8_t *buf,
98-
unsigned buflen, const uint8_t *table);
98+
unsigned buflen, const uint8_t *table)
99+
/* This must be kept in sync with the HOL-Light specification
100+
* in proofs/hol_light/aarch64/proofs/rej_uniform_aarch64_asm.ml. */
101+
__contract__(
102+
requires(buflen % 24 == 0)
103+
requires(memory_no_alias(buf, buflen))
104+
requires(table == mld_rej_uniform_table)
105+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
106+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
107+
ensures(return_value <= MLDSA_N)
108+
ensures(array_bound(r, 0, (unsigned) return_value, 0, MLDSA_Q))
109+
);
99110

100111
#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
101112
#define mld_rej_uniform_eta2_aarch64_asm \

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,18 @@ __contract__(
9595
#define mld_rej_uniform_aarch64_asm MLD_NAMESPACE(rej_uniform_aarch64_asm)
9696
MLD_MUST_CHECK_RETURN_VALUE
9797
uint64_t mld_rej_uniform_aarch64_asm(int32_t *r, const uint8_t *buf,
98-
unsigned buflen, const uint8_t *table);
98+
unsigned buflen, const uint8_t *table)
99+
/* This must be kept in sync with the HOL-Light specification
100+
* in proofs/hol_light/aarch64/proofs/rej_uniform_aarch64_asm.ml. */
101+
__contract__(
102+
requires(buflen % 24 == 0)
103+
requires(memory_no_alias(buf, buflen))
104+
requires(table == mld_rej_uniform_table)
105+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
106+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
107+
ensures(return_value <= MLDSA_N)
108+
ensures(array_bound(r, 0, (unsigned) return_value, 0, MLDSA_Q))
109+
);
99110

100111
#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
101112
#define mld_rej_uniform_eta2_aarch64_asm \

‎mldsa/src/native/aarch64/src/arith_native_aarch64.h‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,18 @@ __contract__(
9595
#define mld_rej_uniform_aarch64_asm MLD_NAMESPACE(rej_uniform_aarch64_asm)
9696
MLD_MUST_CHECK_RETURN_VALUE
9797
uint64_t mld_rej_uniform_aarch64_asm(int32_t *r, const uint8_t *buf,
98-
unsigned buflen, const uint8_t *table);
98+
unsigned buflen, const uint8_t *table)
99+
/* This must be kept in sync with the HOL-Light specification
100+
* in proofs/hol_light/aarch64/proofs/rej_uniform_aarch64_asm.ml. */
101+
__contract__(
102+
requires(buflen % 24 == 0)
103+
requires(memory_no_alias(buf, buflen))
104+
requires(table == mld_rej_uniform_table)
105+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
106+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
107+
ensures(return_value <= MLDSA_N)
108+
ensures(array_bound(r, 0, (unsigned) return_value, 0, MLDSA_Q))
109+
);
99110

100111
#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
101112
#define mld_rej_uniform_eta2_aarch64_asm \

‎proofs/cbmc/rej_uniform_native_aarch64/Makefile‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
include ../Makefile_params.common
5+
6+
HARNESS_ENTRY = harness
7+
HARNESS_FILE = rej_uniform_native_aarch64_harness
8+
9+
# This should be a unique identifier for this proof, and will appear on the
10+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11+
PROOF_UID = rej_uniform_native_aarch64
12+
13+
# We need to set MLD_CHECK_APIS as otherwise mldsa/src/native/api.h won't be
14+
# included, which contains the CBMC specifications.
15+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/aarch64/meta.h\"" -DMLD_CHECK_APIS
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c $(SRCDIR)/mldsa/src/native/aarch64/src/rej_uniform_table.c
23+
24+
CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_native
25+
USE_FUNCTION_CONTRACTS=mld_rej_uniform_aarch64_asm
26+
APPLY_LOOP_CONTRACTS=on
27+
USE_DYNAMIC_FRAMES=1
28+
29+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
30+
EXTERNAL_SAT_SOLVER=
31+
CBMCFLAGS=--smt2
32+
33+
FUNCTION_NAME = rej_uniform_native_aarch64
34+
35+
# If this proof is found to consume huge amounts of RAM, you can set the
36+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
37+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
38+
# documentation in Makefile.common under the "Job Pools" heading for details.
39+
# EXPENSIVE = true
40+
41+
# This function is large enough to need...
42+
CBMC_OBJECT_BITS = 8
43+
44+
# If you require access to a file-local ("static") function or object to conduct
45+
# your proof, set the following (and do not include the original source file
46+
# ("mldsa/src/poly.c") in PROJECT_SOURCES).
47+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
48+
# include ../Makefile.common
49+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c
50+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
51+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
52+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
53+
# be set before including Makefile.common, but any use of variables on the
54+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
55+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
56+
57+
include ../Makefile.common

‎proofs/cbmc/rej_uniform_native_aarch64/rej_uniform_native_aarch64_harness.c‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include <stdint.h>
5+
#include "cbmc.h"
6+
#include "params.h"
7+
8+
9+
int mld_rej_uniform_native(int32_t *r, unsigned len, const uint8_t *buf,
10+
unsigned buflen);
11+
12+
void harness(void)
13+
{
14+
int32_t *r;
15+
unsigned len;
16+
const uint8_t *buf;
17+
unsigned buflen;
18+
19+
mld_rej_uniform_native(r, len, buf, buflen);
20+
}

‎proofs/hol_light/README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -125,6 +125,7 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
125125
* AArch64 pointwise multiplication-accumulation (l=4): [mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.S](aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.S)
126126
* AArch64 pointwise multiplication-accumulation (l=5): [mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S](aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S)
127127
* AArch64 pointwise multiplication-accumulation (l=7): [mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S](aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S)
128+
* AArch64 rejection sampling: [rej_uniform_aarch64_asm.S](aarch64/mldsa/rej_uniform_aarch64_asm.S)
128129
- FIPS202:
129130
* Keccak-F1600 using lazy rotations[^HYBRID]: [keccak_f1600_x1_scalar_aarch64_asm.S](aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S)
130131
* Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x1_v84a_aarch64_asm.S](aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.S)

‎proofs/hol_light/aarch64/Makefile‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,8 @@ OBJ = mldsa/intt_aarch64_asm.o \
7171
mldsa/polyz_unpack_17_aarch64_asm.o \
7272
mldsa/polyz_unpack_19_aarch64_asm.o \
7373
mldsa/poly_use_hint_32_aarch64_asm.o \
74-
mldsa/poly_use_hint_88_aarch64_asm.o
74+
mldsa/poly_use_hint_88_aarch64_asm.o \
75+
mldsa/rej_uniform_aarch64_asm.o
7576

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

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

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
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/rej_uniform_aarch64_asm.S using scripts/simpasm. Do not modify it directly.
11+
*/
12+
13+
.text
14+
.balign 4
15+
#ifdef __APPLE__
16+
.global _PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_aarch64_asm
17+
_PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_aarch64_asm:
18+
#else
19+
.global PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_aarch64_asm
20+
PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_aarch64_asm:
21+
#endif
22+
23+
.cfi_startproc
24+
sub sp, sp, #0x440
25+
.cfi_adjust_cfa_offset 0x440
26+
mov x7, #0x1 // =1
27+
movk x7, #0x2, lsl #32
28+
mov v31.d[0], x7
29+
mov x7, #0x4 // =4
30+
movk x7, #0x8, lsl #32
31+
mov v31.d[1], x7
32+
mov w7, #0xe001 // =57345
33+
movk w7, #0x7f, lsl #16
34+
dup v30.4s, w7
35+
mov x8, sp
36+
mov x7, x8
37+
mov x11, #0x0 // =0
38+
eor v16.16b, v16.16b, v16.16b
39+
40+
Lrej_uniform_initial_zero:
41+
str q16, [x7], #0x40
42+
stur q16, [x7, #-0x30]
43+
stur q16, [x7, #-0x20]
44+
stur q16, [x7, #-0x10]
45+
add x11, x11, #0x10
46+
cmp x11, #0x100
47+
b.lt Lrej_uniform_initial_zero
48+
mov x7, x8
49+
mov x9, #0x0 // =0
50+
mov x4, #0x100 // =256
51+
cmp x2, #0x30
52+
b.lo Lrej_uniform_loop48_end
53+
54+
Lrej_uniform_loop48:
55+
cmp x9, x4
56+
b.hs Lrej_uniform_memory_copy
57+
sub x2, x2, #0x30
58+
ld3 { v0.16b, v1.16b, v2.16b }, [x1], #48
59+
movi v4.16b, #0x80
60+
bic v2.16b, v2.16b, v4.16b
61+
zip1 v4.16b, v0.16b, v1.16b
62+
zip2 v5.16b, v0.16b, v1.16b
63+
ushll v6.8h, v2.8b, #0x0
64+
ushll2 v7.8h, v2.16b, #0x0
65+
zip1 v16.8h, v4.8h, v6.8h
66+
zip2 v17.8h, v4.8h, v6.8h
67+
zip1 v18.8h, v5.8h, v7.8h
68+
zip2 v19.8h, v5.8h, v7.8h
69+
cmhi v4.4s, v30.4s, v16.4s
70+
cmhi v5.4s, v30.4s, v17.4s
71+
cmhi v6.4s, v30.4s, v18.4s
72+
cmhi v7.4s, v30.4s, v19.4s
73+
and v4.16b, v4.16b, v31.16b
74+
and v5.16b, v5.16b, v31.16b
75+
and v6.16b, v6.16b, v31.16b
76+
and v7.16b, v7.16b, v31.16b
77+
uaddlv d20, v4.4s
78+
uaddlv d21, v5.4s
79+
uaddlv d22, v6.4s
80+
uaddlv d23, v7.4s
81+
fmov x12, d20
82+
fmov x13, d21
83+
fmov x14, d22
84+
fmov x15, d23
85+
ldr q24, [x3, x12, lsl #4]
86+
ldr q25, [x3, x13, lsl #4]
87+
ldr q26, [x3, x14, lsl #4]
88+
ldr q27, [x3, x15, lsl #4]
89+
cnt v4.16b, v4.16b
90+
cnt v5.16b, v5.16b
91+
cnt v6.16b, v6.16b
92+
cnt v7.16b, v7.16b
93+
uaddlv d20, v4.4s
94+
uaddlv d21, v5.4s
95+
uaddlv d22, v6.4s
96+
uaddlv d23, v7.4s
97+
fmov x12, d20
98+
fmov x13, d21
99+
fmov x14, d22
100+
fmov x15, d23
101+
tbl v16.16b, { v16.16b }, v24.16b
102+
tbl v17.16b, { v17.16b }, v25.16b
103+
tbl v18.16b, { v18.16b }, v26.16b
104+
tbl v19.16b, { v19.16b }, v27.16b
105+
st1 { v16.4s }, [x7]
106+
add x7, x7, x12, lsl #2
107+
st1 { v17.4s }, [x7]
108+
add x7, x7, x13, lsl #2
109+
st1 { v18.4s }, [x7]
110+
add x7, x7, x14, lsl #2
111+
st1 { v19.4s }, [x7]
112+
add x7, x7, x15, lsl #2
113+
add x12, x12, x13
114+
add x14, x14, x15
115+
add x9, x9, x12
116+
add x9, x9, x14
117+
cmp x2, #0x30
118+
b.hs Lrej_uniform_loop48
119+
120+
Lrej_uniform_loop48_end:
121+
cmp x9, x4
122+
b.hs Lrej_uniform_memory_copy
123+
cmp x2, #0x18
124+
b.lo Lrej_uniform_memory_copy
125+
sub x2, x2, #0x18
126+
ld3 { v0.8b, v1.8b, v2.8b }, [x1], #24
127+
movi v4.16b, #0x80
128+
bic v2.16b, v2.16b, v4.16b
129+
zip1 v4.16b, v0.16b, v1.16b
130+
ushll v6.8h, v2.8b, #0x0
131+
zip1 v16.8h, v4.8h, v6.8h
132+
zip2 v17.8h, v4.8h, v6.8h
133+
cmhi v4.4s, v30.4s, v16.4s
134+
cmhi v5.4s, v30.4s, v17.4s
135+
and v4.16b, v4.16b, v31.16b
136+
and v5.16b, v5.16b, v31.16b
137+
uaddlv d20, v4.4s
138+
uaddlv d21, v5.4s
139+
fmov x12, d20
140+
fmov x13, d21
141+
ldr q24, [x3, x12, lsl #4]
142+
ldr q25, [x3, x13, lsl #4]
143+
cnt v4.16b, v4.16b
144+
cnt v5.16b, v5.16b
145+
uaddlv d20, v4.4s
146+
uaddlv d21, v5.4s
147+
fmov x12, d20
148+
fmov x13, d21
149+
tbl v16.16b, { v16.16b }, v24.16b
150+
tbl v17.16b, { v17.16b }, v25.16b
151+
st1 { v16.4s }, [x7]
152+
add x7, x7, x12, lsl #2
153+
st1 { v17.4s }, [x7]
154+
add x7, x7, x13, lsl #2
155+
add x9, x9, x12
156+
add x9, x9, x13
157+
158+
Lrej_uniform_memory_copy:
159+
cmp x9, x4
160+
csel x9, x9, x4, lo
161+
mov x11, #0x0 // =0
162+
mov x7, x8
163+
164+
Lrej_uniform_final_copy:
165+
ldr q16, [x7], #0x40
166+
ldur q17, [x7, #-0x30]
167+
ldur q18, [x7, #-0x20]
168+
ldur q19, [x7, #-0x10]
169+
str q16, [x0], #0x40
170+
stur q17, [x0, #-0x30]
171+
stur q18, [x0, #-0x20]
172+
stur q19, [x0, #-0x10]
173+
add x11, x11, #0x10
174+
cmp x11, #0x100
175+
b.lt Lrej_uniform_final_copy
176+
mov x0, x9
177+
b Lrej_uniform_return
178+
179+
Lrej_uniform_return:
180+
add sp, sp, #0x440
181+
.cfi_adjust_cfa_offset -0x440
182+
ret
183+
.cfi_endproc
184+
185+
#if defined(__ELF__)
186+
.section .note.GNU-stack,"",%progbits
187+
#endif

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,3 +61,7 @@ print_string "==== bytecode end =====================================\n\n";;
6161
print_string "=== bytecode start: aarch64/mldsa/polyz_unpack_19_aarch64_asm.o ===\n";;
6262
print_literal_from_elf "aarch64/mldsa/polyz_unpack_19_aarch64_asm.o";;
6363
print_string "==== bytecode end =====================================\n\n";;
64+
65+
print_string "=== bytecode start: aarch64/mldsa/rej_uniform_aarch64_asm.o ===\n";;
66+
print_literal_from_elf "aarch64/mldsa/rej_uniform_aarch64_asm.o";;
67+
print_string "==== bytecode end =====================================\n\n";;

0 commit comments

Comments
 (0)