Skip to content

Commit

Permalink
boring C refresh
Browse files Browse the repository at this point in the history
  • Loading branch information
@karthikbhargavan
karthikbhargavan committed Nov 6, 2024
1 parent 7ed909f commit 168a963
Show file tree
Hide file tree
Showing 9 changed files with 143 additions and 158 deletions.
2 changes: 1 addition & 1 deletion libcrux-ml-kem/cg/code_gen.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
2 changes: 1 addition & 1 deletion libcrux-ml-kem/cg/libcrux_core.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
* Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
* F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
* Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
* Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
*/

#ifndef __libcrux_core_H
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/cg/libcrux_ct_ops.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
* Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
* F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
* Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
* Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
*/

#ifndef __libcrux_ct_ops_H
Expand Down
143 changes: 68 additions & 75 deletions libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
* Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
* F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
* Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
* Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
*/

#ifndef __libcrux_mlkem768_avx2_H
Expand Down Expand Up @@ -7030,40 +7030,24 @@ static inline tuple_c2 libcrux_ml_kem_mlkem768_avx2_unpacked_encapsulate(

/**
A monomorphic instance of
libcrux_ml_kem.ind_cca.unpacked.generate_keypair.closure.closure with types
libcrux_ml_kem_vector_avx2_SIMD256Vector,
libcrux_ml_kem_hash_functions_avx2_Simd256Hash, libcrux_ml_kem_variant_MlKem
with const generics
libcrux_ml_kem.ind_cca.unpacked.transpose_a.closure.closure with types
libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics
- K= 3
- CPA_PRIVATE_KEY_SIZE= 1152
- PRIVATE_KEY_SIZE= 2400
- PUBLIC_KEY_SIZE= 1184
- BYTES_PER_RING_ELEMENT= 1152
- ETA1= 2
- ETA1_RANDOMNESS_SIZE= 128
*/
KRML_ATTRIBUTE_TARGET("avx2")
static inline libcrux_ml_kem_polynomial_PolynomialRingElement_f6
libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_closure_d6(size_t _j) {
libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_closure_ab(size_t _j) {
return libcrux_ml_kem_polynomial_ZERO_ef_61();
}

/**
A monomorphic instance of
libcrux_ml_kem.ind_cca.unpacked.generate_keypair.closure with types
libcrux_ml_kem_vector_avx2_SIMD256Vector,
libcrux_ml_kem_hash_functions_avx2_Simd256Hash, libcrux_ml_kem_variant_MlKem
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.closure
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics
- K= 3
- CPA_PRIVATE_KEY_SIZE= 1152
- PRIVATE_KEY_SIZE= 2400
- PUBLIC_KEY_SIZE= 1184
- BYTES_PER_RING_ELEMENT= 1152
- ETA1= 2
- ETA1_RANDOMNESS_SIZE= 128
*/
KRML_ATTRIBUTE_TARGET("avx2")
static inline void libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_d6(
static inline void libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_ab(
size_t _i, libcrux_ml_kem_polynomial_PolynomialRingElement_f6 ret[3U]) {
for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
ret[i] = libcrux_ml_kem_polynomial_ZERO_ef_61();
Expand Down Expand Up @@ -7094,8 +7078,37 @@ libcrux_ml_kem_polynomial_clone_8d_61(
}

/**
Generate Unpacked Keys
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics
- K= 3
*/
KRML_ATTRIBUTE_TARGET("avx2")
static inline void libcrux_ml_kem_ind_cca_unpacked_transpose_a_ab(
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 ind_cpa_a[3U][3U],
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 ret[3U][3U]) {
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 A[3U][3U];
for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_ab(i, A[i]);
}
for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
size_t i0 = i;
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 _a_i[3U][3U];
memcpy(_a_i, A,
(size_t)3U *
sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f6[3U]));
for (size_t i1 = (size_t)0U; i1 < (size_t)3U; i1++) {
size_t j = i1;
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 uu____0 =
libcrux_ml_kem_polynomial_clone_8d_61(&ind_cpa_a[j][i0]);
A[i0][j] = uu____0;
}
}
memcpy(ret, A,
(size_t)3U *
sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f6[3U]));
}

/**
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.generate_keypair
with types libcrux_ml_kem_vector_avx2_SIMD256Vector,
Expand Down Expand Up @@ -7123,20 +7136,12 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ind_cca_unpacked_generate_keypair_d6(
libcrux_ml_kem_ind_cpa_generate_keypair_unpacked_22(
ind_cpa_keypair_randomness, &out->private_key.ind_cpa_private_key,
&out->public_key.ind_cpa_public_key);
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 uu____0[3U][3U];
memcpy(uu____0, out->public_key.ind_cpa_public_key.A,
(size_t)3U *
sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f6[3U]));
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 A[3U][3U];
for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_d6(i, A[i]);
}
for (size_t i0 = (size_t)0U; i0 < (size_t)3U; i0++) {
size_t i1 = i0;
for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
size_t j = i;
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 uu____0 =
libcrux_ml_kem_polynomial_clone_8d_61(
&out->public_key.ind_cpa_public_key.A[j][i1]);
A[i1][j] = uu____0;
}
}
libcrux_ml_kem_ind_cca_unpacked_transpose_a_ab(uu____0, A);
libcrux_ml_kem_polynomial_PolynomialRingElement_f6 uu____1[3U][3U];
memcpy(uu____1, A,
(size_t)3U *
Expand Down Expand Up @@ -7231,17 +7236,17 @@ static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_generate_key_pair(
/**
This function found in impl {(core::default::Default for
libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked<Vector,
K>[TraitClause@0, TraitClause@1])#1}
K>[TraitClause@0, TraitClause@1])}
*/
/**
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.default_1c
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.default_09
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics
- K= 3
*/
KRML_ATTRIBUTE_TARGET("avx2")
static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63
libcrux_ml_kem_ind_cca_unpacked_default_1c_ab(void) {
libcrux_ml_kem_ind_cca_unpacked_default_09_ab(void) {
libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 lit;
lit.ind_cpa_public_key = libcrux_ml_kem_ind_cpa_unpacked_default_8d_ab();
lit.public_key_hash[0U] = 0U;
Expand Down Expand Up @@ -7282,18 +7287,18 @@ libcrux_ml_kem_ind_cca_unpacked_default_1c_ab(void) {
/**
This function found in impl {(core::default::Default for
libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked<Vector,
K>[TraitClause@0, TraitClause@1])#3}
K>[TraitClause@0, TraitClause@1])#1}
*/
/**
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.default_07
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.default_53
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics
- K= 3
*/
KRML_ATTRIBUTE_TARGET("avx2")
static KRML_MUSTINLINE
libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked
libcrux_ml_kem_ind_cca_unpacked_default_07_ab(void) {
libcrux_ml_kem_ind_cca_unpacked_default_53_ab(void) {
libcrux_ml_kem_ind_cca_unpacked_MlKemPrivateKeyUnpacked_63 uu____0;
uu____0.ind_cpa_private_key = libcrux_ml_kem_ind_cpa_unpacked_default_1a_ab();
uu____0.implicit_rejection_value[0U] = 0U;
Expand Down Expand Up @@ -7331,7 +7336,7 @@ static KRML_MUSTINLINE
return (
CLITERAL(libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked){
.private_key = uu____0,
.public_key = libcrux_ml_kem_ind_cca_unpacked_default_1c_ab()});
.public_key = libcrux_ml_kem_ind_cca_unpacked_default_09_ab()});
}

/**
Expand All @@ -7340,7 +7345,7 @@ static KRML_MUSTINLINE
KRML_ATTRIBUTE_TARGET("avx2")
static inline libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked
libcrux_ml_kem_mlkem768_avx2_unpacked_init_key_pair(void) {
return libcrux_ml_kem_ind_cca_unpacked_default_07_ab();
return libcrux_ml_kem_ind_cca_unpacked_default_53_ab();
}

/**
Expand All @@ -7349,28 +7354,25 @@ libcrux_ml_kem_mlkem768_avx2_unpacked_init_key_pair(void) {
KRML_ATTRIBUTE_TARGET("avx2")
static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63
libcrux_ml_kem_mlkem768_avx2_unpacked_init_public_key(void) {
return libcrux_ml_kem_ind_cca_unpacked_default_1c_ab();
return libcrux_ml_kem_ind_cca_unpacked_default_09_ab();
}

/**
Get the serialized public key.
*/
/**
This function found in impl
{libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked<Vector,
K>[TraitClause@0, TraitClause@1]}
K>[TraitClause@0, TraitClause@1]#3}
*/
/**
A monomorphic instance of
libcrux_ml_kem.ind_cca.unpacked.serialized_public_key_mut_dd with types
libcrux_ml_kem.ind_cca.unpacked.serialized_public_key_mut_30 with types
libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics
- K= 3
- RANKED_BYTES_PER_RING_ELEMENT= 1152
- PUBLIC_KEY_SIZE= 1184
*/
KRML_ATTRIBUTE_TARGET("avx2")
static KRML_MUSTINLINE void
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_ed(
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_ed(
libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *self,
libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) {
libcrux_ml_kem_ind_cpa_serialize_public_key_mut_ed(
Expand All @@ -7380,28 +7382,25 @@ libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_ed(
serialized->value);
}

/**
Get the serialized public key.
*/
/**
This function found in impl
{libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked<Vector,
K>[TraitClause@0, TraitClause@1]#2}
K>[TraitClause@0, TraitClause@1]#4}
*/
/**
A monomorphic instance of
libcrux_ml_kem.ind_cca.unpacked.serialized_public_key_mut_de with types
libcrux_ml_kem.ind_cca.unpacked.serialized_public_key_mut_fc with types
libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics
- K= 3
- RANKED_BYTES_PER_RING_ELEMENT= 1152
- PUBLIC_KEY_SIZE= 1184
*/
KRML_ATTRIBUTE_TARGET("avx2")
static KRML_MUSTINLINE void
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_ed(
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_fc_ed(
libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *self,
libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) {
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_ed(
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_ed(
&self->public_key, serialized);
}

Expand All @@ -7413,7 +7412,7 @@ static inline void
libcrux_ml_kem_mlkem768_avx2_unpacked_key_pair_serialized_public_key(
libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *key_pair,
libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) {
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_ed(key_pair,
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_fc_ed(key_pair,
serialized);
}

Expand Down Expand Up @@ -7457,17 +7456,17 @@ libcrux_ml_kem_ind_cpa_unpacked_clone_ef_ab(
/**
This function found in impl {(core::clone::Clone for
libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked<Vector,
K>[TraitClause@0, TraitClause@2])#4}
K>[TraitClause@0, TraitClause@2])#2}
*/
/**
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.clone_28
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.clone_dd
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics
- K= 3
*/
KRML_ATTRIBUTE_TARGET("avx2")
static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63
libcrux_ml_kem_ind_cca_unpacked_clone_28_ab(
libcrux_ml_kem_ind_cca_unpacked_clone_dd_ab(
libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *self) {
libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 lit;
lit.ind_cpa_public_key =
Expand All @@ -7479,23 +7478,20 @@ libcrux_ml_kem_ind_cca_unpacked_clone_28_ab(
return lit;
}

/**
Get the serialized public key.
*/
/**
This function found in impl
{libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked<Vector,
K>[TraitClause@0, TraitClause@1]#2}
K>[TraitClause@0, TraitClause@1]#4}
*/
/**
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.public_key_de
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.public_key_fc
with types libcrux_ml_kem_vector_avx2_SIMD256Vector
with const generics
- K= 3
*/
KRML_ATTRIBUTE_TARGET("avx2")
static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *
libcrux_ml_kem_ind_cca_unpacked_public_key_de_ab(
libcrux_ml_kem_ind_cca_unpacked_public_key_fc_ab(
libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *self) {
return &self->public_key;
}
Expand All @@ -7508,8 +7504,8 @@ static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_public_key(
libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *key_pair,
libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *pk) {
libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 uu____0 =
libcrux_ml_kem_ind_cca_unpacked_clone_28_ab(
libcrux_ml_kem_ind_cca_unpacked_public_key_de_ab(key_pair));
libcrux_ml_kem_ind_cca_unpacked_clone_dd_ab(
libcrux_ml_kem_ind_cca_unpacked_public_key_fc_ab(key_pair));
pk[0U] = uu____0;
}

Expand All @@ -7520,13 +7516,10 @@ KRML_ATTRIBUTE_TARGET("avx2")
static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_serialized_public_key(
libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *public_key,
libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) {
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_ed(public_key,
libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_ed(public_key,
serialized);
}

/**
Generate an unpacked key from a serialized key.
*/
/**
A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.unpack_public_key
with types libcrux_ml_kem_hash_functions_avx2_Simd256Hash,
Expand Down
2 changes: 1 addition & 1 deletion libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
* Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
* F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
* Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
* Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
*/

#ifndef __libcrux_mlkem768_avx2_types_H
Expand Down
Loading

0 comments on commit 168a963

Please sign in to comment.