diff --git a/Cargo.lock b/Cargo.lock index 363acf1a7..94f450b74 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -697,8 +697,8 @@ dependencies = [ [[package]] name = "hax-lib" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax/#1c5e17c9ceee5adede0f4ea7f68bb3d8337f33a0" +version = "0.1.0-rc.1" +source = "git+https://github.com/hacspec/hax/#de59826b832befc82905286d052c8a961c31f3cd" dependencies = [ "hax-lib-macros", "num-bigint", @@ -707,8 +707,8 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax/#1c5e17c9ceee5adede0f4ea7f68bb3d8337f33a0" +version = "0.1.0-rc.1" +source = "git+https://github.com/hacspec/hax/#de59826b832befc82905286d052c8a961c31f3cd" dependencies = [ "hax-lib-macros-types", "paste", @@ -720,8 +720,8 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax/#1c5e17c9ceee5adede0f4ea7f68bb3d8337f33a0" +version = "0.1.0-rc.1" +source = "git+https://github.com/hacspec/hax/#de59826b832befc82905286d052c8a961c31f3cd" dependencies = [ "proc-macro2", "quote", diff --git a/fstar-helpers/fstar-bitvec/BitVecEq.fsti b/fstar-helpers/fstar-bitvec/BitVecEq.fsti index c370f28bf..6792f2b29 100644 --- a/fstar-helpers/fstar-bitvec/BitVecEq.fsti +++ b/fstar-helpers/fstar-bitvec/BitVecEq.fsti @@ -1,5 +1,5 @@ module BitVecEq -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 100" open Core open FStar.Mul open MkSeq @@ -72,7 +72,7 @@ let int_t_array_bitwise_eq // else get_bit_nat (pow2 (bits n) + v x) (v nth)) // with get_bit_intro #n x nth -#push-options "--fuel 0 --ifuel 0 --z3rlimit 80" +#push-options "--fuel 0 --ifuel 0 --z3rlimit 150" /// Rewrite a `bit_vec_of_int_t_array (Seq.slice arr ...)` into a `bit_vec_sub ...` let int_t_seq_slice_to_bv_sub_lemma #t #n (arr: t_Array (int_t t) n) diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt index 420446603..54242b657 100644 --- a/libcrux-ml-kem/c/code_gen.txt +++ b/libcrux-ml-kem/c/code_gen.txt @@ -2,5 +2,5 @@ This code was generated with the following revisions: Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 Karamel: 8c3612018c25889288da6857771be3ad03b75bcd -F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty -Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a +F*: 5643e656b989aca7629723653a2570c7df6252b9 +Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h index 69032a33e..fe89acd19 100644 --- a/libcrux-ml-kem/c/internal/libcrux_core.h +++ b/libcrux-ml-kem/c/internal/libcrux_core.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __internal_libcrux_core_H diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h index 9baf58ca5..466ef3ba0 100644 --- a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h +++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __internal_libcrux_mlkem_avx2_H diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h index 7ba532d5e..f108fb1a3 100644 --- a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h +++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __internal_libcrux_mlkem_portable_H @@ -23,7 +23,7 @@ extern "C" { #include "internal/libcrux_core.h" #include "internal/libcrux_sha3_internal.h" -int16_t libcrux_ml_kem_polynomial_get_zeta(size_t i); +int16_t libcrux_ml_kem_polynomial_zeta(size_t i); #define LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT \ (LIBCRUX_ML_KEM_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT / \ diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h index 0d99b2edd..67b2d4675 100644 --- a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __internal_libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h index 6d47ffcbc..342c481f4 100644 --- a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h +++ b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __internal_libcrux_sha3_internal_H diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c index 03c9cddb6..e69d41843 100644 --- a/libcrux-ml-kem/c/libcrux_core.c +++ b/libcrux-ml-kem/c/libcrux_core.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "internal/libcrux_core.h" diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h index f1e63c7a9..9097eceda 100644 --- a/libcrux-ml-kem/c/libcrux_core.h +++ b/libcrux-ml-kem/c/libcrux_core.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_core_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h index 6ba68daf6..041b2ec09 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem1024_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c index 6aa0b5776..5fec937b0 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "libcrux_mlkem1024_avx2.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h index c662e3584..96971f755 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem1024_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c index bc4294748..c63594eaa 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "libcrux_mlkem1024_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h index 90211f1e5..f951149be 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem1024_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h index d27735aa5..0e850ae5d 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem512_H @@ -21,28 +21,52 @@ extern "C" { #include "eurydice_glue.h" #include "libcrux_core.h" -#define LIBCRUX_ML_KEM_MLKEM512_C1_BLOCK_SIZE_512 ((size_t)320U) +#define LIBCRUX_ML_KEM_MLKEM512_VECTOR_U_COMPRESSION_FACTOR_512 ((size_t)10U) + +#define LIBCRUX_ML_KEM_MLKEM512_C1_BLOCK_SIZE_512 \ + (LIBCRUX_ML_KEM_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * \ + LIBCRUX_ML_KEM_MLKEM512_VECTOR_U_COMPRESSION_FACTOR_512 / (size_t)8U) + +#define LIBCRUX_ML_KEM_MLKEM512_RANK_512 ((size_t)2U) + +#define LIBCRUX_ML_KEM_MLKEM512_C1_SIZE_512 \ + (LIBCRUX_ML_KEM_MLKEM512_C1_BLOCK_SIZE_512 * LIBCRUX_ML_KEM_MLKEM512_RANK_512) + +#define LIBCRUX_ML_KEM_MLKEM512_VECTOR_V_COMPRESSION_FACTOR_512 ((size_t)4U) -#define LIBCRUX_ML_KEM_MLKEM512_C1_SIZE_512 ((size_t)640U) +#define LIBCRUX_ML_KEM_MLKEM512_C2_SIZE_512 \ + (LIBCRUX_ML_KEM_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * \ + LIBCRUX_ML_KEM_MLKEM512_VECTOR_V_COMPRESSION_FACTOR_512 / (size_t)8U) -#define LIBCRUX_ML_KEM_MLKEM512_C2_SIZE_512 ((size_t)128U) +#define LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_CIPHERTEXT_SIZE_512 \ + (LIBCRUX_ML_KEM_MLKEM512_C1_SIZE_512 + LIBCRUX_ML_KEM_MLKEM512_C2_SIZE_512) -#define LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_CIPHERTEXT_SIZE_512 ((size_t)768U) +#define LIBCRUX_ML_KEM_MLKEM512_T_AS_NTT_ENCODED_SIZE_512 \ + (LIBCRUX_ML_KEM_MLKEM512_RANK_512 * \ + LIBCRUX_ML_KEM_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * \ + LIBCRUX_ML_KEM_CONSTANTS_BITS_PER_COEFFICIENT / (size_t)8U) -#define LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_PUBLIC_KEY_SIZE_512 ((size_t)800U) +#define LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_PUBLIC_KEY_SIZE_512 \ + (LIBCRUX_ML_KEM_MLKEM512_T_AS_NTT_ENCODED_SIZE_512 + (size_t)32U) -#define LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_SECRET_KEY_SIZE_512 ((size_t)768U) +#define LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_SECRET_KEY_SIZE_512 \ + (LIBCRUX_ML_KEM_MLKEM512_RANK_512 * \ + LIBCRUX_ML_KEM_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * \ + LIBCRUX_ML_KEM_CONSTANTS_BITS_PER_COEFFICIENT / (size_t)8U) #define LIBCRUX_ML_KEM_MLKEM512_ETA1 ((size_t)3U) -#define LIBCRUX_ML_KEM_MLKEM512_ETA1_RANDOMNESS_SIZE ((size_t)192U) +#define LIBCRUX_ML_KEM_MLKEM512_ETA1_RANDOMNESS_SIZE \ + (LIBCRUX_ML_KEM_MLKEM512_ETA1 * (size_t)64U) #define LIBCRUX_ML_KEM_MLKEM512_ETA2 ((size_t)2U) -#define LIBCRUX_ML_KEM_MLKEM512_ETA2_RANDOMNESS_SIZE ((size_t)128U) +#define LIBCRUX_ML_KEM_MLKEM512_ETA2_RANDOMNESS_SIZE \ + (LIBCRUX_ML_KEM_MLKEM512_ETA2 * (size_t)64U) #define LIBCRUX_ML_KEM_MLKEM512_IMPLICIT_REJECTION_HASH_INPUT_SIZE \ - ((size_t)800U) + (LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE + \ + LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_CIPHERTEXT_SIZE_512) typedef libcrux_ml_kem_types_MlKemCiphertext_1a libcrux_ml_kem_mlkem512_MlKem512Ciphertext; @@ -56,17 +80,15 @@ typedef libcrux_ml_kem_types_MlKemPrivateKey_fa typedef libcrux_ml_kem_types_MlKemPublicKey_52 libcrux_ml_kem_mlkem512_MlKem512PublicKey; -#define LIBCRUX_ML_KEM_MLKEM512_RANKED_BYTES_PER_RING_ELEMENT_512 ((size_t)768U) +#define LIBCRUX_ML_KEM_MLKEM512_RANKED_BYTES_PER_RING_ELEMENT_512 \ + (LIBCRUX_ML_KEM_MLKEM512_RANK_512 * \ + LIBCRUX_ML_KEM_CONSTANTS_BITS_PER_RING_ELEMENT / (size_t)8U) -#define LIBCRUX_ML_KEM_MLKEM512_RANK_512 ((size_t)2U) - -#define LIBCRUX_ML_KEM_MLKEM512_SECRET_KEY_SIZE_512 ((size_t)1632U) - -#define LIBCRUX_ML_KEM_MLKEM512_T_AS_NTT_ENCODED_SIZE_512 ((size_t)768U) - -#define LIBCRUX_ML_KEM_MLKEM512_VECTOR_U_COMPRESSION_FACTOR_512 ((size_t)10U) - -#define LIBCRUX_ML_KEM_MLKEM512_VECTOR_V_COMPRESSION_FACTOR_512 ((size_t)4U) +#define LIBCRUX_ML_KEM_MLKEM512_SECRET_KEY_SIZE_512 \ + (LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_SECRET_KEY_SIZE_512 + \ + LIBCRUX_ML_KEM_MLKEM512_CPA_PKE_PUBLIC_KEY_SIZE_512 + \ + LIBCRUX_ML_KEM_CONSTANTS_H_DIGEST_SIZE + \ + LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE) #if defined(__cplusplus) } diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c index b45c8295b..7971b5c4f 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "libcrux_mlkem512_avx2.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h index d5ec40d83..3c4030f73 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem512_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c index 2fc72d307..b8f6fd756 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "libcrux_mlkem512_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h index 6e3d9755b..7766250f2 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem512_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h index bcfb76ff3..f2c7db21a 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem768_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c index fdf226bd8..d30955e8a 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "libcrux_mlkem768_avx2.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h index 08c3fa5b7..ea29365da 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem768_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c index c59bc0046..1cdebda61 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "libcrux_mlkem768_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h index 03f9d22a4..6c512c865 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem768_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c index 61f343a77..7cd2d548f 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "internal/libcrux_mlkem_avx2.h" @@ -2248,9 +2248,9 @@ static KRML_MUSTINLINE void ntt_at_layer_4_plus_61( for (size_t i = offset_vec; i < offset_vec + step_vec; i++) { size_t j = i; libcrux_ml_kem_vector_avx2_SIMD256Vector_x2 uu____0 = - ntt_layer_int_vec_step_61( - re->coefficients[j], re->coefficients[j + step_vec], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + ntt_layer_int_vec_step_61(re->coefficients[j], + re->coefficients[j + step_vec], + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); __m256i x = uu____0.fst; __m256i y = uu____0.snd; re->coefficients[j] = x; @@ -2272,7 +2272,7 @@ static KRML_MUSTINLINE void ntt_at_layer_3_61( zeta_i[0U] = zeta_i[0U] + (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_avx2_ntt_layer_3_step_09( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]));); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U]));); } /** @@ -2287,9 +2287,8 @@ static KRML_MUSTINLINE void ntt_at_layer_2_61( i, (size_t)0U, (size_t)16U, (size_t)1U, size_t round = i; zeta_i[0U] = zeta_i[0U] + (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_avx2_ntt_layer_2_step_09( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)1U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)1U)); zeta_i[0U] = zeta_i[0U] + (size_t)1U;); } @@ -2305,11 +2304,10 @@ static KRML_MUSTINLINE void ntt_at_layer_1_61( i, (size_t)0U, (size_t)16U, (size_t)1U, size_t round = i; zeta_i[0U] = zeta_i[0U] + (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_avx2_ntt_layer_1_step_09( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)3U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)1U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)2U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)3U)); zeta_i[0U] = zeta_i[0U] + (size_t)3U;); } @@ -2449,13 +2447,13 @@ ntt_multiply_ef_61(libcrux_ml_kem_polynomial_PolynomialRingElement_f6 *self, size_t i0 = i; out.coefficients[i0] = libcrux_ml_kem_vector_avx2_ntt_multiply_09( &self->coefficients[i0], &rhs->coefficients[i0], - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)3U)); + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)1U), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)2U), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)3U)); } return out; } @@ -2979,10 +2977,10 @@ static KRML_MUSTINLINE void invert_ntt_at_layer_1_61( re->coefficients[round] = libcrux_ml_kem_vector_avx2_inv_ntt_layer_1_step_09( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)3U)); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)1U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)2U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)3U)); zeta_i[0U] = zeta_i[0U] - (size_t)3U;); } @@ -3000,8 +2998,8 @@ static KRML_MUSTINLINE void invert_ntt_at_layer_2_61( re->coefficients[round] = libcrux_ml_kem_vector_avx2_inv_ntt_layer_2_step_09( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)1U)); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)1U)); zeta_i[0U] = zeta_i[0U] - (size_t)1U;); } @@ -3018,7 +3016,7 @@ static KRML_MUSTINLINE void invert_ntt_at_layer_3_61( re->coefficients[round] = libcrux_ml_kem_vector_avx2_inv_ntt_layer_3_step_09( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]));); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U]));); } /** @@ -3060,7 +3058,7 @@ static KRML_MUSTINLINE void invert_ntt_at_layer_4_plus_61( libcrux_ml_kem_vector_avx2_SIMD256Vector_x2 uu____0 = inv_ntt_layer_int_vec_step_reduce_61( re->coefficients[j], re->coefficients[j + step_vec], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); __m256i x = uu____0.fst; __m256i y = uu____0.snd; re->coefficients[j] = x; @@ -4555,17 +4553,17 @@ void libcrux_ml_kem_ind_cca_decapsulate_a11( kdf_d8_ae(Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - kdf_d8_ae(shared_secret0, shared_secret1); uint8_t shared_secret[32U]; + kdf_d8_ae(shared_secret0, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_80(ciphertext), Eurydice_array_to_slice((size_t)1088U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } /** @@ -6615,17 +6613,17 @@ void libcrux_ml_kem_ind_cca_decapsulate_a10( kdf_d8_5e(Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - kdf_d8_5e(shared_secret0, shared_secret1); uint8_t shared_secret[32U]; + kdf_d8_5e(shared_secret0, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_af(ciphertext), Eurydice_array_to_slice((size_t)1568U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } /** @@ -8631,15 +8629,15 @@ void libcrux_ml_kem_ind_cca_decapsulate_a1( kdf_d8_4d(Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - kdf_d8_4d(shared_secret0, shared_secret1); uint8_t shared_secret[32U]; + kdf_d8_4d(shared_secret0, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_d0(ciphertext), Eurydice_array_to_slice((size_t)768U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h index c127a7b25..95dad8cf8 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.c b/libcrux-ml-kem/c/libcrux_mlkem_portable.c index 128049b3b..1d3a317a8 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "internal/libcrux_mlkem_portable.h" @@ -66,7 +66,7 @@ static const int16_t ZETAS_TIMES_MONTGOMERY_R[128U] = { (int16_t)-108, (int16_t)-308, (int16_t)996, (int16_t)991, (int16_t)958, (int16_t)-1460, (int16_t)1522, (int16_t)1628}; -int16_t libcrux_ml_kem_polynomial_get_zeta(size_t i) { +int16_t libcrux_ml_kem_polynomial_zeta(size_t i) { return ZETAS_TIMES_MONTGOMERY_R[i]; } @@ -3532,9 +3532,9 @@ static KRML_MUSTINLINE void ntt_at_layer_4_plus_8c( for (size_t i = offset_vec; i < offset_vec + step_vec; i++) { size_t j = i; libcrux_ml_kem_vector_portable_vector_type_PortableVector_x2 uu____0 = - ntt_layer_int_vec_step_8c( - re->coefficients[j], re->coefficients[j + step_vec], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + ntt_layer_int_vec_step_8c(re->coefficients[j], + re->coefficients[j + step_vec], + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); libcrux_ml_kem_vector_portable_vector_type_PortableVector x = uu____0.fst; libcrux_ml_kem_vector_portable_vector_type_PortableVector y = uu____0.snd; re->coefficients[j] = x; @@ -3557,7 +3557,7 @@ static KRML_MUSTINLINE void ntt_at_layer_3_8c( libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 = libcrux_ml_kem_vector_portable_ntt_layer_3_step_0d( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); re->coefficients[round] = uu____0;); } @@ -3575,8 +3575,8 @@ static KRML_MUSTINLINE void ntt_at_layer_2_8c( re->coefficients[round] = libcrux_ml_kem_vector_portable_ntt_layer_2_step_0d( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)1U)); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)1U)); zeta_i[0U] = zeta_i[0U] + (size_t)1U;); } @@ -3594,10 +3594,10 @@ static KRML_MUSTINLINE void ntt_at_layer_1_8c( re->coefficients[round] = libcrux_ml_kem_vector_portable_ntt_layer_1_step_0d( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)3U)); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)1U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)2U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)3U)); zeta_i[0U] = zeta_i[0U] + (size_t)3U;); } @@ -3742,13 +3742,13 @@ ntt_multiply_ef_8c(libcrux_ml_kem_polynomial_PolynomialRingElement_1d *self, libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 = libcrux_ml_kem_vector_portable_ntt_multiply_0d( &self->coefficients[i0], &rhs->coefficients[i0], - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)3U)); + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)1U), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)2U), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)3U)); out.coefficients[i0] = uu____0; } return out; @@ -4284,10 +4284,10 @@ static KRML_MUSTINLINE void invert_ntt_at_layer_1_8c( re->coefficients[round] = libcrux_ml_kem_vector_portable_inv_ntt_layer_1_step_0d( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)3U)); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)1U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)2U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)3U)); zeta_i[0U] = zeta_i[0U] - (size_t)3U;); } @@ -4305,8 +4305,8 @@ static KRML_MUSTINLINE void invert_ntt_at_layer_2_8c( re->coefficients[round] = libcrux_ml_kem_vector_portable_inv_ntt_layer_2_step_0d( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)1U)); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)1U)); zeta_i[0U] = zeta_i[0U] - (size_t)1U;); } @@ -4324,7 +4324,7 @@ static KRML_MUSTINLINE void invert_ntt_at_layer_3_8c( libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 = libcrux_ml_kem_vector_portable_inv_ntt_layer_3_step_0d( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); re->coefficients[round] = uu____0;); } @@ -4373,7 +4373,7 @@ static KRML_MUSTINLINE void invert_ntt_at_layer_4_plus_8c( libcrux_ml_kem_vector_portable_vector_type_PortableVector_x2 uu____0 = inv_ntt_layer_int_vec_step_reduce_8c( re->coefficients[j], re->coefficients[j + step_vec], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); libcrux_ml_kem_vector_portable_vector_type_PortableVector x = uu____0.fst; libcrux_ml_kem_vector_portable_vector_type_PortableVector y = uu____0.snd; re->coefficients[j] = x; @@ -5724,17 +5724,17 @@ void libcrux_ml_kem_ind_cca_decapsulate_621( kdf_d8_60(Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - kdf_d8_60(shared_secret0, shared_secret1); uint8_t shared_secret[32U]; + kdf_d8_60(shared_secret0, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_af(ciphertext), Eurydice_array_to_slice((size_t)1568U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } /** @@ -7793,17 +7793,17 @@ void libcrux_ml_kem_ind_cca_decapsulate_620( kdf_d8_30(Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - kdf_d8_30(shared_secret0, shared_secret1); uint8_t shared_secret[32U]; + kdf_d8_30(shared_secret0, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_d0(ciphertext), Eurydice_array_to_slice((size_t)768U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } /** @@ -9756,15 +9756,15 @@ void libcrux_ml_kem_ind_cca_decapsulate_62( kdf_d8_d6(Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - kdf_d8_d6(shared_secret0, shared_secret1); uint8_t shared_secret[32U]; + kdf_d8_d6(shared_secret0, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_80(ciphertext), Eurydice_array_to_slice((size_t)1088U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/libcrux_mlkem_portable.h index 33fff6338..ccb5a6654 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem_portable_H diff --git a/libcrux-ml-kem/c/libcrux_sha3.h b/libcrux-ml-kem/c/libcrux_sha3.h index 3101a818f..393be1f15 100644 --- a/libcrux-ml-kem/c/libcrux_sha3.h +++ b/libcrux-ml-kem/c/libcrux_sha3.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_sha3_H diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.c b/libcrux-ml-kem/c/libcrux_sha3_avx2.c index 4e234ddec..3274dc64a 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_avx2.c +++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "internal/libcrux_sha3_avx2.h" diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/libcrux_sha3_avx2.h index 7a6e0c8cb..eaa8d8c25 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_sha3_internal.h b/libcrux-ml-kem/c/libcrux_sha3_internal.h index 7c140d2b8..c68ee5802 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_internal.h +++ b/libcrux-ml-kem/c/libcrux_sha3_internal.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_sha3_internal_H diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.c b/libcrux-ml-kem/c/libcrux_sha3_neon.c index c16b77594..8c9edc379 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_neon.c +++ b/libcrux-ml-kem/c/libcrux_sha3_neon.c @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #include "libcrux_sha3_neon.h" diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.h b/libcrux-ml-kem/c/libcrux_sha3_neon.h index 2f179ee38..c51c09cc5 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_neon.h +++ b/libcrux-ml-kem/c/libcrux_sha3_neon.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_sha3_neon_H diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt index 420446603..54242b657 100644 --- a/libcrux-ml-kem/cg/code_gen.txt +++ b/libcrux-ml-kem/cg/code_gen.txt @@ -2,5 +2,5 @@ This code was generated with the following revisions: Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 Karamel: 8c3612018c25889288da6857771be3ad03b75bcd -F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty -Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a +F*: 5643e656b989aca7629723653a2570c7df6252b9 +Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h index b5a34d0e2..b8e2354f8 100644 --- a/libcrux-ml-kem/cg/libcrux_core.h +++ b/libcrux-ml-kem/cg/libcrux_core.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_core_H diff --git a/libcrux-ml-kem/cg/libcrux_ct_ops.h b/libcrux-ml-kem/cg/libcrux_ct_ops.h index ddf47bd96..cf4a616ac 100644 --- a/libcrux-ml-kem/cg/libcrux_ct_ops.h +++ b/libcrux-ml-kem/cg/libcrux_ct_ops.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_ct_ops_H diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h index aa0858642..f6933bc18 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem768_avx2_H @@ -1676,7 +1676,7 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ntt_ntt_at_layer_4_plus_61( libcrux_ml_kem_vector_avx2_SIMD256Vector_x2 uu____0 = libcrux_ml_kem_ntt_ntt_layer_int_vec_step_61( re->coefficients[j], re->coefficients[j + step_vec], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); __m256i x = uu____0.fst; __m256i y = uu____0.snd; re->coefficients[j] = x; @@ -1699,8 +1699,7 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ntt_ntt_at_layer_3_61( size_t round = i; zeta_i[0U] = zeta_i[0U] + (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_avx2_ntt_layer_3_step_09( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); } } @@ -1718,8 +1717,8 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ntt_ntt_at_layer_2_61( size_t round = i; zeta_i[0U] = zeta_i[0U] + (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_avx2_ntt_layer_2_step_09( - re->coefficients[round], libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)1U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)1U)); zeta_i[0U] = zeta_i[0U] + (size_t)1U; } } @@ -1738,10 +1737,10 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ntt_ntt_at_layer_1_61( size_t round = i; zeta_i[0U] = zeta_i[0U] + (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_avx2_ntt_layer_1_step_09( - re->coefficients[round], libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)3U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)1U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)2U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)3U)); zeta_i[0U] = zeta_i[0U] + (size_t)3U; } } @@ -2062,13 +2061,13 @@ libcrux_ml_kem_polynomial_ntt_multiply_ef_61( size_t i0 = i; out.coefficients[i0] = libcrux_ml_kem_vector_avx2_ntt_multiply_09( &self->coefficients[i0], &rhs->coefficients[i0], - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)3U)); + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)1U), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)2U), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)3U)); } return out; } @@ -2114,11 +2113,10 @@ static KRML_MUSTINLINE void libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_1_61( zeta_i[0U] = zeta_i[0U] - (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_avx2_inv_ntt_layer_1_step_09( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)3U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)1U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)2U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)3U)); zeta_i[0U] = zeta_i[0U] - (size_t)3U; } } @@ -2138,9 +2136,8 @@ static KRML_MUSTINLINE void libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_2_61( zeta_i[0U] = zeta_i[0U] - (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_avx2_inv_ntt_layer_2_step_09( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)1U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)1U)); zeta_i[0U] = zeta_i[0U] - (size_t)1U; } } @@ -2161,7 +2158,7 @@ static KRML_MUSTINLINE void libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_3_61( re->coefficients[round] = libcrux_ml_kem_vector_avx2_inv_ntt_layer_3_step_09( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); } } @@ -2209,7 +2206,7 @@ libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_4_plus_61( libcrux_ml_kem_vector_avx2_SIMD256Vector_x2 uu____0 = libcrux_ml_kem_invert_ntt_inv_ntt_layer_int_vec_step_reduce_61( re->coefficients[j], re->coefficients[j + step_vec], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); __m256i x = uu____0.fst; __m256i y = uu____0.snd; re->coefficients[j] = x; @@ -4460,17 +4457,17 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ind_cca_decapsulate_a1( Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), ciphertext, implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - libcrux_ml_kem_variant_kdf_d8_ae(shared_secret0, ciphertext, shared_secret1); uint8_t shared_secret[32U]; + libcrux_ml_kem_variant_kdf_d8_ae(shared_secret0, ciphertext, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_80(ciphertext), Eurydice_array_to_slice((size_t)1088U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } /** @@ -5442,17 +5439,17 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ind_cca_decapsulate_a10( Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), ciphertext, implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - libcrux_ml_kem_variant_kdf_33_ae(shared_secret0, ciphertext, shared_secret1); uint8_t shared_secret[32U]; + libcrux_ml_kem_variant_kdf_33_ae(shared_secret0, ciphertext, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_80(ciphertext), Eurydice_array_to_slice((size_t)1088U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } /** diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h index 519b51565..8f0de6a3e 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_mlkem768_portable_H @@ -87,7 +87,7 @@ static const int16_t libcrux_ml_kem_polynomial_ZETAS_TIMES_MONTGOMERY_R[128U] = (int16_t)-108, (int16_t)-308, (int16_t)996, (int16_t)991, (int16_t)958, (int16_t)-1460, (int16_t)1522, (int16_t)1628}; -static KRML_MUSTINLINE int16_t libcrux_ml_kem_polynomial_get_zeta(size_t i) { +static KRML_MUSTINLINE int16_t libcrux_ml_kem_polynomial_zeta(size_t i) { return libcrux_ml_kem_polynomial_ZETAS_TIMES_MONTGOMERY_R[i]; } @@ -2889,7 +2889,7 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ntt_ntt_at_layer_4_plus_8c( libcrux_ml_kem_vector_portable_vector_type_PortableVector_x2 uu____0 = libcrux_ml_kem_ntt_ntt_layer_int_vec_step_8c( re->coefficients[j], re->coefficients[j + step_vec], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); libcrux_ml_kem_vector_portable_vector_type_PortableVector x = uu____0.fst; libcrux_ml_kem_vector_portable_vector_type_PortableVector y = uu____0.snd; re->coefficients[j] = x; @@ -2913,7 +2913,7 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ntt_ntt_at_layer_3_8c( libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 = libcrux_ml_kem_vector_portable_ntt_layer_3_step_0d( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); re->coefficients[round] = uu____0; } } @@ -2932,9 +2932,8 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ntt_ntt_at_layer_2_8c( zeta_i[0U] = zeta_i[0U] + (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_portable_ntt_layer_2_step_0d( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)1U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)1U)); zeta_i[0U] = zeta_i[0U] + (size_t)1U; } } @@ -2953,11 +2952,10 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ntt_ntt_at_layer_1_8c( zeta_i[0U] = zeta_i[0U] + (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_portable_ntt_layer_1_step_0d( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] + (size_t)3U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)1U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)2U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] + (size_t)3U)); zeta_i[0U] = zeta_i[0U] + (size_t)3U; } } @@ -3222,13 +3220,13 @@ libcrux_ml_kem_polynomial_ntt_multiply_ef_8c( libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 = libcrux_ml_kem_vector_portable_ntt_multiply_0d( &self->coefficients[i0], &rhs->coefficients[i0], - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta((size_t)64U + (size_t)4U * i0 + - (size_t)3U)); + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)1U), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)2U), + libcrux_ml_kem_polynomial_zeta((size_t)64U + (size_t)4U * i0 + + (size_t)3U)); out.coefficients[i0] = uu____0; } return out; @@ -3277,11 +3275,10 @@ static KRML_MUSTINLINE void libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_1_8c( zeta_i[0U] = zeta_i[0U] - (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_portable_inv_ntt_layer_1_step_0d( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)1U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)2U), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)3U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)1U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)2U), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)3U)); zeta_i[0U] = zeta_i[0U] - (size_t)3U; } } @@ -3300,9 +3297,8 @@ static KRML_MUSTINLINE void libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_2_8c( zeta_i[0U] = zeta_i[0U] - (size_t)1U; re->coefficients[round] = libcrux_ml_kem_vector_portable_inv_ntt_layer_2_step_0d( - re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U]), - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U] - (size_t)1U)); + re->coefficients[round], libcrux_ml_kem_polynomial_zeta(zeta_i[0U]), + libcrux_ml_kem_polynomial_zeta(zeta_i[0U] - (size_t)1U)); zeta_i[0U] = zeta_i[0U] - (size_t)1U; } } @@ -3322,7 +3318,7 @@ static KRML_MUSTINLINE void libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_3_8c( libcrux_ml_kem_vector_portable_vector_type_PortableVector uu____0 = libcrux_ml_kem_vector_portable_inv_ntt_layer_3_step_0d( re->coefficients[round], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); re->coefficients[round] = uu____0; } } @@ -3373,7 +3369,7 @@ libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_4_plus_8c( libcrux_ml_kem_vector_portable_vector_type_PortableVector_x2 uu____0 = libcrux_ml_kem_invert_ntt_inv_ntt_layer_int_vec_step_reduce_8c( re->coefficients[j], re->coefficients[j + step_vec], - libcrux_ml_kem_polynomial_get_zeta(zeta_i[0U])); + libcrux_ml_kem_polynomial_zeta(zeta_i[0U])); libcrux_ml_kem_vector_portable_vector_type_PortableVector x = uu____0.fst; libcrux_ml_kem_vector_portable_vector_type_PortableVector y = uu____0.snd; re->coefficients[j] = x; @@ -5456,17 +5452,17 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ind_cca_decapsulate_62( Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), ciphertext, implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - libcrux_ml_kem_variant_kdf_d8_d6(shared_secret0, ciphertext, shared_secret1); uint8_t shared_secret[32U]; + libcrux_ml_kem_variant_kdf_d8_d6(shared_secret0, ciphertext, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_80(ciphertext), Eurydice_array_to_slice((size_t)1088U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } /** @@ -6340,17 +6336,17 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ind_cca_decapsulate_620( Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret0, uint8_t), ciphertext, implicit_rejection_shared_secret); - uint8_t shared_secret1[32U]; - libcrux_ml_kem_variant_kdf_33_d6(shared_secret0, ciphertext, shared_secret1); uint8_t shared_secret[32U]; + libcrux_ml_kem_variant_kdf_33_d6(shared_secret0, ciphertext, shared_secret); + uint8_t ret0[32U]; libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time( libcrux_ml_kem_types_as_ref_43_80(ciphertext), Eurydice_array_to_slice((size_t)1088U, expected_ciphertext, uint8_t), - Eurydice_array_to_slice((size_t)32U, shared_secret1, uint8_t), + Eurydice_array_to_slice((size_t)32U, shared_secret, uint8_t), Eurydice_array_to_slice((size_t)32U, implicit_rejection_shared_secret, uint8_t), - shared_secret); - memcpy(ret, shared_secret, (size_t)32U * sizeof(uint8_t)); + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } /** diff --git a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h index a77bfdbea..7a519bf7c 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/cg/libcrux_sha3_portable.h b/libcrux-ml-kem/cg/libcrux_sha3_portable.h index d85d8e543..a606f5f71 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h @@ -7,8 +7,8 @@ * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9 * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20 * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd - * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty - * Libcrux: 3e54f3c659bef6ee815d197ee5c74dd40c75186a + * F*: 5643e656b989aca7629723653a2570c7df6252b9 + * Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36 */ #ifndef __libcrux_sha3_portable_H diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst index a6ffee609..ee9e56c50 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst @@ -235,7 +235,7 @@ let serialize_kem_secret_key #pop-options -#push-options "--z3rlimit 300" +#push-options "--z3rlimit 300 --ext context_pruning --split_queries always" let encapsulate (v_K v_CIPHERTEXT_SIZE v_PUBLIC_KEY_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_SIZE v_C2_SIZE v_VECTOR_U_COMPRESSION_FACTOR v_VECTOR_V_COMPRESSION_FACTOR v_C1_BLOCK_SIZE v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE: diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst index aeccf049f..53290fba7 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fst @@ -84,10 +84,10 @@ let invert_ntt_at_layer_1_ (Libcrux_ml_kem.Vector.Traits.f_inv_ntt_layer_1_step #v_Vector #FStar.Tactics.Typeclasses.solve (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ round ] <: v_Vector) - (Libcrux_ml_kem.Polynomial.get_zeta zeta_i <: i16) - (Libcrux_ml_kem.Polynomial.get_zeta (zeta_i -! sz 1 <: usize) <: i16) - (Libcrux_ml_kem.Polynomial.get_zeta (zeta_i -! sz 2 <: usize) <: i16) - (Libcrux_ml_kem.Polynomial.get_zeta (zeta_i -! sz 3 <: usize) <: i16) + (Libcrux_ml_kem.Polynomial.zeta zeta_i <: i16) + (Libcrux_ml_kem.Polynomial.zeta (zeta_i -! sz 1 <: usize) <: i16) + (Libcrux_ml_kem.Polynomial.zeta (zeta_i -! sz 2 <: usize) <: i16) + (Libcrux_ml_kem.Polynomial.zeta (zeta_i -! sz 3 <: usize) <: i16) <: v_Vector) } @@ -165,8 +165,8 @@ let invert_ntt_at_layer_2_ (Libcrux_ml_kem.Vector.Traits.f_inv_ntt_layer_2_step #v_Vector #FStar.Tactics.Typeclasses.solve (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ round ] <: v_Vector) - (Libcrux_ml_kem.Polynomial.get_zeta zeta_i <: i16) - (Libcrux_ml_kem.Polynomial.get_zeta (zeta_i -! sz 1 <: usize) <: i16) + (Libcrux_ml_kem.Polynomial.zeta zeta_i <: i16) + (Libcrux_ml_kem.Polynomial.zeta (zeta_i -! sz 1 <: usize) <: i16) <: v_Vector) } @@ -244,7 +244,7 @@ let invert_ntt_at_layer_3_ (Libcrux_ml_kem.Vector.Traits.f_inv_ntt_layer_3_step #v_Vector #FStar.Tactics.Typeclasses.solve (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ round ] <: v_Vector) - (Libcrux_ml_kem.Polynomial.get_zeta zeta_i <: i16) + (Libcrux_ml_kem.Polynomial.zeta zeta_i <: i16) <: v_Vector) } @@ -317,7 +317,7 @@ let invert_ntt_at_layer_4_plus (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ j +! step_vec <: usize ] <: v_Vector) - (Libcrux_ml_kem.Polynomial.get_zeta zeta_i <: i16) + (Libcrux_ml_kem.Polynomial.zeta zeta_i <: i16) in let re:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = { diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.fsti index 28d905063..94590e2ee 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.fsti @@ -3,39 +3,64 @@ module Libcrux_ml_kem.Mlkem512 open Core open FStar.Mul -let v_C1_BLOCK_SIZE_512_: usize = sz 320 +let v_ETA1: usize = sz 3 -let v_C1_SIZE_512_: usize = sz 640 +let v_ETA1_RANDOMNESS_SIZE: usize = v_ETA1 *! sz 64 -let v_C2_SIZE_512_: usize = sz 128 +let v_ETA2: usize = sz 2 -let v_CPA_PKE_CIPHERTEXT_SIZE_512_: usize = sz 768 +let v_ETA2_RANDOMNESS_SIZE: usize = v_ETA2 *! sz 64 -let v_CPA_PKE_PUBLIC_KEY_SIZE_512_: usize = sz 800 +let v_RANK_512_: usize = sz 2 -let v_CPA_PKE_SECRET_KEY_SIZE_512_: usize = sz 768 +let v_CPA_PKE_SECRET_KEY_SIZE_512_: usize = + ((v_RANK_512_ *! Libcrux_ml_kem.Constants.v_COEFFICIENTS_IN_RING_ELEMENT <: usize) *! + Libcrux_ml_kem.Constants.v_BITS_PER_COEFFICIENT + <: + usize) /! + sz 8 -let v_ETA1: usize = sz 3 +let v_RANKED_BYTES_PER_RING_ELEMENT_512_: usize = + (v_RANK_512_ *! Libcrux_ml_kem.Constants.v_BITS_PER_RING_ELEMENT <: usize) /! sz 8 -let v_ETA1_RANDOMNESS_SIZE: usize = sz 192 +let v_T_AS_NTT_ENCODED_SIZE_512_: usize = + ((v_RANK_512_ *! Libcrux_ml_kem.Constants.v_COEFFICIENTS_IN_RING_ELEMENT <: usize) *! + Libcrux_ml_kem.Constants.v_BITS_PER_COEFFICIENT + <: + usize) /! + sz 8 -let v_ETA2: usize = sz 2 +let v_CPA_PKE_PUBLIC_KEY_SIZE_512_: usize = v_T_AS_NTT_ENCODED_SIZE_512_ +! sz 32 -let v_ETA2_RANDOMNESS_SIZE: usize = sz 128 +let v_SECRET_KEY_SIZE_512_: usize = + ((v_CPA_PKE_SECRET_KEY_SIZE_512_ +! v_CPA_PKE_PUBLIC_KEY_SIZE_512_ <: usize) +! + Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE + <: + usize) +! + Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE -let v_IMPLICIT_REJECTION_HASH_INPUT_SIZE: usize = sz 800 +let v_VECTOR_U_COMPRESSION_FACTOR_512_: usize = sz 10 -let v_RANKED_BYTES_PER_RING_ELEMENT_512_: usize = sz 768 +let v_C1_BLOCK_SIZE_512_: usize = + (Libcrux_ml_kem.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_VECTOR_U_COMPRESSION_FACTOR_512_ + <: + usize) /! + sz 8 -let v_RANK_512_: usize = sz 2 +let v_C1_SIZE_512_: usize = v_C1_BLOCK_SIZE_512_ *! v_RANK_512_ -let v_SECRET_KEY_SIZE_512_: usize = sz 1632 +let v_VECTOR_V_COMPRESSION_FACTOR_512_: usize = sz 4 -let v_T_AS_NTT_ENCODED_SIZE_512_: usize = sz 768 +let v_C2_SIZE_512_: usize = + (Libcrux_ml_kem.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_VECTOR_V_COMPRESSION_FACTOR_512_ + <: + usize) /! + sz 8 -let v_VECTOR_U_COMPRESSION_FACTOR_512_: usize = sz 10 +let v_CPA_PKE_CIPHERTEXT_SIZE_512_: usize = v_C1_SIZE_512_ +! v_C2_SIZE_512_ -let v_VECTOR_V_COMPRESSION_FACTOR_512_: usize = sz 4 +let v_IMPLICIT_REJECTION_HASH_INPUT_SIZE: usize = + Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_512_ /// Validate a private key. /// Returns `true` if valid, and `false` otherwise. diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst index 2c5a30cb2..41d6dfad3 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fst @@ -81,10 +81,10 @@ let ntt_at_layer_1_ (Libcrux_ml_kem.Vector.Traits.f_ntt_layer_1_step #v_Vector #FStar.Tactics.Typeclasses.solve (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ round ] <: v_Vector) - (Libcrux_ml_kem.Polynomial.get_zeta zeta_i <: i16) - (Libcrux_ml_kem.Polynomial.get_zeta (zeta_i +! sz 1 <: usize) <: i16) - (Libcrux_ml_kem.Polynomial.get_zeta (zeta_i +! sz 2 <: usize) <: i16) - (Libcrux_ml_kem.Polynomial.get_zeta (zeta_i +! sz 3 <: usize) <: i16) + (Libcrux_ml_kem.Polynomial.zeta zeta_i <: i16) + (Libcrux_ml_kem.Polynomial.zeta (zeta_i +! sz 1 <: usize) <: i16) + (Libcrux_ml_kem.Polynomial.zeta (zeta_i +! sz 2 <: usize) <: i16) + (Libcrux_ml_kem.Polynomial.zeta (zeta_i +! sz 3 <: usize) <: i16) <: v_Vector) } @@ -163,8 +163,8 @@ let ntt_at_layer_2_ (Libcrux_ml_kem.Vector.Traits.f_ntt_layer_2_step #v_Vector #FStar.Tactics.Typeclasses.solve (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ round ] <: v_Vector) - (Libcrux_ml_kem.Polynomial.get_zeta zeta_i <: i16) - (Libcrux_ml_kem.Polynomial.get_zeta (zeta_i +! sz 1 <: usize) <: i16) + (Libcrux_ml_kem.Polynomial.zeta zeta_i <: i16) + (Libcrux_ml_kem.Polynomial.zeta (zeta_i +! sz 1 <: usize) <: i16) <: v_Vector) } @@ -243,7 +243,7 @@ let ntt_at_layer_3_ (Libcrux_ml_kem.Vector.Traits.f_ntt_layer_3_step #v_Vector #FStar.Tactics.Typeclasses.solve (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ round ] <: v_Vector) - (Libcrux_ml_kem.Polynomial.get_zeta zeta_i <: i16) + (Libcrux_ml_kem.Polynomial.zeta zeta_i <: i16) <: v_Vector) } @@ -315,7 +315,7 @@ let ntt_at_layer_4_plus (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ j +! step_vec <: usize ] <: v_Vector) - (Libcrux_ml_kem.Polynomial.get_zeta zeta_i <: i16) + (Libcrux_ml_kem.Polynomial.zeta zeta_i <: i16) in let re:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = { diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst index 4dcc55b91..fec53d917 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst @@ -9,7 +9,7 @@ let _ = let open Libcrux_ml_kem.Vector.Traits in () -let get_zeta (i: usize) = +let zeta (i: usize) = let result:i16 = v_ZETAS_TIMES_MONTGOMERY_R.[ i ] in let _:Prims.unit = admit () (* Panic freedom *) in result @@ -355,10 +355,10 @@ let impl_2__ntt_multiply #FStar.Tactics.Typeclasses.solve (self.f_coefficients.[ i ] <: v_Vector) (rhs.f_coefficients.[ i ] <: v_Vector) - (get_zeta (sz 64 +! (sz 4 *! i <: usize) <: usize) <: i16) - (get_zeta ((sz 64 +! (sz 4 *! i <: usize) <: usize) +! sz 1 <: usize) <: i16) - (get_zeta ((sz 64 +! (sz 4 *! i <: usize) <: usize) +! sz 2 <: usize) <: i16) - (get_zeta ((sz 64 +! (sz 4 *! i <: usize) <: usize) +! sz 3 <: usize) <: i16) + (zeta (sz 64 +! (sz 4 *! i <: usize) <: usize) <: i16) + (zeta ((sz 64 +! (sz 4 *! i <: usize) <: usize) +! sz 1 <: usize) <: i16) + (zeta ((sz 64 +! (sz 4 *! i <: usize) <: usize) +! sz 2 <: usize) <: i16) + (zeta ((sz 64 +! (sz 4 *! i <: usize) <: usize) +! sz 3 <: usize) <: i16) <: v_Vector) <: diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti index 6ad4d7a0b..6dd0db075 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti @@ -29,7 +29,7 @@ let v_ZETAS_TIMES_MONTGOMERY_R: t_Array i16 (sz 128) = FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 128); Rust_primitives.Hax.array_of_list 128 list -val get_zeta (i: usize) +val zeta (i: usize) : Prims.Pure i16 (requires i <. sz 128) (ensures diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst index 3a598d127..5748d2562 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst @@ -9,103 +9,10 @@ let impl_13__len (v_SIZE: usize) (_: Prims.unit) = v_SIZE let impl_20__len (v_SIZE: usize) (_: Prims.unit) = v_SIZE -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_1 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) = - { - f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); - f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemCiphertext v_SIZE) -> true); - f_from - = - fun (value: t_Array u8 v_SIZE) -> - { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value } - <: - t_MlKemCiphertext v_SIZE - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCiphertext v_SIZE) = - { - f_from_pre = (fun (value: t_MlKemCiphertext v_SIZE) -> true); - f_from_post = (fun (value: t_MlKemCiphertext v_SIZE) (out: t_Array u8 v_SIZE) -> true); - f_from = fun (value: t_MlKemCiphertext v_SIZE) -> value.f_value - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_5 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) = - { - f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); - f_from_post - = - (fun (value: t_Array u8 v_SIZE) (result: t_MlKemCiphertext v_SIZE) -> result.f_value = value); - f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemCiphertext v_SIZE - } - let impl_6__as_slice (v_SIZE: usize) (self: t_MlKemCiphertext v_SIZE) = self.f_value -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_8 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) = - { - f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); - f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPrivateKey v_SIZE) -> true); - f_from - = - fun (value: t_Array u8 v_SIZE) -> - { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value } - <: - t_MlKemPrivateKey v_SIZE - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_9 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPrivateKey v_SIZE) = - { - f_from_pre = (fun (value: t_MlKemPrivateKey v_SIZE) -> true); - f_from_post = (fun (value: t_MlKemPrivateKey v_SIZE) (out: t_Array u8 v_SIZE) -> true); - f_from = fun (value: t_MlKemPrivateKey v_SIZE) -> value.f_value - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_12 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) = - { - f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); - f_from_post - = - (fun (value: t_Array u8 v_SIZE) (result: t_MlKemPrivateKey v_SIZE) -> result.f_value = value); - f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemPrivateKey v_SIZE - } - let impl_13__as_slice (v_SIZE: usize) (self: t_MlKemPrivateKey v_SIZE) = self.f_value -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_15 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) = - { - f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); - f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPublicKey v_SIZE) -> true); - f_from - = - fun (value: t_Array u8 v_SIZE) -> - { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value } - <: - t_MlKemPublicKey v_SIZE - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_16 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPublicKey v_SIZE) = - { - f_from_pre = (fun (value: t_MlKemPublicKey v_SIZE) -> true); - f_from_post = (fun (value: t_MlKemPublicKey v_SIZE) (out: t_Array u8 v_SIZE) -> true); - f_from = fun (value: t_MlKemPublicKey v_SIZE) -> value.f_value - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_19 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) = - { - f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); - f_from_post - = - (fun (value: t_Array u8 v_SIZE) (result: t_MlKemPublicKey v_SIZE) -> result.f_value = value); - f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemPublicKey v_SIZE - } - let impl_20__as_slice (v_SIZE: usize) (self: t_MlKemPublicKey v_SIZE) = self.f_value let impl_21__from @@ -178,65 +85,3 @@ let unpack_private_key (v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE: usize) (private <: (t_Slice u8 & t_Slice u8 & t_Slice u8 & t_Slice u8) -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl (v_SIZE: usize) : Core.Default.t_Default (t_MlKemCiphertext v_SIZE) = - { - f_default_pre = (fun (_: Prims.unit) -> true); - f_default_post = (fun (_: Prims.unit) (out: t_MlKemCiphertext v_SIZE) -> true); - f_default - = - fun (_: Prims.unit) -> - { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemCiphertext v_SIZE - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_7 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPrivateKey v_SIZE) = - { - f_default_pre = (fun (_: Prims.unit) -> true); - f_default_post = (fun (_: Prims.unit) (out: t_MlKemPrivateKey v_SIZE) -> true); - f_default - = - fun (_: Prims.unit) -> - { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemPrivateKey v_SIZE - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_14 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPublicKey v_SIZE) = - { - f_default_pre = (fun (_: Prims.unit) -> true); - f_default_post = (fun (_: Prims.unit) (out: t_MlKemPublicKey v_SIZE) -> true); - f_default - = - fun (_: Prims.unit) -> - { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemPublicKey v_SIZE - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_4 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_Slice u8) = - { - f_as_ref_pre = (fun (self: t_MlKemCiphertext v_SIZE) -> true); - f_as_ref_post - = - (fun (self___: t_MlKemCiphertext v_SIZE) (result: t_Slice u8) -> result = self___.f_value); - f_as_ref = fun (self: t_MlKemCiphertext v_SIZE) -> self.f_value <: t_Slice u8 - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_11 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t_Slice u8) = - { - f_as_ref_pre = (fun (self: t_MlKemPrivateKey v_SIZE) -> true); - f_as_ref_post - = - (fun (self___: t_MlKemPrivateKey v_SIZE) (result: t_Slice u8) -> result = self___.f_value); - f_as_ref = fun (self: t_MlKemPrivateKey v_SIZE) -> self.f_value <: t_Slice u8 - } - -[@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_18 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_Slice u8) = - { - f_as_ref_pre = (fun (self: t_MlKemPublicKey v_SIZE) -> true); - f_as_ref_post - = - (fun (self___: t_MlKemPublicKey v_SIZE) (result: t_Slice u8) -> result = self___.f_value); - f_as_ref = fun (self: t_MlKemPublicKey v_SIZE) -> self.f_value <: t_Slice u8 - } diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti index 4f76c2ffc..1947307c5 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti @@ -19,13 +19,35 @@ val impl_20__len: v_SIZE: usize -> Prims.unit type t_MlKemCiphertext (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_1 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) +let impl_1 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) = + { + f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); + f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemCiphertext v_SIZE) -> true); + f_from + = + fun (value: t_Array u8 v_SIZE) -> + { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value } + <: + t_MlKemCiphertext v_SIZE + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCiphertext v_SIZE) +let impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCiphertext v_SIZE) = + { + f_from_pre = (fun (value: t_MlKemCiphertext v_SIZE) -> true); + f_from_post = (fun (value: t_MlKemCiphertext v_SIZE) (out: t_Array u8 v_SIZE) -> true); + f_from = fun (value: t_MlKemCiphertext v_SIZE) -> value.f_value + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_5 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) +let impl_5 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) = + { + f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); + f_from_post + = + (fun (value: t_Array u8 v_SIZE) (result: t_MlKemCiphertext v_SIZE) -> result.f_value = value); + f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemCiphertext v_SIZE + } /// A reference to the raw byte slice. val impl_6__as_slice (v_SIZE: usize) (self: t_MlKemCiphertext v_SIZE) @@ -40,13 +62,35 @@ val impl_6__as_slice (v_SIZE: usize) (self: t_MlKemCiphertext v_SIZE) type t_MlKemPrivateKey (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_8 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) +let impl_8 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) = + { + f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); + f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPrivateKey v_SIZE) -> true); + f_from + = + fun (value: t_Array u8 v_SIZE) -> + { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value } + <: + t_MlKemPrivateKey v_SIZE + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_9 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPrivateKey v_SIZE) +let impl_9 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPrivateKey v_SIZE) = + { + f_from_pre = (fun (value: t_MlKemPrivateKey v_SIZE) -> true); + f_from_post = (fun (value: t_MlKemPrivateKey v_SIZE) (out: t_Array u8 v_SIZE) -> true); + f_from = fun (value: t_MlKemPrivateKey v_SIZE) -> value.f_value + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_12 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) +let impl_12 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) = + { + f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); + f_from_post + = + (fun (value: t_Array u8 v_SIZE) (result: t_MlKemPrivateKey v_SIZE) -> result.f_value = value); + f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemPrivateKey v_SIZE + } /// A reference to the raw byte slice. val impl_13__as_slice (v_SIZE: usize) (self: t_MlKemPrivateKey v_SIZE) @@ -61,13 +105,35 @@ val impl_13__as_slice (v_SIZE: usize) (self: t_MlKemPrivateKey v_SIZE) type t_MlKemPublicKey (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_15 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) +let impl_15 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) = + { + f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); + f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPublicKey v_SIZE) -> true); + f_from + = + fun (value: t_Array u8 v_SIZE) -> + { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value } + <: + t_MlKemPublicKey v_SIZE + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_16 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPublicKey v_SIZE) +let impl_16 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPublicKey v_SIZE) = + { + f_from_pre = (fun (value: t_MlKemPublicKey v_SIZE) -> true); + f_from_post = (fun (value: t_MlKemPublicKey v_SIZE) (out: t_Array u8 v_SIZE) -> true); + f_from = fun (value: t_MlKemPublicKey v_SIZE) -> value.f_value + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_19 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) +let impl_19 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) = + { + f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true); + f_from_post + = + (fun (value: t_Array u8 v_SIZE) (result: t_MlKemPublicKey v_SIZE) -> result.f_value = value); + f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemPublicKey v_SIZE + } /// A reference to the raw byte slice. val impl_20__as_slice (v_SIZE: usize) (self: t_MlKemPublicKey v_SIZE) @@ -169,22 +235,67 @@ val unpack_private_key (v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE: usize) (private v Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE)) [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl (v_SIZE: usize) : Core.Default.t_Default (t_MlKemCiphertext v_SIZE) +let impl (v_SIZE: usize) : Core.Default.t_Default (t_MlKemCiphertext v_SIZE) = + { + f_default_pre = (fun (_: Prims.unit) -> true); + f_default_post = (fun (_: Prims.unit) (out: t_MlKemCiphertext v_SIZE) -> true); + f_default + = + fun (_: Prims.unit) -> + { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemCiphertext v_SIZE + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_7 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPrivateKey v_SIZE) +let impl_7 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPrivateKey v_SIZE) = + { + f_default_pre = (fun (_: Prims.unit) -> true); + f_default_post = (fun (_: Prims.unit) (out: t_MlKemPrivateKey v_SIZE) -> true); + f_default + = + fun (_: Prims.unit) -> + { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemPrivateKey v_SIZE + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_14 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPublicKey v_SIZE) +let impl_14 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPublicKey v_SIZE) = + { + f_default_pre = (fun (_: Prims.unit) -> true); + f_default_post = (fun (_: Prims.unit) (out: t_MlKemPublicKey v_SIZE) -> true); + f_default + = + fun (_: Prims.unit) -> + { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemPublicKey v_SIZE + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_4 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_Slice u8) +let impl_4 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_Slice u8) = + { + f_as_ref_pre = (fun (self: t_MlKemCiphertext v_SIZE) -> true); + f_as_ref_post + = + (fun (self___: t_MlKemCiphertext v_SIZE) (result: t_Slice u8) -> result = self___.f_value); + f_as_ref = fun (self: t_MlKemCiphertext v_SIZE) -> self.f_value <: t_Slice u8 + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_11 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t_Slice u8) +let impl_11 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t_Slice u8) = + { + f_as_ref_pre = (fun (self: t_MlKemPrivateKey v_SIZE) -> true); + f_as_ref_post + = + (fun (self___: t_MlKemPrivateKey v_SIZE) (result: t_Slice u8) -> result = self___.f_value); + f_as_ref = fun (self: t_MlKemPrivateKey v_SIZE) -> self.f_value <: t_Slice u8 + } [@@ FStar.Tactics.Typeclasses.tcinstance] -val impl_18 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_Slice u8) +let impl_18 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_Slice u8) = + { + f_as_ref_pre = (fun (self: t_MlKemPublicKey v_SIZE) -> true); + f_as_ref_post + = + (fun (self___: t_MlKemPublicKey v_SIZE) (result: t_Slice u8) -> result = self___.f_value); + f_as_ref = fun (self: t_MlKemPublicKey v_SIZE) -> self.f_value <: t_Slice u8 + } [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_3 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemCiphertext v_SIZE) (t_Slice u8) = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst index 6f960e706..cba0ea581 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst @@ -184,7 +184,7 @@ let cond_subtract_3329_ (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256) = #pop-options -#push-options "--z3rlimit 200" +#push-options "--z3rlimit 250" let montgomery_multiply_by_constant (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst index b0c197583..00fb6832a 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst @@ -38,7 +38,6 @@ let deserialize_1_ (bytes: t_Slice u8) = deserialize_1___deserialize_1_u8s (bytes.[ sz 0 ] <: u8) (bytes.[ sz 1 ] <: u8) [@@"opaque_to_smt"] - let deserialize_4___deserialize_4_i16s (b0 b1 b2 b3 b4 b5 b6 b7: i16) = let coefficients:Libcrux_intrinsics.Avx2_extract.t_Vec256 = Libcrux_intrinsics.Avx2_extract.mm256_set_epi16 b7 b7 b6 b6 b5 b5 b4 b4 b3 b3 b2 b2 b1 b1 b0 b0 diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst index 9f607fddd..f400f5ccd 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst @@ -28,7 +28,7 @@ let get_n_least_significant_bits (n: u8) (value: u32) = #pop-options -#push-options "--z3rlimit 150" +#push-options "--z3rlimit 200" let barrett_reduce_element (value: i16) = let t:i32 = diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Instances.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Instances.fst index f598ee0ff..0ea02db6c 100644 --- a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Instances.fst +++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.Instances.fst @@ -11,13 +11,14 @@ open Spec.MLKEM let mlkem768_rank : rank = sz 3 -#push-options "--z3rlimit 300" +#set-options "--z3rlimit 350" let mlkem768_generate_keypair (randomness:t_Array u8 (sz 64)): (t_Array u8 (sz 2400) & t_Array u8 (sz 1184)) & bool = ind_cca_generate_keypair mlkem768_rank randomness let mlkem768_encapsulate (public_key: t_Array u8 (sz 1184)) (randomness: t_Array u8 (sz 32)): (t_Array u8 (sz 1088) & t_Array u8 (sz 32)) & bool = + assert (v_CPA_CIPHERTEXT_SIZE mlkem768_rank == sz 1088); ind_cca_encapsulate mlkem768_rank public_key randomness let mlkem768_decapsulate (secret_key: t_Array u8 (sz 2400)) (ciphertext: t_Array u8 (sz 1088)): @@ -32,7 +33,6 @@ let mlkem1024_generate_keypair (randomness:t_Array u8 (sz 64)): (t_Array u8 (sz 3168) & t_Array u8 (sz 1568)) & bool = ind_cca_generate_keypair mlkem1024_rank randomness -#set-options "--z3rlimit 100" let mlkem1024_encapsulate (public_key: t_Array u8 (sz 1568)) (randomness: t_Array u8 (sz 32)): (t_Array u8 (sz 1568) & t_Array u8 (sz 32)) & bool = assert (v_CPA_CIPHERTEXT_SIZE mlkem1024_rank == sz 1568); diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst index 5c77472f2..cbe51c827 100644 --- a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst +++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst @@ -361,7 +361,9 @@ val lemma_mont_mul_red_i16_int (x y:i16): Lemma let result:i16 = mont_mul_red_i16 x y in is_i16b 3328 result /\ v result % 3329 == (v x * v y * 169) % 3329)) - + +#push-options "--z3rlimit 200" + let lemma_mont_mul_red_i16_int (x y:i16) = let vlow = x *. y in let prod = v x * v y in @@ -429,6 +431,7 @@ let lemma_mont_mul_red_i16_int (x y:i16) = ((prod) * 169) % 3329; } +#pop-options val lemma_mont_mul_red_i16 (x y:i16): Lemma (requires (is_i16b 1664 y \/ is_intb (3326 * pow2 15) (v x * v y))) diff --git a/libcrux-ml-kem/src/hash_functions.rs b/libcrux-ml-kem/src/hash_functions.rs index 7641a7266..17d34fdc2 100644 --- a/libcrux-ml-kem/src/hash_functions.rs +++ b/libcrux-ml-kem/src/hash_functions.rs @@ -171,7 +171,6 @@ pub(crate) mod portable { #[hax_lib::attributes] impl Hash for PortableHash { - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("$out == Spec.Utils.v_G $input")) ] @@ -180,7 +179,6 @@ pub(crate) mod portable { G(input) } - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("$out == Spec.Utils.v_H $input")) ] @@ -190,7 +188,6 @@ pub(crate) mod portable { } #[requires(fstar!("v $LEN < pow2 32"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| // We need to repeat the pre-condition here because of https://github.com/hacspec/hax/issues/784 fstar!("v $LEN < pow2 32 ==> $out == Spec.Utils.v_PRF $LEN $input")) @@ -201,7 +198,6 @@ pub(crate) mod portable { } #[requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("(v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)) ==> $out == Spec.Utils.v_PRFxN $K $LEN $input")) @@ -428,7 +424,6 @@ pub(crate) mod avx2 { #[hax_lib::attributes] impl Hash for Simd256Hash { - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("$out == Spec.Utils.v_G $input")) ] @@ -437,7 +432,6 @@ pub(crate) mod avx2 { G(input) } - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("$out == Spec.Utils.v_H $input")) ] @@ -447,7 +441,6 @@ pub(crate) mod avx2 { } #[requires(fstar!("v $LEN < pow2 32"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[hax_lib::ensures(|out| // We need to repeat the pre-condition here because of https://github.com/hacspec/hax/issues/784 fstar!("v $LEN < pow2 32 ==> $out == Spec.Utils.v_PRF $LEN $input")) @@ -458,7 +451,6 @@ pub(crate) mod avx2 { } #[requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("(v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)) ==> $out == Spec.Utils.v_PRFxN $K $LEN $input")) @@ -710,7 +702,6 @@ pub(crate) mod neon { #[hax_lib::attributes] impl Hash for Simd128Hash { - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("$out == Spec.Utils.v_G $input")) ] @@ -719,7 +710,6 @@ pub(crate) mod neon { G(input) } - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("$out == Spec.Utils.v_H $input")) ] @@ -729,7 +719,6 @@ pub(crate) mod neon { } #[requires(fstar!("v $LEN < pow2 32"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| // We need to repeat the pre-condition here because of https://github.com/hacspec/hax/issues/784 fstar!("v $LEN < pow2 32 ==> $out == Spec.Utils.v_PRF $LEN $input")) @@ -740,7 +729,6 @@ pub(crate) mod neon { } #[requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| // We need to repeat the pre-condition here because of https://github.com/hacspec/hax/issues/784 fstar!("(v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)) ==> diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs index 33ec390e5..18ae0db4a 100644 --- a/libcrux-ml-kem/src/ind_cca.rs +++ b/libcrux-ml-kem/src/ind_cca.rs @@ -427,13 +427,12 @@ pub(crate) fn decapsulate< Scheme::kdf::(&implicit_rejection_shared_secret, ciphertext); let shared_secret = Scheme::kdf::(shared_secret, ciphertext); - let shared_secret = compare_ciphertexts_select_shared_secret_in_constant_time( + compare_ciphertexts_select_shared_secret_in_constant_time( ciphertext.as_ref(), &expected_ciphertext, &shared_secret, &implicit_rejection_shared_secret, - ); - shared_secret + ) } /// Types for the unpacked API. @@ -821,7 +820,7 @@ pub(crate) mod unpacked { Seq.index (Seq.index $result i) j == Seq.index (Seq.index $ind_cpa_a j) i)")) ] - pub(crate) fn transpose_a( + fn transpose_a( ind_cpa_a: [[PolynomialRingElement; K]; K], ) -> [[PolynomialRingElement; K]; K] { // We need to un-transpose the A_transpose matrix provided by IND-CPA diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs index 935ef0c95..b40bd07ae 100644 --- a/libcrux-ml-kem/src/ind_cpa.rs +++ b/libcrux-ml-kem/src/ind_cpa.rs @@ -200,6 +200,7 @@ fn sample_ring_element_cbd< ) -> ([PolynomialRingElement; K], u8) { let mut error_1 = from_fn(|_i| PolynomialRingElement::::ZERO()); let mut prf_inputs = [prf_input; K]; + // See https://github.com/hacspec/hax/issues/1167 let _domain_separator_init = domain_separator; domain_separator = prf_input_inc::(&mut prf_inputs, domain_separator); hax_lib::fstar!("let lemma_aux (i:nat{ i < v $K }) : Lemma (${prf_inputs}.[sz i] == (Seq.append (Seq.slice $prf_input 0 32) diff --git a/libcrux-ml-kem/src/invert_ntt.rs b/libcrux-ml-kem/src/invert_ntt.rs index 24866eb82..87bc90fed 100644 --- a/libcrux-ml-kem/src/invert_ntt.rs +++ b/libcrux-ml-kem/src/invert_ntt.rs @@ -1,6 +1,6 @@ use crate::{ hax_utils::hax_debug_assert, - polynomial::{get_zeta, PolynomialRingElement}, + polynomial::{zeta, PolynomialRingElement}, vector::{montgomery_multiply_fe, Operations, FIELD_ELEMENTS_IN_VECTOR}, }; @@ -55,10 +55,10 @@ pub(crate) fn invert_ntt_at_layer_1( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ round ])))"); re.coefficients[round] = Vector::inv_ntt_layer_1_step( re.coefficients[round], - get_zeta(*zeta_i), - get_zeta(*zeta_i - 1), - get_zeta(*zeta_i - 2), - get_zeta(*zeta_i - 3), + zeta(*zeta_i), + zeta(*zeta_i - 1), + zeta(*zeta_i - 2), + zeta(*zeta_i - 3), ); *zeta_i -= 3; hax_lib::fstar!("reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) @@ -102,11 +102,8 @@ pub(crate) fn invert_ntt_at_layer_2( hax_lib::fstar!("reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) (Spec.Utils.is_i16b_array_opaque 3328 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ round ])))"); - re.coefficients[round] = Vector::inv_ntt_layer_2_step( - re.coefficients[round], - get_zeta(*zeta_i), - get_zeta(*zeta_i - 1), - ); + re.coefficients[round] = + Vector::inv_ntt_layer_2_step(re.coefficients[round], zeta(*zeta_i), zeta(*zeta_i - 1)); *zeta_i -= 1; hax_lib::fstar!("reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) (Spec.Utils.is_i16b_array_opaque 3328 @@ -150,7 +147,7 @@ pub(crate) fn invert_ntt_at_layer_3( (Spec.Utils.is_i16b_array_opaque 3328 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ round ])))"); re.coefficients[round] = - Vector::inv_ntt_layer_3_step(re.coefficients[round], get_zeta(*zeta_i)); + Vector::inv_ntt_layer_3_step(re.coefficients[round], zeta(*zeta_i)); hax_lib::fstar!( "reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) (Spec.Utils.is_i16b_array_opaque 3328 @@ -210,7 +207,7 @@ pub(crate) fn invert_ntt_at_layer_4_plus( let (x, y) = inv_ntt_layer_int_vec_step_reduce( re.coefficients[j], re.coefficients[j + step_vec], - get_zeta(*zeta_i), + zeta(*zeta_i), ); re.coefficients[j] = x; re.coefficients[j + step_vec] = y; diff --git a/libcrux-ml-kem/src/mlkem512.rs b/libcrux-ml-kem/src/mlkem512.rs index 0d82a07a8..b9b33596d 100644 --- a/libcrux-ml-kem/src/mlkem512.rs +++ b/libcrux-ml-kem/src/mlkem512.rs @@ -3,31 +3,29 @@ use super::{constants::*, ind_cca::*, types::*, *}; // Kyber 512 parameters const RANK_512: usize = 2; -const RANKED_BYTES_PER_RING_ELEMENT_512: usize = 768; -const T_AS_NTT_ENCODED_SIZE_512: usize = 768; +const RANKED_BYTES_PER_RING_ELEMENT_512: usize = RANK_512 * BITS_PER_RING_ELEMENT / 8; +const T_AS_NTT_ENCODED_SIZE_512: usize = + (RANK_512 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8; const VECTOR_U_COMPRESSION_FACTOR_512: usize = 10; -// [hax]: hacspec/hacspec-v2#27 stealing error -// block_len::() -const C1_BLOCK_SIZE_512: usize = 320; -// [hax]: hacspec/hacspec-v2#27 stealing error -// serialized_len::() -const C1_SIZE_512: usize = 640; +const C1_BLOCK_SIZE_512: usize = + (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR_512) / 8; +const C1_SIZE_512: usize = C1_BLOCK_SIZE_512 * RANK_512; const VECTOR_V_COMPRESSION_FACTOR_512: usize = 4; -// [hax]: hacspec/hacspec-v2#27 stealing error -// block_len::() -const C2_SIZE_512: usize = 128; -const CPA_PKE_SECRET_KEY_SIZE_512: usize = 768; -pub(crate) const CPA_PKE_PUBLIC_KEY_SIZE_512: usize = 800; -const CPA_PKE_CIPHERTEXT_SIZE_512: usize = 768; +const C2_SIZE_512: usize = (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_512) / 8; +const CPA_PKE_SECRET_KEY_SIZE_512: usize = + (RANK_512 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8; +pub(crate) const CPA_PKE_PUBLIC_KEY_SIZE_512: usize = T_AS_NTT_ENCODED_SIZE_512 + 32; +const CPA_PKE_CIPHERTEXT_SIZE_512: usize = C1_SIZE_512 + C2_SIZE_512; -pub(crate) const SECRET_KEY_SIZE_512: usize = 1632; +pub(crate) const SECRET_KEY_SIZE_512: usize = + CPA_PKE_SECRET_KEY_SIZE_512 + CPA_PKE_PUBLIC_KEY_SIZE_512 + H_DIGEST_SIZE + SHARED_SECRET_SIZE; const ETA1: usize = 3; -const ETA1_RANDOMNESS_SIZE: usize = 192; +const ETA1_RANDOMNESS_SIZE: usize = ETA1 * 64; const ETA2: usize = 2; -const ETA2_RANDOMNESS_SIZE: usize = 128; +const ETA2_RANDOMNESS_SIZE: usize = ETA2 * 64; -const IMPLICIT_REJECTION_HASH_INPUT_SIZE: usize = 800; +const IMPLICIT_REJECTION_HASH_INPUT_SIZE: usize = SHARED_SECRET_SIZE + CPA_PKE_CIPHERTEXT_SIZE_512; // Kyber 512 types /// An ML-KEM 512 Ciphertext diff --git a/libcrux-ml-kem/src/ntt.rs b/libcrux-ml-kem/src/ntt.rs index bb769cf1a..fa08e35e5 100644 --- a/libcrux-ml-kem/src/ntt.rs +++ b/libcrux-ml-kem/src/ntt.rs @@ -1,6 +1,6 @@ use crate::{ hax_utils::hax_debug_assert, - polynomial::{get_zeta, PolynomialRingElement, VECTORS_IN_RING_ELEMENT}, + polynomial::{zeta, PolynomialRingElement, VECTORS_IN_RING_ELEMENT}, vector::{montgomery_multiply_fe, Operations}, }; @@ -56,10 +56,10 @@ pub(crate) fn ntt_at_layer_1( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ round ])))"); re.coefficients[round] = Vector::ntt_layer_1_step( re.coefficients[round], - get_zeta(*zeta_i), - get_zeta(*zeta_i + 1), - get_zeta(*zeta_i + 2), - get_zeta(*zeta_i + 3), + zeta(*zeta_i), + zeta(*zeta_i + 1), + zeta(*zeta_i + 2), + zeta(*zeta_i + 3), ); *zeta_i += 3; hax_lib::fstar!("reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) @@ -114,11 +114,8 @@ pub(crate) fn ntt_at_layer_2( hax_lib::fstar!("reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) (Spec.Utils.is_i16b_array_opaque (11207+4*3328) (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ round ])))"); - re.coefficients[round] = Vector::ntt_layer_2_step( - re.coefficients[round], - get_zeta(*zeta_i), - get_zeta(*zeta_i + 1), - ); + re.coefficients[round] = + Vector::ntt_layer_2_step(re.coefficients[round], zeta(*zeta_i), zeta(*zeta_i + 1)); *zeta_i += 1; hax_lib::fstar!("reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) (Spec.Utils.is_i16b_array_opaque (11207+5*3328) @@ -172,8 +169,7 @@ pub(crate) fn ntt_at_layer_3( hax_lib::fstar!("reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) (Spec.Utils.is_i16b_array_opaque (11207+3*3328) (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ round ])))"); - re.coefficients[round] = - Vector::ntt_layer_3_step(re.coefficients[round], get_zeta(*zeta_i)); + re.coefficients[round] = Vector::ntt_layer_3_step(re.coefficients[round], zeta(*zeta_i)); hax_lib::fstar!( "reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) (Spec.Utils.is_i16b_array_opaque (11207+4*3328) @@ -243,7 +239,7 @@ pub(crate) fn ntt_at_layer_4_plus( let (x, y) = ntt_layer_int_vec_step( re.coefficients[j], re.coefficients[j + step_vec], - get_zeta(*zeta_i), + zeta(*zeta_i), ); re.coefficients[j] = x; re.coefficients[j + step_vec] = y; diff --git a/libcrux-ml-kem/src/polynomial.rs b/libcrux-ml-kem/src/polynomial.rs index 9460a0cba..5bad1d43a 100644 --- a/libcrux-ml-kem/src/polynomial.rs +++ b/libcrux-ml-kem/src/polynomial.rs @@ -15,11 +15,12 @@ pub(crate) const ZETAS_TIMES_MONTGOMERY_R: [i16; 128] = { ] }; +// A function to retrieve zetas so that we can add a post-condition #[inline(always)] #[hax_lib::fstar::verification_status(panic_free)] #[hax_lib::requires(i < 128)] #[hax_lib::ensures(|result| fstar!("Spec.Utils.is_i16b 1664 result"))] -pub fn get_zeta(i: usize) -> i16 { +pub fn zeta(i: usize) -> i16 { ZETAS_TIMES_MONTGOMERY_R[i] } @@ -67,7 +68,6 @@ impl PolynomialRingElement { #[allow(non_snake_case)] pub(crate) fn ZERO() -> Self { Self { - // FIXME: The THIR body of item DefId(0:415 ~ libcrux_ml_kem[9000]::polynomial::{impl#0}::ZERO::{constant#0}) was stolen. coefficients: [Vector::ZERO(); 16], } } @@ -213,13 +213,13 @@ impl PolynomialRingElement { /// /// The NIST FIPS 203 standard can be found at /// . + // TODO: Remove or replace with something that works and is useful for the proof. // #[cfg_attr(hax, hax_lib::requires( // hax_lib::forall(|i:usize| // hax_lib::implies(i < COEFFICIENTS_IN_RING_ELEMENT, || // (lhs.coefficients[i] >= 0 && lhs.coefficients[i] < 4096) && // (rhs.coefficients[i].abs() <= FIELD_MODULUS) - // ))))] // #[cfg_attr(hax, hax_lib::ensures(|result| // hax_lib::forall(|i:usize| @@ -228,12 +228,7 @@ impl PolynomialRingElement { // ))))] #[inline(always)] pub(crate) fn ntt_multiply(&self, rhs: &Self) -> Self { - // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting hax_lib::fstar!("admit ()"); - // hax_debug_debug_assert!(lhs - // .coefficients - // .into_iter() - // .all(|coefficient| coefficient >= 0 && coefficient < 4096)); let mut out = PolynomialRingElement::ZERO(); @@ -241,10 +236,10 @@ impl PolynomialRingElement { out.coefficients[i] = Vector::ntt_multiply( &self.coefficients[i], &rhs.coefficients[i], - get_zeta(64 + 4 * i), - get_zeta(64 + 4 * i + 1), - get_zeta(64 + 4 * i + 2), - get_zeta(64 + 4 * i + 3), + zeta(64 + 4 * i), + zeta(64 + 4 * i + 1), + zeta(64 + 4 * i + 2), + zeta(64 + 4 * i + 3), ); } diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs index 9f3035fde..61c7ae159 100644 --- a/libcrux-ml-kem/src/vector/avx2.rs +++ b/libcrux-ml-kem/src/vector/avx2.rs @@ -285,7 +285,6 @@ impl Operations for SIMD256Vector { } #[requires(fstar!("Spec.MLKEM.serialize_pre 1 (impl.f_repr $vector)"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 1 (impl.f_repr $vector) ==> Spec.MLKEM.serialize_post 1 (impl.f_repr $vector) $out"))] #[inline(always)] fn serialize_1(vector: Self) -> [u8; 2] { @@ -293,7 +292,6 @@ impl Operations for SIMD256Vector { } #[requires(bytes.len() == 2)] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("sz (Seq.length $bytes) =. sz 2 ==> Spec.MLKEM.deserialize_post 1 $bytes (impl.f_repr $out)"))] #[inline(always)] fn deserialize_1(bytes: &[u8]) -> Self { @@ -303,7 +301,6 @@ impl Operations for SIMD256Vector { } #[requires(fstar!("Spec.MLKEM.serialize_pre 4 (impl.f_repr $vector)"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 4 (impl.f_repr $vector) ==> Spec.MLKEM.serialize_post 4 (impl.f_repr $vector) $out"))] #[inline(always)] fn serialize_4(vector: Self) -> [u8; 8] { @@ -311,7 +308,6 @@ impl Operations for SIMD256Vector { } #[requires(bytes.len() == 8)] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("sz (Seq.length $bytes) =. sz 8 ==> Spec.MLKEM.deserialize_post 4 $bytes (impl.f_repr $out)"))] #[inline(always)] fn deserialize_4(bytes: &[u8]) -> Self { @@ -336,7 +332,6 @@ impl Operations for SIMD256Vector { } #[requires(fstar!("Spec.MLKEM.serialize_pre 10 (impl.f_repr $vector)"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 10 (impl.f_repr $vector) ==> Spec.MLKEM.serialize_post 10 (impl.f_repr $vector) $out"))] #[inline(always)] fn serialize_10(vector: Self) -> [u8; 20] { @@ -344,7 +339,6 @@ impl Operations for SIMD256Vector { } #[requires(bytes.len() == 20)] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("sz (Seq.length $bytes) =. sz 20 ==> Spec.MLKEM.deserialize_post 10 $bytes (impl.f_repr $out)"))] #[inline(always)] fn deserialize_10(bytes: &[u8]) -> Self { @@ -367,7 +361,6 @@ impl Operations for SIMD256Vector { } #[requires(fstar!("Spec.MLKEM.serialize_pre 12 (impl.f_repr $vector)"))] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 12 (impl.f_repr $vector) ==> Spec.MLKEM.serialize_post 12 (impl.f_repr $vector) $out"))] #[inline(always)] fn serialize_12(vector: Self) -> [u8; 24] { @@ -375,7 +368,6 @@ impl Operations for SIMD256Vector { } #[requires(bytes.len() == 24)] - // Output name has be `out` https://github.com/hacspec/hax/issues/832 #[ensures(|out| fstar!("sz (Seq.length $bytes) =. sz 24 ==> Spec.MLKEM.deserialize_post 12 $bytes (impl.f_repr $out)"))] #[inline(always)] fn deserialize_12(bytes: &[u8]) -> Self { diff --git a/libcrux-ml-kem/src/vector/avx2/arithmetic.rs b/libcrux-ml-kem/src/vector/avx2/arithmetic.rs index 1032ee28d..8c9f3ae9a 100644 --- a/libcrux-ml-kem/src/vector/avx2/arithmetic.rs +++ b/libcrux-ml-kem/src/vector/avx2/arithmetic.rs @@ -94,11 +94,6 @@ pub(crate) fn shift_right(vector: Vec256) -> Vec256 { result } -// #[inline(always)] -// pub(crate) fn shift_left(vector: Vec256) -> Vec256 { -// mm256_slli_epi16::<{ SHIFT_BY }>(vector) -// } - #[inline(always)] #[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"))] #[hax_lib::requires(fstar!("Spec.Utils.is_i16b_array (pow2 12 - 1) (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 $vector)"))] diff --git a/libcrux-ml-kem/src/vector/portable/ntt.rs b/libcrux-ml-kem/src/vector/portable/ntt.rs index 3cfafc9ea..46ef118d5 100644 --- a/libcrux-ml-kem/src/vector/portable/ntt.rs +++ b/libcrux-ml-kem/src/vector/portable/ntt.rs @@ -367,21 +367,6 @@ pub(crate) fn ntt_multiply_binomials( ); } -// #[inline(always)] -// pub(crate) fn ntt_multiply_binomials( -// (a0, a1): (FieldElement, FieldElement), -// (b0, b1): (FieldElement, FieldElement), -// zeta: FieldElementTimesMontgomeryR, -// ) -> (MontgomeryFieldElement, MontgomeryFieldElement) { -// ( -// montgomery_reduce_element( -// (a0 as i32) * (b0 as i32) -// + (montgomery_reduce_element((a1 as i32) * (b1 as i32)) as i32) * (zeta as i32), -// ), -// montgomery_reduce_element((a0 as i32) * (b1 as i32) + (a1 as i32) * (b0 as i32)), -// ) -// } - #[inline(always)] #[hax_lib::fstar::verification_status(panic_free)] #[hax_lib::fstar::options("--z3rlimit 100")] diff --git a/libcrux-ml-kem/src/vector/portable/serialize.rs b/libcrux-ml-kem/src/vector/portable/serialize.rs index 550ed5170..9a6522847 100644 --- a/libcrux-ml-kem/src/vector/portable/serialize.rs +++ b/libcrux-ml-kem/src/vector/portable/serialize.rs @@ -332,35 +332,6 @@ pub(crate) fn serialize_5_int(v: &[i16]) -> (u8, u8, u8, u8, u8) { (r0, r1, r2, r3, r4) } -// #[cfg_attr(hax, hax_lib::fstar::after(interface, " -// val serialize_5_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma -// (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 5)) -// (ensures bit_vec_of_int_t_array (${serialize_5} inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 5) -// "))] -// #[cfg_attr(hax, hax_lib::fstar::after(" -// #push-options \"--z3rlimit 300\" - -// let serialize_5_lemma inputs = -// serialize_5_bit_vec_lemma inputs.f_elements (); -// BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${serialize_5} inputs) 8) -// (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 5)) - -// #pop-options -// "))] -// #[cfg_attr(hax, hax_lib::fstar::after(" -// #push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\" - -// let serialize_5_bit_vec_lemma (v: t_Array i16 (sz 16)) -// (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 5)) -// : squash ( -// let inputs = bit_vec_of_int_t_array v 5 in -// let outputs = bit_vec_of_int_t_array (${serialize_5} ({ f_elements = v })) 8 in -// (forall (i: nat {i < 80}). inputs i == outputs i) -// ) = -// _ by (Tactics.GetBit.prove_bit_vector_equality' ()) - -// #pop-options -// "))] #[inline(always)] pub(crate) fn serialize_5(v: PortableVector) -> [u8; 10] { let r0_4 = serialize_5_int(&v.elements[0..8]); @@ -386,33 +357,6 @@ pub(crate) fn deserialize_5_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16, (v0, v1, v2, v3, v4, v5, v6, v7) } -// #[cfg_attr(hax, hax_lib::fstar::after(interface, " -// val deserialize_5_lemma (inputs: t_Array u8 (sz 10)) : Lemma -// (ensures bit_vec_of_int_t_array (${deserialize_5} inputs).f_elements 5 == bit_vec_of_int_t_array inputs 8) -// "))] -// #[cfg_attr(hax, hax_lib::fstar::after(" -// #push-options \"--z3rlimit 300\" - -// let deserialize_5_lemma inputs = -// deserialize_5_bit_vec_lemma inputs; -// BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${deserialize_5} inputs).f_elements 5) -// (BitVecEq.retype (bit_vec_of_int_t_array inputs 8)) - -// #pop-options -// "))] -// #[cfg_attr(hax, hax_lib::fstar::after(" -// #push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\" - -// let deserialize_5_bit_vec_lemma (v: t_Array u8 (sz 10)) -// : squash ( -// let inputs = bit_vec_of_int_t_array v 8 in -// let outputs = bit_vec_of_int_t_array (${deserialize_5} v).f_elements 5 in -// (forall (i: nat {i < 80}). inputs i == outputs i) -// ) = -// _ by (Tactics.GetBit.prove_bit_vector_equality' ()) - -// #pop-options -// "))] #[hax_lib::requires(fstar!(r#" ${bytes.len() == 10} "#))] @@ -601,35 +545,6 @@ pub(crate) fn serialize_11_int(v: &[i16]) -> (u8, u8, u8, u8, u8, u8, u8, u8, u8 (r0, r1, r2, r3, r4, r5, r6, r7, r8, r9, r10) } -// #[cfg_attr(hax, hax_lib::fstar::after(interface, " -// val serialize_11_lemma (inputs: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) : Lemma -// (requires (forall i. Rust_primitives.bounded (Seq.index inputs.f_elements i) 11)) -// (ensures bit_vec_of_int_t_array (${serialize_11} inputs) 8 == bit_vec_of_int_t_array inputs.f_elements 11) -// "))] -// #[cfg_attr(hax, hax_lib::fstar::after(" -// #push-options \"--z3rlimit 300\" - -// let serialize_11_lemma inputs = -// serialize_11_bit_vec_lemma inputs.f_elements (); -// BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${serialize_11} inputs) 8) -// (BitVecEq.retype (bit_vec_of_int_t_array inputs.f_elements 11)) - -// #pop-options -// "))] -// #[cfg_attr(hax, hax_lib::fstar::after(" -// #push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\" - -// let serialize_11_bit_vec_lemma (v: t_Array i16 (sz 16)) -// (_: squash (forall i. Rust_primitives.bounded (Seq.index v i) 11)) -// : squash ( -// let inputs = bit_vec_of_int_t_array v 11 in -// let outputs = bit_vec_of_int_t_array (${serialize_11} ({ f_elements = v })) 8 in -// (forall (i: nat {i < 176}). inputs i == outputs i) -// ) = -// _ by (Tactics.GetBit.prove_bit_vector_equality' ()) - -// #pop-options -// "))] #[inline(always)] pub(crate) fn serialize_11(v: PortableVector) -> [u8; 22] { let r0_10 = serialize_11_int(&v.elements[0..8]); @@ -657,33 +572,6 @@ pub(crate) fn deserialize_11_int(bytes: &[u8]) -> (i16, i16, i16, i16, i16, i16, (r0, r1, r2, r3, r4, r5, r6, r7) } -// #[cfg_attr(hax, hax_lib::fstar::after(interface, " -// val deserialize_11_lemma (inputs: t_Array u8 (sz 22)) : Lemma -// (ensures bit_vec_of_int_t_array (${deserialize_11} inputs).f_elements 11 == bit_vec_of_int_t_array inputs 8) -// "))] -// #[cfg_attr(hax, hax_lib::fstar::after(" -// #push-options \"--z3rlimit 300\" - -// let deserialize_11_lemma inputs = -// deserialize_11_bit_vec_lemma inputs; -// BitVecEq.bit_vec_equal_intro (bit_vec_of_int_t_array (${deserialize_11} inputs).f_elements 11) -// (BitVecEq.retype (bit_vec_of_int_t_array inputs 8)) - -// #pop-options -// "))] -// #[cfg_attr(hax, hax_lib::fstar::after(" -// #push-options \"--compat_pre_core 2 --z3rlimit 300 --z3refresh\" - -// let deserialize_11_bit_vec_lemma (v: t_Array u8 (sz 22)) -// : squash ( -// let inputs = bit_vec_of_int_t_array v 8 in -// let outputs = bit_vec_of_int_t_array (${deserialize_11} v).f_elements 11 in -// (forall (i: nat {i < 176}). inputs i == outputs i) -// ) = -// _ by (Tactics.GetBit.prove_bit_vector_equality' ()) - -// #pop-options -// "))] #[hax_lib::requires(fstar!(r#" ${bytes.len() == 22} "#))] diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs index 62e67a770..193d0edf6 100644 --- a/libcrux-ml-kem/src/vector/traits.rs +++ b/libcrux-ml-kem/src/vector/traits.rs @@ -5,6 +5,8 @@ pub const INVERSE_OF_MODULUS_MOD_MONTGOMERY_R: u32 = 62209; // FIELD_MODULUS^{-1 pub const BARRETT_SHIFT: i32 = 26; pub const BARRETT_R: i32 = 1 << BARRETT_SHIFT; +// We define a trait that allows us to talk about the contents of a vector. +// This is used extensively in pre- and post-conditions to reason about the code. #[cfg(hax)] #[hax_lib::attributes] pub trait Repr: Copy + Clone {