Skip to content

Commit

Permalink
Work around AeneasVerif/eurydice#12
Browse files Browse the repository at this point in the history
  • Loading branch information
@msprotz
msprotz committed May 30, 2024
1 parent af4e0cf commit a0b0b93
Show file tree
Hide file tree
Showing 8 changed files with 118 additions and 52 deletions.
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/eurydice_glue.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,8 @@ typedef struct {
.snd = EURYDICE_SLICE((element_type*)slice.ptr, mid, slice.len)})
#define core_slice___Slice_T___split_at_mut(slice, mid, element_type, ret_t) \
((ret_t){ \
.fst = EURYDICE_SLICE((element_type*)slice.ptr, 0, mid), \
.snd = EURYDICE_SLICE((element_type*)slice.ptr, mid, slice.len)})
.fst = { .ptr = slice.ptr, .len = mid }, \
.snd = { .ptr = slice.ptr + mid * sizeof(element_type), .len = slice.len - mid }})


// Can't have a flexible array as a member of a union -- this violates strict aliasing rules.
Expand Down
30 changes: 30 additions & 0 deletions libcrux-ml-kem/c/internal/libcrux_core.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,11 @@ libcrux_ml_kem_constant_time_ops_select_shared_secret_in_constant_time(

#define LIBCRUX_ML_KEM_CONSTANTS_H_DIGEST_SIZE ((size_t)32U)

libcrux_ml_kem_types_MlKemPublicKey____800size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___800size_t(
uint8_t value[800U]
);

libcrux_ml_kem_types_MlKemKeyPair____1632size_t__800size_t
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___1632size_t_800size_t(
libcrux_ml_kem_types_MlKemPrivateKey____1632size_t sk,
Expand All @@ -75,6 +80,11 @@ typedef struct K___uint8_t_768size_t__uint8_t_800size_t__s
}
K___uint8_t_768size_t__uint8_t_800size_t_;

libcrux_ml_kem_types_MlKemCiphertext____768size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___768size_t(
uint8_t value[768U]
);

uint8_t
*libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemPublicKey_SIZE__18__as_slice___800size_t(
libcrux_ml_kem_types_MlKemPublicKey____800size_t *self
Expand All @@ -101,6 +111,11 @@ libcrux_ml_kem_types___core__convert__AsRef__Slice_u8___for_libcrux_ml_kem__type
void
libcrux_ml_kem_ind_cpa_into_padded_array___800size_t(Eurydice_slice slice, uint8_t ret[800U]);

libcrux_ml_kem_types_MlKemPublicKey____1568size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1568size_t(
uint8_t value[1568U]
);

libcrux_ml_kem_types_MlKemKeyPair____3168size_t__1568size_t
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___3168size_t_1568size_t(
libcrux_ml_kem_types_MlKemPrivateKey____3168size_t sk,
Expand All @@ -119,6 +134,11 @@ typedef struct K___uint8_t_1536size_t__uint8_t_1568size_t__s
}
K___uint8_t_1536size_t__uint8_t_1568size_t_;

libcrux_ml_kem_types_MlKemCiphertext____1568size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___1568size_t(
uint8_t value[1568U]
);

uint8_t
*libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemPublicKey_SIZE__18__as_slice___1568size_t(
libcrux_ml_kem_types_MlKemPublicKey____1568size_t *self
Expand All @@ -138,6 +158,11 @@ libcrux_ml_kem_types___core__convert__AsRef__Slice_u8___for_libcrux_ml_kem__type
void
libcrux_ml_kem_ind_cpa_into_padded_array___1600size_t(Eurydice_slice slice, uint8_t ret[1600U]);

libcrux_ml_kem_types_MlKemPublicKey____1184size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1184size_t(
uint8_t value[1184U]
);

libcrux_ml_kem_types_MlKemKeyPair____2400size_t__1184size_t
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___2400size_t_1184size_t(
libcrux_ml_kem_types_MlKemPrivateKey____2400size_t sk,
Expand All @@ -156,6 +181,11 @@ typedef struct K___uint8_t_1152size_t__uint8_t_1184size_t__s
}
K___uint8_t_1152size_t__uint8_t_1184size_t_;

libcrux_ml_kem_types_MlKemCiphertext____1088size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___1088size_t(
uint8_t value[1088U]
);

uint8_t
*libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemPublicKey_SIZE__18__as_slice___1184size_t(
libcrux_ml_kem_types_MlKemPublicKey____1184size_t *self
Expand Down
72 changes: 72 additions & 0 deletions libcrux-ml-kem/c/libcrux_core.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,18 @@ libcrux_ml_kem_constant_time_ops_select_shared_secret_in_constant_time(
memcpy(ret, out, (size_t)32U * sizeof (uint8_t));
}

libcrux_ml_kem_types_MlKemPublicKey____800size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___800size_t(
uint8_t value[800U]
)
{
uint8_t uu____0[800U];
memcpy(uu____0, value, (size_t)800U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemPublicKey____800size_t lit;
memcpy(lit.value, uu____0, (size_t)800U * sizeof (uint8_t));
return lit;
}

libcrux_ml_kem_types_MlKemKeyPair____1632size_t__800size_t
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___1632size_t_800size_t(
libcrux_ml_kem_types_MlKemPrivateKey____1632size_t sk,
Expand All @@ -78,6 +90,18 @@ libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem_
return lit;
}

libcrux_ml_kem_types_MlKemCiphertext____768size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___768size_t(
uint8_t value[768U]
)
{
uint8_t uu____0[768U];
memcpy(uu____0, value, (size_t)768U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____768size_t lit;
memcpy(lit.value, uu____0, (size_t)768U * sizeof (uint8_t));
return lit;
}

uint8_t
*libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemPublicKey_SIZE__18__as_slice___800size_t(
libcrux_ml_kem_types_MlKemPublicKey____800size_t *self
Expand Down Expand Up @@ -134,6 +158,18 @@ libcrux_ml_kem_ind_cpa_into_padded_array___800size_t(Eurydice_slice slice, uint8
memcpy(ret, out, (size_t)800U * sizeof (uint8_t));
}

libcrux_ml_kem_types_MlKemPublicKey____1568size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1568size_t(
uint8_t value[1568U]
)
{
uint8_t uu____0[1568U];
memcpy(uu____0, value, (size_t)1568U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemPublicKey____1568size_t lit;
memcpy(lit.value, uu____0, (size_t)1568U * sizeof (uint8_t));
return lit;
}

libcrux_ml_kem_types_MlKemKeyPair____3168size_t__1568size_t
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___3168size_t_1568size_t(
libcrux_ml_kem_types_MlKemPrivateKey____3168size_t sk,
Expand All @@ -155,6 +191,18 @@ libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem_
return lit;
}

libcrux_ml_kem_types_MlKemCiphertext____1568size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___1568size_t(
uint8_t value[1568U]
)
{
uint8_t uu____0[1568U];
memcpy(uu____0, value, (size_t)1568U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____1568size_t lit;
memcpy(lit.value, uu____0, (size_t)1568U * sizeof (uint8_t));
return lit;
}

uint8_t
*libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemPublicKey_SIZE__18__as_slice___1568size_t(
libcrux_ml_kem_types_MlKemPublicKey____1568size_t *self
Expand Down Expand Up @@ -211,6 +259,18 @@ libcrux_ml_kem_ind_cpa_into_padded_array___1600size_t(Eurydice_slice slice, uint
memcpy(ret, out, (size_t)1600U * sizeof (uint8_t));
}

libcrux_ml_kem_types_MlKemPublicKey____1184size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1184size_t(
uint8_t value[1184U]
)
{
uint8_t uu____0[1184U];
memcpy(uu____0, value, (size_t)1184U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemPublicKey____1184size_t lit;
memcpy(lit.value, uu____0, (size_t)1184U * sizeof (uint8_t));
return lit;
}

libcrux_ml_kem_types_MlKemKeyPair____2400size_t__1184size_t
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___2400size_t_1184size_t(
libcrux_ml_kem_types_MlKemPrivateKey____2400size_t sk,
Expand All @@ -232,6 +292,18 @@ libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem_
return lit;
}

libcrux_ml_kem_types_MlKemCiphertext____1088size_t
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___1088size_t(
uint8_t value[1088U]
)
{
uint8_t uu____0[1088U];
memcpy(uu____0, value, (size_t)1088U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____1088size_t lit;
memcpy(lit.value, uu____0, (size_t)1088U * sizeof (uint8_t));
return lit;
}

uint8_t
*libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemPublicKey_SIZE__18__as_slice___1184size_t(
libcrux_ml_kem_types_MlKemPublicKey____1184size_t *self
Expand Down
10 changes: 2 additions & 8 deletions libcrux-ml-kem/c/libcrux_mlkem1024.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1500,10 +1500,7 @@ encapsulate_generic__libcrux_ml_kem_vector_PortableVector_libcrux_ml_kem_hash_fu
memcpy(uu____4, ciphertext, (size_t)1568U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____1568size_t
uu____5 =
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [1568U],
libcrux_ml_kem_types_MlKemCiphertext____1568size_t,
libcrux_ml_kem_types_MlKemCiphertext____1568size_t);
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___1568size_t(uu____4);
uint8_t uu____6[32U];
memcpy(uu____6, shared_secret_array, (size_t)32U * sizeof (uint8_t));
K___libcrux_ml_kem_types_MlKemCiphertext___1568size_t___uint8_t_32size_t_ lit;
Expand Down Expand Up @@ -1934,10 +1931,7 @@ generate_keypair_generic__libcrux_ml_kem_vector_PortableVector_libcrux_ml_kem_ha
memcpy(uu____4, public_key, (size_t)1568U * sizeof (uint8_t));
return
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___3168size_t_1568size_t(uu____3,
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [1568U],
libcrux_ml_kem_types_MlKemPublicKey____1568size_t,
libcrux_ml_kem_types_MlKemPublicKey____1568size_t));
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1568size_t(uu____4));
}

static libcrux_ml_kem_types_MlKemKeyPair____3168size_t__1568size_t
Expand Down
10 changes: 2 additions & 8 deletions libcrux-ml-kem/c/libcrux_mlkem512.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1375,10 +1375,7 @@ encapsulate_generic__libcrux_ml_kem_vector_PortableVector_libcrux_ml_kem_hash_fu
memcpy(uu____4, ciphertext, (size_t)768U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____768size_t
uu____5 =
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [768U],
libcrux_ml_kem_types_MlKemCiphertext____768size_t,
libcrux_ml_kem_types_MlKemCiphertext____768size_t);
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___768size_t(uu____4);
uint8_t uu____6[32U];
memcpy(uu____6, shared_secret_array, (size_t)32U * sizeof (uint8_t));
K___libcrux_ml_kem_types_MlKemCiphertext___768size_t___uint8_t_32size_t_ lit;
Expand Down Expand Up @@ -1809,10 +1806,7 @@ generate_keypair_generic__libcrux_ml_kem_vector_PortableVector_libcrux_ml_kem_ha
memcpy(uu____4, public_key, (size_t)800U * sizeof (uint8_t));
return
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___1632size_t_800size_t(uu____3,
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [800U],
libcrux_ml_kem_types_MlKemPublicKey____800size_t,
libcrux_ml_kem_types_MlKemPublicKey____800size_t));
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___800size_t(uu____4));
}

static libcrux_ml_kem_types_MlKemKeyPair____1632size_t__800size_t
Expand Down
10 changes: 2 additions & 8 deletions libcrux-ml-kem/c/libcrux_mlkem768.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2302,10 +2302,7 @@ encapsulate_generic__libcrux_ml_kem_vector_PortableVector_libcrux_ml_kem_hash_fu
memcpy(uu____4, ciphertext, (size_t)1088U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____1088size_t
uu____5 =
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [1088U],
libcrux_ml_kem_types_MlKemCiphertext____1088size_t,
libcrux_ml_kem_types_MlKemCiphertext____1088size_t);
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___1088size_t(uu____4);
uint8_t uu____6[32U];
memcpy(uu____6, shared_secret_array, (size_t)32U * sizeof (uint8_t));
K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_ lit;
Expand Down Expand Up @@ -2773,10 +2770,7 @@ generate_keypair_generic__libcrux_ml_kem_vector_PortableVector_libcrux_ml_kem_ha
memcpy(uu____4, public_key, (size_t)1184U * sizeof (uint8_t));
return
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___2400size_t_1184size_t(uu____3,
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [1184U],
libcrux_ml_kem_types_MlKemPublicKey____1184size_t,
libcrux_ml_kem_types_MlKemPublicKey____1184size_t));
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1184size_t(uu____4));
}

static libcrux_ml_kem_types_MlKemKeyPair____2400size_t__1184size_t
Expand Down
30 changes: 6 additions & 24 deletions libcrux-ml-kem/c/libcrux_mlkem_avx2.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3846,10 +3846,7 @@ libcrux_ml_kem_ind_cca_generate_keypair_generic__libcrux_ml_kem_vector_avx2_SIMD
memcpy(uu____4, public_key, (size_t)800U * sizeof (uint8_t));
return
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___1632size_t_800size_t(uu____3,
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [800U],
libcrux_ml_kem_types_MlKemPublicKey____800size_t,
libcrux_ml_kem_types_MlKemPublicKey____800size_t));
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___800size_t(uu____4));
}

static libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
Expand Down Expand Up @@ -5112,10 +5109,7 @@ libcrux_ml_kem_ind_cca_encapsulate_generic__libcrux_ml_kem_vector_avx2_SIMD256Ve
memcpy(uu____4, ciphertext, (size_t)768U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____768size_t
uu____5 =
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [768U],
libcrux_ml_kem_types_MlKemCiphertext____768size_t,
libcrux_ml_kem_types_MlKemCiphertext____768size_t);
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___768size_t(uu____4);
uint8_t uu____6[32U];
memcpy(uu____6, shared_secret_array, (size_t)32U * sizeof (uint8_t));
K___libcrux_ml_kem_types_MlKemCiphertext___768size_t___uint8_t_32size_t_ lit;
Expand Down Expand Up @@ -7162,10 +7156,7 @@ libcrux_ml_kem_ind_cca_generate_keypair_generic__libcrux_ml_kem_vector_avx2_SIMD
memcpy(uu____4, public_key, (size_t)1568U * sizeof (uint8_t));
return
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___3168size_t_1568size_t(uu____3,
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [1568U],
libcrux_ml_kem_types_MlKemPublicKey____1568size_t,
libcrux_ml_kem_types_MlKemPublicKey____1568size_t));
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1568size_t(uu____4));
}

static libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
Expand Down Expand Up @@ -7757,10 +7748,7 @@ libcrux_ml_kem_ind_cca_encapsulate_generic__libcrux_ml_kem_vector_avx2_SIMD256Ve
memcpy(uu____4, ciphertext, (size_t)1568U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____1568size_t
uu____5 =
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [1568U],
libcrux_ml_kem_types_MlKemCiphertext____1568size_t,
libcrux_ml_kem_types_MlKemCiphertext____1568size_t);
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___1568size_t(uu____4);
uint8_t uu____6[32U];
memcpy(uu____6, shared_secret_array, (size_t)32U * sizeof (uint8_t));
K___libcrux_ml_kem_types_MlKemCiphertext___1568size_t___uint8_t_32size_t_ lit;
Expand Down Expand Up @@ -9198,10 +9186,7 @@ libcrux_ml_kem_ind_cca_generate_keypair_generic__libcrux_ml_kem_vector_avx2_SIMD
memcpy(uu____4, public_key, (size_t)1184U * sizeof (uint8_t));
return
libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___2400size_t_1184size_t(uu____3,
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [1184U],
libcrux_ml_kem_types_MlKemPublicKey____1184size_t,
libcrux_ml_kem_types_MlKemPublicKey____1184size_t));
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemPublicKey_SIZE___14__from___1184size_t(uu____4));
}

static libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
Expand Down Expand Up @@ -9699,10 +9684,7 @@ libcrux_ml_kem_ind_cca_encapsulate_generic__libcrux_ml_kem_vector_avx2_SIMD256Ve
memcpy(uu____4, ciphertext, (size_t)1088U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext____1088size_t
uu____5 =
core_convert___core__convert__Into_U__for_T__3__into(uu____4,
uint8_t [1088U],
libcrux_ml_kem_types_MlKemCiphertext____1088size_t,
libcrux_ml_kem_types_MlKemCiphertext____1088size_t);
libcrux_ml_kem_types___core__convert__From__Array_u8__SIZE___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___2__from___1088size_t(uu____4);
uint8_t uu____6[32U];
memcpy(uu____6, shared_secret_array, (size_t)32U * sizeof (uint8_t));
K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_ lit;
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/src/ind_cca.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -236,7 +236,7 @@ fn generate_keypair_generic<
let private_key: MlKemPrivateKey<PRIVATE_KEY_SIZE> =
MlKemPrivateKey::from(secret_key_serialized);

MlKemKeyPair::from(private_key, public_key.into())
MlKemKeyPair::from(private_key, MlKemPublicKey::from(public_key))
}

pub(crate) fn encapsulate<
Expand Down Expand Up @@ -402,7 +402,7 @@ fn encapsulate_generic<
>(public_key.as_slice(), randomness, pseudorandomness);
let mut shared_secret_array = [0u8; SHARED_SECRET_SIZE];
shared_secret_array.copy_from_slice(shared_secret);
(ciphertext.into(), shared_secret_array)
(MlKemCiphertext::from(ciphertext), shared_secret_array)
}

pub(crate) fn decapsulate<
Expand Down

0 comments on commit a0b0b93

Please sign in to comment.