/*
* SPDX - FileCopyrightText : 2025 Cryspen Sarl < info @ cryspen . com >
*
* SPDX - License - Identifier : MIT or Apache - 2 . 0
*
* This code was generated with the following revisions :
* Charon : 667 d2fc98984ff7f3df989c2367e6c1fa4a000e7
* Eurydice : 2381 cbc416ef2ad0b561c362c500bc84f36b6785
* Karamel : 80 f5435f2fc505973c469a4afcc8d875cddd0d8b
* F * : 71 d8221589d4d438af3706d89cb653cf53e18aab
* Libcrux : 68 dfed5a4a9e40277f62828471c029afed1ecdcc
*/
#include "internal/libcrux_core.h"
/**
Return 1 if ` value ` is not zero and 0 otherwise .
*/
static KRML_NOINLINE uint8_t
inz(uint8_t value)
{
uint16_t value0 = (uint16_t)value;
uint8_t result =
(uint8_t)((uint32_t)core_num__u16__wrapping_add(~value0, 1 U) >> 8 U);
return (uint32_t)result & 1 U;
}
static KRML_NOINLINE uint8_t
is_non_zero(uint8_t value)
{
return inz(value);
}
/**
Return 1 if the bytes of ` lhs ` and ` rhs ` do not exactly
match and 0 otherwise .
*/
static KRML_NOINLINE uint8_t
compare(Eurydice_slice lhs, Eurydice_slice rhs)
{
uint8_t r = 0 U;
for (size_t i = (size_t)0 U; i < Eurydice_slice_len(lhs, uint8_t); i++) {
size_t i0 = i;
uint8_t nr = (uint32_t)r |
((uint32_t)Eurydice_slice_index(lhs, i0, uint8_t, uint8_t *) ^
(uint32_t)Eurydice_slice_index(rhs, i0, uint8_t, uint8_t *));
r = nr;
}
return is_non_zero(r);
}
static KRML_NOINLINE uint8_t
compare_ciphertexts_in_constant_time(Eurydice_slice lhs, Eurydice_slice rhs)
{
return compare(lhs, rhs);
}
/**
If ` selector ` is not zero , return the bytes in ` rhs ` ; return the bytes in
` lhs ` otherwise .
*/
static KRML_NOINLINE void
select_ct(Eurydice_slice lhs, Eurydice_slice rhs,
uint8_t selector, uint8_t ret[32 U])
{
uint8_t mask = core_num__u8__wrapping_sub(is_non_zero(selector), 1 U);
uint8_t out[32 U] = { 0 U };
for (size_t i = (size_t)0 U; i < LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE;
i++) {
size_t i0 = i;
uint8_t outi =
((uint32_t)Eurydice_slice_index(lhs, i0, uint8_t, uint8_t *) &
(uint32_t)mask) |
((uint32_t)Eurydice_slice_index(rhs, i0, uint8_t, uint8_t *) &
(uint32_t)~mask);
out[i0] = outi;
}
memcpy(ret, out, (size_t)32 U * sizeof (uint8_t));
}
static KRML_NOINLINE void
select_shared_secret_in_constant_time(
Eurydice_slice lhs, Eurydice_slice rhs, uint8_t selector,
uint8_t ret[32 U])
{
select_ct(lhs, rhs, selector, ret);
}
KRML_NOINLINE void
libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(
Eurydice_slice lhs_c, Eurydice_slice rhs_c, Eurydice_slice lhs_s,
Eurydice_slice rhs_s, uint8_t ret[32 U])
{
uint8_t selector = compare_ciphertexts_in_constant_time(lhs_c, rhs_c);
uint8_t ret0[32 U];
select_shared_secret_in_constant_time(lhs_s, rhs_s, selector, ret0);
memcpy(ret, ret0, (size_t)32 U * sizeof (uint8_t));
}
/**
K * BITS_PER_RING_ELEMENT / 8
[ eurydice ] Note that we can ' t use const generics here because that breaks
C extraction with eurydice .
*/
size_t
libcrux_ml_kem_constants_ranked_bytes_per_ring_element(size_t rank)
{
return rank * LIBCRUX_ML_KEM_CONSTANTS_BITS_PER_RING_ELEMENT / (size_t)8 U;
}
/**
Construct a public integer ( identity )
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . secret
with types int16_t
*/
static KRML_MUSTINLINE int16_t
secret_39(int16_t x)
{
return x;
}
int16_t
libcrux_secrets_int_I16(int16_t v)
{
return secret_39(v);
}
/**
This function found in impl { libcrux_secrets : : traits : : Classify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . classify_27
with types int16_t
*/
int16_t
libcrux_secrets_int_public_integers_classify_27_39(int16_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint8_t
*/
static KRML_MUSTINLINE uint8_t
declassify_d8_90(uint8_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for u8 }
*/
int16_t
libcrux_secrets_int_as_i16_59(uint8_t self)
{
return libcrux_secrets_int_public_integers_classify_27_39(
(int16_t)declassify_d8_90(self));
}
/**
This function found in impl { libcrux_secrets : : traits : : Classify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . classify_27
with types uint8_t
*/
static KRML_MUSTINLINE uint8_t
classify_27_90(uint8_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types int16_t
*/
int16_t
libcrux_secrets_int_public_integers_declassify_d8_39(int16_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for i16 }
*/
uint8_t
libcrux_secrets_int_as_u8_f5(int16_t self)
{
return classify_27_90(
(uint8_t)libcrux_secrets_int_public_integers_declassify_d8_39(self));
}
/**
This function found in impl { libcrux_secrets : : traits : : Classify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . classify_27
with types int32_t
*/
static KRML_MUSTINLINE int32_t
classify_27_a8(int32_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for i16 }
*/
int32_t
libcrux_secrets_int_as_i32_f5(int16_t self)
{
return classify_27_a8(
(int32_t)libcrux_secrets_int_public_integers_declassify_d8_39(self));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types int32_t
*/
static KRML_MUSTINLINE int32_t
declassify_d8_a8(int32_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for i32 }
*/
int16_t
libcrux_secrets_int_as_i16_36(int32_t self)
{
return libcrux_secrets_int_public_integers_classify_27_39(
(int16_t)declassify_d8_a8(self));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint32_t
*/
static KRML_MUSTINLINE uint32_t
declassify_d8_df(uint32_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for u32 }
*/
int32_t
libcrux_secrets_int_as_i32_b8(uint32_t self)
{
return classify_27_a8((int32_t)declassify_d8_df(self));
}
/**
This function found in impl { libcrux_secrets : : traits : : Classify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . classify_27
with types uint16_t
*/
static KRML_MUSTINLINE uint16_t
classify_27_de(uint16_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for i16 }
*/
uint16_t
libcrux_secrets_int_as_u16_f5(int16_t self)
{
return classify_27_de(
(uint16_t)libcrux_secrets_int_public_integers_declassify_d8_39(self));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint16_t
*/
static KRML_MUSTINLINE uint16_t
declassify_d8_de(uint16_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for u16 }
*/
int16_t
libcrux_secrets_int_as_i16_ca(uint16_t self)
{
return libcrux_secrets_int_public_integers_classify_27_39(
(int16_t)declassify_d8_de(self));
}
/**
This function found in impl { libcrux_secrets : : traits : : Classify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . classify_27
with types uint64_t
*/
static KRML_MUSTINLINE uint64_t
classify_27_49(uint64_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for u16 }
*/
uint64_t
libcrux_secrets_int_as_u64_ca(uint16_t self)
{
return classify_27_49((uint64_t)declassify_d8_de(self));
}
/**
This function found in impl { libcrux_secrets : : traits : : Classify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . classify_27
with types uint32_t
*/
uint32_t
libcrux_secrets_int_public_integers_classify_27_df(uint32_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint64_t
*/
static KRML_MUSTINLINE uint64_t
declassify_d8_49(uint64_t self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for u64 }
*/
uint32_t
libcrux_secrets_int_as_u32_a3(uint64_t self)
{
return libcrux_secrets_int_public_integers_classify_27_df(
(uint32_t)declassify_d8_49(self));
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for u32 }
*/
int16_t
libcrux_secrets_int_as_i16_b8(uint32_t self)
{
return libcrux_secrets_int_public_integers_classify_27_39(
(int16_t)declassify_d8_df(self));
}
/**
This function found in impl { libcrux_secrets : : int : : CastOps for i16 }
*/
int16_t
libcrux_secrets_int_as_i16_f5(int16_t self)
{
return libcrux_secrets_int_public_integers_classify_27_39(
libcrux_secrets_int_public_integers_declassify_d8_39(self));
}
/**
This function found in impl
{ libcrux_ml_kem : : types : : MlKemKeyPair < PRIVATE_KEY_SIZE , PUBLIC_KEY_SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . from_17
with const generics
- PRIVATE_KEY_SIZE = 3168
- PUBLIC_KEY_SIZE = 1568
*/
libcrux_ml_kem_mlkem1024_MlKem1024KeyPair
libcrux_ml_kem_types_from_17_94(
libcrux_ml_kem_types_MlKemPrivateKey_83 sk,
libcrux_ml_kem_types_MlKemPublicKey_64 pk)
{
return (KRML_CLITERAL(libcrux_ml_kem_mlkem1024_MlKem1024KeyPair){ .sk = sk,
.pk = pk });
}
/**
This function found in impl { core : : convert : : From < @ Array < u8 , SIZE > > for
libcrux_ml_kem : : types : : MlKemPrivateKey < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . from_77
with const generics
- SIZE = 3168
*/
libcrux_ml_kem_types_MlKemPrivateKey_83
libcrux_ml_kem_types_from_77_39(
uint8_t value[3168 U])
{
/* Passing arrays by value in Rust generates a copy in C */
uint8_t copy_of_value[3168 U];
memcpy(copy_of_value, value, (size_t)3168 U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemPrivateKey_83 lit;
memcpy(lit.value, copy_of_value, (size_t)3168 U * sizeof (uint8_t));
return lit;
}
/**
This function found in impl { libcrux_ml_kem : : types : : MlKemCiphertext < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . as_slice_a9
with const generics
- SIZE = 1568
*/
uint8_t *
libcrux_ml_kem_types_as_slice_a9_af(
libcrux_ml_kem_types_MlKemCiphertext_64 *self)
{
return self->value;
}
/**
This function found in impl
{ libcrux_ml_kem : : types : : MlKemKeyPair < PRIVATE_KEY_SIZE , PUBLIC_KEY_SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . from_17
with const generics
- PRIVATE_KEY_SIZE = 2400
- PUBLIC_KEY_SIZE = 1184
*/
libcrux_ml_kem_mlkem768_MlKem768KeyPair
libcrux_ml_kem_types_from_17_74(
libcrux_ml_kem_types_MlKemPrivateKey_d9 sk,
libcrux_ml_kem_types_MlKemPublicKey_30 pk)
{
return (KRML_CLITERAL(libcrux_ml_kem_mlkem768_MlKem768KeyPair){ .sk = sk,
.pk = pk });
}
/**
This function found in impl { core : : convert : : From < @ Array < u8 , SIZE > > for
libcrux_ml_kem : : types : : MlKemPrivateKey < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . from_77
with const generics
- SIZE = 2400
*/
libcrux_ml_kem_types_MlKemPrivateKey_d9
libcrux_ml_kem_types_from_77_28(
uint8_t value[2400 U])
{
/* Passing arrays by value in Rust generates a copy in C */
uint8_t copy_of_value[2400 U];
memcpy(copy_of_value, value, (size_t)2400 U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemPrivateKey_d9 lit;
memcpy(lit.value, copy_of_value, (size_t)2400 U * sizeof (uint8_t));
return lit;
}
/**
This function found in impl { libcrux_ml_kem : : types : : MlKemCiphertext < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . as_slice_a9
with const generics
- SIZE = 1088
*/
uint8_t *
libcrux_ml_kem_types_as_slice_a9_80(
libcrux_ml_kem_mlkem768_MlKem768Ciphertext *self)
{
return self->value;
}
/**
This function found in impl { libcrux_ml_kem : : types : : MlKemPublicKey < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . as_slice_e6
with const generics
- SIZE = 1184
*/
uint8_t *
libcrux_ml_kem_types_as_slice_e6_d0(
libcrux_ml_kem_types_MlKemPublicKey_30 *self)
{
return self->value;
}
/**
This function found in impl { core : : convert : : From < @ Array < u8 , SIZE > > for
libcrux_ml_kem : : types : : MlKemPublicKey < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . from_fd
with const generics
- SIZE = 1184
*/
libcrux_ml_kem_types_MlKemPublicKey_30
libcrux_ml_kem_types_from_fd_d0(
uint8_t value[1184 U])
{
/* Passing arrays by value in Rust generates a copy in C */
uint8_t copy_of_value[1184 U];
memcpy(copy_of_value, value, (size_t)1184 U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemPublicKey_30 lit;
memcpy(lit.value, copy_of_value, (size_t)1184 U * sizeof (uint8_t));
return lit;
}
/**
Unpack an incoming private key into it ' s different parts .
We have this here in types to extract into a common core for C .
*/
/**
A monomorphic instance of libcrux_ml_kem . types . unpack_private_key
with const generics
- CPA_SECRET_KEY_SIZE = 1152
- PUBLIC_KEY_SIZE = 1184
*/
Eurydice_slice_uint8_t_x4
libcrux_ml_kem_types_unpack_private_key_b4(
Eurydice_slice private_key)
{
Eurydice_slice_uint8_t_x2 uu____0 = Eurydice_slice_split_at(
private_key, (size_t)1152 U, uint8_t, Eurydice_slice_uint8_t_x2);
Eurydice_slice ind_cpa_secret_key = uu____0.fst;
Eurydice_slice secret_key0 = uu____0.snd;
Eurydice_slice_uint8_t_x2 uu____1 = Eurydice_slice_split_at(
secret_key0, (size_t)1184 U, uint8_t, Eurydice_slice_uint8_t_x2);
Eurydice_slice ind_cpa_public_key = uu____1.fst;
Eurydice_slice secret_key = uu____1.snd;
Eurydice_slice_uint8_t_x2 uu____2 = Eurydice_slice_split_at(
secret_key, LIBCRUX_ML_KEM_CONSTANTS_H_DIGEST_SIZE, uint8_t,
Eurydice_slice_uint8_t_x2);
Eurydice_slice ind_cpa_public_key_hash = uu____2.fst;
Eurydice_slice implicit_rejection_value = uu____2.snd;
return (
KRML_CLITERAL(Eurydice_slice_uint8_t_x4){ .fst = ind_cpa_secret_key,
.snd = ind_cpa_public_key,
.thd = ind_cpa_public_key_hash,
.f3 = implicit_rejection_value });
}
/**
This function found in impl { core : : convert : : From < @ Array < u8 , SIZE > > for
libcrux_ml_kem : : types : : MlKemCiphertext < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . from_e0
with const generics
- SIZE = 1088
*/
libcrux_ml_kem_mlkem768_MlKem768Ciphertext
libcrux_ml_kem_types_from_e0_80(
uint8_t value[1088 U])
{
/* Passing arrays by value in Rust generates a copy in C */
uint8_t copy_of_value[1088 U];
memcpy(copy_of_value, value, (size_t)1088 U * sizeof (uint8_t));
libcrux_ml_kem_mlkem768_MlKem768Ciphertext lit;
memcpy(lit.value, copy_of_value, (size_t)1088 U * sizeof (uint8_t));
return lit;
}
/**
A monomorphic instance of libcrux_ml_kem . utils . prf_input_inc
with const generics
- K = 3
*/
uint8_t
libcrux_ml_kem_utils_prf_input_inc_e0(uint8_t (*prf_inputs)[33 U],
uint8_t domain_separator)
{
KRML_MAYBE_FOR3(i, (size_t)0 U, (size_t)3 U, (size_t)1 U, size_t i0 = i;
prf_inputs[i0][32 U] = domain_separator;
domain_separator = (uint32_t)domain_separator + 1 U;);
return domain_separator;
}
/**
This function found in impl { core : : convert : : AsRef < @ Slice < u8 > > for
libcrux_ml_kem : : types : : MlKemCiphertext < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . as_ref_d3
with const generics
- SIZE = 1088
*/
Eurydice_slice
libcrux_ml_kem_types_as_ref_d3_80(
libcrux_ml_kem_mlkem768_MlKem768Ciphertext *self)
{
return Eurydice_array_to_slice((size_t)1088 U, self->value, uint8_t);
}
/**
Pad the ` slice ` with ` 0 ` s at the end .
*/
/**
A monomorphic instance of libcrux_ml_kem . utils . into_padded_array
with const generics
- LEN = 1120
*/
void
libcrux_ml_kem_utils_into_padded_array_15(Eurydice_slice slice,
uint8_t ret[1120 U])
{
uint8_t out[1120 U] = { 0 U };
uint8_t *uu____0 = out;
Eurydice_slice_copy(
Eurydice_array_to_subslice3(
uu____0, (size_t)0 U, Eurydice_slice_len(slice, uint8_t), uint8_t *),
slice, uint8_t);
memcpy(ret, out, (size_t)1120 U * sizeof (uint8_t));
}
/**
This function found in impl { libcrux_ml_kem : : types : : MlKemPublicKey < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . as_slice_e6
with const generics
- SIZE = 1568
*/
uint8_t *
libcrux_ml_kem_types_as_slice_e6_af(
libcrux_ml_kem_types_MlKemPublicKey_64 *self)
{
return self->value;
}
/**
This function found in impl { core : : convert : : From < @ Array < u8 , SIZE > > for
libcrux_ml_kem : : types : : MlKemPublicKey < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . from_fd
with const generics
- SIZE = 1568
*/
libcrux_ml_kem_types_MlKemPublicKey_64
libcrux_ml_kem_types_from_fd_af(
uint8_t value[1568 U])
{
/* Passing arrays by value in Rust generates a copy in C */
uint8_t copy_of_value[1568 U];
memcpy(copy_of_value, value, (size_t)1568 U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemPublicKey_64 lit;
memcpy(lit.value, copy_of_value, (size_t)1568 U * sizeof (uint8_t));
return lit;
}
/**
Unpack an incoming private key into it ' s different parts .
We have this here in types to extract into a common core for C .
*/
/**
A monomorphic instance of libcrux_ml_kem . types . unpack_private_key
with const generics
- CPA_SECRET_KEY_SIZE = 1536
- PUBLIC_KEY_SIZE = 1568
*/
Eurydice_slice_uint8_t_x4
libcrux_ml_kem_types_unpack_private_key_1f(
Eurydice_slice private_key)
{
Eurydice_slice_uint8_t_x2 uu____0 = Eurydice_slice_split_at(
private_key, (size_t)1536 U, uint8_t, Eurydice_slice_uint8_t_x2);
Eurydice_slice ind_cpa_secret_key = uu____0.fst;
Eurydice_slice secret_key0 = uu____0.snd;
Eurydice_slice_uint8_t_x2 uu____1 = Eurydice_slice_split_at(
secret_key0, (size_t)1568 U, uint8_t, Eurydice_slice_uint8_t_x2);
Eurydice_slice ind_cpa_public_key = uu____1.fst;
Eurydice_slice secret_key = uu____1.snd;
Eurydice_slice_uint8_t_x2 uu____2 = Eurydice_slice_split_at(
secret_key, LIBCRUX_ML_KEM_CONSTANTS_H_DIGEST_SIZE, uint8_t,
Eurydice_slice_uint8_t_x2);
Eurydice_slice ind_cpa_public_key_hash = uu____2.fst;
Eurydice_slice implicit_rejection_value = uu____2.snd;
return (
KRML_CLITERAL(Eurydice_slice_uint8_t_x4){ .fst = ind_cpa_secret_key,
.snd = ind_cpa_public_key,
.thd = ind_cpa_public_key_hash,
.f3 = implicit_rejection_value });
}
/**
This function found in impl { core : : result : : Result < T , E > [ TraitClause @ 0 ,
TraitClause @ 1 ] }
*/
/**
A monomorphic instance of core . result . unwrap_26
with types uint8_t [ 32 size_t ] , core_array_TryFromSliceError
*/
void
core_result_unwrap_26_b3(core_result_Result_fb self, uint8_t ret[32 U])
{
if (self.tag == core_result_Ok) {
uint8_t f0[32 U];
memcpy(f0, self.val.case_Ok, (size_t)32 U * sizeof (uint8_t));
memcpy(ret, f0, (size_t)32 U * sizeof (uint8_t));
} else {
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n" , __FILE__, __LINE__,
"unwrap not Ok" );
KRML_HOST_EXIT(255 U);
}
}
/**
Pad the ` slice ` with ` 0 ` s at the end .
*/
/**
A monomorphic instance of libcrux_ml_kem . utils . into_padded_array
with const generics
- LEN = 34
*/
void
libcrux_ml_kem_utils_into_padded_array_b6(Eurydice_slice slice,
uint8_t ret[34 U])
{
uint8_t out[34 U] = { 0 U };
uint8_t *uu____0 = out;
Eurydice_slice_copy(
Eurydice_array_to_subslice3(
uu____0, (size_t)0 U, Eurydice_slice_len(slice, uint8_t), uint8_t *),
slice, uint8_t);
memcpy(ret, out, (size_t)34 U * sizeof (uint8_t));
}
/**
This function found in impl { core : : convert : : From < @ Array < u8 , SIZE > > for
libcrux_ml_kem : : types : : MlKemCiphertext < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . from_e0
with const generics
- SIZE = 1568
*/
libcrux_ml_kem_types_MlKemCiphertext_64
libcrux_ml_kem_types_from_e0_af(
uint8_t value[1568 U])
{
/* Passing arrays by value in Rust generates a copy in C */
uint8_t copy_of_value[1568 U];
memcpy(copy_of_value, value, (size_t)1568 U * sizeof (uint8_t));
libcrux_ml_kem_types_MlKemCiphertext_64 lit;
memcpy(lit.value, copy_of_value, (size_t)1568 U * sizeof (uint8_t));
return lit;
}
/**
A monomorphic instance of libcrux_ml_kem . utils . prf_input_inc
with const generics
- K = 4
*/
uint8_t
libcrux_ml_kem_utils_prf_input_inc_ac(uint8_t (*prf_inputs)[33 U],
uint8_t domain_separator)
{
KRML_MAYBE_FOR4(i, (size_t)0 U, (size_t)4 U, (size_t)1 U, size_t i0 = i;
prf_inputs[i0][32 U] = domain_separator;
domain_separator = (uint32_t)domain_separator + 1 U;);
return domain_separator;
}
/**
Pad the ` slice ` with ` 0 ` s at the end .
*/
/**
A monomorphic instance of libcrux_ml_kem . utils . into_padded_array
with const generics
- LEN = 33
*/
void
libcrux_ml_kem_utils_into_padded_array_c8(Eurydice_slice slice,
uint8_t ret[33 U])
{
uint8_t out[33 U] = { 0 U };
uint8_t *uu____0 = out;
Eurydice_slice_copy(
Eurydice_array_to_subslice3(
uu____0, (size_t)0 U, Eurydice_slice_len(slice, uint8_t), uint8_t *),
slice, uint8_t);
memcpy(ret, out, (size_t)33 U * sizeof (uint8_t));
}
/**
This function found in impl { core : : convert : : AsRef < @ Slice < u8 > > for
libcrux_ml_kem : : types : : MlKemCiphertext < SIZE > }
*/
/**
A monomorphic instance of libcrux_ml_kem . types . as_ref_d3
with const generics
- SIZE = 1568
*/
Eurydice_slice
libcrux_ml_kem_types_as_ref_d3_af(
libcrux_ml_kem_types_MlKemCiphertext_64 *self)
{
return Eurydice_array_to_slice((size_t)1568 U, self->value, uint8_t);
}
/**
Pad the ` slice ` with ` 0 ` s at the end .
*/
/**
A monomorphic instance of libcrux_ml_kem . utils . into_padded_array
with const generics
- LEN = 1600
*/
void
libcrux_ml_kem_utils_into_padded_array_7f(Eurydice_slice slice,
uint8_t ret[1600 U])
{
uint8_t out[1600 U] = { 0 U };
uint8_t *uu____0 = out;
Eurydice_slice_copy(
Eurydice_array_to_subslice3(
uu____0, (size_t)0 U, Eurydice_slice_len(slice, uint8_t), uint8_t *),
slice, uint8_t);
memcpy(ret, out, (size_t)1600 U * sizeof (uint8_t));
}
/**
Pad the ` slice ` with ` 0 ` s at the end .
*/
/**
A monomorphic instance of libcrux_ml_kem . utils . into_padded_array
with const generics
- LEN = 64
*/
void
libcrux_ml_kem_utils_into_padded_array_24(Eurydice_slice slice,
uint8_t ret[64 U])
{
uint8_t out[64 U] = { 0 U };
uint8_t *uu____0 = out;
Eurydice_slice_copy(
Eurydice_array_to_subslice3(
uu____0, (size_t)0 U, Eurydice_slice_len(slice, uint8_t), uint8_t *),
slice, uint8_t);
memcpy(ret, out, (size_t)64 U * sizeof (uint8_t));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint8_t [ 24 size_t ]
*/
void
libcrux_secrets_int_public_integers_declassify_d8_d2(uint8_t self[24 U],
uint8_t ret[24 U])
{
memcpy(ret, self, (size_t)24 U * sizeof (uint8_t));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint8_t [ 22 size_t ]
*/
void
libcrux_secrets_int_public_integers_declassify_d8_fa(uint8_t self[22 U],
uint8_t ret[22 U])
{
memcpy(ret, self, (size_t)22 U * sizeof (uint8_t));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint8_t [ 20 size_t ]
*/
void
libcrux_secrets_int_public_integers_declassify_d8_57(uint8_t self[20 U],
uint8_t ret[20 U])
{
memcpy(ret, self, (size_t)20 U * sizeof (uint8_t));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint8_t [ 10 size_t ]
*/
void
libcrux_secrets_int_public_integers_declassify_d8_cc(uint8_t self[10 U],
uint8_t ret[10 U])
{
memcpy(ret, self, (size_t)10 U * sizeof (uint8_t));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint8_t [ 8 size_t ]
*/
void
libcrux_secrets_int_public_integers_declassify_d8_76(uint8_t self[8 U],
uint8_t ret[8 U])
{
memcpy(ret, self, (size_t)8 U * sizeof (uint8_t));
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types uint8_t [ 2 size_t ]
*/
void
libcrux_secrets_int_public_integers_declassify_d8_d4(uint8_t self[2 U],
uint8_t ret[2 U])
{
memcpy(ret, self, (size_t)2 U * sizeof (uint8_t));
}
/**
Classify a mutable slice ( identity )
We define a separate function for this because hax has limited support for
& mut - returning functions
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . classify_mut_slice
with types Eurydice_slice uint8_t
*/
Eurydice_slice
libcrux_secrets_int_public_integers_classify_mut_slice_ba(
Eurydice_slice x)
{
return x;
}
/**
This function found in impl { libcrux_secrets : : traits : : ClassifyRef < & ' a
( @ Slice < T > ) > for & ' a ( @ Slice < T > ) }
*/
/**
A monomorphic instance of libcrux_secrets . int . classify_public . classify_ref_9b
with types uint8_t
*/
Eurydice_slice
libcrux_secrets_int_classify_public_classify_ref_9b_90(
Eurydice_slice self)
{
return self;
}
/**
This function found in impl { libcrux_secrets : : traits : : Declassify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . declassify_d8
with types int16_t [ 16 size_t ]
*/
void
libcrux_secrets_int_public_integers_declassify_d8_46(int16_t self[16 U],
int16_t ret[16 U])
{
memcpy(ret, self, (size_t)16 U * sizeof (int16_t));
}
/**
This function found in impl { libcrux_secrets : : traits : : ClassifyRef < & ' a
( @ Slice < T > ) > for & ' a ( @ Slice < T > ) }
*/
/**
A monomorphic instance of libcrux_secrets . int . classify_public . classify_ref_9b
with types int16_t
*/
Eurydice_slice
libcrux_secrets_int_classify_public_classify_ref_9b_39(
Eurydice_slice self)
{
return self;
}
/**
This function found in impl { core : : result : : Result < T , E > [ TraitClause @ 0 ,
TraitClause @ 1 ] }
*/
/**
A monomorphic instance of core . result . unwrap_26
with types int16_t [ 16 size_t ] , core_array_TryFromSliceError
*/
void
core_result_unwrap_26_00(core_result_Result_0a self, int16_t ret[16 U])
{
if (self.tag == core_result_Ok) {
int16_t f0[16 U];
memcpy(f0, self.val.case_Ok, (size_t)16 U * sizeof (int16_t));
memcpy(ret, f0, (size_t)16 U * sizeof (int16_t));
} else {
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n" , __FILE__, __LINE__,
"unwrap not Ok" );
KRML_HOST_EXIT(255 U);
}
}
/**
This function found in impl { libcrux_secrets : : traits : : Classify < T > for T }
*/
/**
A monomorphic instance of libcrux_secrets . int . public_integers . classify_27
with types int16_t [ 16 size_t ]
*/
void
libcrux_secrets_int_public_integers_classify_27_46(int16_t self[16 U],
int16_t ret[16 U])
{
memcpy(ret, self, (size_t)16 U * sizeof (int16_t));
}
/**
This function found in impl { core : : result : : Result < T , E > [ TraitClause @ 0 ,
TraitClause @ 1 ] }
*/
/**
A monomorphic instance of core . result . unwrap_26
with types uint8_t [ 8 size_t ] , core_array_TryFromSliceError
*/
void
core_result_unwrap_26_68(core_result_Result_15 self, uint8_t ret[8 U])
{
if (self.tag == core_result_Ok) {
uint8_t f0[8 U];
memcpy(f0, self.val.case_Ok, (size_t)8 U * sizeof (uint8_t));
memcpy(ret, f0, (size_t)8 U * sizeof (uint8_t));
} else {
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n" , __FILE__, __LINE__,
"unwrap not Ok" );
KRML_HOST_EXIT(255 U);
}
}
Messung V0.5 in Prozent C=91 H=97 G=93
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet am 2026-09-30)
¤
*© Formatika GbR, Deutschland