Skip to content

Commit b9b5908

Browse files
jakemasjakemas
committed
Add HOL Light pointwise_acc proofs for AArch64 and x86_64
Port the ML-DSA pointwise multiplication-accumulation (l=4,5,7) and their HOL Light proofs of correctness from s2n-bignum to mldsa-native, for both AArch64 (NEON) and x86_64 (AVX2). Includes constant-time and memory safety proofs for both architectures. Ported from s2n-bignum PR #373. Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent f7dccd0 commit b9b5908

28 files changed

+4355
-26
lines changed

‎.github/workflows/hol_light.yml‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,12 @@ jobs:
8585
needs: ["mldsa_specs.ml", "mldsa_zetas.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
8686
- name: mldsa_pointwise
8787
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
88+
- name: mldsa_pointwise_acc_l4
89+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
90+
- name: mldsa_pointwise_acc_l5
91+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
92+
- name: mldsa_pointwise_acc_l7
93+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
8894
- name: mldsa_poly_caddq
8995
needs: ["aarch64_utils.ml"]
9096
- name: mldsa_poly_chknorm
@@ -175,6 +181,12 @@ jobs:
175181
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
176182
- name: mldsa_pointwise
177183
needs: ["mldsa_specs.ml", "mldsa_utils.ml"]
184+
- name: mldsa_pointwise_acc_l4
185+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
186+
- name: mldsa_pointwise_acc_l5
187+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
188+
- name: mldsa_pointwise_acc_l7
189+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
178190
name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
179191
runs-on: pqcp-x64
180192
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

‎BIBLIOGRAPHY.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -251,6 +251,9 @@ source code and documentation.
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)
253253
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S)
254+
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S)
255+
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S)
256+
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l7.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l7.S)
254257

255258
### `Round3_Spec`
256259

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 51 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -149,17 +149,62 @@ __contract__(
149149

150150
#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
151151
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)
152-
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *, const int32_t *,
153-
const int32_t *);
152+
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *r, const int32_t *a,
153+
const int32_t *b)
154+
/* This must be kept in sync with the HOL-Light specification
155+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
156+
__contract__(
157+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
158+
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
159+
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
160+
/* check-magic: off */
161+
requires(array_abs_bound(a, 0, 4 * MLDSA_N, 75423753))
162+
requires(array_abs_bound(b, 0, 4 * MLDSA_N, 75423753))
163+
/* check-magic: on */
164+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
165+
/* check-magic: off */
166+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
167+
/* check-magic: on */
168+
);
154169

155170
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
156171
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
157-
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
158-
const int32_t *);
172+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r, const int32_t *a,
173+
const int32_t *b)
174+
/* This must be kept in sync with the HOL-Light specification
175+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
176+
__contract__(
177+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
178+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
179+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
180+
/* check-magic: off */
181+
requires(array_abs_bound(a, 0, 5 * MLDSA_N, 75423753))
182+
requires(array_abs_bound(b, 0, 5 * MLDSA_N, 75423753))
183+
/* check-magic: on */
184+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
185+
/* check-magic: off */
186+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
187+
/* check-magic: on */
188+
);
159189

160190
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
161191
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
162-
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
163-
const int32_t *);
192+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r, const int32_t *a,
193+
const int32_t *b)
194+
/* This must be kept in sync with the HOL-Light specification
195+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
196+
__contract__(
197+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
198+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
199+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
200+
/* check-magic: off */
201+
requires(array_abs_bound(a, 0, 7 * MLDSA_N, 75423753))
202+
requires(array_abs_bound(b, 0, 7 * MLDSA_N, 75423753))
203+
/* check-magic: on */
204+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
205+
/* check-magic: off */
206+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
207+
/* check-magic: on */
208+
);
164209

165210
#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 51 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -149,17 +149,62 @@ __contract__(
149149

150150
#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
151151
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)
152-
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *, const int32_t *,
153-
const int32_t *);
152+
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *r, const int32_t *a,
153+
const int32_t *b)
154+
/* This must be kept in sync with the HOL-Light specification
155+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
156+
__contract__(
157+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
158+
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
159+
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
160+
/* check-magic: off */
161+
requires(array_abs_bound(a, 0, 4 * MLDSA_N, 75423753))
162+
requires(array_abs_bound(b, 0, 4 * MLDSA_N, 75423753))
163+
/* check-magic: on */
164+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
165+
/* check-magic: off */
166+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
167+
/* check-magic: on */
168+
);
154169

155170
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
156171
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
157-
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
158-
const int32_t *);
172+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r, const int32_t *a,
173+
const int32_t *b)
174+
/* This must be kept in sync with the HOL-Light specification
175+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
176+
__contract__(
177+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
178+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
179+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
180+
/* check-magic: off */
181+
requires(array_abs_bound(a, 0, 5 * MLDSA_N, 75423753))
182+
requires(array_abs_bound(b, 0, 5 * MLDSA_N, 75423753))
183+
/* check-magic: on */
184+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
185+
/* check-magic: off */
186+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
187+
/* check-magic: on */
188+
);
159189

160190
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
161191
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
162-
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
163-
const int32_t *);
192+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r, const int32_t *a,
193+
const int32_t *b)
194+
/* This must be kept in sync with the HOL-Light specification
195+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
196+
__contract__(
197+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
198+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
199+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
200+
/* check-magic: off */
201+
requires(array_abs_bound(a, 0, 7 * MLDSA_N, 75423753))
202+
requires(array_abs_bound(b, 0, 7 * MLDSA_N, 75423753))
203+
/* check-magic: on */
204+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
205+
/* check-magic: off */
206+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
207+
/* check-magic: on */
208+
);
164209

165210
#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 51 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -125,16 +125,64 @@ __contract__(
125125
#define mld_pointwise_acc_l4_avx2 MLD_NAMESPACE(pointwise_acc_l4_avx2)
126126
void mld_pointwise_acc_l4_avx2(int32_t c[MLDSA_N], const int32_t a[4][MLDSA_N],
127127
const int32_t b[4][MLDSA_N],
128-
const int32_t *qdata);
128+
const int32_t *qdata)
129+
/* This must be kept in sync with the HOL-Light specification
130+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4.ml */
131+
__contract__(
132+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
133+
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
134+
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
135+
/* check-magic: off */
136+
requires(array_abs_bound(a, 0, 4 * MLDSA_N, 75423753))
137+
requires(array_abs_bound(b, 0, 4 * MLDSA_N, 75423753))
138+
/* check-magic: on */
139+
requires(qdata == mld_qdata)
140+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
141+
/* check-magic: off */
142+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
143+
/* check-magic: on */
144+
);
129145

130146
#define mld_pointwise_acc_l5_avx2 MLD_NAMESPACE(pointwise_acc_l5_avx2)
131147
void mld_pointwise_acc_l5_avx2(int32_t c[MLDSA_N], const int32_t a[5][MLDSA_N],
132148
const int32_t b[5][MLDSA_N],
133-
const int32_t *qdata);
149+
const int32_t *qdata)
150+
/* This must be kept in sync with the HOL-Light specification
151+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5.ml */
152+
__contract__(
153+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
154+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
155+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
156+
/* check-magic: off */
157+
requires(array_abs_bound(a, 0, 5 * MLDSA_N, 75423753))
158+
requires(array_abs_bound(b, 0, 5 * MLDSA_N, 75423753))
159+
/* check-magic: on */
160+
requires(qdata == mld_qdata)
161+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
162+
/* check-magic: off */
163+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
164+
/* check-magic: on */
165+
);
134166

135167
#define mld_pointwise_acc_l7_avx2 MLD_NAMESPACE(pointwise_acc_l7_avx2)
136168
void mld_pointwise_acc_l7_avx2(int32_t c[MLDSA_N], const int32_t a[7][MLDSA_N],
137169
const int32_t b[7][MLDSA_N],
138-
const int32_t *qdata);
170+
const int32_t *qdata)
171+
/* This must be kept in sync with the HOL-Light specification
172+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7.ml */
173+
__contract__(
174+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
175+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
176+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
177+
/* check-magic: off */
178+
requires(array_abs_bound(a, 0, 7 * MLDSA_N, 75423753))
179+
requires(array_abs_bound(b, 0, 7 * MLDSA_N, 75423753))
180+
/* check-magic: on */
181+
requires(qdata == mld_qdata)
182+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
183+
/* check-magic: off */
184+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
185+
/* check-magic: on */
186+
);
139187

140188
#endif /* !MLD_NATIVE_X86_64_SRC_ARITH_NATIVE_X86_64_H */

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

Lines changed: 51 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -149,17 +149,62 @@ __contract__(
149149

150150
#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
151151
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)
152-
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *, const int32_t *,
153-
const int32_t *);
152+
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *r, const int32_t *a,
153+
const int32_t *b)
154+
/* This must be kept in sync with the HOL-Light specification
155+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
156+
__contract__(
157+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
158+
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
159+
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
160+
/* check-magic: off */
161+
requires(array_abs_bound(a, 0, 4 * MLDSA_N, 75423753))
162+
requires(array_abs_bound(b, 0, 4 * MLDSA_N, 75423753))
163+
/* check-magic: on */
164+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
165+
/* check-magic: off */
166+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
167+
/* check-magic: on */
168+
);
154169

155170
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
156171
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
157-
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
158-
const int32_t *);
172+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r, const int32_t *a,
173+
const int32_t *b)
174+
/* This must be kept in sync with the HOL-Light specification
175+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
176+
__contract__(
177+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
178+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
179+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
180+
/* check-magic: off */
181+
requires(array_abs_bound(a, 0, 5 * MLDSA_N, 75423753))
182+
requires(array_abs_bound(b, 0, 5 * MLDSA_N, 75423753))
183+
/* check-magic: on */
184+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
185+
/* check-magic: off */
186+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
187+
/* check-magic: on */
188+
);
159189

160190
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
161191
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
162-
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
163-
const int32_t *);
192+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r, const int32_t *a,
193+
const int32_t *b)
194+
/* This must be kept in sync with the HOL-Light specification
195+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
196+
__contract__(
197+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
198+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
199+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
200+
/* check-magic: off */
201+
requires(array_abs_bound(a, 0, 7 * MLDSA_N, 75423753))
202+
requires(array_abs_bound(b, 0, 7 * MLDSA_N, 75423753))
203+
/* check-magic: on */
204+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
205+
/* check-magic: off */
206+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
207+
/* check-magic: on */
208+
);
164209

165210
#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */

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

Lines changed: 51 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -125,16 +125,64 @@ __contract__(
125125
#define mld_pointwise_acc_l4_avx2 MLD_NAMESPACE(pointwise_acc_l4_avx2)
126126
void mld_pointwise_acc_l4_avx2(int32_t c[MLDSA_N], const int32_t a[4][MLDSA_N],
127127
const int32_t b[4][MLDSA_N],
128-
const int32_t *qdata);
128+
const int32_t *qdata)
129+
/* This must be kept in sync with the HOL-Light specification
130+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4.ml */
131+
__contract__(
132+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
133+
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
134+
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
135+
/* check-magic: off */
136+
requires(array_abs_bound(a, 0, 4 * MLDSA_N, 75423753))
137+
requires(array_abs_bound(b, 0, 4 * MLDSA_N, 75423753))
138+
/* check-magic: on */
139+
requires(qdata == mld_qdata)
140+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
141+
/* check-magic: off */
142+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
143+
/* check-magic: on */
144+
);
129145

130146
#define mld_pointwise_acc_l5_avx2 MLD_NAMESPACE(pointwise_acc_l5_avx2)
131147
void mld_pointwise_acc_l5_avx2(int32_t c[MLDSA_N], const int32_t a[5][MLDSA_N],
132148
const int32_t b[5][MLDSA_N],
133-
const int32_t *qdata);
149+
const int32_t *qdata)
150+
/* This must be kept in sync with the HOL-Light specification
151+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5.ml */
152+
__contract__(
153+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
154+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
155+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
156+
/* check-magic: off */
157+
requires(array_abs_bound(a, 0, 5 * MLDSA_N, 75423753))
158+
requires(array_abs_bound(b, 0, 5 * MLDSA_N, 75423753))
159+
/* check-magic: on */
160+
requires(qdata == mld_qdata)
161+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
162+
/* check-magic: off */
163+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
164+
/* check-magic: on */
165+
);
134166

135167
#define mld_pointwise_acc_l7_avx2 MLD_NAMESPACE(pointwise_acc_l7_avx2)
136168
void mld_pointwise_acc_l7_avx2(int32_t c[MLDSA_N], const int32_t a[7][MLDSA_N],
137169
const int32_t b[7][MLDSA_N],
138-
const int32_t *qdata);
170+
const int32_t *qdata)
171+
/* This must be kept in sync with the HOL-Light specification
172+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7.ml */
173+
__contract__(
174+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
175+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
176+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
177+
/* check-magic: off */
178+
requires(array_abs_bound(a, 0, 7 * MLDSA_N, 75423753))
179+
requires(array_abs_bound(b, 0, 7 * MLDSA_N, 75423753))
180+
/* check-magic: on */
181+
requires(qdata == mld_qdata)
182+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
183+
/* check-magic: off */
184+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
185+
/* check-magic: on */
186+
);
139187

140188
#endif /* !MLD_NATIVE_X86_64_SRC_ARITH_NATIVE_X86_64_H */

‎proofs/hol_light/README.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,12 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
5454
- AArch64 poly_caddq: [mldsa_poly_caddq.S](aarch64/mldsa/mldsa_poly_caddq.S)
5555
- AArch64 poly_chknorm: [mldsa_poly_chknorm.S](aarch64/mldsa/mldsa_poly_chknorm.S)
5656
- AArch64 pointwise multiplication: [mldsa_pointwise.S](aarch64/mldsa/mldsa_pointwise.S)
57+
- AArch64 pointwise multiplication-accumulation (l=4): [mldsa_pointwise_acc_l4.S](aarch64/mldsa/mldsa_pointwise_acc_l4.S)
58+
- AArch64 pointwise multiplication-accumulation (l=5): [mldsa_pointwise_acc_l5.S](aarch64/mldsa/mldsa_pointwise_acc_l5.S)
59+
- AArch64 pointwise multiplication-accumulation (l=7): [mldsa_pointwise_acc_l7.S](aarch64/mldsa/mldsa_pointwise_acc_l7.S)
5760
- x86_64 forward NTT: [mldsa_ntt.S](x86_64/mldsa/mldsa_ntt.S)
5861
- x86_64 inverse NTT: [mldsa_intt.S](x86_64/mldsa/mldsa_intt.S)
5962
- x86_64 pointwise multiplication: [mldsa_pointwise.S](x86_64/mldsa/mldsa_pointwise.S)
63+
- x86_64 pointwise multiplication-accumulation (l=4): [mldsa_pointwise_acc_l4.S](x86_64/mldsa/mldsa_pointwise_acc_l4.S)
64+
- x86_64 pointwise multiplication-accumulation (l=5): [mldsa_pointwise_acc_l5.S](x86_64/mldsa/mldsa_pointwise_acc_l5.S)
65+
- x86_64 pointwise multiplication-accumulation (l=7): [mldsa_pointwise_acc_l7.S](x86_64/mldsa/mldsa_pointwise_acc_l7.S)

0 commit comments

Comments
 (0)