Skip to content

Commit a3673e9

Browse files
jakemasclaude
jakemas
and
claude
committed
Add HOL Light rej_uniform_eta4 proof for AArch64
Add formal correctness proof for the AArch64 mld_rej_uniform_eta4_asm function, which performs rejection sampling with eta=4 for ML-DSA. The proof verifies that the assembly implementation correctly: - Extracts 4-bit nibbles from input bytes - Filters nibbles < 9 using SIMD comparison + TBL permutation - Maps accepted values n to (4 - n) as signed 32-bit integers - Returns at most 256 coefficients with the correct count Verified against the compiled object code (post-hoc, not trusting the assembler) using the s2n-bignum ARM verification framework in HOL Light. All 86 AArch64 instructions are mechanically verified across every execution path (360+ ARM simulation steps). No CHEAT_TAC remains. New files: - mldsa_rej_uniform_eta4.S: standalone assembly for proof bytecodes - mldsa_rej_uniform_eta4.ml: 547-line HOL Light correctness proof - mldsa_rej_uniform_eta_table.ml: 256-entry lookup table constants Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent 5d619ea commit a3673e9

9 files changed

Lines changed: 1184 additions & 0 deletions

File tree

‎proofs/cbmc/rej_uniform_eta4_native_aarch64/Makefile‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
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_eta4_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_eta4_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_kl.c
23+
24+
CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_eta4_native
25+
USE_FUNCTION_CONTRACTS = mld_rej_uniform_eta4_asm
26+
USE_FUNCTION_CONTRACTS += mld_sys_check_capability
27+
APPLY_LOOP_CONTRACTS=on
28+
USE_DYNAMIC_FRAMES=1
29+
30+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
31+
EXTERNAL_SAT_SOLVER=
32+
CBMCFLAGS=--bitwuzla
33+
34+
FUNCTION_NAME = rej_uniform_eta4_native_aarch64
35+
36+
# If this proof is found to consume huge amounts of RAM, you can set the
37+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
38+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
39+
# documentation in Makefile.common under the "Job Pools" heading for details.
40+
# EXPENSIVE = true
41+
42+
# This function is large enough to need...
43+
CBMC_OBJECT_BITS = 8
44+
45+
include ../Makefile.common

‎proofs/cbmc/rej_uniform_eta4_native_aarch64/rej_uniform_eta4_native_aarch64_harness.c‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
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+
int mld_rej_uniform_eta4_native(int32_t *r, unsigned len, const uint8_t *buf,
9+
unsigned buflen);
10+
11+
void harness(void)
12+
{
13+
int32_t *r;
14+
unsigned len;
15+
const uint8_t *buf;
16+
unsigned buflen;
17+
int t;
18+
t = mld_rej_uniform_eta4_native(r, len, buf, buflen);
19+
}

‎proofs/hol_light/README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
5858
* AArch64 pointwise multiplication-accumulation (l=4): [mldsa_pointwise_acc_l4.S](aarch64/mldsa/mldsa_pointwise_acc_l4.S)
5959
* AArch64 pointwise multiplication-accumulation (l=5): [mldsa_pointwise_acc_l5.S](aarch64/mldsa/mldsa_pointwise_acc_l5.S)
6060
* AArch64 pointwise multiplication-accumulation (l=7): [mldsa_pointwise_acc_l7.S](aarch64/mldsa/mldsa_pointwise_acc_l7.S)
61+
* AArch64 rejection sampling (eta=4): [mldsa_rej_uniform_eta4.S](aarch64/mldsa/mldsa_rej_uniform_eta4.S)
6162
* x86_64 forward NTT: [mldsa_ntt.S](x86_64/mldsa/mldsa_ntt.S)
6263
* x86_64 inverse NTT: [mldsa_intt.S](x86_64/mldsa/mldsa_intt.S)
6364
* x86_64 pointwise multiplication: [mldsa_pointwise.S](x86_64/mldsa/mldsa_pointwise.S)

‎proofs/hol_light/aarch64/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ OBJ = mldsa/mldsa_ntt.o \
6060
mldsa/mldsa_pointwise_acc_l4.o \
6161
mldsa/mldsa_pointwise_acc_l5.o \
6262
mldsa/mldsa_pointwise_acc_l7.o \
63+
mldsa/mldsa_rej_uniform_eta4.o \
6364
mldsa/keccak_f1600_x1_scalar.o \
6465
mldsa/keccak_f1600_x1_v84a.o \
6566
mldsa/keccak_f1600_x2_v84a.o \

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

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
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+
* mldsa/src/native/aarch64/src/rej_uniform_eta4_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_rej_uniform_eta4_asm
21+
_PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta4_asm:
22+
#else
23+
.global PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta4_asm
24+
PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta4_asm:
25+
#endif
26+
27+
.cfi_startproc
28+
sub sp, sp, #0x240
29+
.cfi_adjust_cfa_offset 0x240
30+
mov x7, #0x1 // =1
31+
movk x7, #0x2, lsl #16
32+
movk x7, #0x4, lsl #32
33+
movk x7, #0x8, lsl #48
34+
mov v31.d[0], x7
35+
mov x7, #0x10 // =16
36+
movk x7, #0x20, lsl #16
37+
movk x7, #0x40, lsl #32
38+
movk x7, #0x80, lsl #48
39+
mov v31.d[1], x7
40+
movi v30.8h, #0x9
41+
movi v7.8h, #0x4
42+
mov x8, sp
43+
mov x7, x8
44+
mov x11, #0x0 // =0
45+
eor v16.16b, v16.16b, v16.16b
46+
47+
Lrej_uniform_eta4_initial_zero:
48+
str q16, [x7], #0x40
49+
stur q16, [x7, #-0x30]
50+
stur q16, [x7, #-0x20]
51+
stur q16, [x7, #-0x10]
52+
add x11, x11, #0x20
53+
cmp x11, #0x100
54+
b.lt Lrej_uniform_eta4_initial_zero
55+
mov x7, x8
56+
mov x9, #0x0 // =0
57+
mov x4, #0x100 // =256
58+
59+
Lrej_uniform_eta4_loop8:
60+
cmp x9, x4
61+
b.hs Lrej_uniform_eta4_memory_copy
62+
sub x2, x2, #0x8
63+
ld1 { v0.8b }, [x1], #8
64+
movi v26.8b, #0xf
65+
and v27.8b, v0.8b, v26.8b
66+
ushr v28.8b, v0.8b, #0x4
67+
zip1 v26.8b, v27.8b, v28.8b
68+
zip2 v29.8b, v27.8b, v28.8b
69+
ushll v16.8h, v26.8b, #0x0
70+
ushll v17.8h, v29.8b, #0x0
71+
cmhi v4.8h, v30.8h, v16.8h
72+
cmhi v5.8h, v30.8h, v17.8h
73+
and v4.16b, v4.16b, v31.16b
74+
and v5.16b, v5.16b, v31.16b
75+
uaddlv s20, v4.8h
76+
uaddlv s21, v5.8h
77+
fmov w12, s20
78+
fmov w13, s21
79+
ldr q24, [x3, x12, lsl #4]
80+
ldr q25, [x3, x13, lsl #4]
81+
cnt v4.16b, v4.16b
82+
cnt v5.16b, v5.16b
83+
uaddlv s20, v4.8h
84+
uaddlv s21, v5.8h
85+
fmov w12, s20
86+
fmov w13, s21
87+
tbl v16.16b, { v16.16b }, v24.16b
88+
tbl v17.16b, { v17.16b }, v25.16b
89+
st1 { v16.8h }, [x7]
90+
add x7, x7, x12, lsl #1
91+
st1 { v17.8h }, [x7]
92+
add x7, x7, x13, lsl #1
93+
add x12, x12, x13
94+
add x9, x9, x12
95+
cmp x2, #0x8
96+
b.hs Lrej_uniform_eta4_loop8
97+
98+
Lrej_uniform_eta4_memory_copy:
99+
cmp x9, x4
100+
csel x9, x9, x4, lo
101+
mov x11, #0x0 // =0
102+
mov x7, x8
103+
104+
Lrej_uniform_eta4_final_copy:
105+
ldr q16, [x7], #0x20
106+
ldur q18, [x7, #-0x10]
107+
sub v16.8h, v7.8h, v16.8h
108+
sub v18.8h, v7.8h, v18.8h
109+
sshll2 v17.4s, v16.8h, #0x0
110+
sshll v16.4s, v16.4h, #0x0
111+
sshll2 v19.4s, v18.8h, #0x0
112+
sshll v18.4s, v18.4h, #0x0
113+
str q16, [x0], #0x40
114+
stur q17, [x0, #-0x30]
115+
stur q18, [x0, #-0x20]
116+
stur q19, [x0, #-0x10]
117+
add x11, x11, #0x10
118+
cmp x11, #0x100
119+
b.lt Lrej_uniform_eta4_final_copy
120+
mov x0, x9
121+
add sp, sp, #0x240
122+
.cfi_adjust_cfa_offset -0x240
123+
ret
124+
.cfi_endproc

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,3 +33,7 @@ print_string "==== bytecode end =====================================\n\n";;
3333
print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_chknorm.o ===\n";;
3434
print_literal_from_elf "aarch64/mldsa/mldsa_poly_chknorm.o";;
3535
print_string "==== bytecode end =====================================\n\n";;
36+
37+
print_string "=== bytecode start: aarch64/mldsa/mldsa_rej_uniform_eta4.o ===\n";;
38+
print_literal_from_elf "aarch64/mldsa/mldsa_rej_uniform_eta4.o";;
39+
print_string "==== bytecode end =====================================\n\n";;

0 commit comments

Comments
 (0)