Skip to content

Commit 285fc8a

Browse files
mkannwischermkannwischer
committed
Run autogen and format
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent 0fca210 commit 285fc8a

6 files changed

Lines changed: 56 additions & 38 deletions

File tree

‎mlkem/mlkem_native.c‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,9 @@
204204
#undef MLK_CONTEXT_PARAMETERS_2
205205
#undef MLK_CONTEXT_PARAMETERS_3
206206
#undef MLK_CONTEXT_PARAMETERS_4
207+
#undef MLK_CONTEXT_PARAMETERS_5
208+
#undef MLK_CONTEXT_PARAMETERS_6
209+
#undef MLK_CONTEXT_PARAMETERS_7
207210
#undef MLK_EMPTY_CU
208211
#undef MLK_ERR_FAIL
209212
#undef MLK_ERR_OUT_OF_MEMORY
@@ -224,14 +227,21 @@
224227
#undef mlk_gen_matrix
225228
#undef mlk_indcpa_dec
226229
#undef mlk_indcpa_enc
230+
#undef mlk_indcpa_enc_u
231+
#undef mlk_indcpa_enc_v
227232
#undef mlk_indcpa_keypair_derand
228233
/* mlkem/src/kem.h */
234+
#undef MLKEM_EPP_BYTES
235+
#undef MLKEM_POLY16_BYTES
236+
#undef MLKEM_POLYVEC16_BYTES
229237
#undef MLK_KEM_H
230238
#undef mlk_kem_check_pk
231239
#undef mlk_kem_check_sk
232240
#undef mlk_kem_dec
233241
#undef mlk_kem_enc
234242
#undef mlk_kem_enc_derand
243+
#undef mlk_kem_enc_derand_u
244+
#undef mlk_kem_enc_v
235245
#undef mlk_kem_keypair
236246
#undef mlk_kem_keypair_derand
237247
/* mlkem/src/params.h */

‎mlkem/mlkem_native_asm.S‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -225,6 +225,9 @@
225225
#undef MLK_CONTEXT_PARAMETERS_2
226226
#undef MLK_CONTEXT_PARAMETERS_3
227227
#undef MLK_CONTEXT_PARAMETERS_4
228+
#undef MLK_CONTEXT_PARAMETERS_5
229+
#undef MLK_CONTEXT_PARAMETERS_6
230+
#undef MLK_CONTEXT_PARAMETERS_7
228231
#undef MLK_EMPTY_CU
229232
#undef MLK_ERR_FAIL
230233
#undef MLK_ERR_OUT_OF_MEMORY
@@ -245,14 +248,21 @@
245248
#undef mlk_gen_matrix
246249
#undef mlk_indcpa_dec
247250
#undef mlk_indcpa_enc
251+
#undef mlk_indcpa_enc_u
252+
#undef mlk_indcpa_enc_v
248253
#undef mlk_indcpa_keypair_derand
249254
/* mlkem/src/kem.h */
255+
#undef MLKEM_EPP_BYTES
256+
#undef MLKEM_POLY16_BYTES
257+
#undef MLKEM_POLYVEC16_BYTES
250258
#undef MLK_KEM_H
251259
#undef mlk_kem_check_pk
252260
#undef mlk_kem_check_sk
253261
#undef mlk_kem_dec
254262
#undef mlk_kem_enc
255263
#undef mlk_kem_enc_derand
264+
#undef mlk_kem_enc_derand_u
265+
#undef mlk_kem_enc_v
256266
#undef mlk_kem_keypair
257267
#undef mlk_kem_keypair_derand
258268
/* mlkem/src/params.h */

‎mlkem/src/kem.c‎

Lines changed: 21 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -391,8 +391,7 @@ static void mlk_serialize_epp(uint8_t out[MLKEM_EPP_BYTES], const mlk_poly *p)
391391
}
392392
}
393393

394-
static void mlk_deserialize_epp(mlk_poly *p,
395-
const uint8_t in[MLKEM_EPP_BYTES])
394+
static void mlk_deserialize_epp(mlk_poly *p, const uint8_t in[MLKEM_EPP_BYTES])
396395
{
397396
unsigned j;
398397
for (j = 0; j < MLKEM_N / 2; j++)
@@ -410,7 +409,7 @@ static void mlk_deserialize_epp(mlk_poly *p,
410409
* Stores each int16_t coefficient as 2 bytes in LE order.
411410
* Coefficients must be non-negative (e.g., after reduce). */
412411
static void mlk_serialize_polyvec_16le(uint8_t out[MLKEM_POLYVEC16_BYTES],
413-
const mlk_polyvec *v)
412+
const mlk_polyvec *v)
414413
{
415414
unsigned i, j;
416415
for (i = 0; i < MLKEM_K; i++)
@@ -430,8 +429,8 @@ static void mlk_serialize_polyvec_16le(uint8_t out[MLKEM_POLYVEC16_BYTES],
430429
}
431430
}
432431

433-
static void mlk_deserialize_polyvec_16le(mlk_polyvec *v,
434-
const uint8_t in[MLKEM_POLYVEC16_BYTES])
432+
static void mlk_deserialize_polyvec_16le(
433+
mlk_polyvec *v, const uint8_t in[MLKEM_POLYVEC16_BYTES])
435434
{
436435
unsigned i, j;
437436
for (i = 0; i < MLKEM_K; i++)
@@ -444,22 +443,22 @@ static void mlk_deserialize_polyvec_16le(mlk_polyvec *v,
444443
assigns(j, memory_slice(v, sizeof(mlk_polyvec)))
445444
invariant(j <= MLKEM_N))
446445
{
447-
v->vec[i].coeffs[j] = mlk_cast_uint16_to_int16((uint16_t)(
448-
(unsigned)in[i * MLKEM_POLY16_BYTES + 2 * j] |
449-
((unsigned)in[i * MLKEM_POLY16_BYTES + 2 * j + 1] << 8)));
446+
v->vec[i].coeffs[j] = mlk_cast_uint16_to_int16(
447+
(uint16_t)((unsigned)in[i * MLKEM_POLY16_BYTES + 2 * j] |
448+
((unsigned)in[i * MLKEM_POLY16_BYTES + 2 * j + 1] << 8)));
450449
}
451450
}
452451
}
453452

454453
MLK_INTERNAL_API
455454
int mlk_kem_enc_derand_u(uint8_t ct_u[MLKEM_POLYVECCOMPRESSEDBYTES_DU],
456-
uint8_t ss[MLKEM_SSBYTES],
457-
uint8_t sp_serial[MLKEM_POLYVEC16_BYTES],
458-
uint8_t epp_serial[MLKEM_EPP_BYTES],
459-
const uint8_t seed[MLKEM_SYMBYTES],
460-
const uint8_t hpk[MLKEM_SYMBYTES],
461-
const uint8_t coins[MLKEM_SYMBYTES],
462-
MLK_CONFIG_CONTEXT_PARAMETER_TYPE context)
455+
uint8_t ss[MLKEM_SSBYTES],
456+
uint8_t sp_serial[MLKEM_POLYVEC16_BYTES],
457+
uint8_t epp_serial[MLKEM_EPP_BYTES],
458+
const uint8_t seed[MLKEM_SYMBYTES],
459+
const uint8_t hpk[MLKEM_SYMBYTES],
460+
const uint8_t coins[MLKEM_SYMBYTES],
461+
MLK_CONFIG_CONTEXT_PARAMETER_TYPE context)
463462
{
464463
int ret = 0;
465464
MLK_ALLOC(buf, uint8_t, 2 * MLKEM_SYMBYTES, context);
@@ -507,11 +506,11 @@ int mlk_kem_enc_derand_u(uint8_t ct_u[MLKEM_POLYVECCOMPRESSEDBYTES_DU],
507506

508507
MLK_INTERNAL_API
509508
int mlk_kem_enc_v(uint8_t ct_v[MLKEM_POLYCOMPRESSEDBYTES_DV],
510-
const uint8_t sp_serial[MLKEM_POLYVEC16_BYTES],
511-
const uint8_t epp_serial[MLKEM_EPP_BYTES],
512-
const uint8_t coins[MLKEM_SYMBYTES],
513-
const uint8_t ek_vector[MLKEM_POLYVECBYTES],
514-
MLK_CONFIG_CONTEXT_PARAMETER_TYPE context)
509+
const uint8_t sp_serial[MLKEM_POLYVEC16_BYTES],
510+
const uint8_t epp_serial[MLKEM_EPP_BYTES],
511+
const uint8_t coins[MLKEM_SYMBYTES],
512+
const uint8_t ek_vector[MLKEM_POLYVECBYTES],
513+
MLK_CONFIG_CONTEXT_PARAMETER_TYPE context)
515514
{
516515
int ret = 0;
517516
MLK_ALLOC(sp, mlk_polyvec, 1, context);
@@ -530,9 +529,8 @@ int mlk_kem_enc_v(uint8_t ct_v[MLKEM_POLYCOMPRESSEDBYTES_DV],
530529
mlk_polyvec_frombytes(p, ek_vector);
531530
mlk_polyvec_reduce(p);
532531
mlk_polyvec_tobytes(p_reencoded, p);
533-
ret =
534-
mlk_ct_memcmp(ek_vector, p_reencoded, MLKEM_POLYVECBYTES) ? MLK_ERR_FAIL
535-
: 0;
532+
ret = mlk_ct_memcmp(ek_vector, p_reencoded, MLKEM_POLYVECBYTES) ? MLK_ERR_FAIL
533+
: 0;
536534
if (ret != 0)
537535
{
538536
goto cleanup;

‎mlkem/src/kem.h‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -338,13 +338,13 @@ __contract__(
338338
MLK_INTERNAL_API
339339
MLK_MUST_CHECK_RETURN_VALUE
340340
int mlk_kem_enc_derand_u(uint8_t ct_u[MLKEM_POLYVECCOMPRESSEDBYTES_DU],
341-
uint8_t ss[MLKEM_SSBYTES],
342-
uint8_t sp_serial[MLKEM_POLYVEC16_BYTES],
343-
uint8_t epp_serial[MLKEM_EPP_BYTES],
344-
const uint8_t seed[MLKEM_SYMBYTES],
345-
const uint8_t hpk[MLKEM_SYMBYTES],
346-
const uint8_t coins[MLKEM_SYMBYTES],
347-
MLK_CONFIG_CONTEXT_PARAMETER_TYPE context)
341+
uint8_t ss[MLKEM_SSBYTES],
342+
uint8_t sp_serial[MLKEM_POLYVEC16_BYTES],
343+
uint8_t epp_serial[MLKEM_EPP_BYTES],
344+
const uint8_t seed[MLKEM_SYMBYTES],
345+
const uint8_t hpk[MLKEM_SYMBYTES],
346+
const uint8_t coins[MLKEM_SYMBYTES],
347+
MLK_CONFIG_CONTEXT_PARAMETER_TYPE context)
348348
__contract__(
349349
requires(memory_no_alias(ct_u, MLKEM_POLYVECCOMPRESSEDBYTES_DU))
350350
requires(memory_no_alias(ss, MLKEM_SSBYTES))
@@ -399,11 +399,11 @@ __contract__(
399399
MLK_INTERNAL_API
400400
MLK_MUST_CHECK_RETURN_VALUE
401401
int mlk_kem_enc_v(uint8_t ct_v[MLKEM_POLYCOMPRESSEDBYTES_DV],
402-
const uint8_t sp_serial[MLKEM_POLYVEC16_BYTES],
403-
const uint8_t epp_serial[MLKEM_EPP_BYTES],
404-
const uint8_t coins[MLKEM_SYMBYTES],
405-
const uint8_t ek_vector[MLKEM_POLYVECBYTES],
406-
MLK_CONFIG_CONTEXT_PARAMETER_TYPE context)
402+
const uint8_t sp_serial[MLKEM_POLYVEC16_BYTES],
403+
const uint8_t epp_serial[MLKEM_EPP_BYTES],
404+
const uint8_t coins[MLKEM_SYMBYTES],
405+
const uint8_t ek_vector[MLKEM_POLYVECBYTES],
406+
MLK_CONFIG_CONTEXT_PARAMETER_TYPE context)
407407
__contract__(
408408
requires(memory_no_alias(ct_v, MLKEM_POLYCOMPRESSEDBYTES_DV))
409409
requires(memory_no_alias(sp_serial, MLKEM_POLYVEC16_BYTES))

‎proofs/cbmc/kem_enc_derand_u/kem_enc_derand_u_harness.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,5 @@ void harness(void)
88
uint8_t *ct_u, *ss, *sp_serial, *epp_serial;
99
uint8_t *seed, *hpk, *coins;
1010
mlk_kem_enc_derand_u(ct_u, ss, sp_serial, epp_serial, seed, hpk, coins,
11-
NULL /* context will be dropped by preprocessor */);
11+
NULL /* context will be dropped by preprocessor */);
1212
}

‎test/src/test_mlkem.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -200,8 +200,8 @@ static int test_incremental_enc(void)
200200
/* Incremental encapsulation via KEM-level API */
201201
CHECK(mlk_kem_enc_derand_u(ct_u, ss, sp_serial, epp_serial, ek_seed, hpk,
202202
enc_coins, 0) == 0);
203-
CHECK(mlk_kem_enc_v(ct_v, sp_serial, epp_serial, enc_coins, ek_vector,
204-
0) == 0);
203+
CHECK(mlk_kem_enc_v(ct_v, sp_serial, epp_serial, enc_coins, ek_vector, 0) ==
204+
0);
205205

206206
/* Verify ct_u || ct_v matches reference ciphertext */
207207
MLK_CT_TESTING_DECLASSIFY(ct_u, MLKEM_POLYVECCOMPRESSEDBYTES_DU);

0 commit comments

Comments
 (0)