Skip to content

Commit

Permalink
Merge pull request #647 from cryspen/dev-cpa-compress
Browse files Browse the repository at this point in the history 
Proofs for Ind-cpa and portable compress modules
  • Loading branch information
@karthikbhargavan
karthikbhargavan authored Nov 1, 2024
2 parents fb469cb + cef1e01 commit 8067654
Show file tree
Hide file tree
Showing 95 changed files with 8,746 additions and 9,234 deletions.
192 changes: 96 additions & 96 deletions Cargo.lock
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion libcrux-ml-kem/c/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: 99b4e0ae6147eb731652e0ee355fc77d2c160664
Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
128 changes: 55 additions & 73 deletions libcrux-ml-kem/c/internal/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: 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

0 comments on commit 8067654

Please sign in to comment.