Skip to content

Commit 2f83d57

Browse files
mkannwischermkannwischer
committed
hol_light: Unify asm and proof filenames with exported symbols
Port of pq-code-package/mlkem-native#1663 (commit 3/4). Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
1 parent 3277485 commit 2f83d57

52 files changed

Lines changed: 199 additions & 199 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/hol_light.yml‎

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -72,38 +72,38 @@ jobs:
7272
gh_token: ${{ secrets.GITHUB_TOKEN }}
7373
nix-shell: 'hol_light'
7474
script: |
75-
make -C proofs/hol_light/aarch64 mldsa/mldsa_poly_caddq.o
76-
echo 'needs "aarch64/proofs/mldsa_poly_caddq.ml";;' | hol.sh
75+
make -C proofs/hol_light/aarch64 mldsa/poly_caddq_aarch64_asm.o
76+
echo 'needs "aarch64/proofs/poly_caddq_aarch64_asm.ml";;' | hol.sh
7777
hol_light_proofs:
7878
needs: [ hol_light_bytecode ]
7979
strategy:
8080
fail-fast: false
8181
matrix:
8282
proof:
8383
# Dependencies on {name}.{S,ml} are implicit
84-
- name: mldsa_ntt
84+
- name: ntt_aarch64_asm
8585
needs: ["mldsa_specs.ml", "mldsa_zetas.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
86-
- name: mldsa_pointwise
86+
- name: pointwise_montgomery_aarch64_asm
8787
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
88-
- name: mldsa_pointwise_acc_l4
88+
- name: mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm
8989
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
90-
- name: mldsa_pointwise_acc_l5
90+
- name: mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm
9191
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
92-
- name: mldsa_pointwise_acc_l7
92+
- name: mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm
9393
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
94-
- name: mldsa_poly_caddq
94+
- name: poly_caddq_aarch64_asm
9595
needs: ["aarch64_utils.ml"]
96-
- name: mldsa_poly_chknorm
96+
- name: poly_chknorm_aarch64_asm
9797
needs: ["aarch64_utils.ml"]
98-
- name: keccak_f1600_x1_scalar
98+
- name: keccak_f1600_x1_scalar_aarch64_asm
9999
needs: ["keccak_spec.ml"]
100-
- name: keccak_f1600_x1_v84a
100+
- name: keccak_f1600_x1_v84a_aarch64_asm
101101
needs: ["keccak_spec.ml"]
102-
- name: keccak_f1600_x2_v84a
102+
- name: keccak_f1600_x2_v84a_aarch64_asm
103103
needs: ["keccak_spec.ml"]
104-
- name: keccak_f1600_x4_v8a_scalar
104+
- name: keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
105105
needs: ["keccak_spec.ml"]
106-
- name: keccak_f1600_x4_v8a_v84a_scalar
106+
- name: keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm
107107
needs: ["keccak_spec.ml"]
108108
name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
109109
runs-on: pqcp-arm64
@@ -175,8 +175,8 @@ jobs:
175175
nix-shell: 'hol_light'
176176
script: |
177177
# TODO: Enable when we have a cheaper proof
178-
# make -C proofs/hol_light/x86_64 mldsa/mldsa_ntt.o
179-
# echo 'needs "x86_64/proofs/mldsa_ntt.ml";;' | hol.sh
178+
# make -C proofs/hol_light/x86_64 mldsa/ntt_avx2_asm.o
179+
# echo 'needs "x86_64/proofs/ntt_avx2_asm.ml";;' | hol.sh
180180
echo 'needs "x86/proofs/base.ml";; needs "common/mldsa_specs.ml";; #quit;;' | hol.sh
181181
hol_light_proofs_x86_64:
182182
needs: [ hol_light_bytecode_x86_64 ]
@@ -185,19 +185,19 @@ jobs:
185185
matrix:
186186
proof:
187187
# Dependencies on {name}.{S,ml} are implicit
188-
- name: mldsa_ntt
188+
- name: ntt_avx2_asm
189189
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
190-
- name: mldsa_intt
190+
- name: intt_avx2_asm
191191
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
192-
- name: mldsa_nttunpack
192+
- name: nttunpack_avx2_asm
193193
needs: ["mldsa_specs.ml"]
194-
- name: mldsa_pointwise
194+
- name: pointwise_avx2_asm
195195
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml"]
196-
- name: mldsa_pointwise_acc_l4
196+
- name: pointwise_acc_l4_avx2_asm
197197
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
198-
- name: mldsa_pointwise_acc_l5
198+
- name: pointwise_acc_l5_avx2_asm
199199
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
200-
- name: mldsa_pointwise_acc_l7
200+
- name: pointwise_acc_l7_avx2_asm
201201
needs: ["mldsa_specs.ml", "mldsa_utils.ml", "mldsa_zetas.ml", "subroutine_signatures.ml"]
202202
name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
203203
runs-on: pqcp-x64

‎BIBLIOGRAPHY.md‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -125,8 +125,8 @@ source code and documentation.
125125
- [mldsa/src/fips202/native/aarch64/src/keccak_f1600_x1_v84a_aarch64_asm.S](mldsa/src/fips202/native/aarch64/src/keccak_f1600_x1_v84a_aarch64_asm.S)
126126
- [mldsa/src/fips202/native/aarch64/src/keccak_f1600_x2_v84a_aarch64_asm.S](mldsa/src/fips202/native/aarch64/src/keccak_f1600_x2_v84a_aarch64_asm.S)
127127
- [proofs/hol_light/README.md](proofs/hol_light/README.md)
128-
- [proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_v84a.S](proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_v84a.S)
129-
- [proofs/hol_light/aarch64/mldsa/keccak_f1600_x2_v84a.S](proofs/hol_light/aarch64/mldsa/keccak_f1600_x2_v84a.S)
128+
- [proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.S](proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.S)
129+
- [proofs/hol_light/aarch64/mldsa/keccak_f1600_x2_v84a_aarch64_asm.S](proofs/hol_light/aarch64/mldsa/keccak_f1600_x2_v84a_aarch64_asm.S)
130130

131131
### `KyberSlash`
132132

@@ -182,7 +182,7 @@ source code and documentation.
182182
- [dev/aarch64_opt/src/ntt_aarch64_asm.S](dev/aarch64_opt/src/ntt_aarch64_asm.S)
183183
- [mldsa/src/native/aarch64/src/intt_aarch64_asm.S](mldsa/src/native/aarch64/src/intt_aarch64_asm.S)
184184
- [mldsa/src/native/aarch64/src/ntt_aarch64_asm.S](mldsa/src/native/aarch64/src/ntt_aarch64_asm.S)
185-
- [proofs/hol_light/aarch64/mldsa/mldsa_ntt.S](proofs/hol_light/aarch64/mldsa/mldsa_ntt.S)
185+
- [proofs/hol_light/aarch64/mldsa/ntt_aarch64_asm.S](proofs/hol_light/aarch64/mldsa/ntt_aarch64_asm.S)
186186

187187
### `REF`
188188

@@ -252,13 +252,13 @@ source code and documentation.
252252
- [mldsa/src/native/x86_64/src/rej_uniform_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_avx2.c)
253253
- [mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c)
254254
- [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c)
255-
- [proofs/hol_light/x86_64/mldsa/mldsa_intt.S](proofs/hol_light/x86_64/mldsa/mldsa_intt.S)
256-
- [proofs/hol_light/x86_64/mldsa/mldsa_ntt.S](proofs/hol_light/x86_64/mldsa/mldsa_ntt.S)
257-
- [proofs/hol_light/x86_64/mldsa/mldsa_nttunpack.S](proofs/hol_light/x86_64/mldsa/mldsa_nttunpack.S)
258-
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise.S)
259-
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l4.S)
260-
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l5.S)
261-
- [proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l7.S](proofs/hol_light/x86_64/mldsa/mldsa_pointwise_acc_l7.S)
255+
- [proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S](proofs/hol_light/x86_64/mldsa/intt_avx2_asm.S)
256+
- [proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S](proofs/hol_light/x86_64/mldsa/ntt_avx2_asm.S)
257+
- [proofs/hol_light/x86_64/mldsa/nttunpack_avx2_asm.S](proofs/hol_light/x86_64/mldsa/nttunpack_avx2_asm.S)
258+
- [proofs/hol_light/x86_64/mldsa/pointwise_acc_l4_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_acc_l4_avx2_asm.S)
259+
- [proofs/hol_light/x86_64/mldsa/pointwise_acc_l5_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_acc_l5_avx2_asm.S)
260+
- [proofs/hol_light/x86_64/mldsa/pointwise_acc_l7_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_acc_l7_avx2_asm.S)
261+
- [proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S](proofs/hol_light/x86_64/mldsa/pointwise_avx2_asm.S)
262262

263263
### `Round3_Spec`
264264

@@ -293,7 +293,7 @@ source code and documentation.
293293
- [dev/aarch64_opt/src/ntt_aarch64_asm.S](dev/aarch64_opt/src/ntt_aarch64_asm.S)
294294
- [mldsa/src/native/aarch64/src/intt_aarch64_asm.S](mldsa/src/native/aarch64/src/intt_aarch64_asm.S)
295295
- [mldsa/src/native/aarch64/src/ntt_aarch64_asm.S](mldsa/src/native/aarch64/src/ntt_aarch64_asm.S)
296-
- [proofs/hol_light/aarch64/mldsa/mldsa_ntt.S](proofs/hol_light/aarch64/mldsa/mldsa_ntt.S)
296+
- [proofs/hol_light/aarch64/mldsa/ntt_aarch64_asm.S](proofs/hol_light/aarch64/mldsa/ntt_aarch64_asm.S)
297297

298298
### `libmceliece`
299299

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ MLD_INTERNAL_DATA_DECLARATION const uint8_t mld_polyz_unpack_19_indices[64];
6464
void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456,
6565
const int32_t *zetas_l78)
6666
/* This must be kept in sync with the HOL-Light specification
67-
* in proofs/hol_light/aarch64/proofs/mldsa_ntt.ml */
67+
* in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */
6868
__contract__(
6969
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
7070
requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
@@ -113,7 +113,7 @@ void mld_poly_decompose_88_aarch64_asm(int32_t *a1, int32_t *a0);
113113
#define mld_poly_caddq_aarch64_asm MLD_NAMESPACE(poly_caddq_aarch64_asm)
114114
void mld_poly_caddq_aarch64_asm(int32_t *a)
115115
/* This must be kept in sync with the HOL-Light specification
116-
* in proofs/hol_light/aarch64/proofs/mldsa_poly_caddq.ml */
116+
* in proofs/hol_light/aarch64/proofs/poly_caddq_aarch64_asm.ml */
117117
__contract__(
118118
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
119119
requires(array_abs_bound(a, 0, MLDSA_N, MLDSA_Q))
@@ -137,7 +137,7 @@ void mld_poly_use_hint_88_aarch64_asm(int32_t *b, const int32_t *a,
137137
MLD_MUST_CHECK_RETURN_VALUE
138138
int mld_poly_chknorm_aarch64_asm(const int32_t *a, int32_t B)
139139
/* This must be kept in sync with the HOL-Light specification
140-
* in proofs/hol_light/aarch64/proofs/mldsa_poly_chknorm.ml */
140+
* in proofs/hol_light/aarch64/proofs/poly_chknorm_aarch64_asm.ml */
141141
__contract__(
142142
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
143143
/* HOL Light precondition: abs(ival(x i)) < 2^31, i.e., a[i] != INT32_MIN */
@@ -165,7 +165,7 @@ void mld_polyz_unpack_19_aarch64_asm(int32_t *r, const uint8_t *buf,
165165
void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *r, const int32_t *a,
166166
const int32_t *b)
167167
/* This must be kept in sync with the HOL-Light specification
168-
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise.ml */
168+
* in proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml */
169169
__contract__(
170170
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
171171
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
@@ -185,7 +185,9 @@ __contract__(
185185
void mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm(
186186
int32_t *r, const int32_t a[4][MLDSA_N], const int32_t b[4][MLDSA_N])
187187
/* This must be kept in sync with the HOL-Light specification
188-
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
188+
* in
189+
* proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml
190+
*/
189191
__contract__(
190192
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
191193
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
@@ -203,7 +205,9 @@ __contract__(
203205
void mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm(
204206
int32_t *r, const int32_t a[5][MLDSA_N], const int32_t b[5][MLDSA_N])
205207
/* This must be kept in sync with the HOL-Light specification
206-
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
208+
* in
209+
* proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml
210+
*/
207211
__contract__(
208212
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
209213
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
@@ -221,7 +225,9 @@ __contract__(
221225
void mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm(
222226
int32_t *r, const int32_t a[7][MLDSA_N], const int32_t b[7][MLDSA_N])
223227
/* This must be kept in sync with the HOL-Light specification
224-
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
228+
* in
229+
* proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml
230+
*/
225231
__contract__(
226232
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
227233
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ MLD_INTERNAL_DATA_DECLARATION const uint8_t mld_polyz_unpack_19_indices[64];
6464
void mld_ntt_aarch64_asm(int32_t *r, const int32_t *zetas_l123456,
6565
const int32_t *zetas_l78)
6666
/* This must be kept in sync with the HOL-Light specification
67-
* in proofs/hol_light/aarch64/proofs/mldsa_ntt.ml */
67+
* in proofs/hol_light/aarch64/proofs/ntt_aarch64_asm.ml */
6868
__contract__(
6969
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
7070
requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
@@ -113,7 +113,7 @@ void mld_poly_decompose_88_aarch64_asm(int32_t *a1, int32_t *a0);
113113
#define mld_poly_caddq_aarch64_asm MLD_NAMESPACE(poly_caddq_aarch64_asm)
114114
void mld_poly_caddq_aarch64_asm(int32_t *a)
115115
/* This must be kept in sync with the HOL-Light specification
116-
* in proofs/hol_light/aarch64/proofs/mldsa_poly_caddq.ml */
116+
* in proofs/hol_light/aarch64/proofs/poly_caddq_aarch64_asm.ml */
117117
__contract__(
118118
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
119119
requires(array_abs_bound(a, 0, MLDSA_N, MLDSA_Q))
@@ -137,7 +137,7 @@ void mld_poly_use_hint_88_aarch64_asm(int32_t *b, const int32_t *a,
137137
MLD_MUST_CHECK_RETURN_VALUE
138138
int mld_poly_chknorm_aarch64_asm(const int32_t *a, int32_t B)
139139
/* This must be kept in sync with the HOL-Light specification
140-
* in proofs/hol_light/aarch64/proofs/mldsa_poly_chknorm.ml */
140+
* in proofs/hol_light/aarch64/proofs/poly_chknorm_aarch64_asm.ml */
141141
__contract__(
142142
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
143143
/* HOL Light precondition: abs(ival(x i)) < 2^31, i.e., a[i] != INT32_MIN */
@@ -165,7 +165,7 @@ void mld_polyz_unpack_19_aarch64_asm(int32_t *r, const uint8_t *buf,
165165
void mld_poly_pointwise_montgomery_aarch64_asm(int32_t *r, const int32_t *a,
166166
const int32_t *b)
167167
/* This must be kept in sync with the HOL-Light specification
168-
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise.ml */
168+
* in proofs/hol_light/aarch64/proofs/pointwise_montgomery_aarch64_asm.ml */
169169
__contract__(
170170
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
171171
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
@@ -185,7 +185,9 @@ __contract__(
185185
void mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm(
186186
int32_t *r, const int32_t a[4][MLDSA_N], const int32_t b[4][MLDSA_N])
187187
/* This must be kept in sync with the HOL-Light specification
188-
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l4.ml */
188+
* in
189+
* proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.ml
190+
*/
189191
__contract__(
190192
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
191193
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
@@ -203,7 +205,9 @@ __contract__(
203205
void mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm(
204206
int32_t *r, const int32_t a[5][MLDSA_N], const int32_t b[5][MLDSA_N])
205207
/* This must be kept in sync with the HOL-Light specification
206-
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l5.ml */
208+
* in
209+
* proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.ml
210+
*/
207211
__contract__(
208212
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
209213
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
@@ -221,7 +225,9 @@ __contract__(
221225
void mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm(
222226
int32_t *r, const int32_t a[7][MLDSA_N], const int32_t b[7][MLDSA_N])
223227
/* This must be kept in sync with the HOL-Light specification
224-
* in proofs/hol_light/aarch64/proofs/mldsa_pointwise_acc_l7.ml */
228+
* in
229+
* proofs/hol_light/aarch64/proofs/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.ml
230+
*/
225231
__contract__(
226232
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
227233
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ MLD_INTERNAL_DATA_DECLARATION const uint8_t mld_rej_uniform_table[256][8];
3434
#define mld_ntt_avx2_asm MLD_NAMESPACE(ntt_avx2_asm)
3535
void mld_ntt_avx2_asm(int32_t *r, const int32_t *qdata)
3636
/* This must be kept in sync with the HOL-Light specification
37-
* in proofs/hol_light/x86_64/proofs/mldsa_ntt.ml */
37+
* in proofs/hol_light/x86_64/proofs/ntt_avx2_asm.ml */
3838
__contract__(
3939
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
4040
requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
@@ -48,7 +48,7 @@ __contract__(
4848
#define mld_invntt_avx2_asm MLD_NAMESPACE(invntt_avx2_asm)
4949
void mld_invntt_avx2_asm(int32_t *r, const int32_t *qdata)
5050
/* This must be kept in sync with the HOL-Light specification
51-
* in proofs/hol_light/x86_64/proofs/mldsa_intt.ml */
51+
* in proofs/hol_light/x86_64/proofs/intt_avx2_asm.ml */
5252
__contract__(
5353
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
5454
requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
@@ -62,7 +62,7 @@ __contract__(
6262
#define mld_nttunpack_avx2_asm MLD_NAMESPACE(nttunpack_avx2_asm)
6363
void mld_nttunpack_avx2_asm(int32_t *r)
6464
/* This must be kept in sync with the HOL-Light specification
65-
* in proofs/hol_light/x86_64/proofs/mldsa_nttunpack.ml */
65+
* in proofs/hol_light/x86_64/proofs/nttunpack_avx2_asm.ml */
6666
__contract__(
6767
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
6868
requires(array_abs_bound(r, 0, MLDSA_N, 8380417))
@@ -125,7 +125,7 @@ void mld_polyz_unpack_19_avx2(int32_t *r, const uint8_t *a);
125125
void mld_pointwise_avx2_asm(int32_t *c, const int32_t *a, const int32_t *b,
126126
const int32_t *qdata)
127127
/* This must be kept in sync with the HOL-Light specification
128-
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise.ml */
128+
* in proofs/hol_light/x86_64/proofs/pointwise_avx2_asm.ml */
129129
__contract__(
130130
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
131131
requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
@@ -145,7 +145,7 @@ void mld_pointwise_acc_l4_avx2_asm(int32_t c[MLDSA_N],
145145
const int32_t b[4][MLDSA_N],
146146
const int32_t *qdata)
147147
/* This must be kept in sync with the HOL-Light specification
148-
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l4.ml */
148+
* in proofs/hol_light/x86_64/proofs/pointwise_acc_l4_avx2_asm.ml */
149149
__contract__(
150150
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
151151
requires(memory_no_alias(a, sizeof(int32_t) * 4 * MLDSA_N))
@@ -165,7 +165,7 @@ void mld_pointwise_acc_l5_avx2_asm(int32_t c[MLDSA_N],
165165
const int32_t b[5][MLDSA_N],
166166
const int32_t *qdata)
167167
/* This must be kept in sync with the HOL-Light specification
168-
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l5.ml */
168+
* in proofs/hol_light/x86_64/proofs/pointwise_acc_l5_avx2_asm.ml */
169169
__contract__(
170170
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
171171
requires(memory_no_alias(a, sizeof(int32_t) * 5 * MLDSA_N))
@@ -185,7 +185,7 @@ void mld_pointwise_acc_l7_avx2_asm(int32_t c[MLDSA_N],
185185
const int32_t b[7][MLDSA_N],
186186
const int32_t *qdata)
187187
/* This must be kept in sync with the HOL-Light specification
188-
* in proofs/hol_light/x86_64/proofs/mldsa_pointwise_acc_l7.ml */
188+
* in proofs/hol_light/x86_64/proofs/pointwise_acc_l7_avx2_asm.ml */
189189
__contract__(
190190
requires(memory_no_alias(c, sizeof(int32_t) * MLDSA_N))
191191
requires(memory_no_alias(a, sizeof(int32_t) * 7 * MLDSA_N))

0 commit comments

Comments
 (0)