Skip to content

Commit b464b88

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 e9c0f60 commit b464b88

35 files changed

Lines changed: 4566 additions & 43 deletions

‎.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", "mldsa_zetas.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/meta.h‎

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -213,8 +213,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native(
213213
int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N],
214214
const int32_t v[4][MLDSA_N])
215215
{
216-
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, (const int32_t *)u,
217-
(const int32_t *)v);
216+
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, u, v);
218217
return MLD_NATIVE_FUNC_SUCCESS;
219218
}
220219
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 4 */
@@ -225,8 +224,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native(
225224
int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N],
226225
const int32_t v[5][MLDSA_N])
227226
{
228-
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, (const int32_t *)u,
229-
(const int32_t *)v);
227+
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, u, v);
230228
return MLD_NATIVE_FUNC_SUCCESS;
231229
}
232230
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 5 */
@@ -237,8 +235,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native(
237235
int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N],
238236
const int32_t v[7][MLDSA_N])
239237
{
240-
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, (const int32_t *)u,
241-
(const int32_t *)v);
238+
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, u, v);
242239
return MLD_NATIVE_FUNC_SUCCESS;
243240
}
244241
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 7 */

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 48 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -147,17 +147,59 @@ __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,
151+
const int32_t a[4][MLDSA_N],
152+
const int32_t b[4][MLDSA_N])
153+
/* This must be kept in sync with the HOL-Light specification
154+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
155+
__contract__(
156+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
157+
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
158+
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
159+
/* check-magic: off */
160+
requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
161+
requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
162+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
163+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
164+
/* check-magic: on */
165+
);
152166

153167
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
154168
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 *);
169+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r,
170+
const int32_t a[5][MLDSA_N],
171+
const int32_t b[5][MLDSA_N])
172+
/* This must be kept in sync with the HOL-Light specification
173+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
174+
__contract__(
175+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
176+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
177+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
178+
/* check-magic: off */
179+
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
180+
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
181+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
182+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
183+
/* check-magic: on */
184+
);
157185

158186
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
159187
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 *);
188+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r,
189+
const int32_t a[7][MLDSA_N],
190+
const int32_t b[7][MLDSA_N])
191+
/* This must be kept in sync with the HOL-Light specification
192+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
193+
__contract__(
194+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
195+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
196+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
197+
/* check-magic: off */
198+
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
199+
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
200+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
201+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
202+
/* check-magic: on */
203+
);
162204

163205
#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */

‎dev/aarch64_opt/meta.h‎

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -213,8 +213,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native(
213213
int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N],
214214
const int32_t v[4][MLDSA_N])
215215
{
216-
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, (const int32_t *)u,
217-
(const int32_t *)v);
216+
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, u, v);
218217
return MLD_NATIVE_FUNC_SUCCESS;
219218
}
220219
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 4 */
@@ -225,8 +224,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native(
225224
int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N],
226225
const int32_t v[5][MLDSA_N])
227226
{
228-
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, (const int32_t *)u,
229-
(const int32_t *)v);
227+
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, u, v);
230228
return MLD_NATIVE_FUNC_SUCCESS;
231229
}
232230
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 5 */
@@ -237,8 +235,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native(
237235
int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N],
238236
const int32_t v[7][MLDSA_N])
239237
{
240-
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, (const int32_t *)u,
241-
(const int32_t *)v);
238+
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, u, v);
242239
return MLD_NATIVE_FUNC_SUCCESS;
243240
}
244241
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 7 */

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 48 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -147,17 +147,59 @@ __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,
151+
const int32_t a[4][MLDSA_N],
152+
const int32_t b[4][MLDSA_N])
153+
/* This must be kept in sync with the HOL-Light specification
154+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
155+
__contract__(
156+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
157+
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
158+
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
159+
/* check-magic: off */
160+
requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
161+
requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
162+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
163+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
164+
/* check-magic: on */
165+
);
152166

153167
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
154168
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 *);
169+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r,
170+
const int32_t a[5][MLDSA_N],
171+
const int32_t b[5][MLDSA_N])
172+
/* This must be kept in sync with the HOL-Light specification
173+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
174+
__contract__(
175+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
176+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
177+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
178+
/* check-magic: off */
179+
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
180+
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
181+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
182+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
183+
/* check-magic: on */
184+
);
157185

158186
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
159187
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 *);
188+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r,
189+
const int32_t a[7][MLDSA_N],
190+
const int32_t b[7][MLDSA_N])
191+
/* This must be kept in sync with the HOL-Light specification
192+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
193+
__contract__(
194+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
195+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
196+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
197+
/* check-magic: off */
198+
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
199+
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
200+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
201+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
202+
/* check-magic: on */
203+
);
162204

163205
#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/meta.h‎

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -213,8 +213,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native(
213213
int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N],
214214
const int32_t v[4][MLDSA_N])
215215
{
216-
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, (const int32_t *)u,
217-
(const int32_t *)v);
216+
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, u, v);
218217
return MLD_NATIVE_FUNC_SUCCESS;
219218
}
220219
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 4 */
@@ -225,8 +224,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native(
225224
int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N],
226225
const int32_t v[5][MLDSA_N])
227226
{
228-
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, (const int32_t *)u,
229-
(const int32_t *)v);
227+
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, u, v);
230228
return MLD_NATIVE_FUNC_SUCCESS;
231229
}
232230
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 5 */
@@ -237,8 +235,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native(
237235
int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N],
238236
const int32_t v[7][MLDSA_N])
239237
{
240-
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, (const int32_t *)u,
241-
(const int32_t *)v);
238+
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, u, v);
242239
return MLD_NATIVE_FUNC_SUCCESS;
243240
}
244241
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 7 */

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

Lines changed: 48 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -147,17 +147,59 @@ __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,
151+
const int32_t a[4][MLDSA_N],
152+
const int32_t b[4][MLDSA_N])
153+
/* This must be kept in sync with the HOL-Light specification
154+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
155+
__contract__(
156+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
157+
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
158+
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
159+
/* check-magic: off */
160+
requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
161+
requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
162+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
163+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
164+
/* check-magic: on */
165+
);
152166

153167
#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
154168
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 *);
169+
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r,
170+
const int32_t a[5][MLDSA_N],
171+
const int32_t b[5][MLDSA_N])
172+
/* This must be kept in sync with the HOL-Light specification
173+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
174+
__contract__(
175+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
176+
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
177+
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
178+
/* check-magic: off */
179+
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
180+
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
181+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
182+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
183+
/* check-magic: on */
184+
);
157185

158186
#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
159187
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 *);
188+
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r,
189+
const int32_t a[7][MLDSA_N],
190+
const int32_t b[7][MLDSA_N])
191+
/* This must be kept in sync with the HOL-Light specification
192+
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
193+
__contract__(
194+
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
195+
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
196+
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
197+
/* check-magic: off */
198+
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
199+
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
200+
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
201+
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
202+
/* check-magic: on */
203+
);
162204

163205
#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */

0 commit comments

Comments
 (0)