Update charon

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
 

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

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 })),

lib/Cleanup2.ml

@@ -1070,10 +1070,10 @@ let bonus_cleanups =
 
     method! visit_lident _ lid =
       match lid with
-      | [ "core"; "slice"; "{@Slice<T>}" ], "len" -> [ "Eurydice" ], "slice_len"
-      | [ "core"; "slice"; "{@Slice<T>}" ], "copy_from_slice" -> [ "Eurydice" ], "slice_copy"
-      | [ "core"; "slice"; "{@Slice<T>}" ], "split_at" -> [ "Eurydice" ], "slice_split_at"
-      | [ "core"; "slice"; "{@Slice<T>}" ], "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<T>}" -> n
+        when impl = "{[T]}" -> n
       | [%cremepat {| core::slice::?impl::len<?>(Eurydice::array_to_slice_mut[#?n]<?>(?)) |}]
-        when impl = "{@Slice<T>}" -> n
-      | [%cremepat {| core::slice::?impl::len<?>(?e) |}] when impl = "{@Slice<T>}" ->
+        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<?t>(?s, ?i) |}] ->
           with_type e.typ

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<U, N>> for @Array<T, N>}" ->
+            | "{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<U>)> for @Array<T, N>}" ->
+            | "{core::cmp::PartialEq<&0 ([U])> for [T; N]}" ->
                 let hd =
                   if !Options.no_const then
                     Builtin.array_eq_slice_mut

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<usize, K>> for array::nested_from_fn::closure<K>}
+This function found in impl {core::ops::function::FnMut<(usize), [usize; K]> for array::nested_from_fn::closure<K>}
 */
 /**
-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<usize, K>> for array::nested_from_fn::closure<K>}
+This function found in impl {core::ops::function::FnOnce<(usize), [usize; K]> for array::nested_from_fn::closure<K>}
 */
 /**
-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;
 }
 

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<usize, K>> for array::nested_from_fn::closure<K>}
+This function found in impl {core::ops::function::FnMut<(usize), [usize; K]> for array::nested_from_fn::closure<K>}
 */
 /**
-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<usize, K>> for array::nested_from_fn::closure<K>}
+This function found in impl {core::ops::function::FnOnce<(usize), [usize; K]> for array::nested_from_fn::closure<K>}
 */
 /**
-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

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<usize, 1usize>> 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<usize, 1usize>> 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;

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<usize, 1usize>> 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<usize, 1usize>> 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