Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proofs for Ind-cpa and portable compress modules #647

Merged
merged 6 commits into from
Nov 1, 2024
Merged

Proofs for Ind-cpa and portable compress modules #647

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
e6f5c98
Proofs for Ind-cpa and portable compress modules
mamonet Oct 30, 2024
020cd93
Update Cargo.lock
mamonet Oct 30, 2024
7f7e08c
refreshed C code
karthikbhargavan Oct 30, 2024
4b0d787
restored c/cg
karthikbhargavan Oct 30, 2024
18a089c
c code refresh
karthikbhargavan Oct 30, 2024
cef1e01
regen c files
karthikbhargavan Nov 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
192 changes: 96 additions & 96 deletions Cargo.lock
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/code_gen.txt
View file
Open in desktop
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: 99b4e0ae6147eb731652e0ee355fc77d2c160664
Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
128 changes: 55 additions & 73 deletions libcrux-ml-kem/c/internal/libcrux_core.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
* Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
* F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
* Libcrux: 99b4e0ae6147eb731652e0ee355fc77d2c160664
* Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
*/

#ifndef __internal_libcrux_core_H
Expand Down Expand Up @@ -62,163 +62,151 @@ typedef struct libcrux_ml_kem_utils_extraction_helper_Keypair768_s {

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#16}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_40
A monomorphic instance of libcrux_ml_kem.types.from_5a
with const generics
- SIZE= 1568
*/
libcrux_ml_kem_types_MlKemPublicKey_64 libcrux_ml_kem_types_from_40_af(
libcrux_ml_kem_types_MlKemPublicKey_64 libcrux_ml_kem_types_from_5a_af(
uint8_t value[1568U]);

/**
Create a new [`MlKemKeyPair`] from the secret and public key.
*/
/**
This function found in impl
{libcrux_ml_kem::types::MlKemKeyPair<PRIVATE_KEY_SIZE, PUBLIC_KEY_SIZE>}
{libcrux_ml_kem::types::MlKemKeyPair<PRIVATE_KEY_SIZE, PUBLIC_KEY_SIZE>#21}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_17
A monomorphic instance of libcrux_ml_kem.types.from_3a
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_mlkem1024_MlKem1024KeyPair libcrux_ml_kem_types_from_3a_94(
libcrux_ml_kem_types_MlKemPrivateKey_83 sk,
libcrux_ml_kem_types_MlKemPublicKey_64 pk);

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemPrivateKey<SIZE>)#10}
libcrux_ml_kem::types::MlKemPrivateKey<SIZE>)#9}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_88
A monomorphic instance of libcrux_ml_kem.types.from_7f
with const generics
- SIZE= 3168
*/
libcrux_ml_kem_types_MlKemPrivateKey_83 libcrux_ml_kem_types_from_88_39(
libcrux_ml_kem_types_MlKemPrivateKey_83 libcrux_ml_kem_types_from_7f_39(
uint8_t value[3168U]);

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#16}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_40
A monomorphic instance of libcrux_ml_kem.types.from_5a
with const generics
- SIZE= 1184
*/
libcrux_ml_kem_types_MlKemPublicKey_30 libcrux_ml_kem_types_from_40_d0(
libcrux_ml_kem_types_MlKemPublicKey_30 libcrux_ml_kem_types_from_5a_d0(
uint8_t value[1184U]);

/**
Create a new [`MlKemKeyPair`] from the secret and public key.
*/
/**
This function found in impl
{libcrux_ml_kem::types::MlKemKeyPair<PRIVATE_KEY_SIZE, PUBLIC_KEY_SIZE>}
{libcrux_ml_kem::types::MlKemKeyPair<PRIVATE_KEY_SIZE, PUBLIC_KEY_SIZE>#21}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_17
A monomorphic instance of libcrux_ml_kem.types.from_3a
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_mlkem768_MlKem768KeyPair libcrux_ml_kem_types_from_3a_74(
libcrux_ml_kem_types_MlKemPrivateKey_d9 sk,
libcrux_ml_kem_types_MlKemPublicKey_30 pk);

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemPrivateKey<SIZE>)#10}
libcrux_ml_kem::types::MlKemPrivateKey<SIZE>)#9}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_88
A monomorphic instance of libcrux_ml_kem.types.from_7f
with const generics
- SIZE= 2400
*/
libcrux_ml_kem_types_MlKemPrivateKey_d9 libcrux_ml_kem_types_from_88_28(
libcrux_ml_kem_types_MlKemPrivateKey_d9 libcrux_ml_kem_types_from_7f_28(
uint8_t value[2400U]);

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#16}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_40
A monomorphic instance of libcrux_ml_kem.types.from_5a
with const generics
- SIZE= 800
*/
libcrux_ml_kem_types_MlKemPublicKey_52 libcrux_ml_kem_types_from_40_4d(
libcrux_ml_kem_types_MlKemPublicKey_52 libcrux_ml_kem_types_from_5a_4d(
uint8_t value[800U]);

/**
Create a new [`MlKemKeyPair`] from the secret and public key.
*/
/**
This function found in impl
{libcrux_ml_kem::types::MlKemKeyPair<PRIVATE_KEY_SIZE, PUBLIC_KEY_SIZE>}
{libcrux_ml_kem::types::MlKemKeyPair<PRIVATE_KEY_SIZE, PUBLIC_KEY_SIZE>#21}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_17
A monomorphic instance of libcrux_ml_kem.types.from_3a
with const generics
- PRIVATE_KEY_SIZE= 1632
- PUBLIC_KEY_SIZE= 800
*/
libcrux_ml_kem_types_MlKemKeyPair_3e libcrux_ml_kem_types_from_17_fa(
libcrux_ml_kem_types_MlKemKeyPair_3e libcrux_ml_kem_types_from_3a_fa(
libcrux_ml_kem_types_MlKemPrivateKey_fa sk,
libcrux_ml_kem_types_MlKemPublicKey_52 pk);

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemPrivateKey<SIZE>)#10}
libcrux_ml_kem::types::MlKemPrivateKey<SIZE>)#9}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_88
A monomorphic instance of libcrux_ml_kem.types.from_7f
with const generics
- SIZE= 1632
*/
libcrux_ml_kem_types_MlKemPrivateKey_fa libcrux_ml_kem_types_from_88_2a(
libcrux_ml_kem_types_MlKemPrivateKey_fa libcrux_ml_kem_types_from_7f_2a(
uint8_t value[1632U]);

/**
A reference to the raw byte slice.
*/
/**
This function found in impl {libcrux_ml_kem::types::MlKemPublicKey<SIZE>#21}
This function found in impl {libcrux_ml_kem::types::MlKemPublicKey<SIZE>#20}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.as_slice_ba
A monomorphic instance of libcrux_ml_kem.types.as_slice_fd
with const generics
- SIZE= 1184
*/
uint8_t *libcrux_ml_kem_types_as_slice_ba_d0(
uint8_t *libcrux_ml_kem_types_as_slice_fd_d0(
libcrux_ml_kem_types_MlKemPublicKey_30 *self);

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#3}
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#2}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_fc
A monomorphic instance of libcrux_ml_kem.types.from_01
with const generics
- SIZE= 1088
*/
libcrux_ml_kem_mlkem768_MlKem768Ciphertext libcrux_ml_kem_types_from_fc_80(
libcrux_ml_kem_mlkem768_MlKem768Ciphertext libcrux_ml_kem_types_from_01_80(
uint8_t value[1088U]);

/**
This function found in impl {(core::convert::AsRef<@Slice<u8>> for
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#2}
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#1}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.as_ref_fd
A monomorphic instance of libcrux_ml_kem.types.as_ref_00
with const generics
- SIZE= 1088
*/
Eurydice_slice libcrux_ml_kem_types_as_ref_fd_80(
Eurydice_slice libcrux_ml_kem_types_as_ref_00_80(
libcrux_ml_kem_mlkem768_MlKem768Ciphertext *self);

/**
Expand All @@ -233,41 +221,38 @@ void libcrux_ml_kem_utils_into_padded_array_15(Eurydice_slice slice,
uint8_t ret[1120U]);

/**
A reference to the raw byte slice.
*/
/**
This function found in impl {libcrux_ml_kem::types::MlKemPublicKey<SIZE>#21}
This function found in impl {libcrux_ml_kem::types::MlKemPublicKey<SIZE>#20}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.as_slice_ba
A monomorphic instance of libcrux_ml_kem.types.as_slice_fd
with const generics
- SIZE= 800
*/
uint8_t *libcrux_ml_kem_types_as_slice_ba_4d(
uint8_t *libcrux_ml_kem_types_as_slice_fd_4d(
libcrux_ml_kem_types_MlKemPublicKey_52 *self);

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#3}
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#2}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_fc
A monomorphic instance of libcrux_ml_kem.types.from_01
with const generics
- SIZE= 768
*/
libcrux_ml_kem_types_MlKemCiphertext_1a libcrux_ml_kem_types_from_fc_d0(
libcrux_ml_kem_types_MlKemCiphertext_1a libcrux_ml_kem_types_from_01_d0(
uint8_t value[768U]);

/**
This function found in impl {(core::convert::AsRef<@Slice<u8>> for
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#2}
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#1}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.as_ref_fd
A monomorphic instance of libcrux_ml_kem.types.as_ref_00
with const generics
- SIZE= 768
*/
Eurydice_slice libcrux_ml_kem_types_as_ref_fd_d0(
Eurydice_slice libcrux_ml_kem_types_as_ref_00_d0(
libcrux_ml_kem_types_MlKemCiphertext_1a *self);

/**
Expand All @@ -282,17 +267,14 @@ void libcrux_ml_kem_utils_into_padded_array_4d(Eurydice_slice slice,
uint8_t ret[800U]);

/**
A reference to the raw byte slice.
This function found in impl {libcrux_ml_kem::types::MlKemPublicKey<SIZE>#20}
*/
/**
This function found in impl {libcrux_ml_kem::types::MlKemPublicKey<SIZE>#21}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.as_slice_ba
A monomorphic instance of libcrux_ml_kem.types.as_slice_fd
with const generics
- SIZE= 1568
*/
uint8_t *libcrux_ml_kem_types_as_slice_ba_af(
uint8_t *libcrux_ml_kem_types_as_slice_fd_af(
libcrux_ml_kem_types_MlKemPublicKey_64 *self);

/**
Expand Down Expand Up @@ -332,14 +314,14 @@ void libcrux_ml_kem_utils_into_padded_array_b6(Eurydice_slice slice,

/**
This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#3}
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#2}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.from_fc
A monomorphic instance of libcrux_ml_kem.types.from_01
with const generics
- SIZE= 1568
*/
libcrux_ml_kem_types_MlKemCiphertext_64 libcrux_ml_kem_types_from_fc_af(
libcrux_ml_kem_types_MlKemCiphertext_64 libcrux_ml_kem_types_from_01_af(
uint8_t value[1568U]);

/**
Expand All @@ -355,14 +337,14 @@ void libcrux_ml_kem_utils_into_padded_array_c8(Eurydice_slice slice,

/**
This function found in impl {(core::convert::AsRef<@Slice<u8>> for
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#2}
libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#1}
*/
/**
A monomorphic instance of libcrux_ml_kem.types.as_ref_fd
A monomorphic instance of libcrux_ml_kem.types.as_ref_00
with const generics
- SIZE= 1568
*/
Eurydice_slice libcrux_ml_kem_types_as_ref_fd_af(
Eurydice_slice libcrux_ml_kem_types_as_ref_00_af(
libcrux_ml_kem_types_MlKemCiphertext_64 *self);

/**
Expand Down
Loading
Loading