diff --git a/Makefile b/Makefile index 0b55923c..8456afda 100644 --- a/Makefile +++ b/Makefile @@ -57,7 +57,7 @@ clean-and-test: .PRECIOUS: %.llbc %.llbc: %.rs .charon_version # --mir elaborated --add-drop-bounds - $(CHARON) rustc --preset=eurydice --dest-file "$@" $(CHARON_EXTRA) -- $< + $(CHARON) rustc --preset=eurydice --dest-file "$@" $(CHARON_EXTRA) -- -Aunused $< out/test-%/main.c: test/main.c mkdir -p out/test-$* @@ -155,11 +155,12 @@ test/libcrux.llbc: RUSTFLAGS="-Cdebug-assertions=no --cfg eurydice" $(CHARON) cargo --preset eurydice \ --include 'libcrux_sha3' \ --include 'libcrux_secrets' \ + --rustc-arg='-Aunused' \ --start-from libcrux_ml_kem --start-from libcrux_sha3 \ --include 'core::num::*::BITS' --include 'core::num::*::MAX' \ --dest-file $$PWD/$@ -- \ --manifest-path $(LIBCRUX_HOME)/libcrux-ml-kem/Cargo.toml \ - --target=x86_64-apple-darwin + --target=x86_64-apple-darwin @# Commit the `Cargo.lock` so that the nix CI can use it cp $(LIBCRUX_HOME)/Cargo.lock libcrux-Cargo.lock diff --git a/flake.lock b/flake.lock index aa68ed62..23f4b90e 100644 --- a/flake.lock +++ b/flake.lock @@ -26,11 +26,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1765803402, - "narHash": "sha256-vyKAcVlq5UURJNT4Zt1cxdS/TEWHPXcX6FsVkcJF0VI=", + "lastModified": 1767093296, + "narHash": "sha256-xVO/cOWzKJFcht6tkqXA9aErR02Xdj4XxKDgt5Gn54Q=", "owner": "aeneasverif", "repo": "charon", - "rev": "85a1ee1cdfe1d7f2672bece3d190425e1f06c881", + "rev": "e587fcdad522736b216c23563cb6a7715450844d", "type": "github" }, "original": { diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 7655f6db..8aaaf623 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -113,12 +113,12 @@ typedef struct Eurydice_mut_borrow_slice_i16_s { #define Eurydice_slice_copy(dst, src, t) \ memcpy(dst.ptr, src.ptr, dst.meta * sizeof(t)) -#define core_array___Array_T__N___as_slice(len_, ptr_, t, ret_t) \ +#define core_array___T__N___as_slice(len_, ptr_, t, ret_t) \ (KRML_CLITERAL(ret_t){EURYDICE_CFIELD(.ptr =)(ptr_)->data, \ EURYDICE_CFIELD(.meta =) len_}) -#define core_array__core__clone__Clone_for__Array_T__N___clone( \ - len, src, elem_type, _ret_t) \ +#define core_array__core__clone__Clone_for__T__N___clone(len, src, elem_type, \ + _ret_t) \ (*(src)) #define TryFromSliceError uint8_t #define core_array_TryFromSliceError uint8_t diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index ea874d6f..8c392013 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -512,9 +512,11 @@ and metadata_typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ option = (* For tuple, the type of metadata is the last element *) | last :: _ -> metadata_typ_of_ty env last end - | C.TBuiltin C.TBox | C.TBuiltin C.TArray -> None - | C.TBuiltin C.TSlice | C.TBuiltin C.TStr -> Some Krml.Helpers.usize + | C.TBuiltin C.TBox -> None + | C.TBuiltin C.TStr -> Some Krml.Helpers.usize end + | C.TArray _ -> None + | C.TSlice _ -> Some Krml.Helpers.usize | C.TVar _ -> (* TEMPORARY: this needs to be enabled once the monomorphization PR lands -- for now, there are still polymorphic type definitions of the form type @@ -559,8 +561,7 @@ and ptr_typ_of_ty (env : env) ~const (ty : Charon.Types.ty) : K.typ = (* Handle special cases first *) match ty with (* Special case to handle slice : &[T] *) - | TAdt { id = TBuiltin TSlice; generics = { types = [ t ]; _ } } -> - Builtin.mk_slice ~const (typ_of_ty env t) + | TSlice t -> Builtin.mk_slice ~const (typ_of_ty env t) (* Special case to handle &str *) | TAdt { id = TBuiltin TStr; _ } -> Builtin.str_t ~const (* Special case to handle DynTrait *) @@ -598,9 +599,8 @@ and typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ = | [ t ] -> typ_of_ty env t (* charon issue #205 *) | _ -> TTuple (List.map (typ_of_ty env) args) end - | TAdt { id = TBuiltin TArray; generics = { types = [ t ]; const_generics = [ cg ]; _ } } -> - typ_of_struct_arr env t cg - | TAdt { id = TBuiltin TSlice; generics = { types = [ t ]; _ } } -> + | TArray (t, cg) -> typ_of_struct_arr env t cg + | TSlice t -> (* Appears in instantiations of patterns and generics, so we translate it to a placeholder. *) TApp (Builtin.derefed_slice, [ typ_of_ty env t ]) | TAdt { id = TBuiltin TStr; generics = { types = []; _ } } -> Builtin.deref_str_t @@ -886,8 +886,7 @@ let rec expression_of_place (env : env) (p : C.place) : K.expr = match pe, sub_place, sub_place.ty with (* slices simply cannot be dereferenced into places which have unknown size. They are supposed to be reborrowed again directly after the deref which is handled in expression_of_rvalue *) - | C.Deref, _, TRef (_, TAdt { id = TBuiltin TSlice; _ }, _) - | C.Deref, _, TRawPtr (TAdt { id = TBuiltin TSlice; _ }, _) -> assert false + | C.Deref, _, TRef (_, TSlice _, _) | C.Deref, _, TRawPtr (TSlice _, _) -> assert false | ( C.Deref, _, (TRawPtr _ | TRef _ | TAdt { id = TBuiltin TBox; generics = { types = [ _ ]; _ } }) ) -> @@ -1551,16 +1550,7 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = (* Translate effective type and cg arguments. *) let const_generic_args = match f, type_args with - | ( EQualified lid, - [ - _; - TRef - ( _, - TAdt - { id = TBuiltin TArray; generics = { types = [ _ ]; const_generics = [ cg ]; _ } }, - _ ); - _; - ] ) + | EQualified lid, [ _; TRef (_, TArray (_, cg), _); _ ] when lid = Builtin.slice_to_ref_array.name -> (* Special case, we *do* need to retain the length, which would disappear if we simply did typ_of_ty (owing to array decay rules). *) @@ -2339,7 +2329,7 @@ and expression_of_statement_kind (env : env) (ret_var : C.local_id) (s : C.state in match fn_ptr.kind, fn_ptr.generics.types @ extra_types with | ( FunId (FBuiltin (Index { is_array = false; mutability = _; is_range = false })), - [ TAdt { id = TBuiltin TSlice; _ } ] ) -> + [ TSlice _ ] ) -> (* Will decay. See comment above maybe_addrof *) rhs | ( FunId (FBuiltin (Index { is_array = false; mutability = _; is_range = false })), diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 8f7c0d90..c2521b7c 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -1070,10 +1070,10 @@ let bonus_cleanups = method! visit_lident _ lid = match lid with - | [ "core"; "slice"; "{@Slice}" ], "len" -> [ "Eurydice" ], "slice_len" - | [ "core"; "slice"; "{@Slice}" ], "copy_from_slice" -> [ "Eurydice" ], "slice_copy" - | [ "core"; "slice"; "{@Slice}" ], "split_at" -> [ "Eurydice" ], "slice_split_at" - | [ "core"; "slice"; "{@Slice}" ], "split_at_mut" -> [ "Eurydice" ], "slice_split_at_mut" + | [ "core"; "slice"; "{[T]}" ], "len" -> [ "Eurydice" ], "slice_len" + | [ "core"; "slice"; "{[T]}" ], "copy_from_slice" -> [ "Eurydice" ], "slice_copy" + | [ "core"; "slice"; "{[T]}" ], "split_at" -> [ "Eurydice" ], "slice_split_at" + | [ "core"; "slice"; "{[T]}" ], "split_at_mut" -> [ "Eurydice" ], "slice_split_at_mut" | _ -> lid (* { f = e; ... }.f ~~> e @@ -1136,10 +1136,10 @@ let cosmetic = method! visit_expr _ e = match e with | [%cremepat {| core::slice::?impl::len(Eurydice::array_to_slice_shared[#?n](?)) |}] - when impl = "{@Slice}" -> n + when impl = "{[T]}" -> n | [%cremepat {| core::slice::?impl::len(Eurydice::array_to_slice_mut[#?n](?)) |}] - when impl = "{@Slice}" -> n - | [%cremepat {| core::slice::?impl::len(?e) |}] when impl = "{@Slice}" -> + when impl = "{[T]}" -> n + | [%cremepat {| core::slice::?impl::len(?e) |}] when impl = "{[T]}" -> with_type (TInt SizeT) (EField (e, "meta")) | [%cremepat {| Eurydice::slice_index_mut(?s, ?i) |}] -> with_type e.typ diff --git a/lib/PreCleanup.ml b/lib/PreCleanup.ml index 4d90faa5..d4d31b2d 100644 --- a/lib/PreCleanup.ml +++ b/lib/PreCleanup.ml @@ -22,10 +22,10 @@ let remove_array_eq = if is_flat t then let diff = n_binders - n_cgs in match impl with - | "{core::cmp::PartialEq<@Array> for @Array}" -> + | "{core::cmp::PartialEq<[U; N]> for [T; N]}" -> with_type TBool (EApp (Builtin.(expr_of_builtin_t ~cgs:(diff, [ n ]) array_eq [ t ]), [ a1; a2 ])) - | "{core::cmp::PartialEq<&0 (@Slice)> for @Array}" -> + | "{core::cmp::PartialEq<&0 ([U])> for [T; N]}" -> let hd = if !Options.no_const then Builtin.array_eq_slice_mut diff --git a/out/test-array/array.c b/out/test-array/array.c index 953c1cf2..96425b63 100644 --- a/out/test-array/array.c +++ b/out/test-array/array.c @@ -227,14 +227,14 @@ size_t array_nested_from_fn_closure_call_once_4d_ac(const size_t *_, size_t _0) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array> for array::nested_from_fn::closure} +This function found in impl {core::ops::function::FnMut<(usize), [usize; K]> for array::nested_from_fn::closure} */ /** -A monomorphic instance of array.nested_from_fn.call_mut_af +A monomorphic instance of array.nested_from_fn.call_mut_6c with const generics - K= 4 */ -Eurydice_arr_33 array_nested_from_fn_call_mut_af_ac(void **_, size_t tupled_args) +Eurydice_arr_33 array_nested_from_fn_call_mut_6c_ac(void **_, size_t tupled_args) { size_t j = tupled_args; Eurydice_arr_33 arr_struct; @@ -249,18 +249,18 @@ Eurydice_arr_33 array_nested_from_fn_call_mut_af_ac(void **_, size_t tupled_args } /** -This function found in impl {core::ops::function::FnOnce<(usize), @Array> for array::nested_from_fn::closure} +This function found in impl {core::ops::function::FnOnce<(usize), [usize; K]> for array::nested_from_fn::closure} */ /** -A monomorphic instance of array.nested_from_fn.call_once_f6 +A monomorphic instance of array.nested_from_fn.call_once_d9 with const generics - K= 4 */ -Eurydice_arr_33 array_nested_from_fn_call_once_f6_ac(size_t _) +Eurydice_arr_33 array_nested_from_fn_call_once_d9_ac(size_t _) { /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - return array_nested_from_fn_call_mut_af_ac(&lvalue, _); + return array_nested_from_fn_call_mut_6c_ac(&lvalue, _); } /** @@ -277,7 +277,7 @@ Eurydice_arr_c6 array_nested_from_fn_ac(void) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = array_nested_from_fn_call_mut_af_ac(&lvalue, i);); + arr_struct.data[i] = array_nested_from_fn_call_mut_6c_ac(&lvalue, i);); return arr_struct; } diff --git a/out/test-array/array.h b/out/test-array/array.h index fec31e13..0fca7a38 100644 --- a/out/test-array/array.h +++ b/out/test-array/array.h @@ -231,24 +231,24 @@ with const generics typedef struct Eurydice_arr_33_s { size_t data[4U]; } Eurydice_arr_33; /** -This function found in impl {core::ops::function::FnMut<(usize), @Array> for array::nested_from_fn::closure} +This function found in impl {core::ops::function::FnMut<(usize), [usize; K]> for array::nested_from_fn::closure} */ /** -A monomorphic instance of array.nested_from_fn.call_mut_af +A monomorphic instance of array.nested_from_fn.call_mut_6c with const generics - K= 4 */ -Eurydice_arr_33 array_nested_from_fn_call_mut_af_ac(void **_, size_t tupled_args); +Eurydice_arr_33 array_nested_from_fn_call_mut_6c_ac(void **_, size_t tupled_args); /** -This function found in impl {core::ops::function::FnOnce<(usize), @Array> for array::nested_from_fn::closure} +This function found in impl {core::ops::function::FnOnce<(usize), [usize; K]> for array::nested_from_fn::closure} */ /** -A monomorphic instance of array.nested_from_fn.call_once_f6 +A monomorphic instance of array.nested_from_fn.call_once_d9 with const generics - K= 4 */ -Eurydice_arr_33 array_nested_from_fn_call_once_f6_ac(size_t _); +Eurydice_arr_33 array_nested_from_fn_call_once_d9_ac(size_t _); /** A monomorphic instance of Eurydice.arr diff --git a/out/test-closure/closure.c b/out/test-closure/closure.c index 392df9d3..bd57b268 100644 --- a/out/test-closure/closure.c +++ b/out/test-closure/closure.c @@ -25,9 +25,9 @@ size_t closure_f_closure_call_once_b7(closure_f_closure_closure _, size_t _0) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array> for closure::f::closure<0>} +This function found in impl {core::ops::function::FnMut<(usize), [usize; 1usize]> for closure::f::closure<0>} */ -Eurydice_arr_e4 closure_f_call_mut_59(const Eurydice_arr_e4 **_, size_t tupled_args) +Eurydice_arr_e4 closure_f_call_mut_82(const Eurydice_arr_e4 **_, size_t tupled_args) { size_t i0 = tupled_args; Eurydice_arr_e4 arr_struct; @@ -40,11 +40,11 @@ Eurydice_arr_e4 closure_f_call_mut_59(const Eurydice_arr_e4 **_, size_t tupled_a } /** -This function found in impl {core::ops::function::FnOnce<(usize), @Array> for closure::f::closure<0>} +This function found in impl {core::ops::function::FnOnce<(usize), [usize; 1usize]> for closure::f::closure<0>} */ -Eurydice_arr_e4 closure_f_call_once_71(const Eurydice_arr_e4 *_, size_t _0) +Eurydice_arr_e4 closure_f_call_once_86(const Eurydice_arr_e4 *_, size_t _0) { - return closure_f_call_mut_59(&_, _0); + return closure_f_call_mut_82(&_, _0); } Eurydice_arr_6a closure_f(void) @@ -54,7 +54,7 @@ Eurydice_arr_6a closure_f(void) { /* original Rust expression is not an lvalue in C */ const Eurydice_arr_e4 *lvalue = &s; - arr_struct.data[0U] = closure_f_call_mut_59(&lvalue, (size_t)0U); + arr_struct.data[0U] = closure_f_call_mut_82(&lvalue, (size_t)0U); } Eurydice_arr_6a a = arr_struct; return a; diff --git a/out/test-closure/closure.h b/out/test-closure/closure.h index 4759824c..2022da6c 100644 --- a/out/test-closure/closure.h +++ b/out/test-closure/closure.h @@ -43,14 +43,14 @@ This function found in impl {core::ops::function::FnOnce<(usize), usize> for clo size_t closure_f_closure_call_once_b7(closure_f_closure_closure _, size_t _0); /** -This function found in impl {core::ops::function::FnMut<(usize), @Array> for closure::f::closure<0>} +This function found in impl {core::ops::function::FnMut<(usize), [usize; 1usize]> for closure::f::closure<0>} */ -Eurydice_arr_e4 closure_f_call_mut_59(const Eurydice_arr_e4 **_, size_t tupled_args); +Eurydice_arr_e4 closure_f_call_mut_82(const Eurydice_arr_e4 **_, size_t tupled_args); /** -This function found in impl {core::ops::function::FnOnce<(usize), @Array> for closure::f::closure<0>} +This function found in impl {core::ops::function::FnOnce<(usize), [usize; 1usize]> for closure::f::closure<0>} */ -Eurydice_arr_e4 closure_f_call_once_71(const Eurydice_arr_e4 *_, size_t _0); +Eurydice_arr_e4 closure_f_call_once_86(const Eurydice_arr_e4 *_, size_t _0); /** A monomorphic instance of Eurydice.arr diff --git a/out/test-libcrux-no-const/internal/libcrux_core.h b/out/test-libcrux-no-const/internal/libcrux_core.h index 1d08f61a..3e443eb8 100644 --- a/out/test-libcrux-no-const/internal/libcrux_core.h +++ b/out/test-libcrux-no-const/internal/libcrux_core.h @@ -187,14 +187,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_subslice_to_mut_6e1(Eurydice_arr_00 *a, size_t r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 1568 */ -Eurydice_arr_00 libcrux_ml_kem_types_from_fd_af(Eurydice_arr_00 value); +Eurydice_arr_00 libcrux_ml_kem_types_from_51_af(Eurydice_arr_00 value); /** This function found in impl {libcrux_ml_kem::types::MlKemKeyPair} @@ -209,14 +209,14 @@ libcrux_ml_kem_mlkem1024_MlKem1024KeyPair libcrux_ml_kem_types_from_17_94(Eurydice_arr_17 sk, Eurydice_arr_00 pk); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 3168 */ -Eurydice_arr_17 libcrux_ml_kem_types_from_77_39(Eurydice_arr_17 value); +Eurydice_arr_17 libcrux_ml_kem_types_from_b2_39(Eurydice_arr_17 value); /** A monomorphic instance of Eurydice.array_to_subslice_mut @@ -244,14 +244,14 @@ with const generics Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_c9(Eurydice_arr_38 *a); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 1568 */ -Eurydice_arr_00 libcrux_ml_kem_types_from_e0_af(Eurydice_arr_00 value); +Eurydice_arr_00 libcrux_ml_kem_types_from_19_af(Eurydice_arr_00 value); /** This function found in impl {libcrux_ml_kem::types::MlKemPublicKey} @@ -419,14 +419,14 @@ with const generics Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_4e(Eurydice_arr_00 *a); /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 1568 */ -Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_af(Eurydice_arr_00 *self); +Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_af(Eurydice_arr_00 *self); /** A monomorphic instance of Eurydice.array_to_subslice_from_mut @@ -523,14 +523,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_subslice_to_mut_6e0(Eurydice_arr_74 *a, size_t r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 1184 */ -Eurydice_arr_74 libcrux_ml_kem_types_from_fd_d0(Eurydice_arr_74 value); +Eurydice_arr_74 libcrux_ml_kem_types_from_51_d0(Eurydice_arr_74 value); /** This function found in impl {libcrux_ml_kem::types::MlKemKeyPair} @@ -545,14 +545,14 @@ libcrux_ml_kem_mlkem768_MlKem768KeyPair libcrux_ml_kem_types_from_17_74(Eurydice_arr_ea sk, Eurydice_arr_74 pk); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 2400 */ -Eurydice_arr_ea libcrux_ml_kem_types_from_77_28(Eurydice_arr_ea value); +Eurydice_arr_ea libcrux_ml_kem_types_from_b2_28(Eurydice_arr_ea value); /** A monomorphic instance of Eurydice.array_to_subslice_mut @@ -598,14 +598,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_subslice_mut_3618(Eurydice_arr_74 *a, core_ops_range_Range_08 r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 1088 */ -Eurydice_arr_2c libcrux_ml_kem_types_from_e0_80(Eurydice_arr_2c value); +Eurydice_arr_2c libcrux_ml_kem_types_from_19_80(Eurydice_arr_2c value); /** This function found in impl {libcrux_ml_kem::types::MlKemPublicKey} @@ -724,14 +724,14 @@ with const generics Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_42(Eurydice_arr_2c *a); /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 1088 */ -Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_80(Eurydice_arr_2c *self); +Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_80(Eurydice_arr_2c *self); /** A monomorphic instance of Eurydice.array_to_subslice_from_mut @@ -831,14 +831,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_subslice_to_mut_6e(Eurydice_arr_30 *a, size_t r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 800 */ -Eurydice_arr_30 libcrux_ml_kem_types_from_fd_4d(Eurydice_arr_30 value); +Eurydice_arr_30 libcrux_ml_kem_types_from_51_4d(Eurydice_arr_30 value); /** This function found in impl {libcrux_ml_kem::types::MlKemKeyPair} @@ -853,14 +853,14 @@ libcrux_ml_kem_types_MlKemKeyPair_3e libcrux_ml_kem_types_from_17_fa(Eurydice_arr_7f sk, Eurydice_arr_30 pk); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 1632 */ -Eurydice_arr_7f libcrux_ml_kem_types_from_77_2a(Eurydice_arr_7f value); +Eurydice_arr_7f libcrux_ml_kem_types_from_b2_2a(Eurydice_arr_7f value); /** A monomorphic instance of Eurydice.array_to_subslice_mut @@ -936,14 +936,14 @@ with types Eurydice_arr uint8_t[[$32size_t]], core_array_TryFromSliceError Eurydice_arr_60 core_result_unwrap_26_07(core_result_Result_2b self); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 768 */ -Eurydice_arr_56 libcrux_ml_kem_types_from_e0_d0(Eurydice_arr_56 value); +Eurydice_arr_56 libcrux_ml_kem_types_from_19_d0(Eurydice_arr_56 value); /** This function found in impl {libcrux_ml_kem::types::MlKemPublicKey} @@ -1230,14 +1230,14 @@ with const generics Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_ee(Eurydice_arr_56 *a); /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 768 */ -Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_d0(Eurydice_arr_56 *self); +Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_d0(Eurydice_arr_56 *self); /** A monomorphic instance of Eurydice.array_to_subslice_from_mut @@ -1531,15 +1531,15 @@ with types Eurydice_arr int16_t[[$16size_t]] Eurydice_arr_e2 libcrux_secrets_int_public_integers_declassify_d8_3a(Eurydice_arr_e2 self); /** -This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a (@Slice)> for &'a (@Slice)} +This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a ([T])> for &'a ([T])} */ /** -A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_9b +A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_6d with types uint8_t */ Eurydice_mut_borrow_slice_u8 -libcrux_secrets_int_classify_public_classify_ref_9b_90(Eurydice_mut_borrow_slice_u8 self); +libcrux_secrets_int_classify_public_classify_ref_6d_90(Eurydice_mut_borrow_slice_u8 self); /** This function found in impl {libcrux_secrets::traits::Declassify for T} @@ -1561,15 +1561,15 @@ Eurydice_mut_borrow_slice_i16 Eurydice_array_to_subslice_mut_85(Eurydice_arr_e2 *a, core_ops_range_Range_08 r); /** -This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a (@Slice)> for &'a (@Slice)} +This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a ([T])> for &'a ([T])} */ /** -A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_9b +A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_6d with types int16_t */ Eurydice_mut_borrow_slice_i16 -libcrux_secrets_int_classify_public_classify_ref_9b_39(Eurydice_mut_borrow_slice_i16 self); +libcrux_secrets_int_classify_public_classify_ref_6d_39(Eurydice_mut_borrow_slice_i16 self); /** A monomorphic instance of Eurydice.slice_subslice_mut diff --git a/out/test-libcrux-no-const/libcrux_core.c b/out/test-libcrux-no-const/libcrux_core.c index b213c1fb..87b64ccc 100644 --- a/out/test-libcrux-no-const/libcrux_core.c +++ b/out/test-libcrux-no-const/libcrux_core.c @@ -396,14 +396,14 @@ Eurydice_array_to_subslice_to_mut_6e1(Eurydice_arr_00 *a, size_t r) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 1568 */ -Eurydice_arr_00 libcrux_ml_kem_types_from_fd_af(Eurydice_arr_00 value) +Eurydice_arr_00 libcrux_ml_kem_types_from_51_af(Eurydice_arr_00 value) { return value; } @@ -424,14 +424,14 @@ libcrux_ml_kem_types_from_17_94(Eurydice_arr_17 sk, Eurydice_arr_00 pk) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 3168 */ -Eurydice_arr_17 libcrux_ml_kem_types_from_77_39(Eurydice_arr_17 value) +Eurydice_arr_17 libcrux_ml_kem_types_from_b2_39(Eurydice_arr_17 value) { return value; } @@ -469,14 +469,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_c9(Eurydice_arr_38 *a) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 1568 */ -Eurydice_arr_00 libcrux_ml_kem_types_from_e0_af(Eurydice_arr_00 value) +Eurydice_arr_00 libcrux_ml_kem_types_from_19_af(Eurydice_arr_00 value) { return value; } @@ -586,14 +586,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_4e(Eurydice_arr_00 *a) } /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 1568 */ -Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_af(Eurydice_arr_00 *self) +Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_af(Eurydice_arr_00 *self) { return Eurydice_array_to_slice_mut_4e(self); } @@ -770,14 +770,14 @@ Eurydice_array_to_subslice_to_mut_6e0(Eurydice_arr_74 *a, size_t r) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 1184 */ -Eurydice_arr_74 libcrux_ml_kem_types_from_fd_d0(Eurydice_arr_74 value) +Eurydice_arr_74 libcrux_ml_kem_types_from_51_d0(Eurydice_arr_74 value) { return value; } @@ -798,14 +798,14 @@ libcrux_ml_kem_types_from_17_74(Eurydice_arr_ea sk, Eurydice_arr_74 pk) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 2400 */ -Eurydice_arr_ea libcrux_ml_kem_types_from_77_28(Eurydice_arr_ea value) +Eurydice_arr_ea libcrux_ml_kem_types_from_b2_28(Eurydice_arr_ea value) { return value; } @@ -874,14 +874,14 @@ Eurydice_array_to_subslice_mut_3618(Eurydice_arr_74 *a, core_ops_range_Range_08 } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 1088 */ -Eurydice_arr_2c libcrux_ml_kem_types_from_e0_80(Eurydice_arr_2c value) +Eurydice_arr_2c libcrux_ml_kem_types_from_19_80(Eurydice_arr_2c value) { return value; } @@ -973,14 +973,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_42(Eurydice_arr_2c *a) } /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 1088 */ -Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_80(Eurydice_arr_2c *self) +Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_80(Eurydice_arr_2c *self) { return Eurydice_array_to_slice_mut_42(self); } @@ -1192,14 +1192,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_subslice_to_mut_6e(Eurydice_arr_3 } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 800 */ -Eurydice_arr_30 libcrux_ml_kem_types_from_fd_4d(Eurydice_arr_30 value) +Eurydice_arr_30 libcrux_ml_kem_types_from_51_4d(Eurydice_arr_30 value) { return value; } @@ -1220,14 +1220,14 @@ libcrux_ml_kem_types_from_17_fa(Eurydice_arr_7f sk, Eurydice_arr_30 pk) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 1632 */ -Eurydice_arr_7f libcrux_ml_kem_types_from_77_2a(Eurydice_arr_7f value) +Eurydice_arr_7f libcrux_ml_kem_types_from_b2_2a(Eurydice_arr_7f value) { return value; } @@ -1318,14 +1318,14 @@ Eurydice_arr_60 core_result_unwrap_26_07(core_result_Result_2b self) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 768 */ -Eurydice_arr_56 libcrux_ml_kem_types_from_e0_d0(Eurydice_arr_56 value) +Eurydice_arr_56 libcrux_ml_kem_types_from_19_d0(Eurydice_arr_56 value) { return value; } @@ -1691,14 +1691,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_ee(Eurydice_arr_56 *a) } /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 768 */ -Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_d0(Eurydice_arr_56 *self) +Eurydice_mut_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_d0(Eurydice_arr_56 *self) { return Eurydice_array_to_slice_mut_ee(self); } @@ -2127,15 +2127,15 @@ Eurydice_arr_e2 libcrux_secrets_int_public_integers_declassify_d8_3a(Eurydice_ar } /** -This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a (@Slice)> for &'a (@Slice)} +This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a ([T])> for &'a ([T])} */ /** -A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_9b +A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_6d with types uint8_t */ Eurydice_mut_borrow_slice_u8 -libcrux_secrets_int_classify_public_classify_ref_9b_90(Eurydice_mut_borrow_slice_u8 self) +libcrux_secrets_int_classify_public_classify_ref_6d_90(Eurydice_mut_borrow_slice_u8 self) { return self; } @@ -2172,15 +2172,15 @@ Eurydice_array_to_subslice_mut_85(Eurydice_arr_e2 *a, core_ops_range_Range_08 r) } /** -This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a (@Slice)> for &'a (@Slice)} +This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a ([T])> for &'a ([T])} */ /** -A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_9b +A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_6d with types int16_t */ Eurydice_mut_borrow_slice_i16 -libcrux_secrets_int_classify_public_classify_ref_9b_39(Eurydice_mut_borrow_slice_i16 self) +libcrux_secrets_int_classify_public_classify_ref_6d_39(Eurydice_mut_borrow_slice_i16 self) { return self; } diff --git a/out/test-libcrux-no-const/libcrux_mlkem_avx2.c b/out/test-libcrux-no-const/libcrux_mlkem_avx2.c index 7acc3eca..7fb72ea0 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem_avx2.c +++ b/out/test-libcrux-no-const/libcrux_mlkem_avx2.c @@ -2246,15 +2246,15 @@ static KRML_MUSTINLINE Eurydice_arr_51 from_i16_array_d6_84(Eurydice_mut_borrow_ } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics - K= 3 */ -static Eurydice_arr_51 call_mut_e7_6c1(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_6c1(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -2294,7 +2294,7 @@ static KRML_MUSTINLINE Eurydice_arr_9d sample_from_xof_6c1(Eurydice_arr_c3 *seed (size_t)0U, (size_t)3U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_6c1(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_6c1(out.data[i]);); return arr_mapped_str; } @@ -2319,7 +2319,7 @@ sample_matrix_A_6c1(Eurydice_arr_7d *A_transpose, Eurydice_arr_48 *seed, bool tr (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -2429,13 +2429,13 @@ clone_91_ab(libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_63 *self) { Eurydice_arr_9d uu____0 = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)3U, + core_array__core__clone__Clone_for__T__N___clone((size_t)3U, &self->t_as_ntt, Eurydice_arr_51, Eurydice_arr_9d); Eurydice_arr_60 uu____1 = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)32U, + core_array__core__clone__Clone_for__T__N___clone((size_t)32U, &self->seed_for_A, uint8_t, Eurydice_arr_60); @@ -2444,7 +2444,7 @@ clone_91_ab(libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_63 *self) KRML_CLITERAL(libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_63){ .t_as_ntt = uu____0, .seed_for_A = uu____1, - .A = core_array__core__clone__Clone_for__Array_T__N___clone((size_t)3U, + .A = core_array__core__clone__Clone_for__T__N___clone((size_t)3U, &self->A, Eurydice_arr_9d, Eurydice_arr_7d) @@ -2472,7 +2472,7 @@ libcrux_ml_kem_ind_cca_unpacked_clone_d7_ab( ( KRML_CLITERAL(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63){ .ind_cpa_public_key = uu____0, - .public_key_hash = core_array__core__clone__Clone_for__Array_T__N___clone((size_t)32U, + .public_key_hash = core_array__core__clone__Clone_for__T__N___clone((size_t)32U, &self->public_key_hash, uint8_t, Eurydice_arr_60) @@ -2654,7 +2654,7 @@ static KRML_MUSTINLINE Eurydice_arr_74 serialized_dd_ed(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *self) { return - libcrux_ml_kem_types_from_fd_d0(serialize_public_key_ed(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_d0(serialize_public_key_ed(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_mut_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -2811,15 +2811,15 @@ deserialize_vector_ab(Eurydice_mut_borrow_slice_u8 secret_key, Eurydice_arr_9d * } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$3size_t]] with const generics - K= 3 */ -static Eurydice_arr_51 call_mut_e7_b31(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_b31(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -2864,7 +2864,7 @@ static KRML_MUSTINLINE Eurydice_arr_9d sample_from_xof_b31(Eurydice_arr_c3 *seed (size_t)0U, (size_t)3U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_b31(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_b31(out.data[i]);); return arr_mapped_str; } @@ -2889,7 +2889,7 @@ sample_matrix_A_b31(Eurydice_arr_7d *A_transpose, Eurydice_arr_48 *seed, bool tr (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -3519,7 +3519,7 @@ sample_vector_cbd_then_ntt_b41( (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -3847,15 +3847,15 @@ static Eurydice_arr_51 call_mut_b4_ab(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 3 */ -static Eurydice_arr_9d call_mut_7b_ab(void **_) +static Eurydice_arr_9d call_mut_22_ab(void **_) { Eurydice_arr_9d arr_struct; KRML_MAYBE_FOR3(i, @@ -3880,7 +3880,7 @@ with const generics static inline Eurydice_arr_51 clone_c1_84(Eurydice_arr_51 *self) { return - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)16U, + core_array__core__clone__Clone_for__T__N___clone((size_t)16U, self, __m256i, Eurydice_arr_51); @@ -3901,7 +3901,7 @@ static Eurydice_arr_7d transpose_a_ab(Eurydice_arr_7d ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_ab(&lvalue);); + arr_struct.data[i] = call_mut_22_ab(&lvalue);); Eurydice_arr_7d A = arr_struct; KRML_MAYBE_FOR3(i0, (size_t)0U, @@ -4071,7 +4071,7 @@ sample_ring_element_cbd_b41( (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -5036,7 +5036,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_701( return ( KRML_CLITERAL(tuple_7f){ - .fst = libcrux_ml_kem_types_from_e0_80(ciphertext), + .fst = libcrux_ml_kem_types_from_19_80(ciphertext), .snd = shared_secret_array } ); @@ -5650,7 +5650,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_121( uu____2 = Eurydice_array_to_subslice_from_mut_8c3(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_80(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_80(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_41(Eurydice_array_to_slice_mut_74(&to_hash)); Eurydice_arr_2c @@ -5658,7 +5658,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_121( encrypt_unpacked_741(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_80(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_80(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -5937,10 +5937,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_bb1(Eurydice_arr_06 *randomness) serialize_kem_secret_key_ae(Eurydice_array_to_slice_mut_06(&ind_cpa_private_key), Eurydice_array_to_slice_mut_45(&public_key), implicit_rejection_value); - Eurydice_arr_ea private_key = libcrux_ml_kem_types_from_77_28(secret_key_serialized); + Eurydice_arr_ea private_key = libcrux_ml_kem_types_from_b2_28(secret_key_serialized); return libcrux_ml_kem_types_from_17_74(private_key, - libcrux_ml_kem_types_from_fd_d0(public_key)); + libcrux_ml_kem_types_from_51_d0(public_key)); } /** @@ -6098,7 +6098,7 @@ libcrux_ml_kem_ind_cca_encapsulate_701( encrypt_741(Eurydice_array_to_slice_mut_45(libcrux_ml_kem_types_as_slice_e6_d0(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_2c uu____2 = libcrux_ml_kem_types_from_e0_80(ciphertext); + Eurydice_arr_2c uu____2 = libcrux_ml_kem_types_from_19_80(ciphertext); return (KRML_CLITERAL(tuple_7f){ .fst = uu____2, .snd = kdf_39_ae(shared_secret) }); } @@ -6205,7 +6205,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a11( uu____2 = Eurydice_array_to_subslice_from_mut_8c3(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_80(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_80(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_41(Eurydice_array_to_slice_mut_74(&to_hash)); Eurydice_arr_2c @@ -6214,7 +6214,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a11( uu____3 = Eurydice_array_to_slice_mut_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_ae(uu____3); Eurydice_arr_60 shared_secret = kdf_39_ae(shared_secret0); - Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_80(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_80(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_mut_42(&expected_ciphertext), @@ -6572,15 +6572,15 @@ sample_from_uniform_distribution_next_780( } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics - K= 4 */ -static Eurydice_arr_51 call_mut_e7_6c0(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_6c0(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -6621,7 +6621,7 @@ static KRML_MUSTINLINE Eurydice_arr_c5 sample_from_xof_6c0(Eurydice_arr_c50 *see (size_t)0U, (size_t)4U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_6c0(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_6c0(out.data[i]);); return arr_mapped_str; } @@ -6646,7 +6646,7 @@ sample_matrix_A_6c0(Eurydice_arr_43 *A_transpose, Eurydice_arr_48 *seed, bool tr (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -6860,7 +6860,7 @@ static KRML_MUSTINLINE Eurydice_arr_00 serialized_dd_78(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_39 *self) { return - libcrux_ml_kem_types_from_fd_af(serialize_public_key_78(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_af(serialize_public_key_78(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_mut_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -6990,15 +6990,15 @@ deserialize_vector_42(Eurydice_mut_borrow_slice_u8 secret_key, Eurydice_arr_c5 * } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$4size_t]] with const generics - K= 4 */ -static Eurydice_arr_51 call_mut_e7_b30(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_b30(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -7044,7 +7044,7 @@ static KRML_MUSTINLINE Eurydice_arr_c5 sample_from_xof_b30(Eurydice_arr_c50 *see (size_t)0U, (size_t)4U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_b30(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_b30(out.data[i]);); return arr_mapped_str; } @@ -7069,7 +7069,7 @@ sample_matrix_A_b30(Eurydice_arr_43 *A_transpose, Eurydice_arr_48 *seed, bool tr (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -7367,7 +7367,7 @@ sample_vector_cbd_then_ntt_b40( (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -7582,15 +7582,15 @@ static Eurydice_arr_51 call_mut_b4_42(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 4 */ -static Eurydice_arr_c5 call_mut_7b_42(void **_) +static Eurydice_arr_c5 call_mut_22_42(void **_) { Eurydice_arr_c5 arr_struct; KRML_MAYBE_FOR4(i, @@ -7618,7 +7618,7 @@ static Eurydice_arr_43 transpose_a_42(Eurydice_arr_43 ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_42(&lvalue);); + arr_struct.data[i] = call_mut_22_42(&lvalue);); Eurydice_arr_43 A = arr_struct; KRML_MAYBE_FOR4(i0, (size_t)0U, @@ -7788,7 +7788,7 @@ sample_ring_element_cbd_b40( (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -8222,7 +8222,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_700( return ( KRML_CLITERAL(tuple_4d){ - .fst = libcrux_ml_kem_types_from_e0_af(ciphertext), + .fst = libcrux_ml_kem_types_from_19_af(ciphertext), .snd = shared_secret_array } ); @@ -8485,7 +8485,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_120( uu____2 = Eurydice_array_to_subslice_from_mut_8c6(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_af(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_af(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_44(Eurydice_array_to_slice_mut_8e(&to_hash)); Eurydice_arr_00 @@ -8493,7 +8493,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_120( encrypt_unpacked_740(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_af(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_af(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -8772,10 +8772,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_bb0(Eurydice_arr_06 *randomness) serialize_kem_secret_key_5e(Eurydice_array_to_slice_mut_c9(&ind_cpa_private_key), Eurydice_array_to_slice_mut_4e(&public_key), implicit_rejection_value); - Eurydice_arr_17 private_key = libcrux_ml_kem_types_from_77_39(secret_key_serialized); + Eurydice_arr_17 private_key = libcrux_ml_kem_types_from_b2_39(secret_key_serialized); return libcrux_ml_kem_types_from_17_94(private_key, - libcrux_ml_kem_types_from_fd_af(public_key)); + libcrux_ml_kem_types_from_51_af(public_key)); } /** @@ -8933,7 +8933,7 @@ libcrux_ml_kem_ind_cca_encapsulate_700( encrypt_740(Eurydice_array_to_slice_mut_4e(libcrux_ml_kem_types_as_slice_e6_af(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_00 uu____2 = libcrux_ml_kem_types_from_e0_af(ciphertext); + Eurydice_arr_00 uu____2 = libcrux_ml_kem_types_from_19_af(ciphertext); return (KRML_CLITERAL(tuple_4d){ .fst = uu____2, .snd = kdf_39_5e(shared_secret) }); } @@ -9040,7 +9040,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a10( uu____2 = Eurydice_array_to_subslice_from_mut_8c6(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_af(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_af(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_44(Eurydice_array_to_slice_mut_8e(&to_hash)); Eurydice_arr_00 @@ -9049,7 +9049,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a10( uu____3 = Eurydice_array_to_slice_mut_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_5e(uu____3); Eurydice_arr_60 shared_secret = kdf_39_5e(shared_secret0); - Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_af(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_af(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_mut_4e(&expected_ciphertext), @@ -9400,15 +9400,15 @@ sample_from_uniform_distribution_next_290( } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics - K= 2 */ -static Eurydice_arr_51 call_mut_e7_6c(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_6c(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -9447,7 +9447,7 @@ static KRML_MUSTINLINE Eurydice_arr_d3 sample_from_xof_6c(Eurydice_arr_f90 *seed (size_t)0U, (size_t)2U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_6c(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_6c(out.data[i]);); return arr_mapped_str; } @@ -9472,7 +9472,7 @@ sample_matrix_A_6c(Eurydice_arr_9a *A_transpose, Eurydice_arr_48 *seed, bool tra (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -9686,7 +9686,7 @@ static KRML_MUSTINLINE Eurydice_arr_30 serialized_dd_29(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_94 *self) { return - libcrux_ml_kem_types_from_fd_4d(serialize_public_key_29(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_4d(serialize_public_key_29(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_mut_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -9816,15 +9816,15 @@ deserialize_vector_89(Eurydice_mut_borrow_slice_u8 secret_key, Eurydice_arr_d3 * } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$2size_t]] with const generics - K= 2 */ -static Eurydice_arr_51 call_mut_e7_b3(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_b3(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -9868,7 +9868,7 @@ static KRML_MUSTINLINE Eurydice_arr_d3 sample_from_xof_b3(Eurydice_arr_f90 *seed (size_t)0U, (size_t)2U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_b3(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_b3(out.data[i]);); return arr_mapped_str; } @@ -9893,7 +9893,7 @@ sample_matrix_A_b3(Eurydice_arr_9a *A_transpose, Eurydice_arr_48 *seed, bool tra (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -10198,7 +10198,7 @@ sample_vector_cbd_then_ntt_b4( (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -10413,15 +10413,15 @@ static Eurydice_arr_51 call_mut_b4_89(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 2 */ -static Eurydice_arr_d3 call_mut_7b_89(void **_) +static Eurydice_arr_d3 call_mut_22_89(void **_) { Eurydice_arr_d3 arr_struct; KRML_MAYBE_FOR2(i, @@ -10449,7 +10449,7 @@ static Eurydice_arr_9a transpose_a_89(Eurydice_arr_9a ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_89(&lvalue);); + arr_struct.data[i] = call_mut_22_89(&lvalue);); Eurydice_arr_9a A = arr_struct; KRML_MAYBE_FOR2(i0, (size_t)0U, @@ -10659,7 +10659,7 @@ sample_ring_element_cbd_b4( (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -11047,7 +11047,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_70( return ( KRML_CLITERAL(tuple_50){ - .fst = libcrux_ml_kem_types_from_e0_d0(ciphertext), + .fst = libcrux_ml_kem_types_from_19_d0(ciphertext), .snd = shared_secret_array } ); @@ -11279,7 +11279,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_12( uu____2 = Eurydice_array_to_subslice_from_mut_8c1(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_d0(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_d0(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_49(Eurydice_array_to_slice_mut_03(&to_hash)); Eurydice_arr_56 @@ -11287,7 +11287,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_12( encrypt_unpacked_74(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_d0(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_d0(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -11566,10 +11566,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_bb(Eurydice_arr_06 *randomness) serialize_kem_secret_key_4d(Eurydice_array_to_slice_mut_ee(&ind_cpa_private_key), Eurydice_array_to_slice_mut_03(&public_key), implicit_rejection_value); - Eurydice_arr_7f private_key = libcrux_ml_kem_types_from_77_2a(secret_key_serialized); + Eurydice_arr_7f private_key = libcrux_ml_kem_types_from_b2_2a(secret_key_serialized); return libcrux_ml_kem_types_from_17_fa(private_key, - libcrux_ml_kem_types_from_fd_4d(public_key)); + libcrux_ml_kem_types_from_51_4d(public_key)); } /** @@ -11724,7 +11724,7 @@ libcrux_ml_kem_ind_cca_encapsulate_70(Eurydice_arr_30 *public_key, Eurydice_arr_ encrypt_74(Eurydice_array_to_slice_mut_03(libcrux_ml_kem_types_as_slice_e6_4d(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_56 uu____2 = libcrux_ml_kem_types_from_e0_d0(ciphertext); + Eurydice_arr_56 uu____2 = libcrux_ml_kem_types_from_19_d0(ciphertext); return (KRML_CLITERAL(tuple_50){ .fst = uu____2, .snd = kdf_39_4d(shared_secret) }); } @@ -11831,7 +11831,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a1( uu____2 = Eurydice_array_to_subslice_from_mut_8c1(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_d0(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_d0(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_49(Eurydice_array_to_slice_mut_03(&to_hash)); Eurydice_arr_56 @@ -11840,7 +11840,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a1( uu____3 = Eurydice_array_to_slice_mut_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_4d(uu____3); Eurydice_arr_60 shared_secret = kdf_39_4d(shared_secret0); - Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_d0(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_d0(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_mut_ee(&expected_ciphertext), diff --git a/out/test-libcrux-no-const/libcrux_mlkem_portable.c b/out/test-libcrux-no-const/libcrux_mlkem_portable.c index 9a693f13..879a0f49 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem_portable.c +++ b/out/test-libcrux-no-const/libcrux_mlkem_portable.c @@ -55,7 +55,7 @@ Eurydice_arr_e2 libcrux_ml_kem_vector_portable_from_i16_array_b8(Eurydice_mut_borrow_slice_i16 array) { return - libcrux_ml_kem_vector_portable_vector_type_from_i16_array(libcrux_secrets_int_classify_public_classify_ref_9b_39(array)); + libcrux_ml_kem_vector_portable_vector_type_from_i16_array(libcrux_secrets_int_classify_public_classify_ref_6d_39(array)); } KRML_MUSTINLINE uint8_t_x11 @@ -225,7 +225,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_11(Eurydice_mut_borrow_slic Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_11(Eurydice_mut_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_11(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_11(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -296,7 +296,7 @@ Eurydice_arr_e2 libcrux_ml_kem_vector_portable_from_bytes_b8(Eurydice_mut_borrow_slice_u8 array) { return - libcrux_ml_kem_vector_portable_vector_type_from_bytes(libcrux_secrets_int_classify_public_classify_ref_9b_90(array)); + libcrux_ml_kem_vector_portable_vector_type_from_bytes(libcrux_secrets_int_classify_public_classify_ref_6d_90(array)); } KRML_MUSTINLINE void @@ -1108,7 +1108,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_1(Eurydice_mut_borrow_slice Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_1(Eurydice_mut_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_1(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_1(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -1229,7 +1229,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_4(Eurydice_mut_borrow_slice Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_4(Eurydice_mut_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_4(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_4(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -1352,7 +1352,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_5(Eurydice_mut_borrow_slice Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_5(Eurydice_mut_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_5(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_5(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -1507,7 +1507,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_10(Eurydice_mut_borrow_slic Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_10(Eurydice_mut_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_10(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_10(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -1650,7 +1650,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_12(Eurydice_mut_borrow_slic Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_12(Eurydice_mut_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_12(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_12(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -2186,15 +2186,15 @@ static KRML_MUSTINLINE Eurydice_arr_b9 from_i16_array_d6_ea(Eurydice_mut_borrow_ } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$4size_t]] with const generics - K= 4 */ -static Eurydice_arr_b9 call_mut_e7_2b1(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_b9 call_mut_0a_2b1(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -2240,7 +2240,7 @@ static KRML_MUSTINLINE Eurydice_arr_cf sample_from_xof_2b1(Eurydice_arr_c50 *see (size_t)0U, (size_t)4U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_2b1(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_2b1(out.data[i]);); return arr_mapped_str; } @@ -2265,7 +2265,7 @@ sample_matrix_A_2b1(Eurydice_arr_5c *A_transpose, Eurydice_arr_48 *seed, bool tr (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -2518,7 +2518,7 @@ static KRML_MUSTINLINE Eurydice_arr_00 serialized_dd_ff(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_af *self) { return - libcrux_ml_kem_types_from_fd_af(serialize_public_key_ff(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_af(serialize_public_key_ff(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_mut_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -3338,7 +3338,7 @@ sample_vector_cbd_then_ntt_3b1( (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -3671,15 +3671,15 @@ static Eurydice_arr_b9 call_mut_b4_d0(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 4 */ -static Eurydice_arr_cf call_mut_7b_d0(void **_) +static Eurydice_arr_cf call_mut_22_d0(void **_) { Eurydice_arr_cf arr_struct; KRML_MAYBE_FOR4(i, @@ -3704,7 +3704,7 @@ with const generics static inline Eurydice_arr_b9 clone_c1_ea(Eurydice_arr_b9 *self) { return - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)16U, + core_array__core__clone__Clone_for__T__N___clone((size_t)16U, self, Eurydice_arr_e2, Eurydice_arr_b9); @@ -3725,7 +3725,7 @@ static Eurydice_arr_5c transpose_a_d0(Eurydice_arr_5c ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_d0(&lvalue);); + arr_struct.data[i] = call_mut_22_d0(&lvalue);); Eurydice_arr_5c A = arr_struct; KRML_MAYBE_FOR4(i0, (size_t)0U, @@ -3895,7 +3895,7 @@ sample_ring_element_cbd_3b1( (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -4759,7 +4759,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_0c1( return ( KRML_CLITERAL(tuple_4d){ - .fst = libcrux_ml_kem_types_from_e0_af(ciphertext), + .fst = libcrux_ml_kem_types_from_19_af(ciphertext), .snd = shared_secret_array } ); @@ -5356,7 +5356,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_511( uu____2 = Eurydice_array_to_subslice_from_mut_8c6(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_af(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_af(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_44(Eurydice_array_to_slice_mut_8e(&to_hash)); Eurydice_arr_00 @@ -5364,7 +5364,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_511( encrypt_unpacked_2a1(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_af(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_af(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -5588,10 +5588,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_151(Eurydice_arr_06 *randomness) serialize_kem_secret_key_60(Eurydice_array_to_slice_mut_c9(&ind_cpa_private_key), Eurydice_array_to_slice_mut_4e(&public_key), implicit_rejection_value); - Eurydice_arr_17 private_key = libcrux_ml_kem_types_from_77_39(secret_key_serialized); + Eurydice_arr_17 private_key = libcrux_ml_kem_types_from_b2_39(secret_key_serialized); return libcrux_ml_kem_types_from_17_94(private_key, - libcrux_ml_kem_types_from_fd_af(public_key)); + libcrux_ml_kem_types_from_51_af(public_key)); } /** @@ -5725,7 +5725,7 @@ libcrux_ml_kem_ind_cca_encapsulate_ca1( encrypt_2a1(Eurydice_array_to_slice_mut_4e(libcrux_ml_kem_types_as_slice_e6_af(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_00 uu____2 = libcrux_ml_kem_types_from_e0_af(ciphertext); + Eurydice_arr_00 uu____2 = libcrux_ml_kem_types_from_19_af(ciphertext); return (KRML_CLITERAL(tuple_4d){ .fst = uu____2, .snd = kdf_39_60(shared_secret) }); } @@ -5832,7 +5832,7 @@ libcrux_ml_kem_ind_cca_decapsulate_621( uu____2 = Eurydice_array_to_subslice_from_mut_8c6(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_af(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_af(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_44(Eurydice_array_to_slice_mut_8e(&to_hash)); Eurydice_arr_00 @@ -5841,7 +5841,7 @@ libcrux_ml_kem_ind_cca_decapsulate_621( uu____3 = Eurydice_array_to_slice_mut_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_60(uu____3); Eurydice_arr_60 shared_secret = kdf_39_60(shared_secret0); - Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_af(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_af(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_mut_4e(&expected_ciphertext), @@ -6196,15 +6196,15 @@ sample_from_uniform_distribution_next_640( } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$2size_t]] with const generics - K= 2 */ -static Eurydice_arr_b9 call_mut_e7_2b0(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_b9 call_mut_0a_2b0(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -6248,7 +6248,7 @@ static KRML_MUSTINLINE Eurydice_arr_3d0 sample_from_xof_2b0(Eurydice_arr_f90 *se (size_t)0U, (size_t)2U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_2b0(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_2b0(out.data[i]);); return arr_mapped_str; } @@ -6273,7 +6273,7 @@ sample_matrix_A_2b0(Eurydice_arr_6d0 *A_transpose, Eurydice_arr_48 *seed, bool t (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -6487,7 +6487,7 @@ static KRML_MUSTINLINE Eurydice_arr_30 serialized_dd_64(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_d4 *self) { return - libcrux_ml_kem_types_from_fd_4d(serialize_public_key_64(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_4d(serialize_public_key_64(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_mut_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -6944,7 +6944,7 @@ sample_vector_cbd_then_ntt_3b0( (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -7161,15 +7161,15 @@ static Eurydice_arr_b9 call_mut_b4_a0(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 2 */ -static Eurydice_arr_3d0 call_mut_7b_a0(void **_) +static Eurydice_arr_3d0 call_mut_22_a0(void **_) { Eurydice_arr_3d0 arr_struct; KRML_MAYBE_FOR2(i, @@ -7197,7 +7197,7 @@ static Eurydice_arr_6d0 transpose_a_a0(Eurydice_arr_6d0 ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_a0(&lvalue);); + arr_struct.data[i] = call_mut_22_a0(&lvalue);); Eurydice_arr_6d0 A = arr_struct; KRML_MAYBE_FOR2(i0, (size_t)0U, @@ -7400,7 +7400,7 @@ sample_ring_element_cbd_3b0( (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -7832,7 +7832,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_0c0( return ( KRML_CLITERAL(tuple_50){ - .fst = libcrux_ml_kem_types_from_e0_d0(ciphertext), + .fst = libcrux_ml_kem_types_from_19_d0(ciphertext), .snd = shared_secret_array } ); @@ -8095,7 +8095,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_510( uu____2 = Eurydice_array_to_subslice_from_mut_8c1(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_d0(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_d0(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_49(Eurydice_array_to_slice_mut_03(&to_hash)); Eurydice_arr_56 @@ -8103,7 +8103,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_510( encrypt_unpacked_2a0(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_d0(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_d0(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -8327,10 +8327,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_150(Eurydice_arr_06 *randomness) serialize_kem_secret_key_30(Eurydice_array_to_slice_mut_ee(&ind_cpa_private_key), Eurydice_array_to_slice_mut_03(&public_key), implicit_rejection_value); - Eurydice_arr_7f private_key = libcrux_ml_kem_types_from_77_2a(secret_key_serialized); + Eurydice_arr_7f private_key = libcrux_ml_kem_types_from_b2_2a(secret_key_serialized); return libcrux_ml_kem_types_from_17_fa(private_key, - libcrux_ml_kem_types_from_fd_4d(public_key)); + libcrux_ml_kem_types_from_51_4d(public_key)); } /** @@ -8464,7 +8464,7 @@ libcrux_ml_kem_ind_cca_encapsulate_ca0( encrypt_2a0(Eurydice_array_to_slice_mut_03(libcrux_ml_kem_types_as_slice_e6_4d(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_56 uu____2 = libcrux_ml_kem_types_from_e0_d0(ciphertext); + Eurydice_arr_56 uu____2 = libcrux_ml_kem_types_from_19_d0(ciphertext); return (KRML_CLITERAL(tuple_50){ .fst = uu____2, .snd = kdf_39_30(shared_secret) }); } @@ -8571,7 +8571,7 @@ libcrux_ml_kem_ind_cca_decapsulate_620( uu____2 = Eurydice_array_to_subslice_from_mut_8c1(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_d0(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_d0(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_49(Eurydice_array_to_slice_mut_03(&to_hash)); Eurydice_arr_56 @@ -8580,7 +8580,7 @@ libcrux_ml_kem_ind_cca_decapsulate_620( uu____3 = Eurydice_array_to_slice_mut_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_30(uu____3); Eurydice_arr_60 shared_secret = kdf_39_30(shared_secret0); - Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_d0(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_d0(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_mut_ee(&expected_ciphertext), @@ -8935,15 +8935,15 @@ sample_from_uniform_distribution_next_890( } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$3size_t]] with const generics - K= 3 */ -static Eurydice_arr_b9 call_mut_e7_2b(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_b9 call_mut_0a_2b(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -8988,7 +8988,7 @@ static KRML_MUSTINLINE Eurydice_arr_1d sample_from_xof_2b(Eurydice_arr_c3 *seeds (size_t)0U, (size_t)3U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_2b(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_2b(out.data[i]);); return arr_mapped_str; } @@ -9013,7 +9013,7 @@ sample_matrix_A_2b(Eurydice_arr_dd *A_transpose, Eurydice_arr_48 *seed, bool tra (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -9123,13 +9123,13 @@ clone_91_1b(libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_a0 *self) { Eurydice_arr_1d uu____0 = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)3U, + core_array__core__clone__Clone_for__T__N___clone((size_t)3U, &self->t_as_ntt, Eurydice_arr_b9, Eurydice_arr_1d); Eurydice_arr_60 uu____1 = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)32U, + core_array__core__clone__Clone_for__T__N___clone((size_t)32U, &self->seed_for_A, uint8_t, Eurydice_arr_60); @@ -9138,7 +9138,7 @@ clone_91_1b(libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_a0 *self) KRML_CLITERAL(libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_a0){ .t_as_ntt = uu____0, .seed_for_A = uu____1, - .A = core_array__core__clone__Clone_for__Array_T__N___clone((size_t)3U, + .A = core_array__core__clone__Clone_for__T__N___clone((size_t)3U, &self->A, Eurydice_arr_1d, Eurydice_arr_dd) @@ -9166,7 +9166,7 @@ libcrux_ml_kem_ind_cca_unpacked_clone_d7_1b( ( KRML_CLITERAL(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0){ .ind_cpa_public_key = uu____0, - .public_key_hash = core_array__core__clone__Clone_for__Array_T__N___clone((size_t)32U, + .public_key_hash = core_array__core__clone__Clone_for__T__N___clone((size_t)32U, &self->public_key_hash, uint8_t, Eurydice_arr_60) @@ -9309,7 +9309,7 @@ static KRML_MUSTINLINE Eurydice_arr_74 serialized_dd_89(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *self) { return - libcrux_ml_kem_types_from_fd_d0(serialize_public_key_89(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_d0(serialize_public_key_89(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_mut_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -9754,7 +9754,7 @@ sample_vector_cbd_then_ntt_3b( (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -9971,15 +9971,15 @@ static Eurydice_arr_b9 call_mut_b4_1b(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 3 */ -static Eurydice_arr_1d call_mut_7b_1b(void **_) +static Eurydice_arr_1d call_mut_22_1b(void **_) { Eurydice_arr_1d arr_struct; KRML_MAYBE_FOR3(i, @@ -10007,7 +10007,7 @@ static Eurydice_arr_dd transpose_a_1b(Eurydice_arr_dd ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_1b(&lvalue);); + arr_struct.data[i] = call_mut_22_1b(&lvalue);); Eurydice_arr_dd A = arr_struct; KRML_MAYBE_FOR3(i0, (size_t)0U, @@ -10177,7 +10177,7 @@ sample_ring_element_cbd_3b( (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -10565,7 +10565,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_0c( return ( KRML_CLITERAL(tuple_7f){ - .fst = libcrux_ml_kem_types_from_e0_80(ciphertext), + .fst = libcrux_ml_kem_types_from_19_80(ciphertext), .snd = shared_secret_array } ); @@ -10797,7 +10797,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_51( uu____2 = Eurydice_array_to_subslice_from_mut_8c3(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_80(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_80(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_41(Eurydice_array_to_slice_mut_74(&to_hash)); Eurydice_arr_2c @@ -10805,7 +10805,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_51( encrypt_unpacked_2a(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_80(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_80(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -11029,10 +11029,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_15(Eurydice_arr_06 *randomness) serialize_kem_secret_key_d6(Eurydice_array_to_slice_mut_06(&ind_cpa_private_key), Eurydice_array_to_slice_mut_45(&public_key), implicit_rejection_value); - Eurydice_arr_ea private_key = libcrux_ml_kem_types_from_77_28(secret_key_serialized); + Eurydice_arr_ea private_key = libcrux_ml_kem_types_from_b2_28(secret_key_serialized); return libcrux_ml_kem_types_from_17_74(private_key, - libcrux_ml_kem_types_from_fd_d0(public_key)); + libcrux_ml_kem_types_from_51_d0(public_key)); } /** @@ -11163,7 +11163,7 @@ libcrux_ml_kem_ind_cca_encapsulate_ca(Eurydice_arr_74 *public_key, Eurydice_arr_ encrypt_2a(Eurydice_array_to_slice_mut_45(libcrux_ml_kem_types_as_slice_e6_d0(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_2c uu____2 = libcrux_ml_kem_types_from_e0_80(ciphertext); + Eurydice_arr_2c uu____2 = libcrux_ml_kem_types_from_19_80(ciphertext); return (KRML_CLITERAL(tuple_7f){ .fst = uu____2, .snd = kdf_39_d6(shared_secret) }); } @@ -11270,7 +11270,7 @@ libcrux_ml_kem_ind_cca_decapsulate_62( uu____2 = Eurydice_array_to_subslice_from_mut_8c3(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_80(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_80(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_41(Eurydice_array_to_slice_mut_74(&to_hash)); Eurydice_arr_2c @@ -11279,7 +11279,7 @@ libcrux_ml_kem_ind_cca_decapsulate_62( uu____3 = Eurydice_array_to_slice_mut_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_d6(uu____3); Eurydice_arr_60 shared_secret = kdf_39_d6(shared_secret0); - Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_80(ciphertext); + Eurydice_mut_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_80(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_mut_42(&expected_ciphertext), diff --git a/out/test-libcrux-no-const/libcrux_sha3_avx2.c b/out/test-libcrux-no-const/libcrux_sha3_avx2.c index ff1b7fc2..b4861336 100644 --- a/out/test-libcrux-no-const/libcrux_sha3_avx2.c +++ b/out/test-libcrux-no-const/libcrux_sha3_avx2.c @@ -214,7 +214,7 @@ load_block_5b(Eurydice_arr_05 *state, Eurydice_arr_7b *blocks, size_t offset) uint8_t); __m256i u = - mm256_loadu_si256_u8(core_array___Array_T__N___as_slice((size_t)32U, + mm256_loadu_si256_u8(core_array___T__N___as_slice((size_t)32U, &u8s, uint8_t, Eurydice_mut_borrow_slice_u8)); @@ -266,7 +266,7 @@ load_block_5b(Eurydice_arr_05 *state, Eurydice_arr_7b *blocks, size_t offset) uint8_t); __m256i u0 = - mm256_loadu_si256_u8(core_array___Array_T__N___as_slice((size_t)32U, + mm256_loadu_si256_u8(core_array___T__N___as_slice((size_t)32U, &u8s0, uint8_t, Eurydice_mut_borrow_slice_u8)); @@ -2116,7 +2116,7 @@ load_block_3a(Eurydice_arr_05 *state, Eurydice_arr_7b *blocks, size_t offset) uint8_t); __m256i u = - mm256_loadu_si256_u8(core_array___Array_T__N___as_slice((size_t)32U, + mm256_loadu_si256_u8(core_array___T__N___as_slice((size_t)32U, &u8s, uint8_t, Eurydice_mut_borrow_slice_u8)); @@ -2168,7 +2168,7 @@ load_block_3a(Eurydice_arr_05 *state, Eurydice_arr_7b *blocks, size_t offset) uint8_t); __m256i u0 = - mm256_loadu_si256_u8(core_array___Array_T__N___as_slice((size_t)32U, + mm256_loadu_si256_u8(core_array___T__N___as_slice((size_t)32U, &u8s0, uint8_t, Eurydice_mut_borrow_slice_u8)); diff --git a/out/test-libcrux/internal/libcrux_core.h b/out/test-libcrux/internal/libcrux_core.h index d1136b8c..dc9c0e79 100644 --- a/out/test-libcrux/internal/libcrux_core.h +++ b/out/test-libcrux/internal/libcrux_core.h @@ -196,14 +196,14 @@ Eurydice_borrow_slice_u8 Eurydice_array_to_subslice_shared_3610(const Eurydice_arr_17 *a, core_ops_range_Range_08 r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 1568 */ -Eurydice_arr_00 libcrux_ml_kem_types_from_fd_af(Eurydice_arr_00 value); +Eurydice_arr_00 libcrux_ml_kem_types_from_51_af(Eurydice_arr_00 value); /** This function found in impl {libcrux_ml_kem::types::MlKemKeyPair} @@ -218,14 +218,14 @@ libcrux_ml_kem_mlkem1024_MlKem1024KeyPair libcrux_ml_kem_types_from_17_94(Eurydice_arr_17 sk, Eurydice_arr_00 pk); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 3168 */ -Eurydice_arr_17 libcrux_ml_kem_types_from_77_39(Eurydice_arr_17 value); +Eurydice_arr_17 libcrux_ml_kem_types_from_b2_39(Eurydice_arr_17 value); /** A monomorphic instance of Eurydice.arr @@ -261,14 +261,14 @@ with const generics Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_c9(Eurydice_arr_38 *a); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 1568 */ -Eurydice_arr_00 libcrux_ml_kem_types_from_e0_af(Eurydice_arr_00 value); +Eurydice_arr_00 libcrux_ml_kem_types_from_19_af(Eurydice_arr_00 value); /** This function found in impl {libcrux_ml_kem::types::MlKemPublicKey} @@ -454,14 +454,14 @@ with const generics Eurydice_borrow_slice_u8 Eurydice_array_to_slice_shared_4e(const Eurydice_arr_00 *a); /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 1568 */ -Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_af(const Eurydice_arr_00 *self); +Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_af(const Eurydice_arr_00 *self); /** A monomorphic instance of Eurydice.array_to_subslice_from_mut @@ -576,14 +576,14 @@ Eurydice_borrow_slice_u8 Eurydice_array_to_subslice_shared_368(const Eurydice_arr_ea *a, core_ops_range_Range_08 r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 1184 */ -Eurydice_arr_74 libcrux_ml_kem_types_from_fd_d0(Eurydice_arr_74 value); +Eurydice_arr_74 libcrux_ml_kem_types_from_51_d0(Eurydice_arr_74 value); /** This function found in impl {libcrux_ml_kem::types::MlKemKeyPair} @@ -598,14 +598,14 @@ libcrux_ml_kem_mlkem768_MlKem768KeyPair libcrux_ml_kem_types_from_17_74(Eurydice_arr_ea sk, Eurydice_arr_74 pk); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 2400 */ -Eurydice_arr_ea libcrux_ml_kem_types_from_77_28(Eurydice_arr_ea value); +Eurydice_arr_ea libcrux_ml_kem_types_from_b2_28(Eurydice_arr_ea value); /** A monomorphic instance of Eurydice.arr @@ -659,14 +659,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_subslice_mut_3615(Eurydice_arr_74 *a, core_ops_range_Range_08 r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 1088 */ -Eurydice_arr_2c libcrux_ml_kem_types_from_e0_80(Eurydice_arr_2c value); +Eurydice_arr_2c libcrux_ml_kem_types_from_19_80(Eurydice_arr_2c value); /** This function found in impl {libcrux_ml_kem::types::MlKemPublicKey} @@ -803,14 +803,14 @@ with const generics Eurydice_borrow_slice_u8 Eurydice_array_to_slice_shared_42(const Eurydice_arr_2c *a); /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 1088 */ -Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_80(const Eurydice_arr_2c *self); +Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_80(const Eurydice_arr_2c *self); /** A monomorphic instance of Eurydice.array_to_subslice_from_mut @@ -928,14 +928,14 @@ Eurydice_borrow_slice_u8 Eurydice_array_to_subslice_shared_366(const Eurydice_arr_7f *a, core_ops_range_Range_08 r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 800 */ -Eurydice_arr_30 libcrux_ml_kem_types_from_fd_4d(Eurydice_arr_30 value); +Eurydice_arr_30 libcrux_ml_kem_types_from_51_4d(Eurydice_arr_30 value); /** This function found in impl {libcrux_ml_kem::types::MlKemKeyPair} @@ -950,14 +950,14 @@ libcrux_ml_kem_types_MlKemKeyPair_3e libcrux_ml_kem_types_from_17_fa(Eurydice_arr_7f sk, Eurydice_arr_30 pk); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 1632 */ -Eurydice_arr_7f libcrux_ml_kem_types_from_77_2a(Eurydice_arr_7f value); +Eurydice_arr_7f libcrux_ml_kem_types_from_b2_2a(Eurydice_arr_7f value); /** A monomorphic instance of Eurydice.array_to_subslice_mut @@ -1059,14 +1059,14 @@ Eurydice_borrow_slice_u8 Eurydice_array_to_subslice_shared_365(const Eurydice_arr_060 *a, core_ops_range_Range_08 r); /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 768 */ -Eurydice_arr_56 libcrux_ml_kem_types_from_e0_d0(Eurydice_arr_56 value); +Eurydice_arr_56 libcrux_ml_kem_types_from_19_d0(Eurydice_arr_56 value); /** This function found in impl {libcrux_ml_kem::types::MlKemPublicKey} @@ -1413,14 +1413,14 @@ with const generics Eurydice_borrow_slice_u8 Eurydice_array_to_slice_shared_ee(const Eurydice_arr_56 *a); /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 768 */ -Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_d0(const Eurydice_arr_56 *self); +Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_d0(const Eurydice_arr_56 *self); /** A monomorphic instance of Eurydice.array_to_subslice_from_mut @@ -1745,15 +1745,15 @@ with types Eurydice_arr int16_t[[$16size_t]] Eurydice_arr_e2 libcrux_secrets_int_public_integers_declassify_d8_3a(Eurydice_arr_e2 self); /** -This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a (@Slice)> for &'a (@Slice)} +This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a ([T])> for &'a ([T])} */ /** -A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_9b +A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_6d with types uint8_t */ Eurydice_borrow_slice_u8 -libcrux_secrets_int_classify_public_classify_ref_9b_90(Eurydice_borrow_slice_u8 self); +libcrux_secrets_int_classify_public_classify_ref_6d_90(Eurydice_borrow_slice_u8 self); /** This function found in impl {libcrux_secrets::traits::Declassify for T} @@ -1775,15 +1775,15 @@ Eurydice_borrow_slice_i16 Eurydice_array_to_subslice_shared_85(const Eurydice_arr_e2 *a, core_ops_range_Range_08 r); /** -This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a (@Slice)> for &'a (@Slice)} +This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a ([T])> for &'a ([T])} */ /** -A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_9b +A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_6d with types int16_t */ Eurydice_borrow_slice_i16 -libcrux_secrets_int_classify_public_classify_ref_9b_39(Eurydice_borrow_slice_i16 self); +libcrux_secrets_int_classify_public_classify_ref_6d_39(Eurydice_borrow_slice_i16 self); /** A monomorphic instance of Eurydice.slice_subslice_shared diff --git a/out/test-libcrux/libcrux_core.c b/out/test-libcrux/libcrux_core.c index 55059d15..a79d95a2 100644 --- a/out/test-libcrux/libcrux_core.c +++ b/out/test-libcrux/libcrux_core.c @@ -409,14 +409,14 @@ Eurydice_array_to_subslice_shared_3610(const Eurydice_arr_17 *a, core_ops_range_ } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 1568 */ -Eurydice_arr_00 libcrux_ml_kem_types_from_fd_af(Eurydice_arr_00 value) +Eurydice_arr_00 libcrux_ml_kem_types_from_51_af(Eurydice_arr_00 value) { return value; } @@ -437,14 +437,14 @@ libcrux_ml_kem_types_from_17_94(Eurydice_arr_17 sk, Eurydice_arr_00 pk) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 3168 */ -Eurydice_arr_17 libcrux_ml_kem_types_from_77_39(Eurydice_arr_17 value) +Eurydice_arr_17 libcrux_ml_kem_types_from_b2_39(Eurydice_arr_17 value) { return value; } @@ -496,14 +496,14 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_c9(Eurydice_arr_38 *a) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 1568 */ -Eurydice_arr_00 libcrux_ml_kem_types_from_e0_af(Eurydice_arr_00 value) +Eurydice_arr_00 libcrux_ml_kem_types_from_19_af(Eurydice_arr_00 value) { return value; } @@ -644,14 +644,14 @@ Eurydice_borrow_slice_u8 Eurydice_array_to_slice_shared_4e(const Eurydice_arr_00 } /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 1568 */ -Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_af(const Eurydice_arr_00 *self) +Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_af(const Eurydice_arr_00 *self) { return Eurydice_array_to_slice_shared_4e(self); } @@ -849,14 +849,14 @@ Eurydice_array_to_subslice_shared_368(const Eurydice_arr_ea *a, core_ops_range_R } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 1184 */ -Eurydice_arr_74 libcrux_ml_kem_types_from_fd_d0(Eurydice_arr_74 value) +Eurydice_arr_74 libcrux_ml_kem_types_from_51_d0(Eurydice_arr_74 value) { return value; } @@ -877,14 +877,14 @@ libcrux_ml_kem_types_from_17_74(Eurydice_arr_ea sk, Eurydice_arr_74 pk) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 2400 */ -Eurydice_arr_ea libcrux_ml_kem_types_from_77_28(Eurydice_arr_ea value) +Eurydice_arr_ea libcrux_ml_kem_types_from_b2_28(Eurydice_arr_ea value) { return value; } @@ -967,14 +967,14 @@ Eurydice_array_to_subslice_mut_3615(Eurydice_arr_74 *a, core_ops_range_Range_08 } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 1088 */ -Eurydice_arr_2c libcrux_ml_kem_types_from_e0_80(Eurydice_arr_2c value) +Eurydice_arr_2c libcrux_ml_kem_types_from_19_80(Eurydice_arr_2c value) { return value; } @@ -1097,14 +1097,14 @@ Eurydice_borrow_slice_u8 Eurydice_array_to_slice_shared_42(const Eurydice_arr_2c } /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 1088 */ -Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_80(const Eurydice_arr_2c *self) +Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_80(const Eurydice_arr_2c *self) { return Eurydice_array_to_slice_shared_42(self); } @@ -1338,14 +1338,14 @@ Eurydice_array_to_subslice_shared_366(const Eurydice_arr_7f *a, core_ops_range_R } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPublicKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPublicKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_fd +A monomorphic instance of libcrux_ml_kem.types.from_51 with const generics - SIZE= 800 */ -Eurydice_arr_30 libcrux_ml_kem_types_from_fd_4d(Eurydice_arr_30 value) +Eurydice_arr_30 libcrux_ml_kem_types_from_51_4d(Eurydice_arr_30 value) { return value; } @@ -1366,14 +1366,14 @@ libcrux_ml_kem_types_from_17_fa(Eurydice_arr_7f sk, Eurydice_arr_30 pk) } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemPrivateKey} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemPrivateKey} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_77 +A monomorphic instance of libcrux_ml_kem.types.from_b2 with const generics - SIZE= 1632 */ -Eurydice_arr_7f libcrux_ml_kem_types_from_77_2a(Eurydice_arr_7f value) +Eurydice_arr_7f libcrux_ml_kem_types_from_b2_2a(Eurydice_arr_7f value) { return value; } @@ -1504,14 +1504,14 @@ Eurydice_array_to_subslice_shared_365(const Eurydice_arr_060 *a, core_ops_range_ } /** -This function found in impl {core::convert::From<@Array> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::From<[u8; SIZE]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.from_e0 +A monomorphic instance of libcrux_ml_kem.types.from_19 with const generics - SIZE= 768 */ -Eurydice_arr_56 libcrux_ml_kem_types_from_e0_d0(Eurydice_arr_56 value) +Eurydice_arr_56 libcrux_ml_kem_types_from_19_d0(Eurydice_arr_56 value) { return value; } @@ -1971,14 +1971,14 @@ Eurydice_borrow_slice_u8 Eurydice_array_to_slice_shared_ee(const Eurydice_arr_56 } /** -This function found in impl {core::convert::AsRef<@Slice> for libcrux_ml_kem::types::MlKemCiphertext} +This function found in impl {core::convert::AsRef<[u8]> for libcrux_ml_kem::types::MlKemCiphertext} */ /** -A monomorphic instance of libcrux_ml_kem.types.as_ref_d3 +A monomorphic instance of libcrux_ml_kem.types.as_ref_c1 with const generics - SIZE= 768 */ -Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_d3_d0(const Eurydice_arr_56 *self) +Eurydice_borrow_slice_u8 libcrux_ml_kem_types_as_ref_c1_d0(const Eurydice_arr_56 *self) { return Eurydice_array_to_slice_shared_ee(self); } @@ -2470,15 +2470,15 @@ Eurydice_arr_e2 libcrux_secrets_int_public_integers_declassify_d8_3a(Eurydice_ar } /** -This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a (@Slice)> for &'a (@Slice)} +This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a ([T])> for &'a ([T])} */ /** -A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_9b +A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_6d with types uint8_t */ Eurydice_borrow_slice_u8 -libcrux_secrets_int_classify_public_classify_ref_9b_90(Eurydice_borrow_slice_u8 self) +libcrux_secrets_int_classify_public_classify_ref_6d_90(Eurydice_borrow_slice_u8 self) { return self; } @@ -2510,15 +2510,15 @@ Eurydice_array_to_subslice_shared_85(const Eurydice_arr_e2 *a, core_ops_range_Ra } /** -This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a (@Slice)> for &'a (@Slice)} +This function found in impl {libcrux_secrets::traits::ClassifyRef<&'a ([T])> for &'a ([T])} */ /** -A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_9b +A monomorphic instance of libcrux_secrets.int.classify_public.classify_ref_6d with types int16_t */ Eurydice_borrow_slice_i16 -libcrux_secrets_int_classify_public_classify_ref_9b_39(Eurydice_borrow_slice_i16 self) +libcrux_secrets_int_classify_public_classify_ref_6d_39(Eurydice_borrow_slice_i16 self) { return self; } diff --git a/out/test-libcrux/libcrux_mlkem_avx2.c b/out/test-libcrux/libcrux_mlkem_avx2.c index 18eb4e1f..d8318330 100644 --- a/out/test-libcrux/libcrux_mlkem_avx2.c +++ b/out/test-libcrux/libcrux_mlkem_avx2.c @@ -2247,15 +2247,15 @@ static KRML_MUSTINLINE Eurydice_arr_51 from_i16_array_d6_84(Eurydice_borrow_slic } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics - K= 3 */ -static Eurydice_arr_51 call_mut_e7_6c1(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_6c1(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -2295,7 +2295,7 @@ static KRML_MUSTINLINE Eurydice_arr_9d sample_from_xof_6c1(const Eurydice_arr_c3 (size_t)0U, (size_t)3U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_6c1(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_6c1(out.data[i]);); return arr_mapped_str; } @@ -2320,7 +2320,7 @@ sample_matrix_A_6c1(Eurydice_arr_7d *A_transpose, const Eurydice_arr_48 *seed, b (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -2431,13 +2431,13 @@ clone_91_ab(const libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_63 *se { Eurydice_arr_9d uu____0 = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)3U, + core_array__core__clone__Clone_for__T__N___clone((size_t)3U, &self->t_as_ntt, Eurydice_arr_51, Eurydice_arr_9d); Eurydice_arr_60 uu____1 = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)32U, + core_array__core__clone__Clone_for__T__N___clone((size_t)32U, &self->seed_for_A, uint8_t, Eurydice_arr_60); @@ -2446,7 +2446,7 @@ clone_91_ab(const libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_63 *se KRML_CLITERAL(libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_63){ .t_as_ntt = uu____0, .seed_for_A = uu____1, - .A = core_array__core__clone__Clone_for__Array_T__N___clone((size_t)3U, + .A = core_array__core__clone__Clone_for__T__N___clone((size_t)3U, &self->A, Eurydice_arr_9d, Eurydice_arr_7d) @@ -2474,7 +2474,7 @@ libcrux_ml_kem_ind_cca_unpacked_clone_d7_ab( ( KRML_CLITERAL(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63){ .ind_cpa_public_key = uu____0, - .public_key_hash = core_array__core__clone__Clone_for__Array_T__N___clone((size_t)32U, + .public_key_hash = core_array__core__clone__Clone_for__T__N___clone((size_t)32U, &self->public_key_hash, uint8_t, Eurydice_arr_60) @@ -2656,7 +2656,7 @@ static KRML_MUSTINLINE Eurydice_arr_74 serialized_dd_ed(const libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *self) { return - libcrux_ml_kem_types_from_fd_d0(serialize_public_key_ed(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_d0(serialize_public_key_ed(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_shared_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -2813,15 +2813,15 @@ deserialize_vector_ab(Eurydice_borrow_slice_u8 secret_key, Eurydice_arr_9d *secr } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$3size_t]] with const generics - K= 3 */ -static Eurydice_arr_51 call_mut_e7_b31(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_b31(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -2866,7 +2866,7 @@ static KRML_MUSTINLINE Eurydice_arr_9d sample_from_xof_b31(const Eurydice_arr_c3 (size_t)0U, (size_t)3U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_b31(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_b31(out.data[i]);); return arr_mapped_str; } @@ -2891,7 +2891,7 @@ sample_matrix_A_b31(Eurydice_arr_7d *A_transpose, const Eurydice_arr_48 *seed, b (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -3521,7 +3521,7 @@ sample_vector_cbd_then_ntt_b41( (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -3849,15 +3849,15 @@ static Eurydice_arr_51 call_mut_b4_ab(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 3 */ -static Eurydice_arr_9d call_mut_7b_ab(void **_) +static Eurydice_arr_9d call_mut_22_ab(void **_) { Eurydice_arr_9d arr_struct; KRML_MAYBE_FOR3(i, @@ -3882,7 +3882,7 @@ with const generics static inline Eurydice_arr_51 clone_c1_84(const Eurydice_arr_51 *self) { return - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)16U, + core_array__core__clone__Clone_for__T__N___clone((size_t)16U, self, __m256i, Eurydice_arr_51); @@ -3903,7 +3903,7 @@ static Eurydice_arr_7d transpose_a_ab(Eurydice_arr_7d ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_ab(&lvalue);); + arr_struct.data[i] = call_mut_22_ab(&lvalue);); Eurydice_arr_7d A = arr_struct; KRML_MAYBE_FOR3(i0, (size_t)0U, @@ -4070,7 +4070,7 @@ sample_ring_element_cbd_b41( (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -5035,7 +5035,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_701( return ( KRML_CLITERAL(tuple_7f){ - .fst = libcrux_ml_kem_types_from_e0_80(ciphertext), + .fst = libcrux_ml_kem_types_from_19_80(ciphertext), .snd = shared_secret_array } ); @@ -5649,7 +5649,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_121( uu____2 = Eurydice_array_to_subslice_from_mut_8c2(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_80(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_80(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_41(Eurydice_array_to_slice_shared_74(&to_hash)); Eurydice_arr_2c @@ -5657,7 +5657,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_121( encrypt_unpacked_741(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_80(ciphertext); + Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_80(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -5936,10 +5936,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_bb1(const Eurydice_arr_060 *randomness) serialize_kem_secret_key_ae(Eurydice_array_to_slice_shared_06(&ind_cpa_private_key), Eurydice_array_to_slice_shared_45(&public_key), implicit_rejection_value); - Eurydice_arr_ea private_key = libcrux_ml_kem_types_from_77_28(secret_key_serialized); + Eurydice_arr_ea private_key = libcrux_ml_kem_types_from_b2_28(secret_key_serialized); return libcrux_ml_kem_types_from_17_74(private_key, - libcrux_ml_kem_types_from_fd_d0(public_key)); + libcrux_ml_kem_types_from_51_d0(public_key)); } /** @@ -6097,7 +6097,7 @@ libcrux_ml_kem_ind_cca_encapsulate_701( encrypt_741(Eurydice_array_to_slice_shared_45(libcrux_ml_kem_types_as_slice_e6_d0(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_2c uu____2 = libcrux_ml_kem_types_from_e0_80(ciphertext); + Eurydice_arr_2c uu____2 = libcrux_ml_kem_types_from_19_80(ciphertext); return (KRML_CLITERAL(tuple_7f){ .fst = uu____2, .snd = kdf_39_ae(shared_secret) }); } @@ -6204,7 +6204,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a11( uu____2 = Eurydice_array_to_subslice_from_mut_8c2(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_80(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_80(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_41(Eurydice_array_to_slice_shared_74(&to_hash)); Eurydice_arr_2c @@ -6213,7 +6213,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a11( uu____3 = Eurydice_array_to_slice_shared_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_ae(uu____3); Eurydice_arr_60 shared_secret = kdf_39_ae(shared_secret0); - Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_80(ciphertext); + Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_80(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_shared_42(&expected_ciphertext), @@ -6572,15 +6572,15 @@ sample_from_uniform_distribution_next_780( } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics - K= 4 */ -static Eurydice_arr_51 call_mut_e7_6c0(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_6c0(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -6621,7 +6621,7 @@ static KRML_MUSTINLINE Eurydice_arr_c5 sample_from_xof_6c0(const Eurydice_arr_c5 (size_t)0U, (size_t)4U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_6c0(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_6c0(out.data[i]);); return arr_mapped_str; } @@ -6646,7 +6646,7 @@ sample_matrix_A_6c0(Eurydice_arr_43 *A_transpose, const Eurydice_arr_48 *seed, b (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -6860,7 +6860,7 @@ static KRML_MUSTINLINE Eurydice_arr_00 serialized_dd_78(const libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_39 *self) { return - libcrux_ml_kem_types_from_fd_af(serialize_public_key_78(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_af(serialize_public_key_78(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_shared_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -6990,15 +6990,15 @@ deserialize_vector_42(Eurydice_borrow_slice_u8 secret_key, Eurydice_arr_c5 *secr } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$4size_t]] with const generics - K= 4 */ -static Eurydice_arr_51 call_mut_e7_b30(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_b30(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -7044,7 +7044,7 @@ static KRML_MUSTINLINE Eurydice_arr_c5 sample_from_xof_b30(const Eurydice_arr_c5 (size_t)0U, (size_t)4U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_b30(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_b30(out.data[i]);); return arr_mapped_str; } @@ -7069,7 +7069,7 @@ sample_matrix_A_b30(Eurydice_arr_43 *A_transpose, const Eurydice_arr_48 *seed, b (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -7367,7 +7367,7 @@ sample_vector_cbd_then_ntt_b40( (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -7582,15 +7582,15 @@ static Eurydice_arr_51 call_mut_b4_42(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 4 */ -static Eurydice_arr_c5 call_mut_7b_42(void **_) +static Eurydice_arr_c5 call_mut_22_42(void **_) { Eurydice_arr_c5 arr_struct; KRML_MAYBE_FOR4(i, @@ -7618,7 +7618,7 @@ static Eurydice_arr_43 transpose_a_42(Eurydice_arr_43 ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_42(&lvalue);); + arr_struct.data[i] = call_mut_22_42(&lvalue);); Eurydice_arr_43 A = arr_struct; KRML_MAYBE_FOR4(i0, (size_t)0U, @@ -7785,7 +7785,7 @@ sample_ring_element_cbd_b40( (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -8220,7 +8220,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_700( return ( KRML_CLITERAL(tuple_4d){ - .fst = libcrux_ml_kem_types_from_e0_af(ciphertext), + .fst = libcrux_ml_kem_types_from_19_af(ciphertext), .snd = shared_secret_array } ); @@ -8483,7 +8483,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_120( uu____2 = Eurydice_array_to_subslice_from_mut_8c5(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_af(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_af(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_44(Eurydice_array_to_slice_shared_8e(&to_hash)); Eurydice_arr_00 @@ -8491,7 +8491,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_120( encrypt_unpacked_740(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_af(ciphertext); + Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_af(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -8770,10 +8770,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_bb0(const Eurydice_arr_060 *randomness) serialize_kem_secret_key_5e(Eurydice_array_to_slice_shared_c9(&ind_cpa_private_key), Eurydice_array_to_slice_shared_4e(&public_key), implicit_rejection_value); - Eurydice_arr_17 private_key = libcrux_ml_kem_types_from_77_39(secret_key_serialized); + Eurydice_arr_17 private_key = libcrux_ml_kem_types_from_b2_39(secret_key_serialized); return libcrux_ml_kem_types_from_17_94(private_key, - libcrux_ml_kem_types_from_fd_af(public_key)); + libcrux_ml_kem_types_from_51_af(public_key)); } /** @@ -8931,7 +8931,7 @@ libcrux_ml_kem_ind_cca_encapsulate_700( encrypt_740(Eurydice_array_to_slice_shared_4e(libcrux_ml_kem_types_as_slice_e6_af(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_00 uu____2 = libcrux_ml_kem_types_from_e0_af(ciphertext); + Eurydice_arr_00 uu____2 = libcrux_ml_kem_types_from_19_af(ciphertext); return (KRML_CLITERAL(tuple_4d){ .fst = uu____2, .snd = kdf_39_5e(shared_secret) }); } @@ -9038,7 +9038,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a10( uu____2 = Eurydice_array_to_subslice_from_mut_8c5(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_af(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_af(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_44(Eurydice_array_to_slice_shared_8e(&to_hash)); Eurydice_arr_00 @@ -9047,7 +9047,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a10( uu____3 = Eurydice_array_to_slice_shared_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_5e(uu____3); Eurydice_arr_60 shared_secret = kdf_39_5e(shared_secret0); - Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_af(ciphertext); + Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_af(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_shared_4e(&expected_ciphertext), @@ -9399,15 +9399,15 @@ sample_from_uniform_distribution_next_290( } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics - K= 2 */ -static Eurydice_arr_51 call_mut_e7_6c(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_6c(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -9446,7 +9446,7 @@ static KRML_MUSTINLINE Eurydice_arr_d3 sample_from_xof_6c(const Eurydice_arr_f9 (size_t)0U, (size_t)2U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_6c(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_6c(out.data[i]);); return arr_mapped_str; } @@ -9471,7 +9471,7 @@ sample_matrix_A_6c(Eurydice_arr_9a *A_transpose, const Eurydice_arr_48 *seed, bo (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -9685,7 +9685,7 @@ static KRML_MUSTINLINE Eurydice_arr_30 serialized_dd_29(const libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_94 *self) { return - libcrux_ml_kem_types_from_fd_4d(serialize_public_key_29(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_4d(serialize_public_key_29(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_shared_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -9815,15 +9815,15 @@ deserialize_vector_89(Eurydice_borrow_slice_u8 secret_key, Eurydice_arr_d3 *secr } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_avx2_SIMD256Vector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$2size_t]] with const generics - K= 2 */ -static Eurydice_arr_51 call_mut_e7_b3(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_51 call_mut_0a_b3(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -9867,7 +9867,7 @@ static KRML_MUSTINLINE Eurydice_arr_d3 sample_from_xof_b3(const Eurydice_arr_f9 (size_t)0U, (size_t)2U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_b3(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_b3(out.data[i]);); return arr_mapped_str; } @@ -9892,7 +9892,7 @@ sample_matrix_A_b3(Eurydice_arr_9a *A_transpose, const Eurydice_arr_48 *seed, bo (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -10197,7 +10197,7 @@ sample_vector_cbd_then_ntt_b4( (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -10412,15 +10412,15 @@ static Eurydice_arr_51 call_mut_b4_89(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 2 */ -static Eurydice_arr_d3 call_mut_7b_89(void **_) +static Eurydice_arr_d3 call_mut_22_89(void **_) { Eurydice_arr_d3 arr_struct; KRML_MAYBE_FOR2(i, @@ -10448,7 +10448,7 @@ static Eurydice_arr_9a transpose_a_89(Eurydice_arr_9a ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_89(&lvalue);); + arr_struct.data[i] = call_mut_22_89(&lvalue);); Eurydice_arr_9a A = arr_struct; KRML_MAYBE_FOR2(i0, (size_t)0U, @@ -10655,7 +10655,7 @@ sample_ring_element_cbd_b4( (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -11043,7 +11043,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_70( return ( KRML_CLITERAL(tuple_50){ - .fst = libcrux_ml_kem_types_from_e0_d0(ciphertext), + .fst = libcrux_ml_kem_types_from_19_d0(ciphertext), .snd = shared_secret_array } ); @@ -11275,7 +11275,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_12( uu____2 = Eurydice_array_to_subslice_from_mut_8c0(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_d0(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_d0(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_49(Eurydice_array_to_slice_shared_03(&to_hash)); Eurydice_arr_56 @@ -11283,7 +11283,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_12( encrypt_unpacked_74(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_d0(ciphertext); + Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_d0(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -11562,10 +11562,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_bb(const Eurydice_arr_060 *randomness) serialize_kem_secret_key_4d(Eurydice_array_to_slice_shared_ee(&ind_cpa_private_key), Eurydice_array_to_slice_shared_03(&public_key), implicit_rejection_value); - Eurydice_arr_7f private_key = libcrux_ml_kem_types_from_77_2a(secret_key_serialized); + Eurydice_arr_7f private_key = libcrux_ml_kem_types_from_b2_2a(secret_key_serialized); return libcrux_ml_kem_types_from_17_fa(private_key, - libcrux_ml_kem_types_from_fd_4d(public_key)); + libcrux_ml_kem_types_from_51_4d(public_key)); } /** @@ -11723,7 +11723,7 @@ libcrux_ml_kem_ind_cca_encapsulate_70( encrypt_74(Eurydice_array_to_slice_shared_03(libcrux_ml_kem_types_as_slice_e6_4d(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_56 uu____2 = libcrux_ml_kem_types_from_e0_d0(ciphertext); + Eurydice_arr_56 uu____2 = libcrux_ml_kem_types_from_19_d0(ciphertext); return (KRML_CLITERAL(tuple_50){ .fst = uu____2, .snd = kdf_39_4d(shared_secret) }); } @@ -11830,7 +11830,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a1( uu____2 = Eurydice_array_to_subslice_from_mut_8c0(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_d0(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_d0(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_41_49(Eurydice_array_to_slice_shared_03(&to_hash)); Eurydice_arr_56 @@ -11839,7 +11839,7 @@ libcrux_ml_kem_ind_cca_decapsulate_a1( uu____3 = Eurydice_array_to_slice_shared_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_4d(uu____3); Eurydice_arr_60 shared_secret = kdf_39_4d(shared_secret0); - Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_d0(ciphertext); + Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_d0(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_shared_ee(&expected_ciphertext), diff --git a/out/test-libcrux/libcrux_mlkem_portable.c b/out/test-libcrux/libcrux_mlkem_portable.c index d241e771..fe3cd2bd 100644 --- a/out/test-libcrux/libcrux_mlkem_portable.c +++ b/out/test-libcrux/libcrux_mlkem_portable.c @@ -54,7 +54,7 @@ Eurydice_arr_e2 libcrux_ml_kem_vector_portable_from_i16_array_b8(Eurydice_borrow_slice_i16 array) { return - libcrux_ml_kem_vector_portable_vector_type_from_i16_array(libcrux_secrets_int_classify_public_classify_ref_9b_39(array)); + libcrux_ml_kem_vector_portable_vector_type_from_i16_array(libcrux_secrets_int_classify_public_classify_ref_6d_39(array)); } KRML_MUSTINLINE uint8_t_x11 @@ -224,7 +224,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_11(Eurydice_borrow_slice_u8 Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_11(Eurydice_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_11(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_11(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -293,7 +293,7 @@ This function found in impl {libcrux_ml_kem::vector::traits::Operations for libc Eurydice_arr_e2 libcrux_ml_kem_vector_portable_from_bytes_b8(Eurydice_borrow_slice_u8 array) { return - libcrux_ml_kem_vector_portable_vector_type_from_bytes(libcrux_secrets_int_classify_public_classify_ref_9b_90(array)); + libcrux_ml_kem_vector_portable_vector_type_from_bytes(libcrux_secrets_int_classify_public_classify_ref_6d_90(array)); } KRML_MUSTINLINE void @@ -1105,7 +1105,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_1(Eurydice_borrow_slice_u8 Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_1(Eurydice_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_1(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_1(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -1226,7 +1226,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_4(Eurydice_borrow_slice_u8 Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_4(Eurydice_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_4(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_4(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -1349,7 +1349,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_5(Eurydice_borrow_slice_u8 Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_5(Eurydice_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_5(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_5(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -1504,7 +1504,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_10(Eurydice_borrow_slice_u8 Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_10(Eurydice_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_10(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_10(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -1646,7 +1646,7 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_12(Eurydice_borrow_slice_u8 Eurydice_arr_e2 libcrux_ml_kem_vector_portable_deserialize_12(Eurydice_borrow_slice_u8 a) { return - libcrux_ml_kem_vector_portable_serialize_deserialize_12(libcrux_secrets_int_classify_public_classify_ref_9b_90(a)); + libcrux_ml_kem_vector_portable_serialize_deserialize_12(libcrux_secrets_int_classify_public_classify_ref_6d_90(a)); } /** @@ -2181,15 +2181,15 @@ static KRML_MUSTINLINE Eurydice_arr_b9 from_i16_array_d6_ea(Eurydice_borrow_slic } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$4size_t]] with const generics - K= 4 */ -static Eurydice_arr_b9 call_mut_e7_2b1(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_b9 call_mut_0a_2b1(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -2235,7 +2235,7 @@ static KRML_MUSTINLINE Eurydice_arr_cf sample_from_xof_2b1(const Eurydice_arr_c5 (size_t)0U, (size_t)4U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_2b1(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_2b1(out.data[i]);); return arr_mapped_str; } @@ -2260,7 +2260,7 @@ sample_matrix_A_2b1(Eurydice_arr_5c *A_transpose, const Eurydice_arr_48 *seed, b (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -2513,7 +2513,7 @@ static KRML_MUSTINLINE Eurydice_arr_00 serialized_dd_ff(const libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_af *self) { return - libcrux_ml_kem_types_from_fd_af(serialize_public_key_ff(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_af(serialize_public_key_ff(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_shared_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -3333,7 +3333,7 @@ sample_vector_cbd_then_ntt_3b1( (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -3666,15 +3666,15 @@ static Eurydice_arr_b9 call_mut_b4_d0(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 4 */ -static Eurydice_arr_cf call_mut_7b_d0(void **_) +static Eurydice_arr_cf call_mut_22_d0(void **_) { Eurydice_arr_cf arr_struct; KRML_MAYBE_FOR4(i, @@ -3699,7 +3699,7 @@ with const generics static inline Eurydice_arr_b9 clone_c1_ea(const Eurydice_arr_b9 *self) { return - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)16U, + core_array__core__clone__Clone_for__T__N___clone((size_t)16U, self, Eurydice_arr_e2, Eurydice_arr_b9); @@ -3720,7 +3720,7 @@ static Eurydice_arr_5c transpose_a_d0(Eurydice_arr_5c ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_d0(&lvalue);); + arr_struct.data[i] = call_mut_22_d0(&lvalue);); Eurydice_arr_5c A = arr_struct; KRML_MAYBE_FOR4(i0, (size_t)0U, @@ -3887,7 +3887,7 @@ sample_ring_element_cbd_3b1( (size_t)4U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -4752,7 +4752,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_0c1( return ( KRML_CLITERAL(tuple_4d){ - .fst = libcrux_ml_kem_types_from_e0_af(ciphertext), + .fst = libcrux_ml_kem_types_from_19_af(ciphertext), .snd = shared_secret_array } ); @@ -5349,7 +5349,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_511( uu____2 = Eurydice_array_to_subslice_from_mut_8c5(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_af(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_af(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_44(Eurydice_array_to_slice_shared_8e(&to_hash)); Eurydice_arr_00 @@ -5357,7 +5357,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_511( encrypt_unpacked_2a1(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_af(ciphertext); + Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_af(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -5581,10 +5581,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_151(const Eurydice_arr_060 *randomness) serialize_kem_secret_key_60(Eurydice_array_to_slice_shared_c9(&ind_cpa_private_key), Eurydice_array_to_slice_shared_4e(&public_key), implicit_rejection_value); - Eurydice_arr_17 private_key = libcrux_ml_kem_types_from_77_39(secret_key_serialized); + Eurydice_arr_17 private_key = libcrux_ml_kem_types_from_b2_39(secret_key_serialized); return libcrux_ml_kem_types_from_17_94(private_key, - libcrux_ml_kem_types_from_fd_af(public_key)); + libcrux_ml_kem_types_from_51_af(public_key)); } /** @@ -5718,7 +5718,7 @@ libcrux_ml_kem_ind_cca_encapsulate_ca1( encrypt_2a1(Eurydice_array_to_slice_shared_4e(libcrux_ml_kem_types_as_slice_e6_af(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_00 uu____2 = libcrux_ml_kem_types_from_e0_af(ciphertext); + Eurydice_arr_00 uu____2 = libcrux_ml_kem_types_from_19_af(ciphertext); return (KRML_CLITERAL(tuple_4d){ .fst = uu____2, .snd = kdf_39_60(shared_secret) }); } @@ -5825,7 +5825,7 @@ libcrux_ml_kem_ind_cca_decapsulate_621( uu____2 = Eurydice_array_to_subslice_from_mut_8c5(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_af(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_af(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_44(Eurydice_array_to_slice_shared_8e(&to_hash)); Eurydice_arr_00 @@ -5834,7 +5834,7 @@ libcrux_ml_kem_ind_cca_decapsulate_621( uu____3 = Eurydice_array_to_slice_shared_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_60(uu____3); Eurydice_arr_60 shared_secret = kdf_39_60(shared_secret0); - Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_af(ciphertext); + Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_af(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_shared_4e(&expected_ciphertext), @@ -6189,15 +6189,15 @@ sample_from_uniform_distribution_next_640( } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$2size_t]] with const generics - K= 2 */ -static Eurydice_arr_b9 call_mut_e7_2b0(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_b9 call_mut_0a_2b0(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -6241,7 +6241,7 @@ static KRML_MUSTINLINE Eurydice_arr_3d0 sample_from_xof_2b0(const Eurydice_arr_f (size_t)0U, (size_t)2U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_2b0(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_2b0(out.data[i]);); return arr_mapped_str; } @@ -6266,7 +6266,7 @@ sample_matrix_A_2b0(Eurydice_arr_6d0 *A_transpose, const Eurydice_arr_48 *seed, (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -6480,7 +6480,7 @@ static KRML_MUSTINLINE Eurydice_arr_30 serialized_dd_64(const libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_d4 *self) { return - libcrux_ml_kem_types_from_fd_4d(serialize_public_key_64(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_4d(serialize_public_key_64(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_shared_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -6937,7 +6937,7 @@ sample_vector_cbd_then_ntt_3b0( (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -7154,15 +7154,15 @@ static Eurydice_arr_b9 call_mut_b4_a0(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 2 */ -static Eurydice_arr_3d0 call_mut_7b_a0(void **_) +static Eurydice_arr_3d0 call_mut_22_a0(void **_) { Eurydice_arr_3d0 arr_struct; KRML_MAYBE_FOR2(i, @@ -7190,7 +7190,7 @@ static Eurydice_arr_6d0 transpose_a_a0(Eurydice_arr_6d0 ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_a0(&lvalue);); + arr_struct.data[i] = call_mut_22_a0(&lvalue);); Eurydice_arr_6d0 A = arr_struct; KRML_MAYBE_FOR2(i0, (size_t)0U, @@ -7390,7 +7390,7 @@ sample_ring_element_cbd_3b0( (size_t)2U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -7822,7 +7822,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_0c0( return ( KRML_CLITERAL(tuple_50){ - .fst = libcrux_ml_kem_types_from_e0_d0(ciphertext), + .fst = libcrux_ml_kem_types_from_19_d0(ciphertext), .snd = shared_secret_array } ); @@ -8085,7 +8085,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_510( uu____2 = Eurydice_array_to_subslice_from_mut_8c0(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_d0(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_d0(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_49(Eurydice_array_to_slice_shared_03(&to_hash)); Eurydice_arr_56 @@ -8093,7 +8093,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_510( encrypt_unpacked_2a0(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_d0(ciphertext); + Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_d0(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -8317,10 +8317,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_150(const Eurydice_arr_060 *randomness) serialize_kem_secret_key_30(Eurydice_array_to_slice_shared_ee(&ind_cpa_private_key), Eurydice_array_to_slice_shared_03(&public_key), implicit_rejection_value); - Eurydice_arr_7f private_key = libcrux_ml_kem_types_from_77_2a(secret_key_serialized); + Eurydice_arr_7f private_key = libcrux_ml_kem_types_from_b2_2a(secret_key_serialized); return libcrux_ml_kem_types_from_17_fa(private_key, - libcrux_ml_kem_types_from_fd_4d(public_key)); + libcrux_ml_kem_types_from_51_4d(public_key)); } /** @@ -8454,7 +8454,7 @@ libcrux_ml_kem_ind_cca_encapsulate_ca0( encrypt_2a0(Eurydice_array_to_slice_shared_03(libcrux_ml_kem_types_as_slice_e6_4d(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_56 uu____2 = libcrux_ml_kem_types_from_e0_d0(ciphertext); + Eurydice_arr_56 uu____2 = libcrux_ml_kem_types_from_19_d0(ciphertext); return (KRML_CLITERAL(tuple_50){ .fst = uu____2, .snd = kdf_39_30(shared_secret) }); } @@ -8561,7 +8561,7 @@ libcrux_ml_kem_ind_cca_decapsulate_620( uu____2 = Eurydice_array_to_subslice_from_mut_8c0(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_d0(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_d0(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_49(Eurydice_array_to_slice_shared_03(&to_hash)); Eurydice_arr_56 @@ -8570,7 +8570,7 @@ libcrux_ml_kem_ind_cca_decapsulate_620( uu____3 = Eurydice_array_to_slice_shared_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_30(uu____3); Eurydice_arr_60 shared_secret = kdf_39_30(shared_secret0); - Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_d0(ciphertext); + Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_d0(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_shared_ee(&expected_ciphertext), @@ -8927,15 +8927,15 @@ sample_from_uniform_distribution_next_890( } /** -This function found in impl {core::ops::function::FnMut<(@Array), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} +This function found in impl {core::ops::function::FnMut<([i16; 272usize]), libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@2]> for libcrux_ml_kem::sampling::sample_from_xof::closure[TraitClause@0, TraitClause@1, TraitClause@2, TraitClause@3]} */ /** -A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_e7 +A monomorphic instance of libcrux_ml_kem.sampling.sample_from_xof.call_mut_0a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector, libcrux_ml_kem_hash_functions_portable_PortableHash[[$3size_t]] with const generics - K= 3 */ -static Eurydice_arr_b9 call_mut_e7_2b(Eurydice_arr_a00 tupled_args) +static Eurydice_arr_b9 call_mut_0a_2b(Eurydice_arr_a00 tupled_args) { Eurydice_arr_a00 s = tupled_args; return @@ -8980,7 +8980,7 @@ static KRML_MUSTINLINE Eurydice_arr_1d sample_from_xof_2b(const Eurydice_arr_c3 (size_t)0U, (size_t)3U, (size_t)1U, - arr_mapped_str.data[i] = call_mut_e7_2b(out.data[i]);); + arr_mapped_str.data[i] = call_mut_0a_2b(out.data[i]);); return arr_mapped_str; } @@ -9005,7 +9005,7 @@ sample_matrix_A_2b(Eurydice_arr_dd *A_transpose, const Eurydice_arr_48 *seed, bo (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)34U, + core_array__core__clone__Clone_for__T__N___clone((size_t)34U, seed, uint8_t, Eurydice_arr_48);); @@ -9116,13 +9116,13 @@ clone_91_1b(const libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_a0 *se { Eurydice_arr_1d uu____0 = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)3U, + core_array__core__clone__Clone_for__T__N___clone((size_t)3U, &self->t_as_ntt, Eurydice_arr_b9, Eurydice_arr_1d); Eurydice_arr_60 uu____1 = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)32U, + core_array__core__clone__Clone_for__T__N___clone((size_t)32U, &self->seed_for_A, uint8_t, Eurydice_arr_60); @@ -9131,7 +9131,7 @@ clone_91_1b(const libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_a0 *se KRML_CLITERAL(libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_a0){ .t_as_ntt = uu____0, .seed_for_A = uu____1, - .A = core_array__core__clone__Clone_for__Array_T__N___clone((size_t)3U, + .A = core_array__core__clone__Clone_for__T__N___clone((size_t)3U, &self->A, Eurydice_arr_1d, Eurydice_arr_dd) @@ -9159,7 +9159,7 @@ libcrux_ml_kem_ind_cca_unpacked_clone_d7_1b( ( KRML_CLITERAL(libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0){ .ind_cpa_public_key = uu____0, - .public_key_hash = core_array__core__clone__Clone_for__Array_T__N___clone((size_t)32U, + .public_key_hash = core_array__core__clone__Clone_for__T__N___clone((size_t)32U, &self->public_key_hash, uint8_t, Eurydice_arr_60) @@ -9302,7 +9302,7 @@ static KRML_MUSTINLINE Eurydice_arr_74 serialized_dd_89(const libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *self) { return - libcrux_ml_kem_types_from_fd_d0(serialize_public_key_89(&self->ind_cpa_public_key.t_as_ntt, + libcrux_ml_kem_types_from_51_d0(serialize_public_key_89(&self->ind_cpa_public_key.t_as_ntt, Eurydice_array_to_slice_shared_6e(&self->ind_cpa_public_key.seed_for_A))); } @@ -9747,7 +9747,7 @@ sample_vector_cbd_then_ntt_3b( (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -9964,15 +9964,15 @@ static Eurydice_arr_b9 call_mut_b4_1b(void **_) } /** -This function found in impl {core::ops::function::FnMut<(usize), @Array[TraitClause@0, TraitClause@1], K>> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} +This function found in impl {core::ops::function::FnMut<(usize), [libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, TraitClause@1]; K]> for libcrux_ml_kem::ind_cca::unpacked::transpose_a::closure[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_7b +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.call_mut_22 with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 3 */ -static Eurydice_arr_1d call_mut_7b_1b(void **_) +static Eurydice_arr_1d call_mut_22_1b(void **_) { Eurydice_arr_1d arr_struct; KRML_MAYBE_FOR3(i, @@ -10000,7 +10000,7 @@ static Eurydice_arr_dd transpose_a_1b(Eurydice_arr_dd ind_cpa_a) (size_t)1U, /* original Rust expression is not an lvalue in C */ void *lvalue = (void *)0U; - arr_struct.data[i] = call_mut_7b_1b(&lvalue);); + arr_struct.data[i] = call_mut_22_1b(&lvalue);); Eurydice_arr_dd A = arr_struct; KRML_MAYBE_FOR3(i0, (size_t)0U, @@ -10167,7 +10167,7 @@ sample_ring_element_cbd_3b( (size_t)3U, (size_t)1U, repeat_expression[i] = - core_array__core__clone__Clone_for__Array_T__N___clone((size_t)33U, + core_array__core__clone__Clone_for__T__N___clone((size_t)33U, prf_input, uint8_t, Eurydice_arr_3e0);); @@ -10555,7 +10555,7 @@ libcrux_ml_kem_ind_cca_unpacked_encapsulate_0c( return ( KRML_CLITERAL(tuple_7f){ - .fst = libcrux_ml_kem_types_from_e0_80(ciphertext), + .fst = libcrux_ml_kem_types_from_19_80(ciphertext), .snd = shared_secret_array } ); @@ -10787,7 +10787,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_51( uu____2 = Eurydice_array_to_subslice_from_mut_8c2(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_80(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_80(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_41(Eurydice_array_to_slice_shared_74(&to_hash)); Eurydice_arr_2c @@ -10795,7 +10795,7 @@ libcrux_ml_kem_ind_cca_unpacked_decapsulate_51( encrypt_unpacked_2a(&key_pair->public_key.ind_cpa_public_key, &decrypted, pseudorandomness); - Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_d3_80(ciphertext); + Eurydice_borrow_slice_u8 uu____3 = libcrux_ml_kem_types_as_ref_c1_80(ciphertext); uint8_t selector = libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(uu____3, @@ -11019,10 +11019,10 @@ libcrux_ml_kem_ind_cca_generate_keypair_15(const Eurydice_arr_060 *randomness) serialize_kem_secret_key_d6(Eurydice_array_to_slice_shared_06(&ind_cpa_private_key), Eurydice_array_to_slice_shared_45(&public_key), implicit_rejection_value); - Eurydice_arr_ea private_key = libcrux_ml_kem_types_from_77_28(secret_key_serialized); + Eurydice_arr_ea private_key = libcrux_ml_kem_types_from_b2_28(secret_key_serialized); return libcrux_ml_kem_types_from_17_74(private_key, - libcrux_ml_kem_types_from_fd_d0(public_key)); + libcrux_ml_kem_types_from_51_d0(public_key)); } /** @@ -11156,7 +11156,7 @@ libcrux_ml_kem_ind_cca_encapsulate_ca( encrypt_2a(Eurydice_array_to_slice_shared_45(libcrux_ml_kem_types_as_slice_e6_d0(public_key)), &randomness0, pseudorandomness); - Eurydice_arr_2c uu____2 = libcrux_ml_kem_types_from_e0_80(ciphertext); + Eurydice_arr_2c uu____2 = libcrux_ml_kem_types_from_19_80(ciphertext); return (KRML_CLITERAL(tuple_7f){ .fst = uu____2, .snd = kdf_39_d6(shared_secret) }); } @@ -11263,7 +11263,7 @@ libcrux_ml_kem_ind_cca_decapsulate_62( uu____2 = Eurydice_array_to_subslice_from_mut_8c2(&to_hash, LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE); - Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_d3_80(ciphertext), uint8_t); + Eurydice_slice_copy(uu____2, libcrux_ml_kem_types_as_ref_c1_80(ciphertext), uint8_t); Eurydice_arr_60 implicit_rejection_shared_secret = PRF_4a_41(Eurydice_array_to_slice_shared_74(&to_hash)); Eurydice_arr_2c @@ -11272,7 +11272,7 @@ libcrux_ml_kem_ind_cca_decapsulate_62( uu____3 = Eurydice_array_to_slice_shared_6e(&implicit_rejection_shared_secret); Eurydice_arr_60 implicit_rejection_shared_secret0 = kdf_39_d6(uu____3); Eurydice_arr_60 shared_secret = kdf_39_d6(shared_secret0); - Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_d3_80(ciphertext); + Eurydice_borrow_slice_u8 uu____4 = libcrux_ml_kem_types_as_ref_c1_80(ciphertext); return libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(uu____4, Eurydice_array_to_slice_shared_42(&expected_ciphertext), diff --git a/out/test-libcrux/libcrux_sha3_avx2.c b/out/test-libcrux/libcrux_sha3_avx2.c index 8a20aa77..a430cff7 100644 --- a/out/test-libcrux/libcrux_sha3_avx2.c +++ b/out/test-libcrux/libcrux_sha3_avx2.c @@ -214,7 +214,7 @@ load_block_5b(Eurydice_arr_05 *state, const Eurydice_arr_cd *blocks, size_t offs uint8_t); __m256i u = - mm256_loadu_si256_u8(core_array___Array_T__N___as_slice((size_t)32U, + mm256_loadu_si256_u8(core_array___T__N___as_slice((size_t)32U, &u8s, uint8_t, Eurydice_borrow_slice_u8)); @@ -266,7 +266,7 @@ load_block_5b(Eurydice_arr_05 *state, const Eurydice_arr_cd *blocks, size_t offs uint8_t); __m256i u0 = - mm256_loadu_si256_u8(core_array___Array_T__N___as_slice((size_t)32U, + mm256_loadu_si256_u8(core_array___T__N___as_slice((size_t)32U, &u8s0, uint8_t, Eurydice_borrow_slice_u8)); @@ -2121,7 +2121,7 @@ load_block_3a(Eurydice_arr_05 *state, const Eurydice_arr_cd *blocks, size_t offs uint8_t); __m256i u = - mm256_loadu_si256_u8(core_array___Array_T__N___as_slice((size_t)32U, + mm256_loadu_si256_u8(core_array___T__N___as_slice((size_t)32U, &u8s, uint8_t, Eurydice_borrow_slice_u8)); @@ -2173,7 +2173,7 @@ load_block_3a(Eurydice_arr_05 *state, const Eurydice_arr_cd *blocks, size_t offs uint8_t); __m256i u0 = - mm256_loadu_si256_u8(core_array___Array_T__N___as_slice((size_t)32U, + mm256_loadu_si256_u8(core_array___T__N___as_slice((size_t)32U, &u8s0, uint8_t, Eurydice_borrow_slice_u8)); diff --git a/out/test-slice_array/slice_array.c b/out/test-slice_array/slice_array.c index 8a923c4f..00892e31 100644 --- a/out/test-slice_array/slice_array.c +++ b/out/test-slice_array/slice_array.c @@ -226,7 +226,7 @@ void slice_array_f5_ac(void) /* original Rust expression is not an lvalue in C */ Eurydice_array_u8x4 lvalue = { .data = { 0U } }; Eurydice_borrow_slice_u8 - x2 = core_array___Array_T__N___as_slice((size_t)4U, &lvalue, uint8_t, Eurydice_borrow_slice_u8); + x2 = core_array___T__N___as_slice((size_t)4U, &lvalue, uint8_t, Eurydice_borrow_slice_u8); Eurydice_borrow_slice_u8 uu____0 = x2; Eurydice_array_u8x4 arr; memcpy(arr.data, uu____0.ptr, (size_t)4U * sizeof (uint8_t)); diff --git a/out/test-traits/traits.c b/out/test-traits/traits.c index 8877a87f..7ac43956 100644 --- a/out/test-traits/traits.c +++ b/out/test-traits/traits.c @@ -32,9 +32,9 @@ uint32_t traits_to_int_ac(const traits_Foo *self) } /** -This function found in impl {traits::ToInt for &0 (@Slice)} +This function found in impl {traits::ToInt for &0 ([traits::Foo])} */ -uint32_t traits_to_int_88(const Eurydice_dst_ref_shared_e2 *self) +uint32_t traits_to_int_0f(const Eurydice_dst_ref_shared_e2 *self) { uint32_t uu____0 = traits_to_int_ac(&self->ptr[0U]); return uu____0 * traits_to_int_ac(&self->ptr[1U]); @@ -63,7 +63,7 @@ void traits_main(void) lvalue = array_to_subslice_shared_91(&foos, (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)2U })); - if (!(traits_to_int_88(&lvalue) != 2U)) + if (!(traits_to_int_0f(&lvalue) != 2U)) { return; } diff --git a/out/test-traits/traits.h b/out/test-traits/traits.h index a6ca2ab1..6b49ef6e 100644 --- a/out/test-traits/traits.h +++ b/out/test-traits/traits.h @@ -50,9 +50,9 @@ typedef struct Eurydice_dst_ref_shared_e2_s Eurydice_dst_ref_shared_e2; /** -This function found in impl {traits::ToInt for &0 (@Slice)} +This function found in impl {traits::ToInt for &0 ([traits::Foo])} */ -uint32_t traits_to_int_88(const Eurydice_dst_ref_shared_e2 *self); +uint32_t traits_to_int_0f(const Eurydice_dst_ref_shared_e2 *self); /** A monomorphic instance of Eurydice.arr