Skip to content

Commit d370ad7

Browse files
willieyzhanno-becker
willieyz
authored and
hanno-becker
committed
CBMC: Add x86-64 HOL-Light-based contracts and proofs
- This commit introduces CBMC verification for several x86-64 optimized assembly functions. The contracts for these functions are derived from their corresponding HOL-Light correctness proofs. - For each assembly function, a CBMC contract has been added to `arith_native_x86_64.h`. Additionally, new proof harnesses have been creat to formally verify that the generic C implementations (`*_native`) correctly utilize these assembly backends and adhere to the top-level API contracts. - The following functions now have CBMC proofs based on their HOL-Light specifications: - polyvec_basemul_acc_montgomery_cached_asm_k2/k3/k4: - Pre-conditions: `<= &2 pow 12`(HOL_LIGHT) v.s. `MLKEM_UINT12_LIMIT + 1`(CBMC) - Adds a CBMC pre-condition: `requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT +` `1))` - ntt_avx2: - Pre-condition: `<= &8191`(HOL_LIGHT) v.s. `8191 + 1`(CBMC) - Post-condition: `<= &23594`(HOL_LIGHT) v.s. `23594 + 1`(CBMC) - Adds a CBMC pre-condition: `requires(array_abs_bound(r, 0, MLKEM_N, 8192))` - Adds a CBMC post-condition: `ensures(array_abs_bound(r, 0, MLKEM_N, 23595))` - intt_avx2: - Post-condition: `<= &26631` v.s. `26631 + 1`(CBMC) - Adds a CBMC post-condition: `ensures(array_abs_bound(r, 0, MLKEM_N, 26632))` - reduce_avx2: - Post-condition: `< &3329`(HOL_LIGHT) v.s. `3329 == MLKEM_Q`(CBMC) - Adds a CBMC post-condition: `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` - tobytes_avx2: - Pre-condition: `(!i. i < LENGTH l ==> val(EL i l) < 3329)`(HOL_LIGHT) v.s. `MLKEM_UINT12_LIMIT`(CBMC) - Adds a CBMC pre-condition: `requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))` - frombytes_avx2: - Post-conditions: `read (memory :> bytes(a,dimindex(:32) * 12)) s0 = num_of_wordlist (l:(12 word)list)` - Adds a CBMC post-condition: `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))` - mlk_rej_uniform_asm: - This proof are reference from aarch64 one, and change requires: `requires(buflen % 24 == 0)` to `requires(buflen % 12 == 0)` - mlk_tomont_avx2: - Post conditions: `(ival z_i == (tomont_3329 (ival o x)) i) (mod &3329) /\ abs(ival z_i) <= &3328)` v.s. `ensures(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))` - Add a CBMC post-condition: `ensures(array_abs_bound(r, 0, MLKEM_N, 3328 + 1))` - mlk_poly_mulcache_compute_avx2: - Post conditions: ``` (ival zi == avx2_mulcache (ival o x) i) (mod &3329)) /\ (abs(ival zi) <= &3328)) ``` v.s. `ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))` - Add a CBMC post-condition: `ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))` - mlk_nttunpack_avx2: - Pre-condition: `read(memory :> bytes(a, 512)) s = num_of_wordlist (unpermute_list l)` v.s. `requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` - Post-condition: `read(memory :> bytes(a, 512)) s = num_of_wordlist (unpermute_list l)))` v.s. `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` - Add CBMC pre-condition and post-condition: `requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` Signed-off-by: willieyz <willie.zhao@chelpis.com>
1 parent 180a401 commit d370ad7

File tree

27 files changed

+1163
-33
lines changed

27 files changed

+1163
-33
lines changed

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 130 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7,65 +7,179 @@
77

88
#include "../../../common.h"
99

10-
#include <immintrin.h>
1110
#include <stdint.h>
1211
#include "consts.h"
1312

1413
#define MLK_AVX2_REJ_UNIFORM_BUFLEN \
1514
(3 * 168) /* REJ_UNIFORM_NBLOCKS * SHAKE128_RATE */
1615

17-
#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
18-
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
19-
const uint8_t *table);
20-
2116
#define mlk_rej_uniform_table MLK_NAMESPACE(rej_uniform_table)
2217
extern const uint8_t mlk_rej_uniform_table[];
2318

19+
#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
20+
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
21+
const uint8_t *table)
22+
/* This must be kept in sync with the HOL-Light specification
23+
* in proofs/hol_light/x86/proofs/mlkem_rej_uniform.ml. */
24+
__contract__(
25+
requires(buflen % 12 == 0)
26+
requires(memory_no_alias(buf, buflen))
27+
requires(table == mlk_rej_uniform_table)
28+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
29+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
30+
ensures(return_value <= MLKEM_N)
31+
ensures(array_bound(r, 0, (unsigned) return_value, 0, MLKEM_Q))
32+
);
33+
2434
#define mlk_ntt_avx2 MLK_NAMESPACE(ntt_avx2)
25-
void mlk_ntt_avx2(int16_t *r, const int16_t *mlk_qdata);
35+
void mlk_ntt_avx2(int16_t *r, const int16_t *qdata)
36+
/* This must be kept in sync with the HOL-Light specification
37+
* in proofs/hol_light/x86/proofs/mlkem_ntt.ml */
38+
__contract__(
39+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
40+
requires(array_abs_bound(r, 0, MLKEM_N, 8192))
41+
requires(qdata == mlk_qdata)
42+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
43+
/* check-magic: off */
44+
ensures(array_abs_bound(r, 0, MLKEM_N, 23595))
45+
/* check-magic: on */
46+
);
2647

2748
#define mlk_invntt_avx2 MLK_NAMESPACE(invntt_avx2)
28-
void mlk_invntt_avx2(int16_t *r, const int16_t *mlk_qdata);
49+
void mlk_invntt_avx2(int16_t *r, const int16_t *qdata)
50+
/* This must be kept in sync with the HOL-Light specification
51+
* in proofs/hol_light/x86/proofs/mlkem_intt.ml */
52+
__contract__(
53+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
54+
requires(qdata == mlk_qdata)
55+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
56+
/* check-magic: off */
57+
ensures(array_abs_bound(r, 0, MLKEM_N, 26632))
58+
/* check-magic: on */
59+
);
2960

3061
#define mlk_nttunpack_avx2 MLK_NAMESPACE(nttunpack_avx2)
31-
void mlk_nttunpack_avx2(int16_t *r);
62+
void mlk_nttunpack_avx2(int16_t *r)
63+
/* This must be kept in sync with the HOL-Light specification
64+
* in proofs/hol_light/x86/proofs/mlkem_unpack.ml */
65+
__contract__(
66+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
67+
requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
68+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
69+
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
70+
);
3271

3372
#define mlk_reduce_avx2 MLK_NAMESPACE(reduce_avx2)
34-
void mlk_reduce_avx2(int16_t *r);
73+
void mlk_reduce_avx2(int16_t *r)
74+
/* This must be kept in sync with the HOL-Light specification
75+
* in proofs/hol_light/x86/proofs/mlkem_reduce.ml */
76+
__contract__(
77+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
78+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
79+
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
80+
);
3581

3682
#define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2)
3783
void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
38-
const int16_t *mlk_qdata);
84+
const int16_t *qdata)
85+
/* This must be kept in sync with the HOL-Light specification
86+
* in proofs/hol_light/x86/proofs/mlkem_mulcache_compute.ml */
87+
__contract__(
88+
requires(memory_no_alias(out, sizeof(int16_t) * (MLKEM_N / 2)))
89+
requires(memory_no_alias(in, sizeof(int16_t) * MLKEM_N))
90+
requires(qdata == mlk_qdata)
91+
assigns(memory_slice(out, sizeof(int16_t) * (MLKEM_N / 2)))
92+
ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))
93+
);
3994

4095
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
4196
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)
4297
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
4398
const int16_t *a,
4499
const int16_t *b,
45-
const int16_t *b_cache);
100+
const int16_t *b_cache)
101+
/* This must be kept in sync with the HOL-Light specification in
102+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
103+
*/
104+
__contract__(
105+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
106+
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
107+
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
108+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
109+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
110+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
111+
);
46112

47113
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
48114
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
49115
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
50116
const int16_t *a,
51117
const int16_t *b,
52-
const int16_t *b_cache);
118+
const int16_t *b_cache)
119+
/* This must be kept in sync with the HOL-Light specification in
120+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
121+
*/
122+
__contract__(
123+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
124+
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
125+
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
126+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
127+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
128+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
129+
);
53130

54131
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
55132
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
56133
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
57134
const int16_t *a,
58135
const int16_t *b,
59-
const int16_t *b_cache);
136+
const int16_t *b_cache)
137+
/* This must be kept in sync with the HOL-Light specification in
138+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
139+
*/
140+
__contract__(
141+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
142+
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
143+
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
144+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
145+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
146+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
147+
);
60148

61149
#define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2)
62-
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a);
150+
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a)
151+
/* This must be kept in sync with the HOL-Light specification in
152+
* proofs/hol_light/x86/proofs/mlkem_tobytes.ml.
153+
*/
154+
__contract__(
155+
requires(memory_no_alias(r, MLKEM_POLYBYTES))
156+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
157+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
158+
assigns(object_whole(r))
159+
);
63160

64161
#define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2)
65-
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a);
162+
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a)
163+
/* This must be kept in sync with the HOL-Light specification in
164+
* proofs/hol_light/x86/proofs/mlkem_frombytes.ml.
165+
*/
166+
__contract__(
167+
requires(memory_no_alias(a, MLKEM_POLYBYTES))
168+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
169+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
170+
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
171+
);
66172

67173
#define mlk_tomont_avx2 MLK_NAMESPACE(tomont_avx2)
68-
void mlk_tomont_avx2(int16_t *r);
174+
void mlk_tomont_avx2(int16_t *r)
175+
/* This must be kept in sync with the HOL-Light specification in
176+
* proofs/hol_light/x86/proofs/mlkem_tomont.ml.
177+
*/
178+
__contract__(
179+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
180+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
181+
ensures(array_abs_bound(r, 0, MLKEM_N, 3329))
182+
);
69183

70184
#define mlk_poly_compress_d4_avx2 MLK_NAMESPACE(poly_compress_d4_avx2)
71185
void mlk_poly_compress_d4_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],

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

Lines changed: 130 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7,65 +7,179 @@
77

88
#include "../../../common.h"
99

10-
#include <immintrin.h>
1110
#include <stdint.h>
1211
#include "consts.h"
1312

1413
#define MLK_AVX2_REJ_UNIFORM_BUFLEN \
1514
(3 * 168) /* REJ_UNIFORM_NBLOCKS * SHAKE128_RATE */
1615

17-
#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
18-
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
19-
const uint8_t *table);
20-
2116
#define mlk_rej_uniform_table MLK_NAMESPACE(rej_uniform_table)
2217
extern const uint8_t mlk_rej_uniform_table[];
2318

19+
#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
20+
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
21+
const uint8_t *table)
22+
/* This must be kept in sync with the HOL-Light specification
23+
* in proofs/hol_light/x86/proofs/mlkem_rej_uniform.ml. */
24+
__contract__(
25+
requires(buflen % 12 == 0)
26+
requires(memory_no_alias(buf, buflen))
27+
requires(table == mlk_rej_uniform_table)
28+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
29+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
30+
ensures(return_value <= MLKEM_N)
31+
ensures(array_bound(r, 0, (unsigned) return_value, 0, MLKEM_Q))
32+
);
33+
2434
#define mlk_ntt_avx2 MLK_NAMESPACE(ntt_avx2)
25-
void mlk_ntt_avx2(int16_t *r, const int16_t *mlk_qdata);
35+
void mlk_ntt_avx2(int16_t *r, const int16_t *qdata)
36+
/* This must be kept in sync with the HOL-Light specification
37+
* in proofs/hol_light/x86/proofs/mlkem_ntt.ml */
38+
__contract__(
39+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
40+
requires(array_abs_bound(r, 0, MLKEM_N, 8192))
41+
requires(qdata == mlk_qdata)
42+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
43+
/* check-magic: off */
44+
ensures(array_abs_bound(r, 0, MLKEM_N, 23595))
45+
/* check-magic: on */
46+
);
2647

2748
#define mlk_invntt_avx2 MLK_NAMESPACE(invntt_avx2)
28-
void mlk_invntt_avx2(int16_t *r, const int16_t *mlk_qdata);
49+
void mlk_invntt_avx2(int16_t *r, const int16_t *qdata)
50+
/* This must be kept in sync with the HOL-Light specification
51+
* in proofs/hol_light/x86/proofs/mlkem_intt.ml */
52+
__contract__(
53+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
54+
requires(qdata == mlk_qdata)
55+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
56+
/* check-magic: off */
57+
ensures(array_abs_bound(r, 0, MLKEM_N, 26632))
58+
/* check-magic: on */
59+
);
2960

3061
#define mlk_nttunpack_avx2 MLK_NAMESPACE(nttunpack_avx2)
31-
void mlk_nttunpack_avx2(int16_t *r);
62+
void mlk_nttunpack_avx2(int16_t *r)
63+
/* This must be kept in sync with the HOL-Light specification
64+
* in proofs/hol_light/x86/proofs/mlkem_unpack.ml */
65+
__contract__(
66+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
67+
requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
68+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
69+
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
70+
);
3271

3372
#define mlk_reduce_avx2 MLK_NAMESPACE(reduce_avx2)
34-
void mlk_reduce_avx2(int16_t *r);
73+
void mlk_reduce_avx2(int16_t *r)
74+
/* This must be kept in sync with the HOL-Light specification
75+
* in proofs/hol_light/x86/proofs/mlkem_reduce.ml */
76+
__contract__(
77+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
78+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
79+
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
80+
);
3581

3682
#define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2)
3783
void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
38-
const int16_t *mlk_qdata);
84+
const int16_t *qdata)
85+
/* This must be kept in sync with the HOL-Light specification
86+
* in proofs/hol_light/x86/proofs/mlkem_mulcache_compute.ml */
87+
__contract__(
88+
requires(memory_no_alias(out, sizeof(int16_t) * (MLKEM_N / 2)))
89+
requires(memory_no_alias(in, sizeof(int16_t) * MLKEM_N))
90+
requires(qdata == mlk_qdata)
91+
assigns(memory_slice(out, sizeof(int16_t) * (MLKEM_N / 2)))
92+
ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))
93+
);
3994

4095
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
4196
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)
4297
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
4398
const int16_t *a,
4499
const int16_t *b,
45-
const int16_t *b_cache);
100+
const int16_t *b_cache)
101+
/* This must be kept in sync with the HOL-Light specification in
102+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
103+
*/
104+
__contract__(
105+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
106+
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
107+
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
108+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
109+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
110+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
111+
);
46112

47113
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
48114
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
49115
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
50116
const int16_t *a,
51117
const int16_t *b,
52-
const int16_t *b_cache);
118+
const int16_t *b_cache)
119+
/* This must be kept in sync with the HOL-Light specification in
120+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
121+
*/
122+
__contract__(
123+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
124+
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
125+
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
126+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
127+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
128+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
129+
);
53130

54131
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
55132
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
56133
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
57134
const int16_t *a,
58135
const int16_t *b,
59-
const int16_t *b_cache);
136+
const int16_t *b_cache)
137+
/* This must be kept in sync with the HOL-Light specification in
138+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
139+
*/
140+
__contract__(
141+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
142+
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
143+
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
144+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
145+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
146+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
147+
);
60148

61149
#define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2)
62-
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a);
150+
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a)
151+
/* This must be kept in sync with the HOL-Light specification in
152+
* proofs/hol_light/x86/proofs/mlkem_tobytes.ml.
153+
*/
154+
__contract__(
155+
requires(memory_no_alias(r, MLKEM_POLYBYTES))
156+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
157+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
158+
assigns(object_whole(r))
159+
);
63160

64161
#define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2)
65-
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a);
162+
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a)
163+
/* This must be kept in sync with the HOL-Light specification in
164+
* proofs/hol_light/x86/proofs/mlkem_frombytes.ml.
165+
*/
166+
__contract__(
167+
requires(memory_no_alias(a, MLKEM_POLYBYTES))
168+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
169+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
170+
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
171+
);
66172

67173
#define mlk_tomont_avx2 MLK_NAMESPACE(tomont_avx2)
68-
void mlk_tomont_avx2(int16_t *r);
174+
void mlk_tomont_avx2(int16_t *r)
175+
/* This must be kept in sync with the HOL-Light specification in
176+
* proofs/hol_light/x86/proofs/mlkem_tomont.ml.
177+
*/
178+
__contract__(
179+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
180+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
181+
ensures(array_abs_bound(r, 0, MLKEM_N, 3329))
182+
);
69183

70184
#define mlk_poly_compress_d4_avx2 MLK_NAMESPACE(poly_compress_d4_avx2)
71185
void mlk_poly_compress_d4_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],

0 commit comments

Comments
 (0)