Skip to content

Commit d213ca8

Browse files
hanno-beckerhanno-becker
committed
Use consistent architecture identifier
Use `aarch64` and `x86_64` consistently, removing uses of `arm` and `x86`, most notably the HOL-Light proof directories. While testing, noticed a missing bytecode dump for the native `tomont` implementation on x86_64 and added it to x86_64/proofs/dump_bytecode.ml. Also, noticed that ASM simplification from mlkem -> proofs/hol_light was so far only done for the native architecture in scripts/autogen. This is adjusted to run whenever a cross-compiler is available, matching the behavior of autogen for the simplification from dev -> mlkem. Signed-off-by: Hanno Becker <[email protected]>
1 parent 18da457 commit d213ca8

File tree

80 files changed

+417
-377
lines changed

Some content is hidden

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

80 files changed

+417
-377
lines changed

‎.github/workflows/hol_light.yml‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,12 @@ on:
99
branches: ["main"]
1010
paths:
1111
- '.github/workflows/hol_light.yml'
12-
- 'proofs/hol_light/arm/Makefile'
13-
- 'proofs/hol_light/arm/**/*.S'
14-
- 'proofs/hol_light/arm/**/*.ml'
15-
- 'proofs/hol_light/x86/Makefile'
16-
- 'proofs/hol_light/x86/**/*.S'
17-
- 'proofs/hol_light/x86/**/*.ml'
12+
- 'proofs/hol_light/aarch64/Makefile'
13+
- 'proofs/hol_light/aarch64/**/*.S'
14+
- 'proofs/hol_light/aarch64/**/*.ml'
15+
- 'proofs/hol_light/x86_64/Makefile'
16+
- 'proofs/hol_light/x86_64/**/*.S'
17+
- 'proofs/hol_light/x86_64/**/*.ml'
1818
- 'flake.nix'
1919
- 'flake.lock'
2020
- 'nix/hol_light/*'
@@ -23,12 +23,12 @@ on:
2323
branches: ["main"]
2424
paths:
2525
- '.github/workflows/hol_light.yml'
26-
- 'proofs/hol_light/arm/Makefile'
27-
- 'proofs/hol_light/arm/**/*.S'
28-
- 'proofs/hol_light/arm/**/*.ml'
29-
- 'proofs/hol_light/x86/Makefile'
30-
- 'proofs/hol_light/x86/**/*.S'
31-
- 'proofs/hol_light/x86/**/*.ml'
26+
- 'proofs/hol_light/aarch64/Makefile'
27+
- 'proofs/hol_light/aarch64/**/*.S'
28+
- 'proofs/hol_light/aarch64/**/*.ml'
29+
- 'proofs/hol_light/x86_64/Makefile'
30+
- 'proofs/hol_light/x86_64/**/*.S'
31+
- 'proofs/hol_light/x86_64/**/*.ml'
3232
- 'flake.nix'
3333
- 'flake.lock'
3434
- 'nix/hol_light/*'
@@ -70,8 +70,8 @@ jobs:
7070
gh_token: ${{ secrets.GITHUB_TOKEN }}
7171
nix-shell: 'hol_light'
7272
script: |
73-
make -C proofs/hol_light/arm mlkem/mlkem_poly_tobytes.o
74-
echo 'needs "arm/proofs/mlkem_poly_tobytes.ml";;' | hol.sh
73+
make -C proofs/hol_light/aarch64 mlkem/mlkem_poly_tobytes.o
74+
echo 'needs "aarch64/proofs/mlkem_poly_tobytes.ml";;' | hol.sh
7575
hol_light_proofs:
7676
needs: [ hol_light_bytecode ]
7777
strategy:
@@ -135,7 +135,7 @@ jobs:
135135
done
136136
137137
# Always re-run upon change to nix files for HOL-Light
138-
if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/arm/Makefile"* ]]; then
138+
if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/aarch64/Makefile"* ]]; then
139139
run_needed=1
140140
fi
141141
@@ -178,8 +178,8 @@ jobs:
178178
gh_token: ${{ secrets.GITHUB_TOKEN }}
179179
nix-shell: 'hol_light'
180180
script: |
181-
make -C proofs/hol_light/x86 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
182-
echo 'needs "x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
181+
make -C proofs/hol_light/x86_64 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
182+
echo 'needs "x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
183183
hol_light_proofs_x86_64:
184184
needs: [ hol_light_bytecode_x86_64 ]
185185
strategy:
@@ -237,7 +237,7 @@ jobs:
237237
done
238238
239239
# Always re-run upon change to nix files for HOL-Light
240-
if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86/Makefile"* ]]; then
240+
if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86_64/Makefile"* ]]; then
241241
run_needed=1
242242
fi
243243

‎BIBLIOGRAPHY.md‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,8 @@ source code and documentation.
2727
- [dev/x86_64/src/ntt.S](dev/x86_64/src/ntt.S)
2828
- [mlkem/src/native/x86_64/src/intt.S](mlkem/src/native/x86_64/src/intt.S)
2929
- [mlkem/src/native/x86_64/src/ntt.S](mlkem/src/native/x86_64/src/ntt.S)
30-
- [proofs/hol_light/x86/mlkem/mlkem_intt.S](proofs/hol_light/x86/mlkem/mlkem_intt.S)
31-
- [proofs/hol_light/x86/mlkem/mlkem_ntt.S](proofs/hol_light/x86/mlkem/mlkem_ntt.S)
30+
- [proofs/hol_light/x86_64/mlkem/mlkem_intt.S](proofs/hol_light/x86_64/mlkem/mlkem_intt.S)
31+
- [proofs/hol_light/x86_64/mlkem/mlkem_ntt.S](proofs/hol_light/x86_64/mlkem/mlkem_ntt.S)
3232

3333
### `FIPS140_3_IG`
3434

@@ -145,8 +145,8 @@ source code and documentation.
145145
- [mlkem/src/fips202/native/aarch64/src/keccak_f1600_x1_v84a_asm.S](mlkem/src/fips202/native/aarch64/src/keccak_f1600_x1_v84a_asm.S)
146146
- [mlkem/src/fips202/native/aarch64/src/keccak_f1600_x2_v84a_asm.S](mlkem/src/fips202/native/aarch64/src/keccak_f1600_x2_v84a_asm.S)
147147
- [proofs/hol_light/README.md](proofs/hol_light/README.md)
148-
- [proofs/hol_light/arm/mlkem/keccak_f1600_x1_v84a.S](proofs/hol_light/arm/mlkem/keccak_f1600_x1_v84a.S)
149-
- [proofs/hol_light/arm/mlkem/keccak_f1600_x2_v84a.S](proofs/hol_light/arm/mlkem/keccak_f1600_x2_v84a.S)
148+
- [proofs/hol_light/aarch64/mlkem/keccak_f1600_x1_v84a.S](proofs/hol_light/aarch64/mlkem/keccak_f1600_x1_v84a.S)
149+
- [proofs/hol_light/aarch64/mlkem/keccak_f1600_x2_v84a.S](proofs/hol_light/aarch64/mlkem/keccak_f1600_x2_v84a.S)
150150

151151
### `KyberSlash`
152152

@@ -198,11 +198,11 @@ source code and documentation.
198198
- [mlkem/src/native/aarch64/src/polyvec_basemul_acc_montgomery_cached_asm_k4.S](mlkem/src/native/aarch64/src/polyvec_basemul_acc_montgomery_cached_asm_k4.S)
199199
- [mlkem/src/poly.c](mlkem/src/poly.c)
200200
- [mlkem/src/poly_k.c](mlkem/src/poly_k.c)
201-
- [proofs/hol_light/arm/mlkem/mlkem_intt.S](proofs/hol_light/arm/mlkem/mlkem_intt.S)
202-
- [proofs/hol_light/arm/mlkem/mlkem_ntt.S](proofs/hol_light/arm/mlkem/mlkem_ntt.S)
203-
- [proofs/hol_light/arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S](proofs/hol_light/arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S)
204-
- [proofs/hol_light/arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S](proofs/hol_light/arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S)
205-
- [proofs/hol_light/arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S](proofs/hol_light/arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
201+
- [proofs/hol_light/aarch64/mlkem/mlkem_intt.S](proofs/hol_light/aarch64/mlkem/mlkem_intt.S)
202+
- [proofs/hol_light/aarch64/mlkem/mlkem_ntt.S](proofs/hol_light/aarch64/mlkem/mlkem_ntt.S)
203+
- [proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S](proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S)
204+
- [proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S](proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S)
205+
- [proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S](proofs/hol_light/aarch64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
206206

207207
### `REF`
208208

@@ -263,13 +263,13 @@ source code and documentation.
263263
- [mlkem/src/native/x86_64/src/nttunpack.S](mlkem/src/native/x86_64/src/nttunpack.S)
264264
- [mlkem/src/native/x86_64/src/reduce.S](mlkem/src/native/x86_64/src/reduce.S)
265265
- [mlkem/src/native/x86_64/src/tomont.S](mlkem/src/native/x86_64/src/tomont.S)
266-
- [proofs/hol_light/x86/mlkem/mlkem_frombytes.S](proofs/hol_light/x86/mlkem/mlkem_frombytes.S)
267-
- [proofs/hol_light/x86/mlkem/mlkem_intt.S](proofs/hol_light/x86/mlkem/mlkem_intt.S)
268-
- [proofs/hol_light/x86/mlkem/mlkem_ntt.S](proofs/hol_light/x86/mlkem/mlkem_ntt.S)
269-
- [proofs/hol_light/x86/mlkem/mlkem_reduce.S](proofs/hol_light/x86/mlkem/mlkem_reduce.S)
270-
- [proofs/hol_light/x86/mlkem/mlkem_tobytes.S](proofs/hol_light/x86/mlkem/mlkem_tobytes.S)
271-
- [proofs/hol_light/x86/mlkem/mlkem_tomont.S](proofs/hol_light/x86/mlkem/mlkem_tomont.S)
272-
- [proofs/hol_light/x86/mlkem/mlkem_unpack.S](proofs/hol_light/x86/mlkem/mlkem_unpack.S)
266+
- [proofs/hol_light/x86_64/mlkem/mlkem_frombytes.S](proofs/hol_light/x86_64/mlkem/mlkem_frombytes.S)
267+
- [proofs/hol_light/x86_64/mlkem/mlkem_intt.S](proofs/hol_light/x86_64/mlkem/mlkem_intt.S)
268+
- [proofs/hol_light/x86_64/mlkem/mlkem_ntt.S](proofs/hol_light/x86_64/mlkem/mlkem_ntt.S)
269+
- [proofs/hol_light/x86_64/mlkem/mlkem_reduce.S](proofs/hol_light/x86_64/mlkem/mlkem_reduce.S)
270+
- [proofs/hol_light/x86_64/mlkem/mlkem_tobytes.S](proofs/hol_light/x86_64/mlkem/mlkem_tobytes.S)
271+
- [proofs/hol_light/x86_64/mlkem/mlkem_tomont.S](proofs/hol_light/x86_64/mlkem/mlkem_tomont.S)
272+
- [proofs/hol_light/x86_64/mlkem/mlkem_unpack.S](proofs/hol_light/x86_64/mlkem/mlkem_unpack.S)
273273

274274
### `SLOTHY`
275275

@@ -305,8 +305,8 @@ source code and documentation.
305305
- [mlkem/src/native/aarch64/README.md](mlkem/src/native/aarch64/README.md)
306306
- [mlkem/src/native/aarch64/src/intt.S](mlkem/src/native/aarch64/src/intt.S)
307307
- [mlkem/src/native/aarch64/src/ntt.S](mlkem/src/native/aarch64/src/ntt.S)
308-
- [proofs/hol_light/arm/mlkem/mlkem_intt.S](proofs/hol_light/arm/mlkem/mlkem_intt.S)
309-
- [proofs/hol_light/arm/mlkem/mlkem_ntt.S](proofs/hol_light/arm/mlkem/mlkem_ntt.S)
308+
- [proofs/hol_light/aarch64/mlkem/mlkem_intt.S](proofs/hol_light/aarch64/mlkem/mlkem_intt.S)
309+
- [proofs/hol_light/aarch64/mlkem/mlkem_ntt.S](proofs/hol_light/aarch64/mlkem/mlkem_ntt.S)
310310

311311
### `clangover`
312312

‎README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ in the source code. See [proofs/cbmc](proofs/cbmc) for details.
6363

6464
All AArch64 assembly is proved functionally correct at the object-code level. This uses the [HOL-Light](https://github.com/jrh13/hol-light)
6565
interactive theorem prover and the [s2n-bignum](https://github.com/awslabs/s2n-bignum/) verification infrastructure (which includes a model of the
66-
relevant parts of the Arm architecture). See [proofs/hol_light/arm](proofs/hol_light/arm) for details.
66+
relevant parts of the Arm architecture). See [proofs/hol_light/aarch64](proofs/hol_light/aarch64) for details.
6767

6868
## Security
6969

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ extern const uint8_t mlk_rej_uniform_table[];
3535
void mlk_ntt_asm(int16_t p[256], const int16_t twiddles12345[80],
3636
const int16_t twiddles56[384])
3737
/* This must be kept in sync with the HOL-Light specification
38-
* in proofs/hol_light/arm/proofs/mlkem_ntt.ml */
38+
* in proofs/hol_light/aarch64/proofs/mlkem_ntt.ml */
3939
__contract__(
4040
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
4141
requires(array_abs_bound(p, 0, MLKEM_N, 8192))
@@ -51,7 +51,7 @@ __contract__(
5151
void mlk_intt_asm(int16_t p[256], const int16_t twiddles12345[80],
5252
const int16_t twiddles56[384])
5353
/* This must be kept in sync with the HOL-Light specification
54-
* in proofs/hol_light/arm/proofs/mlkem_intt.ml */
54+
* in proofs/hol_light/aarch64/proofs/mlkem_intt.ml */
5555
__contract__(
5656
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
5757
requires(twiddles12345 == mlk_aarch64_invntt_zetas_layer12345)
@@ -65,7 +65,7 @@ __contract__(
6565
#define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm)
6666
void mlk_poly_reduce_asm(int16_t p[256])
6767
/* This must be kept in sync with the HOL-Light specification
68-
* in proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml */
68+
* in proofs/hol_light/aarch64/proofs/mlkem_poly_reduce.ml */
6969
__contract__(
7070
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
7171
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
@@ -75,7 +75,7 @@ __contract__(
7575
#define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm)
7676
void mlk_poly_tomont_asm(int16_t p[256])
7777
/* This must be kept in sync with the HOL-Light specification
78-
* in proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml */
78+
* in proofs/hol_light/aarch64/proofs/mlkem_poly_tomont.ml */
7979
__contract__(
8080
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
8181
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
@@ -88,7 +88,7 @@ void mlk_poly_mulcache_compute_asm(int16_t cache[128],
8888
const int16_t zetas[128],
8989
const int16_t zetas_twisted[128])
9090
/* This must be kept in sync with the HOL-Light specification
91-
* in proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml */
91+
* in proofs/hol_light/aarch64/proofs/mlkem_poly_mulcache_compute.ml */
9292
__contract__(
9393
requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
9494
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
@@ -101,7 +101,7 @@ __contract__(
101101
#define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)
102102
void mlk_poly_tobytes_asm(uint8_t r[384], const int16_t a[256])
103103
/* This must be kept in sync with the HOL-Light specification
104-
* in proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml */
104+
* in proofs/hol_light/aarch64/proofs/mlkem_poly_tobytes.ml */
105105
__contract__(
106106
requires(memory_no_alias(r, MLKEM_POLYBYTES))
107107
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
@@ -115,7 +115,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
115115
int16_t r[256], const int16_t a[512], const int16_t b[512],
116116
const int16_t b_cache[256])
117117
/* This must be kept in sync with the HOL-Light specification in
118-
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
118+
* proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
119119
*/
120120
__contract__(
121121
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -132,7 +132,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
132132
int16_t r[256], const int16_t a[768], const int16_t b[768],
133133
const int16_t b_cache[384])
134134
/* This must be kept in sync with the HOL-Light specification in
135-
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
135+
* proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
136136
*/
137137
__contract__(
138138
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -149,7 +149,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
149149
int16_t r[256], const int16_t a[1024], const int16_t b[1024],
150150
const int16_t b_cache[512])
151151
/* This must be kept in sync with the HOL-Light specification in
152-
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
152+
* proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
153153
*/
154154
__contract__(
155155
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -164,7 +164,7 @@ __contract__(
164164
uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf,
165165
unsigned buflen, const uint8_t table[2048])
166166
/* This must be kept in sync with the HOL-Light specification
167-
* in proofs/hol_light/arm/proofs/mlkem_rej_uniform.ml. */
167+
* in proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml. */
168168
__contract__(
169169
requires(buflen % 24 == 0)
170170
requires(memory_no_alias(buf, buflen))

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ extern const uint8_t mlk_rej_uniform_table[];
3434
void mlk_ntt_asm(int16_t p[256], const int16_t twiddles12345[80],
3535
const int16_t twiddles56[384])
3636
/* This must be kept in sync with the HOL-Light specification
37-
* in proofs/hol_light/arm/proofs/mlkem_ntt.ml */
37+
* in proofs/hol_light/aarch64/proofs/mlkem_ntt.ml */
3838
__contract__(
3939
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
4040
requires(array_abs_bound(p, 0, MLKEM_N, 8192))
@@ -50,7 +50,7 @@ __contract__(
5050
void mlk_intt_asm(int16_t p[256], const int16_t twiddles12345[80],
5151
const int16_t twiddles56[384])
5252
/* This must be kept in sync with the HOL-Light specification
53-
* in proofs/hol_light/arm/proofs/mlkem_intt.ml */
53+
* in proofs/hol_light/aarch64/proofs/mlkem_intt.ml */
5454
__contract__(
5555
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
5656
requires(twiddles12345 == mlk_aarch64_invntt_zetas_layer12345)
@@ -64,7 +64,7 @@ __contract__(
6464
#define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm)
6565
void mlk_poly_reduce_asm(int16_t p[256])
6666
/* This must be kept in sync with the HOL-Light specification
67-
* in proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml */
67+
* in proofs/hol_light/aarch64/proofs/mlkem_poly_reduce.ml */
6868
__contract__(
6969
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
7070
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
@@ -74,7 +74,7 @@ __contract__(
7474
#define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm)
7575
void mlk_poly_tomont_asm(int16_t p[256])
7676
/* This must be kept in sync with the HOL-Light specification
77-
* in proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml */
77+
* in proofs/hol_light/aarch64/proofs/mlkem_poly_tomont.ml */
7878
__contract__(
7979
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
8080
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
@@ -87,7 +87,7 @@ void mlk_poly_mulcache_compute_asm(int16_t cache[128],
8787
const int16_t zetas[128],
8888
const int16_t zetas_twisted[128])
8989
/* This must be kept in sync with the HOL-Light specification
90-
* in proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml */
90+
* in proofs/hol_light/aarch64/proofs/mlkem_poly_mulcache_compute.ml */
9191
__contract__(
9292
requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
9393
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
@@ -100,7 +100,7 @@ __contract__(
100100
#define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)
101101
void mlk_poly_tobytes_asm(uint8_t r[384], const int16_t a[256])
102102
/* This must be kept in sync with the HOL-Light specification
103-
* in proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml */
103+
* in proofs/hol_light/aarch64/proofs/mlkem_poly_tobytes.ml */
104104
__contract__(
105105
requires(memory_no_alias(r, MLKEM_POLYBYTES))
106106
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
@@ -114,7 +114,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
114114
int16_t r[256], const int16_t a[512], const int16_t b[512],
115115
const int16_t b_cache[256])
116116
/* This must be kept in sync with the HOL-Light specification in
117-
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
117+
* proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
118118
*/
119119
__contract__(
120120
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -131,7 +131,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
131131
int16_t r[256], const int16_t a[768], const int16_t b[768],
132132
const int16_t b_cache[384])
133133
/* This must be kept in sync with the HOL-Light specification in
134-
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
134+
* proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
135135
*/
136136
__contract__(
137137
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -148,7 +148,7 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
148148
int16_t r[256], const int16_t a[1024], const int16_t b[1024],
149149
const int16_t b_cache[512])
150150
/* This must be kept in sync with the HOL-Light specification in
151-
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
151+
* proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
152152
*/
153153
__contract__(
154154
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
@@ -163,7 +163,7 @@ __contract__(
163163
uint64_t mlk_rej_uniform_asm(int16_t r[256], const uint8_t *buf,
164164
unsigned buflen, const uint8_t table[2048])
165165
/* This must be kept in sync with the HOL-Light specification
166-
* in proofs/hol_light/arm/proofs/mlkem_rej_uniform.ml. */
166+
* in proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml. */
167167
__contract__(
168168
requires(buflen % 24 == 0)
169169
requires(memory_no_alias(buf, buflen))

0 commit comments

Comments
 (0)