Skip to content

Commit f7dccd0

Browse files
jakemasUbuntu
jakemas
authored and
Ubuntu
committed
Add HOL Light pointwise multiplication proofs for AArch64 and x86_64
Port the ML-DSA pointwise polynomial multiplication (Montgomery form) and its HOL Light proofs of correctness from s2n-bignum to mldsa-native, for both AArch64 (NEON) and x86_64 (AVX2). The proofs verify the assembly implementations at the object-code level, showing that output coefficients are congruent to the pointwise product of the inputs modulo Q=8380417, with bounded output coefficients (|output| <= Q-1). For AArch64, a constant-time and memory safety proof is also included. Ported from s2n-bignum commit ca6ec31a225a. Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent db65535 commit f7dccd0

File tree

25 files changed

+1570
-11
lines changed

25 files changed

+1570
-11
lines changed

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,8 @@ jobs:
8383
# Dependencies on {name}.{S,ml} are implicit
8484
- name: mldsa_ntt
8585
needs: ["mldsa_specs.ml", "mldsa_zetas.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
86+
- name: mldsa_pointwise
87+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
8688
- name: mldsa_poly_caddq
8789
needs: ["aarch64_utils.ml"]
8890
- name: mldsa_poly_chknorm
@@ -171,6 +173,8 @@ jobs:
171173
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
172174
- name: mldsa_intt
173175
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
176+
- name: mldsa_pointwise
177+
needs: ["mldsa_specs.ml", "mldsa_utils.ml"]
174178
name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
175179
runs-on: pqcp-x64
176180
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

‎BIBLIOGRAPHY.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -250,6 +250,7 @@ source code and documentation.
250250
- [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c)
251251
- [proofs/hol_light/x86_64/mldsa/mldsa_intt.S](proofs/hol_light/x86_64/mldsa/mldsa_intt.S)
252252
- [proofs/hol_light/x86_64/mldsa/mldsa_ntt.S](proofs/hol_light/x86_64/mldsa/mldsa_ntt.S)
253+
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S)
253254

254255
### `Round3_Spec`
255256

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -129,8 +129,23 @@ void mld_polyz_unpack_19_asm(int32_t *r, const uint8_t *buf,
129129

130130
#define mld_poly_pointwise_montgomery_asm \
131131
MLD_NAMESPACE(poly_pointwise_montgomery_asm)
132-
void mld_poly_pointwise_montgomery_asm(int32_t *, const int32_t *,
133-
const int32_t *);
132+
void mld_poly_pointwise_montgomery_asm(int32_t *r, const int32_t *a,
133+
const int32_t *b)
134+
/* This must be kept in sync with the HOL-Light specification
135+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise.ml */
136+
__contract__(
137+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
138+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
139+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
140+
/* check-magic: off */
141+
requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
142+
requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
143+
/* check-magic: on */
144+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
145+
/* check-magic: off */
146+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
147+
/* check-magic: on */
148+
);
134149

135150
#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
136151
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -129,8 +129,23 @@ void mld_polyz_unpack_19_asm(int32_t *r, const uint8_t *buf,
129129

130130
#define mld_poly_pointwise_montgomery_asm \
131131
MLD_NAMESPACE(poly_pointwise_montgomery_asm)
132-
void mld_poly_pointwise_montgomery_asm(int32_t *, const int32_t *,
133-
const int32_t *);
132+
void mld_poly_pointwise_montgomery_asm(int32_t *r, const int32_t *a,
133+
const int32_t *b)
134+
/* This must be kept in sync with the HOL-Light specification
135+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise.ml */
136+
__contract__(
137+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
138+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
139+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
140+
/* check-magic: off */
141+
requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
142+
requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
143+
/* check-magic: on */
144+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
145+
/* check-magic: off */
146+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
147+
/* check-magic: on */
148+
);
134149

135150
#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
136151
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,23 @@ void mld_polyz_unpack_19_avx2(int32_t *r, const uint8_t *a);
104104

105105
#define mld_pointwise_avx2 MLD_NAMESPACE(pointwise_avx2)
106106
void mld_pointwise_avx2(int32_t *c, const int32_t *a, const int32_t *b,
107-
const int32_t *qdata);
107+
const int32_t *qdata)
108+
/* This must be kept in sync with the HOL-Light specification
109+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise.ml */
110+
__contract__(
111+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
112+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
113+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
114+
/* check-magic: off */
115+
requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
116+
requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
117+
/* check-magic: on */
118+
requires(qdata == mld_qdata)
119+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
120+
/* check-magic: off */
121+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
122+
/* check-magic: on */
123+
);
108124

109125
#define mld_pointwise_acc_l4_avx2 MLD_NAMESPACE(pointwise_acc_l4_avx2)
110126
void mld_pointwise_acc_l4_avx2(int32_t c[MLDSA_N], const int32_t a[4][MLDSA_N],

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

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -129,8 +129,23 @@ void mld_polyz_unpack_19_asm(int32_t *r, const uint8_t *buf,
129129

130130
#define mld_poly_pointwise_montgomery_asm \
131131
MLD_NAMESPACE(poly_pointwise_montgomery_asm)
132-
void mld_poly_pointwise_montgomery_asm(int32_t *, const int32_t *,
133-
const int32_t *);
132+
void mld_poly_pointwise_montgomery_asm(int32_t *r, const int32_t *a,
133+
const int32_t *b)
134+
/* This must be kept in sync with the HOL-Light specification
135+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise.ml */
136+
__contract__(
137+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
138+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
139+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
140+
/* check-magic: off */
141+
requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
142+
requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
143+
/* check-magic: on */
144+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
145+
/* check-magic: off */
146+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
147+
/* check-magic: on */
148+
);
134149

135150
#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
136151
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)

‎mldsa/src/native/x86_64/src/arith_native_x86_64.h‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,23 @@ void mld_polyz_unpack_19_avx2(int32_t *r, const uint8_t *a);
104104

105105
#define mld_pointwise_avx2 MLD_NAMESPACE(pointwise_avx2)
106106
void mld_pointwise_avx2(int32_t *c, const int32_t *a, const int32_t *b,
107-
const int32_t *qdata);
107+
const int32_t *qdata)
108+
/* This must be kept in sync with the HOL-Light specification
109+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise.ml */
110+
__contract__(
111+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
112+
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
113+
requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
114+
/* check-magic: off */
115+
requires(array_abs_bound(a, 0, MLDSA_N, 75423753))
116+
requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
117+
/* check-magic: on */
118+
requires(qdata == mld_qdata)
119+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
120+
/* check-magic: off */
121+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
122+
/* check-magic: on */
123+
);
108124

109125
#define mld_pointwise_acc_l4_avx2 MLD_NAMESPACE(pointwise_acc_l4_avx2)
110126
void mld_pointwise_acc_l4_avx2(int32_t c[MLDSA_N], const int32_t a[4][MLDSA_N],

‎nix/s2n_bignum/default.nix‎

Lines changed: 2 additions & 2 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 = "ca6ec31a225aaac11813d4055bbc55a0251b9452";
88
src = fetchFromGitHub {
99
owner = "awslabs";
1010
repo = "s2n-bignum";
1111
rev = "${version}";
12-
hash = "sha256-C3SdYZ/PhfTmHefz3klO3l/lbEgtA8Hq9wjDmjd+Fek=";
12+
hash = "sha256-60gaEW0Afkn/Ukd4wZAab0Nz7XkbWvN4+Q+LgqUv0Ho=";
1313
};
1414
setupHook = writeText "setup-hook.sh" ''
1515
export S2N_BIGNUM_DIR="$1"

‎proofs/cbmc/pointwise_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 = pointwise_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 = pointwise_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
23+
24+
CHECK_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery_native
25+
USE_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery_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=--smt2
33+
34+
FUNCTION_NAME = pointwise_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/pointwise_native_aarch64/pointwise_native_aarch64_harness.c‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
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_poly_pointwise_montgomery_native(int32_t c[MLDSA_N],
10+
const int32_t a[MLDSA_N],
11+
const int32_t b[MLDSA_N]);
12+
13+
void harness(void)
14+
{
15+
int32_t *c, *a, *b;
16+
int t;
17+
t = mld_poly_pointwise_montgomery_native(c, a, b);
18+
}

0 commit comments

Comments
 (0)