Skip to content

Commit 248fe13

Browse files
mkannwischermkannwischer
committed
Extended API: Adjust CBMC proofs
Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent eb80797 commit 248fe13

File tree

45 files changed

+1286
-35
lines changed

Some content is hidden

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

45 files changed

+1286
-35
lines changed

‎mlkem/indcpa.c

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ void mlk_indcpa_parse_pk(mlk_indcpa_public_key *pks,
9090
{
9191
mlk_polyvec_frombytes(pks->pkpv, pk);
9292
memcpy(pks->seed, pk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES);
93-
mlk_gen_matrix(pks->at, pks->seed, 1);
93+
mlk_gen_matrix(pks->at, pk + MLKEM_POLYVECBYTES, 1);
9494

9595
/* NOTE: If a modulus check was conducted on the PK, we know at this
9696
* point that the coefficients of `pk` are unsigned canonical. The
@@ -200,6 +200,14 @@ __contract__(
200200
#endif /* !MLK_USE_NATIVE_NTT_CUSTOM_ORDER */
201201

202202
static void mlk_transpose_matrix(mlk_polymat a)
203+
__contract__(
204+
requires(memory_no_alias(a, MLKEM_K*MLKEM_K*sizeof(mlk_poly)))
205+
requires(forall(k0, 0, MLKEM_K * MLKEM_K,
206+
array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
207+
assigns(memory_slice(a, MLKEM_K*MLKEM_K*sizeof(mlk_poly)))
208+
ensures(forall(k0, 0, MLKEM_K * MLKEM_K,
209+
array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
210+
)
203211
{
204212
unsigned int i, j, k;
205213
int16_t t;
@@ -334,7 +342,7 @@ __contract__(
334342
requires(memory_no_alias(vc, sizeof(mlk_polyvec_mulcache)))
335343
requires(forall(k0, 0, MLKEM_K * MLKEM_K,
336344
array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
337-
assigns(object_whole(out)))
345+
assigns(memory_slice(out, sizeof(mlk_polyvec))))
338346
{
339347
unsigned i;
340348
for (i = 0; i < MLKEM_K; i++)

‎mlkem/indcpa.h

Lines changed: 49 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -37,22 +37,52 @@ typedef struct
3737
#define mlk_indcpa_marshal_pk MLK_NAMESPACE_K(indcpa_marshal_pk)
3838
MLK_INTERNAL_API
3939
void mlk_indcpa_marshal_pk(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
40-
const mlk_indcpa_public_key *pks);
40+
const mlk_indcpa_public_key *pks)
41+
__contract__(
42+
requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES))
43+
requires(memory_no_alias(pks, sizeof(mlk_indcpa_public_key)))
44+
requires(forall(k0, 0, MLKEM_K,
45+
array_bound(pks->pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
46+
assigns(object_whole(pk))
47+
);
4148

4249
#define mlk_indcpa_parse_pk MLK_NAMESPACE_K(indcpa_parse_pk)
4350
MLK_INTERNAL_API
4451
void mlk_indcpa_parse_pk(mlk_indcpa_public_key *pks,
45-
const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES]);
52+
const uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES])
53+
__contract__(
54+
requires(memory_no_alias(pks, sizeof(mlk_indcpa_public_key)))
55+
requires(memory_no_alias(pk, MLKEM_INDCPA_PUBLICKEYBYTES))
56+
assigns(memory_slice(pks, sizeof(mlk_indcpa_public_key)))
57+
ensures(forall(k1, 0, MLKEM_K,
58+
array_bound(pks->pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
59+
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
60+
array_bound(pks->at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
61+
);
4662

4763
#define mlk_indcpa_marshal_sk MLK_NAMESPACE_K(indcpa_marshal_sk)
4864
MLK_INTERNAL_API
4965
void mlk_indcpa_marshal_sk(uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES],
50-
const mlk_indcpa_secret_key *sks);
66+
const mlk_indcpa_secret_key *sks)
67+
__contract__(
68+
requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES))
69+
requires(memory_no_alias(sks, sizeof(mlk_indcpa_secret_key)))
70+
requires(forall(k0, 0, MLKEM_K,
71+
array_bound(sks->skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
72+
assigns(object_whole(sk))
73+
);
5174

5275
#define mlk_indcpa_parse_sk MLK_NAMESPACE_K(indcpa_parse_sk)
5376
MLK_INTERNAL_API
5477
void mlk_indcpa_parse_sk(mlk_indcpa_secret_key *sks,
55-
const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES]);
78+
const uint8_t sk[MLKEM_INDCPA_SECRETKEYBYTES])
79+
__contract__(
80+
requires(memory_no_alias(sks, sizeof(mlk_indcpa_secret_key)))
81+
requires(memory_no_alias(sk, MLKEM_INDCPA_SECRETKEYBYTES))
82+
assigns(memory_slice(sks, sizeof(mlk_indcpa_secret_key)))
83+
ensures(forall(k0, 0, MLKEM_K,
84+
array_bound(sks->skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
85+
);
5686

5787
#define mlk_gen_matrix MLK_NAMESPACE_K(gen_matrix)
5888
/*************************************************
@@ -79,7 +109,7 @@ __contract__(
79109
requires(memory_no_alias(a, sizeof(mlk_polymat)))
80110
requires(memory_no_alias(seed, MLKEM_SYMBYTES))
81111
requires(transposed == 0 || transposed == 1)
82-
assigns(object_whole(a))
112+
assigns(memory_slice(a, sizeof(mlk_poly) * MLKEM_K * MLKEM_K))
83113
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
84114
array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
85115
);
@@ -109,8 +139,14 @@ __contract__(
109139
requires(memory_no_alias(pk, sizeof(mlk_indcpa_public_key)))
110140
requires(memory_no_alias(sk, sizeof(mlk_indcpa_secret_key)))
111141
requires(memory_no_alias(coins, MLKEM_SYMBYTES))
112-
assigns(object_whole(pk))
113-
assigns(object_whole(sk))
142+
assigns(memory_slice(pk, sizeof(mlk_indcpa_public_key)))
143+
assigns(memory_slice(sk, sizeof(mlk_indcpa_secret_key)))
144+
ensures(forall(k0, 0, MLKEM_K,
145+
array_bound(pk->pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
146+
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
147+
array_bound(pk->at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
148+
ensures(forall(k1, 0, MLKEM_K,
149+
array_bound(sk->skpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
114150
);
115151

116152
#define mlk_indcpa_enc MLK_NAMESPACE_K(indcpa_enc)
@@ -142,6 +178,10 @@ __contract__(
142178
requires(memory_no_alias(c, MLKEM_INDCPA_BYTES))
143179
requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES))
144180
requires(memory_no_alias(pk, sizeof(mlk_indcpa_public_key)))
181+
requires(forall(k0, 0, MLKEM_K,
182+
array_bound(pk->pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
183+
requires(forall(x, 0, MLKEM_K * MLKEM_K,
184+
array_bound(pk->at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
145185
requires(memory_no_alias(coins, MLKEM_SYMBYTES))
146186
assigns(object_whole(c))
147187
);
@@ -171,6 +211,8 @@ __contract__(
171211
requires(memory_no_alias(c, MLKEM_INDCPA_BYTES))
172212
requires(memory_no_alias(m, MLKEM_INDCPA_MSGBYTES))
173213
requires(memory_no_alias(sk, sizeof(mlk_indcpa_secret_key)))
214+
requires(forall(k0, 0, MLKEM_K,
215+
array_bound(sk->skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
174216
assigns(object_whole(m))
175217
);
176218

‎mlkem/kem.c

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -291,7 +291,6 @@ int crypto_kem_keypair_derand_struct(mlk_public_key *pk, mlk_secret_key *sk,
291291
MLK_CT_TESTING_DECLASSIFY((uint8_t *)(&pks->indcpa_pk),
292292
sizeof(mlk_indcpa_public_key));
293293

294-
295294
/* Specification: Partially implements
296295
* [FIPS 203, Section 3.3, Destruction of intermediate values] */
297296
mlk_zeroize(pks, sizeof(pks));
@@ -522,6 +521,8 @@ int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
522521
}
523522

524523
res = crypto_kem_dec_struct(ss, ct, &sks);
524+
/* Specification: Partially implements
525+
* [FIPS 203, Section 3.3, Destruction of intermediate values] */
525526
mlk_zeroize(&sks, sizeof(mlk_secret_key));
526527
return res;
527528
}
@@ -531,7 +532,13 @@ MLK_MUST_CHECK_RETURN_VALUE
531532
int crypto_kem_sk_from_seed(mlk_secret_key *sk,
532533
const uint8_t coins[2 * MLKEM_SYMBYTES])
533534
{
534-
return crypto_kem_keypair_derand_struct(NULL, sk, coins);
535+
mlk_public_key pk;
536+
int ret;
537+
ret = crypto_kem_keypair_derand_struct(&pk, sk, coins);
538+
/* Specification: Partially implements
539+
* [FIPS 203, Section 3.3, Destruction of intermediate values] */
540+
mlk_zeroize(&pk, sizeof(mlk_public_key));
541+
return ret;
535542
}
536543

537544
MLK_EXTERNAL_API

‎mlkem/kem.h

Lines changed: 141 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -81,60 +81,189 @@ typedef struct
8181

8282
MLK_EXTERNAL_API
8383
void crypto_kem_marshal_pk(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
84-
const mlk_public_key *pks);
84+
const mlk_public_key *pks)
85+
__contract__(
86+
requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
87+
requires(memory_no_alias(pks, sizeof(mlk_public_key)))
88+
requires(forall(k0, 0, MLKEM_K,
89+
array_bound(pks->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
90+
assigns(object_whole(pk))
91+
);
8592

8693
MLK_EXTERNAL_API
8794
MLK_MUST_CHECK_RETURN_VALUE
8895
int crypto_kem_parse_pk(mlk_public_key *pks,
89-
const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES]);
96+
const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
97+
__contract__(
98+
requires(memory_no_alias(pks, sizeof(mlk_public_key)))
99+
requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
100+
assigns(object_whole(pks))
101+
ensures(forall(k0, 0, MLKEM_K,
102+
array_bound(pks->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
103+
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
104+
array_bound(pks->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
105+
);
90106

91107

92108
MLK_EXTERNAL_API
93109
void crypto_kem_marshal_sk(uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
94-
const mlk_secret_key *sks);
110+
const mlk_secret_key *sks)
111+
__contract__(
112+
requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
113+
requires(memory_no_alias(sks, sizeof(mlk_secret_key)))
114+
requires(forall(k0, 0, MLKEM_K,
115+
array_bound(sks->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
116+
requires(forall(k1, 0, MLKEM_K,
117+
array_bound(sks->indcpa_sk.skpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
118+
assigns(object_whole(sk))
119+
);
95120

96121
MLK_EXTERNAL_API
97122
MLK_MUST_CHECK_RETURN_VALUE
98123
int crypto_kem_parse_sk(mlk_secret_key *sks,
99-
const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES]);
124+
const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
125+
__contract__(
126+
requires(memory_no_alias(sks, sizeof(mlk_secret_key)))
127+
requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
128+
assigns(object_whole(sks))
129+
ensures(forall(k0, 0, MLKEM_K,
130+
array_bound(sks->indcpa_sk.skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
131+
ensures(forall(k1, 0, MLKEM_K,
132+
array_bound(sks->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
133+
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
134+
array_bound(sks->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
135+
);
100136

101137

102138
MLK_EXTERNAL_API
103139
MLK_MUST_CHECK_RETURN_VALUE
104140
int crypto_kem_keypair_derand_struct(mlk_public_key *pk, mlk_secret_key *sk,
105-
const uint8_t coins[2 * MLKEM_SYMBYTES]);
141+
const uint8_t coins[2 * MLKEM_SYMBYTES])
142+
__contract__(
143+
requires(memory_no_alias(pk, sizeof(mlk_public_key)))
144+
requires(memory_no_alias(sk, sizeof(mlk_secret_key)))
145+
requires(memory_no_alias(coins, 2 * MLKEM_SYMBYTES))
146+
assigns(object_whole(pk))
147+
assigns(object_whole(sk))
148+
ensures(forall(k0, 0, MLKEM_K,
149+
array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
150+
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
151+
array_bound(pk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
152+
ensures(forall(k1, 0, MLKEM_K,
153+
array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
154+
ensures(forall(k2, 0, MLKEM_K,
155+
array_bound(sk->indcpa_sk.skpv[k2].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
156+
ensures(forall(y, 0, MLKEM_K * MLKEM_K,
157+
array_bound(sk->indcpa_pk.at[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
158+
);
106159

107160
MLK_EXTERNAL_API
108161
MLK_MUST_CHECK_RETURN_VALUE
109-
int crypto_kem_keypair_struct(mlk_public_key *pk, mlk_secret_key *sk);
162+
int crypto_kem_keypair_struct(mlk_public_key *pk, mlk_secret_key *sk)
163+
__contract__(
164+
requires(memory_no_alias(pk, sizeof(mlk_public_key)))
165+
requires(memory_no_alias(sk, sizeof(mlk_secret_key)))
166+
assigns(object_whole(pk))
167+
assigns(object_whole(sk))
168+
ensures(forall(k0, 0, MLKEM_K,
169+
array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
170+
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
171+
array_bound(pk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
172+
ensures(forall(k1, 0, MLKEM_K,
173+
array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
174+
ensures(forall(k2, 0, MLKEM_K,
175+
array_bound(sk->indcpa_sk.skpv[k2].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
176+
ensures(forall(y, 0, MLKEM_K * MLKEM_K,
177+
array_bound(sk->indcpa_pk.at[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
178+
);
179+
110180

111181
MLK_EXTERNAL_API
112182
MLK_MUST_CHECK_RETURN_VALUE
113183
int crypto_kem_enc_derand_struct(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
114184
uint8_t ss[MLKEM_SSBYTES],
115185
const mlk_public_key *pk,
116-
const uint8_t coins[MLKEM_SYMBYTES]);
186+
const uint8_t coins[MLKEM_SYMBYTES])
187+
__contract__(
188+
requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
189+
requires(memory_no_alias(ss, MLKEM_SSBYTES))
190+
requires(memory_no_alias(pk, sizeof(mlk_public_key)))
191+
requires(memory_no_alias(coins, MLKEM_SYMBYTES))
192+
requires(forall(k0, 0, MLKEM_K,
193+
array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
194+
requires(forall(x, 0, MLKEM_K * MLKEM_K,
195+
array_bound(pk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
196+
assigns(object_whole(ct))
197+
assigns(object_whole(ss))
198+
);
117199

118200
MLK_EXTERNAL_API
119201
MLK_MUST_CHECK_RETURN_VALUE
120202
int crypto_kem_enc_struct(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
121-
uint8_t ss[MLKEM_SSBYTES], const mlk_public_key *pk);
203+
uint8_t ss[MLKEM_SSBYTES], const mlk_public_key *pk)
204+
__contract__(
205+
requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
206+
requires(memory_no_alias(ss, MLKEM_SSBYTES))
207+
requires(memory_no_alias(pk, sizeof(mlk_public_key)))
208+
requires(forall(k0, 0, MLKEM_K,
209+
array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
210+
requires(forall(x, 0, MLKEM_K * MLKEM_K,
211+
array_bound(pk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
212+
assigns(object_whole(ct))
213+
assigns(object_whole(ss))
214+
);
122215

123216
MLK_EXTERNAL_API
124217
MLK_MUST_CHECK_RETURN_VALUE
125218
int crypto_kem_dec_struct(uint8_t ss[MLKEM_SSBYTES],
126219
const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
127-
const mlk_secret_key *sk);
128-
220+
const mlk_secret_key *sk)
221+
__contract__(
222+
requires(memory_no_alias(ss, MLKEM_SSBYTES))
223+
requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
224+
requires(memory_no_alias(sk, sizeof(mlk_secret_key)))
225+
requires(forall(k0, 0, MLKEM_K,
226+
array_bound(sk->indcpa_sk.skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
227+
requires(forall(k1, 0, MLKEM_K,
228+
array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
229+
requires(forall(x, 0, MLKEM_K * MLKEM_K,
230+
array_bound(sk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
231+
assigns(object_whole(ss))
232+
);
129233

130234
MLK_EXTERNAL_API
131235
MLK_MUST_CHECK_RETURN_VALUE
132236
int crypto_kem_sk_from_seed(mlk_secret_key *sk,
133-
const uint8_t coins[2 * MLKEM_SYMBYTES]);
237+
const uint8_t coins[2 * MLKEM_SYMBYTES])
238+
__contract__(
239+
requires(memory_no_alias(sk, sizeof(mlk_secret_key)))
240+
requires(memory_no_alias(coins, 2 * MLKEM_SYMBYTES))
241+
assigns(object_whole(sk))
242+
assigns(object_whole(coins))
243+
ensures(forall(k0, 0, MLKEM_K,
244+
array_bound(sk->indcpa_sk.skpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
245+
ensures(forall(k1, 0, MLKEM_K,
246+
array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
247+
ensures(forall(x, 0, MLKEM_K * MLKEM_K,
248+
array_bound(sk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
249+
);
134250

135251
MLK_EXTERNAL_API
136252
MLK_MUST_CHECK_RETURN_VALUE
137-
int crypto_kem_pk_from_sk(mlk_public_key *pk, const mlk_secret_key *sk);
253+
int crypto_kem_pk_from_sk(mlk_public_key *pk, const mlk_secret_key *sk)
254+
__contract__(
255+
requires(memory_no_alias(pk, sizeof(mlk_public_key)))
256+
requires(memory_no_alias(sk, sizeof(mlk_secret_key)))
257+
requires(forall(k1, 0, MLKEM_K,
258+
array_bound(sk->indcpa_pk.pkpv[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
259+
requires(forall(x, 0, MLKEM_K * MLKEM_K,
260+
array_bound(sk->indcpa_pk.at[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
261+
assigns(object_whole(pk))
262+
ensures(forall(k0, 0, MLKEM_K,
263+
array_bound(pk->indcpa_pk.pkpv[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
264+
ensures(forall(y, 0, MLKEM_K * MLKEM_K,
265+
array_bound(pk->indcpa_pk.at[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
266+
);
138267

139268
/*************************************************
140269
* Name: crypto_kem_keypair_derand

0 commit comments

Comments
 (0)