Skip to content

Commit 8afaabe

Browse files
jakemasUbuntu
jakemas
authored and
Ubuntu
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> Signed-off-by: Ubuntu <ubuntu@ip-172-31-29-57.us-west-2.compute.internal>
1 parent 6010ea2 commit 8afaabe

33 files changed

+4552
-29
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
@@ -185,6 +191,12 @@ jobs:
185191
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
186192
- name: mldsa_pointwise
187193
needs: ["mldsa_specs.ml", "mldsa_utils.ml"]
194+
- name: mldsa_pointwise_acc_l4
195+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
196+
- name: mldsa_pointwise_acc_l5
197+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
198+
- name: mldsa_pointwise_acc_l7
199+
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
188200
name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
189201
runs-on: pqcp-x64
190202
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
@@ -254,6 +254,9 @@ source code and documentation.
254254
- [proofs/hol_light/x86_64/mldsa/mldsa_intt.S](proofs/hol_light/x86_64/mldsa/mldsa_intt.S)
255255
- [proofs/hol_light/x86_64/mldsa/mldsa_ntt.S](proofs/hol_light/x86_64/mldsa/mldsa_ntt.S)
256256
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S)
257+
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S)
258+
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S)
259+
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l7.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l7.S)
257260

258261
### `Round3_Spec`
259262

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 45 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -147,17 +147,56 @@ __contract__(
147147

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

153166
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
154167
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
155-
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
156-
const int32_t *);
168+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r, const int32_t *a,
169+
const int32_t *b)
170+
/* This must be kept in sync with the HOL-Light specification
171+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
172+
__contract__(
173+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
174+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
175+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
176+
/* check-magic: off */
177+
requires(array_abs_bound(a, 0, 5 * MLDSA_N, 8380417))
178+
requires(array_abs_bound(b, 0, 5 * MLDSA_N, 75423753))
179+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
180+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
181+
/* check-magic: on */
182+
);
157183

158184
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
159185
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
160-
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
161-
const int32_t *);
186+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r, const int32_t *a,
187+
const int32_t *b)
188+
/* This must be kept in sync with the HOL-Light specification
189+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
190+
__contract__(
191+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
192+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
193+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
194+
/* check-magic: off */
195+
requires(array_abs_bound(a, 0, 7 * MLDSA_N, 8380417))
196+
requires(array_abs_bound(b, 0, 7 * MLDSA_N, 75423753))
197+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
198+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
199+
/* check-magic: on */
200+
);
162201

163202
#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 45 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -147,17 +147,56 @@ __contract__(
147147

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

153166
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
154167
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
155-
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
156-
const int32_t *);
168+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r, const int32_t *a,
169+
const int32_t *b)
170+
/* This must be kept in sync with the HOL-Light specification
171+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
172+
__contract__(
173+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
174+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
175+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
176+
/* check-magic: off */
177+
requires(array_abs_bound(a, 0, 5 * MLDSA_N, 8380417))
178+
requires(array_abs_bound(b, 0, 5 * MLDSA_N, 75423753))
179+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
180+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
181+
/* check-magic: on */
182+
);
157183

158184
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
159185
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
160-
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
161-
const int32_t *);
186+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r, const int32_t *a,
187+
const int32_t *b)
188+
/* This must be kept in sync with the HOL-Light specification
189+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
190+
__contract__(
191+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
192+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
193+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
194+
/* check-magic: off */
195+
requires(array_abs_bound(a, 0, 7 * MLDSA_N, 8380417))
196+
requires(array_abs_bound(b, 0, 7 * MLDSA_N, 75423753))
197+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
198+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
199+
/* check-magic: on */
200+
);
162201

163202
#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */

‎dev/x86_64/src/arith_native_x86_64.h‎

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

128142
#define mld_pointwise_acc_l5_avx2 MLD_NAMESPACE(pointwise_acc_l5_avx2)
129143
void mld_pointwise_acc_l5_avx2(int32_t c[MLDSA_N], const int32_t a[5][MLDSA_N],
130144
const int32_t b[5][MLDSA_N],
131-
const int32_t *qdata);
145+
const int32_t *qdata)
146+
/* This must be kept in sync with the HOL-Light specification
147+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5.ml */
148+
__contract__(
149+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
150+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
151+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
152+
/* check-magic: off */
153+
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
154+
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
155+
requires(qdata == mld_qdata)
156+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
157+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
158+
/* check-magic: on */
159+
);
132160

133161
#define mld_pointwise_acc_l7_avx2 MLD_NAMESPACE(pointwise_acc_l7_avx2)
134162
void mld_pointwise_acc_l7_avx2(int32_t c[MLDSA_N], const int32_t a[7][MLDSA_N],
135163
const int32_t b[7][MLDSA_N],
136-
const int32_t *qdata);
164+
const int32_t *qdata)
165+
/* This must be kept in sync with the HOL-Light specification
166+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7.ml */
167+
__contract__(
168+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
169+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
170+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
171+
/* check-magic: off */
172+
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
173+
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
174+
requires(qdata == mld_qdata)
175+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
176+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
177+
/* check-magic: on */
178+
);
137179

138180
#endif /* !MLD_NATIVE_X86_64_SRC_ARITH_NATIVE_X86_64_H */

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

Lines changed: 45 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -147,17 +147,56 @@ __contract__(
147147

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

153166
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
154167
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
155-
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
156-
const int32_t *);
168+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r, const int32_t *a,
169+
const int32_t *b)
170+
/* This must be kept in sync with the HOL-Light specification
171+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
172+
__contract__(
173+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
174+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
175+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
176+
/* check-magic: off */
177+
requires(array_abs_bound(a, 0, 5 * MLDSA_N, 8380417))
178+
requires(array_abs_bound(b, 0, 5 * MLDSA_N, 75423753))
179+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
180+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
181+
/* check-magic: on */
182+
);
157183

158184
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
159185
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
160-
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
161-
const int32_t *);
186+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r, const int32_t *a,
187+
const int32_t *b)
188+
/* This must be kept in sync with the HOL-Light specification
189+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
190+
__contract__(
191+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
192+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
193+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
194+
/* check-magic: off */
195+
requires(array_abs_bound(a, 0, 7 * MLDSA_N, 8380417))
196+
requires(array_abs_bound(b, 0, 7 * MLDSA_N, 75423753))
197+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
198+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
199+
/* check-magic: on */
200+
);
162201

163202
#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */

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

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

128142
#define mld_pointwise_acc_l5_avx2 MLD_NAMESPACE(pointwise_acc_l5_avx2)
129143
void mld_pointwise_acc_l5_avx2(int32_t c[MLDSA_N], const int32_t a[5][MLDSA_N],
130144
const int32_t b[5][MLDSA_N],
131-
const int32_t *qdata);
145+
const int32_t *qdata)
146+
/* This must be kept in sync with the HOL-Light specification
147+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5.ml */
148+
__contract__(
149+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
150+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
151+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
152+
/* check-magic: off */
153+
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
154+
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
155+
requires(qdata == mld_qdata)
156+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
157+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
158+
/* check-magic: on */
159+
);
132160

133161
#define mld_pointwise_acc_l7_avx2 MLD_NAMESPACE(pointwise_acc_l7_avx2)
134162
void mld_pointwise_acc_l7_avx2(int32_t c[MLDSA_N], const int32_t a[7][MLDSA_N],
135163
const int32_t b[7][MLDSA_N],
136-
const int32_t *qdata);
164+
const int32_t *qdata)
165+
/* This must be kept in sync with the HOL-Light specification
166+
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7.ml */
167+
__contract__(
168+
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
169+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
170+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
171+
/* check-magic: off */
172+
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
173+
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
174+
requires(qdata == mld_qdata)
175+
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
176+
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
177+
/* check-magic: on */
178+
);
137179

138180
#endif /* !MLD_NATIVE_X86_64_SRC_ARITH_NATIVE_X86_64_H */

0 commit comments

Comments
 (0)