Skip to content

Commit f986df8

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 f986df8

17 files changed

Lines changed: 2114 additions & 7 deletions

File tree

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,10 @@ jobs:
9595
needs: ["aarch64_utils.ml"]
9696
- name: mldsa_poly_chknorm
9797
needs: ["aarch64_utils.ml"]
98+
- name: mldsa_rej_uniform_eta2
99+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_eta_table.ml", "subroutine_signatures.ml"]
100+
- name: mldsa_rej_uniform_eta4
101+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_eta_table.ml", "subroutine_signatures.ml"]
98102
- name: keccak_f1600_x1_scalar
99103
needs: ["keccak_spec.ml"]
100104
- name: keccak_f1600_x1_v84a

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 26 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -81,12 +81,36 @@ uint64_t mld_rej_uniform_asm(int32_t *r, const uint8_t *buf, unsigned buflen,
8181
#define mld_rej_uniform_eta2_asm MLD_NAMESPACE(rej_uniform_eta2_asm)
8282
MLD_MUST_CHECK_RETURN_VALUE
8383
uint64_t mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf,
84-
unsigned buflen, const uint8_t *table);
84+
unsigned buflen, const uint8_t *table)
85+
/* This must be kept in sync with the HOL-Light specification
86+
* in proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2.ml */
87+
__contract__(
88+
requires(buflen % 8 == 0)
89+
requires(buflen >= 8)
90+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
91+
requires(memory_no_alias(buf, buflen))
92+
requires(memory_no_alias(table, 4096)) /* check-magic: 4096 == 256 * 16 */
93+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
94+
ensures(return_value <= MLDSA_N)
95+
ensures(array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))
96+
);
8597

8698
#define mld_rej_uniform_eta4_asm MLD_NAMESPACE(rej_uniform_eta4_asm)
8799
MLD_MUST_CHECK_RETURN_VALUE
88100
uint64_t mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf,
89-
unsigned buflen, const uint8_t *table);
101+
unsigned buflen, const uint8_t *table)
102+
/* This must be kept in sync with the HOL-Light specification
103+
* in proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta4.ml */
104+
__contract__(
105+
requires(buflen % 8 == 0)
106+
requires(buflen >= 8)
107+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
108+
requires(memory_no_alias(buf, buflen))
109+
requires(memory_no_alias(table, 4096)) /* check-magic: 4096 == 256 * 16 */
110+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
111+
ensures(return_value <= MLDSA_N)
112+
ensures(array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))
113+
);
90114

91115
#define mld_poly_decompose_32_asm MLD_NAMESPACE(poly_decompose_32_asm)
92116
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0);

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

Lines changed: 26 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -81,12 +81,36 @@ uint64_t mld_rej_uniform_asm(int32_t *r, const uint8_t *buf, unsigned buflen,
8181
#define mld_rej_uniform_eta2_asm MLD_NAMESPACE(rej_uniform_eta2_asm)
8282
MLD_MUST_CHECK_RETURN_VALUE
8383
uint64_t mld_rej_uniform_eta2_asm(int32_t *r, const uint8_t *buf,
84-
unsigned buflen, const uint8_t *table);
84+
unsigned buflen, const uint8_t *table)
85+
/* This must be kept in sync with the HOL-Light specification
86+
* in proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2.ml */
87+
__contract__(
88+
requires(buflen % 8 == 0)
89+
requires(buflen >= 8)
90+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
91+
requires(memory_no_alias(buf, buflen))
92+
requires(memory_no_alias(table, 4096)) /* check-magic: 4096 == 256 * 16 */
93+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
94+
ensures(return_value <= MLDSA_N)
95+
ensures(array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))
96+
);
8597

8698
#define mld_rej_uniform_eta4_asm MLD_NAMESPACE(rej_uniform_eta4_asm)
8799
MLD_MUST_CHECK_RETURN_VALUE
88100
uint64_t mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf,
89-
unsigned buflen, const uint8_t *table);
101+
unsigned buflen, const uint8_t *table)
102+
/* This must be kept in sync with the HOL-Light specification
103+
* in proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta4.ml */
104+
__contract__(
105+
requires(buflen % 8 == 0)
106+
requires(buflen >= 8)
107+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
108+
requires(memory_no_alias(buf, buflen))
109+
requires(memory_no_alias(table, 4096)) /* check-magic: 4096 == 256 * 16 */
110+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
111+
ensures(return_value <= MLDSA_N)
112+
ensures(array_abs_bound(r, 0, return_value, MLDSA_ETA + 1))
113+
);
90114

91115
#define mld_poly_decompose_32_asm MLD_NAMESPACE(poly_decompose_32_asm)
92116
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0);

‎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 = "ca6ec31a225aaac11813d4055bbc55a0251b9452";
7+
version = "bc5165085c04c37baf02acff5919006bb97f74dc";
88
src = fetchFromGitHub {
9-
owner = "awslabs";
9+
owner = "jakemas";
1010
repo = "s2n-bignum";
1111
rev = "${version}";
12-
hash = "sha256-60gaEW0Afkn/Ukd4wZAab0Nz7XkbWvN4+Q+LgqUv0Ho=";
12+
hash = "sha256-pGi1lMPUo1nx35zF8JkRC6GcnpgtS80dd6MxYlvSKn4=";
1313
};
1414
setupHook = writeText "setup-hook.sh" ''
1515
export S2N_BIGNUM_DIR="$1"

‎proofs/cbmc/rej_uniform_eta2_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_eta2_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_eta2_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_eta2_native
25+
USE_FUNCTION_CONTRACTS = mld_rej_uniform_eta2_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_eta2_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_eta2_native_aarch64/rej_uniform_eta2_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_eta2_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_eta2_native(r, len, buf, buflen);
19+
}

‎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: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,8 @@ 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=2): [mldsa_rej_uniform_eta2.S](aarch64/mldsa/mldsa_rej_uniform_eta2.S)
62+
* AArch64 rejection sampling (eta=4): [mldsa_rej_uniform_eta4.S](aarch64/mldsa/mldsa_rej_uniform_eta4.S)
6163
* x86_64 forward NTT: [mldsa_ntt.S](x86_64/mldsa/mldsa_ntt.S)
6264
* x86_64 inverse NTT: [mldsa_intt.S](x86_64/mldsa/mldsa_intt.S)
6365
* x86_64 pointwise multiplication: [mldsa_pointwise.S](x86_64/mldsa/mldsa_pointwise.S)

‎proofs/hol_light/aarch64/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,8 @@ 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_eta2.o \
64+
mldsa/mldsa_rej_uniform_eta4.o \
6365
mldsa/keccak_f1600_x1_scalar.o \
6466
mldsa/keccak_f1600_x1_v84a.o \
6567
mldsa/keccak_f1600_x2_v84a.o \

0 commit comments

Comments
 (0)