Skip to content

Add HOL Light pointwise-acc multiplication proofs for AArch64 and x86_64 #1010

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jakemas wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add HOL Light pointwise-acc multiplication proofs for AArch64 and x86_64 #1010

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions .github/workflows/hol_light.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,12 @@ jobs:
needs: ["mldsa_specs.ml", "mldsa_zetas.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
- name: mldsa_pointwise
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
- name: mldsa_pointwise_acc_l4
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
- name: mldsa_pointwise_acc_l5
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
- name: mldsa_pointwise_acc_l7
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
- name: mldsa_poly_caddq
needs: ["aarch64_utils.ml"]
- name: mldsa_poly_chknorm
Expand Down Expand Up @@ -185,6 +191,12 @@ jobs:
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
- name: mldsa_pointwise
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
- name: mldsa_pointwise_acc_l4
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
- name: mldsa_pointwise_acc_l5
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
- name: mldsa_pointwise_acc_l7
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
runs-on: pqcp-x64
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
Expand Down
3 changes: 3 additions & 0 deletions BIBLIOGRAPHY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -254,6 +254,9 @@ source code and documentation.
- [proofs/hol_light/x86_64/mldsa/mldsa_intt.S](proofs/hol_light/x86_64/mldsa/mldsa_intt.S)
- [proofs/hol_light/x86_64/mldsa/mldsa_ntt.S](proofs/hol_light/x86_64/mldsa/mldsa_ntt.S)
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S)
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S)
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S)
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l7.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l7.S)

### `Round3_Spec`

Expand Down
9 changes: 3 additions & 6 deletions dev/aarch64_clean/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,8 +213,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native(
int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N],
const int32_t v[4][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 4 */
Expand All @@ -225,8 +224,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native(
int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N],
const int32_t v[5][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 5 */
Expand All @@ -237,8 +235,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native(
int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N],
const int32_t v[7][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 7 */
Expand Down
54 changes: 48 additions & 6 deletions dev/aarch64_clean/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,17 +152,59 @@ __contract__(

#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *r,
const int32_t a[4][MLDSA_N],
const int32_t b[4][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r,
const int32_t a[5][MLDSA_N],
const int32_t b[5][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r,
const int32_t a[7][MLDSA_N],
const int32_t b[7][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */
9 changes: 3 additions & 6 deletions dev/aarch64_opt/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,8 +213,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native(
int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N],
const int32_t v[4][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 4 */
Expand All @@ -225,8 +224,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native(
int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N],
const int32_t v[5][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 5 */
Expand All @@ -237,8 +235,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native(
int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N],
const int32_t v[7][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 7 */
Expand Down
54 changes: 48 additions & 6 deletions dev/aarch64_opt/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,17 +152,59 @@ __contract__(

#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *r,
const int32_t a[4][MLDSA_N],
const int32_t b[4][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r,
const int32_t a[5][MLDSA_N],
const int32_t b[5][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r,
const int32_t a[7][MLDSA_N],
const int32_t b[7][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */
48 changes: 45 additions & 3 deletions dev/x86_64/src/arith_native_x86_64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,16 +123,58 @@ __contract__(
#define mld_pointwise_acc_l4_avx2 MLD_NAMESPACE(pointwise_acc_l4_avx2)
void mld_pointwise_acc_l4_avx2(int32_t c[MLDSA_N], const int32_t a[4][MLDSA_N],
const int32_t b[4][MLDSA_N],
const int32_t *qdata);
const int32_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4.ml */
__contract__(
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
requires(qdata == mld_qdata)
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#define mld_pointwise_acc_l5_avx2 MLD_NAMESPACE(pointwise_acc_l5_avx2)
void mld_pointwise_acc_l5_avx2(int32_t c[MLDSA_N], const int32_t a[5][MLDSA_N],
const int32_t b[5][MLDSA_N],
const int32_t *qdata);
const int32_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5.ml */
__contract__(
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
requires(qdata == mld_qdata)
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#define mld_pointwise_acc_l7_avx2 MLD_NAMESPACE(pointwise_acc_l7_avx2)
void mld_pointwise_acc_l7_avx2(int32_t c[MLDSA_N], const int32_t a[7][MLDSA_N],
const int32_t b[7][MLDSA_N],
const int32_t *qdata);
const int32_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7.ml */
__contract__(
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
requires(qdata == mld_qdata)
assigns(memory_slice(c, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(c, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#endif /* !MLD_NATIVE_X86_64_SRC_ARITH_NATIVE_X86_64_H */
9 changes: 3 additions & 6 deletions mldsa/src/native/aarch64/meta.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,8 +213,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native(
int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N],
const int32_t v[4][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l4_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 4 */
Expand All @@ -225,8 +224,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native(
int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N],
const int32_t v[5][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l5_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 5 */
Expand All @@ -237,8 +235,7 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native(
int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N],
const int32_t v[7][MLDSA_N])
{
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, (const int32_t *)u,
(const int32_t *)v);
mld_polyvecl_pointwise_acc_montgomery_l7_asm(w, u, v);
return MLD_NATIVE_FUNC_SUCCESS;
}
#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_L == 7 */
Expand Down
54 changes: 48 additions & 6 deletions mldsa/src/native/aarch64/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,17 +152,59 @@ __contract__(

#define mld_polyvecl_pointwise_acc_montgomery_l4_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l4_asm)
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l4_asm(int32_t *r,
const int32_t a[4][MLDSA_N],
const int32_t b[4][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 4 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 4, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 4, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#define mld_polyvecl_pointwise_acc_montgomery_l5_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l5_asm)
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l5_asm(int32_t *r,
const int32_t a[5][MLDSA_N],
const int32_t b[5][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 5 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 5, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 5, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#define mld_polyvecl_pointwise_acc_montgomery_l7_asm \
MLD_NAMESPACE(polyvecl_pointwise_acc_montgomery_l7_asm)
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *, const int32_t *,
const int32_t *);
void mld_polyvecl_pointwise_acc_montgomery_l7_asm(int32_t *r,
const int32_t a[7][MLDSA_N],
const int32_t b[7][MLDSA_N])
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))
requires(memory_no_alias(b, sizeof(int32_t) * 7 * MLDSA_N))
/* check-magic: off */
requires(forall(l0, 0, 7, array_abs_bound(a[l0], 0, MLDSA_N, 8380417)))
requires(forall(l1, 0, 7, array_abs_bound(b[l1], 0, MLDSA_N, 75423753)))
assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
ensures(array_abs_bound(r, 0, MLDSA_N, 8380417))
/* check-magic: on */
);

#endif /* !MLD_NATIVE_AARCH64_SRC_ARITH_NATIVE_AARCH64_H */
Loading
Loading