Update hax and rustc

charon/Cargo.toml

@@ -86,7 +86,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] }
 wait-timeout = { version = "0.2.0", optional = true }
 which = "7.0"
 
-hax-frontend-exporter = { git = "https://github.com/cryspen/hax", branch = "main", optional = true }
+hax-frontend-exporter = { git = "https://github.com/AeneasVerif/hax", branch = "main", optional = true }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 

charon/rust-toolchain

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2025-05-26"
+channel = "nightly-2025-06-30"
 components = [ "rustc-dev", "llvm-tools-preview", "rust-src" ]

charon/src/bin/charon-driver/driver.rs

@@ -154,8 +154,11 @@ impl<'a> Callbacks for CharonCallbacks<'a> {
         rustc_hir::def_id::DEF_ID_DEBUG
             .swap(&(def_id_debug as fn(_, &mut fmt::Formatter<'_>) -> _));
 
-        let transform_ctx =
-            translate_crate::translate(&self.options, tcx, compiler.sess.sysroot.clone());
+        let transform_ctx = translate_crate::translate(
+            &self.options,
+            tcx,
+            compiler.sess.opts.sysroot.path().to_owned(),
+        );
         self.transform_ctx = Some(transform_ctx);
         Compilation::Continue
     }

charon/src/bin/charon-driver/translate/translate_closures.rs

@@ -618,6 +618,9 @@ impl ItemTransCtx<'_, '_> {
         let sized_trait = self.get_lang_item(rustc_hir::LangItem::Sized);
         let sized_trait = self.register_trait_decl_id(span, &sized_trait);
 
+        let meta_sized_trait = self.get_lang_item(rustc_hir::LangItem::MetaSized);
+        let meta_sized_trait = self.register_trait_decl_id(span, &meta_sized_trait);
+
         let tuple_trait = self.get_lang_item(rustc_hir::LangItem::Tuple);
         let tuple_trait = self.register_trait_decl_id(span, &tuple_trait);
 
@@ -649,6 +652,7 @@ impl ItemTransCtx<'_, '_> {
 
             match target_kind {
                 ClosureKind::FnOnce => [
+                    builtin_tref(meta_sized_trait, input.clone()),
                     builtin_tref(sized_trait, input.clone()),
                     builtin_tref(tuple_trait, input.clone()),
                     builtin_tref(sized_trait, output.clone()),
@@ -669,6 +673,7 @@ impl ItemTransCtx<'_, '_> {
                         trait_decl_ref: RegionBinder::empty(parent_predicate),
                     };
                     [
+                        builtin_tref(meta_sized_trait, input.clone()),
                         parent_trait_ref,
                         builtin_tref(sized_trait, input.clone()),
                         builtin_tref(tuple_trait, input.clone()),

charon/src/bin/charon-driver/translate/translate_types.rs

@@ -536,13 +536,11 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
                         untagged_variant: translate_variant_id(*untagged_variant),
                     },
                 };
-                offsets
-                    .get(r_abi::FieldIdx::from_usize(*tag_field))
-                    .map(|s| DiscriminantLayout {
-                        offset: r_abi::Size::bytes(*s),
-                        tag_ty,
-                        encoding,
-                    })
+                offsets.get(*tag_field).map(|s| DiscriminantLayout {
+                    offset: r_abi::Size::bytes(*s),
+                    tag_ty,
+                    encoding,
+                })
             }
             r_abi::Variants::Single { .. } | r_abi::Variants::Empty => None,
         };

charon/src/transform/hide_marker_traits.rs

@@ -61,6 +61,9 @@ impl TransformPass for Transform {
         // remove.
         let exclude: &[_] = if ctx.options.hide_marker_traits {
             &[
+                "core::marker::Destruct",
+                "core::marker::PointeeSized",
+                "core::marker::MetaSized",
                 "core::marker::Sized",
                 "core::marker::Tuple",
                 "core::marker::Send",

charon/tests/cargo/dependencies.out

@@ -6,21 +6,32 @@ pub opaque type Arguments<'a>
 where
     'a : 'a,
 
+// Full name: core::marker::MetaSized
+#[lang_item("meta_sized")]
+pub trait MetaSized<Self>
+
 // Full name: core::marker::Sized
 #[lang_item("sized")]
 pub trait Sized<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+}
 
 // Full name: core::marker::Tuple
 #[lang_item("tuple_trait")]
 pub trait Tuple<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+}
 
 // Full name: core::ops::function::FnOnce
 #[lang_item("fn_once")]
 pub trait FnOnce<Self, Args>
 {
-    parent_clause0 : [@TraitClause0]: Sized<Args>
-    parent_clause1 : [@TraitClause1]: Tuple<Args>
-    parent_clause2 : [@TraitClause2]: Sized<Self::Output>
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: Sized<Args>
+    parent_clause2 : [@TraitClause2]: Tuple<Args>
+    parent_clause3 : [@TraitClause3]: Sized<Self::Output>
     type Output
     fn call_once = core::ops::function::FnOnce::call_once<Self, Args>[Self]
 }
@@ -80,9 +91,10 @@ fn {impl FnOnce<(u32)> for closure}::call_once(@1: closure, @2: (u32)) -> u32
 
 // Full name: test_cargo_dependencies::main::silly_incr::{impl FnOnce<(u32)> for closure}
 impl FnOnce<(u32)> for closure {
-    parent_clause0 = Sized<(u32)>
-    parent_clause1 = Tuple<(u32)>
-    parent_clause2 = Sized<u32>
+    parent_clause0 = MetaSized<(u32)>
+    parent_clause1 = Sized<(u32)>
+    parent_clause2 = Tuple<(u32)>
+    parent_clause3 = Sized<u32>
     type Output = u32
     fn call_once = {impl FnOnce<(u32)> for closure}::call_once
 }

charon/tests/cargo/toml.out

@@ -1,8 +1,15 @@
 # Final LLBC before serialization:
 
+// Full name: core::marker::MetaSized
+#[lang_item("meta_sized")]
+pub trait MetaSized<Self>
+
 // Full name: core::marker::Sized
 #[lang_item("sized")]
 pub trait Sized<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+}
 
 // Full name: core::option::Option
 #[lang_item("Option")]

charon/tests/crate_data.rs

@@ -179,6 +179,7 @@ fn predicate_origins() -> anyhow::Result<()> {
         (
             "test_crate::Trait",
             vec![
+                (WhereClauseOnTrait, "MetaSized"),
                 (WhereClauseOnTrait, "Clone"),
                 (WhereClauseOnTrait, "Sized"),
                 (WhereClauseOnTrait, "Copy"),
@@ -306,11 +307,7 @@ fn attributes() -> anyhow::Result<()> {
         unknown_attrs(&crate_data.global_decls[1].item_meta),
         vec!["clippy::foo"]
     );
-    // We don't parse that attribute ourselves, we let rustc do it.
-    assert_eq!(
-        unknown_attrs(&crate_data.fun_decls[0].item_meta),
-        vec!["inline(never)"]
-    );
+    assert!(unknown_attrs(&crate_data.fun_decls[0].item_meta).is_empty());
     assert_eq!(
         crate_data.fun_decls[0].item_meta.attr_info.inline,
         Some(InlineAttr::Never)
@@ -588,7 +585,7 @@ fn declaration_groups() -> anyhow::Result<()> {
     // There are two function items: one for `foo`, one for the initializer of `Trait::FOO`.
     assert_eq!(crate_data.fun_decls.iter().count(), 2);
     let decl_groups = crate_data.ordered_decls.unwrap();
-    assert_eq!(decl_groups.len(), 5);
+    assert_eq!(decl_groups.len(), 6);
 
     Ok(())
 }
@@ -615,7 +612,7 @@ fn source_text() -> anyhow::Result<()> {
 
     let sources = crate_data
         .all_items()
-        .map(|i| i.item_meta().source_text.as_ref().unwrap())
+        .filter_map(|i| i.item_meta().source_text.as_ref())
         .collect_vec();
     assert_eq!(sources[0], "struct Foo { x: usize }");
     assert_eq!(

charon/tests/ui/arrays.out

@@ -1,15 +1,25 @@
 # Final LLBC before serialization:
 
+// Full name: core::marker::MetaSized
+#[lang_item("meta_sized")]
+pub trait MetaSized<Self>
+
 // Full name: core::ops::index::Index
 #[lang_item("index")]
 pub trait Index<Self, Idx, Self_Output>
 {
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: MetaSized<Idx>
+    parent_clause2 : [@TraitClause2]: MetaSized<Self_Output>
     fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx, Self_Output>[Self]
 }
 
 // Full name: core::marker::Sized
 #[lang_item("sized")]
 pub trait Sized<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+}
 
 // Full name: core::array::{impl Index<I, Clause2_Output> for Array<T, const N : usize>}::index
 pub fn {impl Index<I, Clause2_Output> for Array<T, const N : usize>}::index<'_0, T, I, Clause2_Output, const N : usize>(@1: &'_0 (Array<T, const N : usize>), @2: I) -> &'_0 (Clause2_Output)
@@ -25,42 +35,49 @@ where
     [@TraitClause1]: Sized<I>,
     [@TraitClause2]: Index<Slice<T>, I, Clause2_Output>,
 {
+    parent_clause0 = MetaSized<Array<T, const N : usize>>
+    parent_clause1 = @TraitClause1::parent_clause0
+    parent_clause2 = @TraitClause2::parent_clause2
     fn index<'_0> = {impl Index<I, Clause2_Output> for Array<T, const N : usize>}::index<'_0_0, T, I, Clause2_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2]
 }
 
 // Full name: core::ops::index::IndexMut
 #[lang_item("index_mut")]
-pub trait IndexMut<Self, Idx, Self_Clause0_Output>
+pub trait IndexMut<Self, Idx, Self_Clause1_Output>
 {
-    parent_clause0 : [@TraitClause0]: Index<Self, Idx, Self_Clause0_Output>
-    fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx, Self_Clause0_Output>[Self]
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: Index<Self, Idx, Self_Clause1_Output>
+    parent_clause2 : [@TraitClause2]: MetaSized<Idx>
+    fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx, Self_Clause1_Output>[Self]
 }
 
-// Full name: core::array::{impl IndexMut<I, Clause2_Clause0_Output> for Array<T, const N : usize>}::index_mut
-pub fn {impl IndexMut<I, Clause2_Clause0_Output> for Array<T, const N : usize>}::index_mut<'_0, T, I, Clause2_Clause0_Output, const N : usize>(@1: &'_0 mut (Array<T, const N : usize>), @2: I) -> &'_0 mut (Clause2_Clause0_Output)
+// Full name: core::array::{impl IndexMut<I, Clause2_Clause1_Output> for Array<T, const N : usize>}::index_mut
+pub fn {impl IndexMut<I, Clause2_Clause1_Output> for Array<T, const N : usize>}::index_mut<'_0, T, I, Clause2_Clause1_Output, const N : usize>(@1: &'_0 mut (Array<T, const N : usize>), @2: I) -> &'_0 mut (Clause2_Clause1_Output)
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Sized<I>,
-    [@TraitClause2]: IndexMut<Slice<T>, I, Clause2_Clause0_Output>,
+    [@TraitClause2]: IndexMut<Slice<T>, I, Clause2_Clause1_Output>,
 
-// Full name: core::array::{impl IndexMut<I, Clause2_Clause0_Output> for Array<T, const N : usize>}
-impl<T, I, Clause2_Clause0_Output, const N : usize> IndexMut<I, Clause2_Clause0_Output> for Array<T, const N : usize>
+// Full name: core::array::{impl IndexMut<I, Clause2_Clause1_Output> for Array<T, const N : usize>}
+impl<T, I, Clause2_Clause1_Output, const N : usize> IndexMut<I, Clause2_Clause1_Output> for Array<T, const N : usize>
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Sized<I>,
-    [@TraitClause2]: IndexMut<Slice<T>, I, Clause2_Clause0_Output>,
+    [@TraitClause2]: IndexMut<Slice<T>, I, Clause2_Clause1_Output>,
 {
-    parent_clause0 = {impl Index<I, Clause2_Output> for Array<T, const N : usize>}<T, I, Clause2_Clause0_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2::parent_clause0]
-    fn index_mut<'_0> = {impl IndexMut<I, Clause2_Clause0_Output> for Array<T, const N : usize>}::index_mut<'_0_0, T, I, Clause2_Clause0_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2]
+    parent_clause0 = MetaSized<Array<T, const N : usize>>
+    parent_clause1 = {impl Index<I, Clause2_Output> for Array<T, const N : usize>}<T, I, Clause2_Clause1_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2::parent_clause1]
+    parent_clause2 = @TraitClause1::parent_clause0
+    fn index_mut<'_0> = {impl IndexMut<I, Clause2_Clause1_Output> for Array<T, const N : usize>}::index_mut<'_0_0, T, I, Clause2_Clause1_Output, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2]
 }
 
 pub fn core::ops::index::Index::index<'_0, Self, Idx, Clause0_Output>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Clause0_Output)
 where
     [@TraitClause0]: Index<Self, Idx, Clause0_Output>,
 
-pub fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx, Clause0_Clause0_Output>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut (Clause0_Clause0_Output)
+pub fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx, Clause0_Clause1_Output>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut (Clause0_Clause1_Output)
 where
-    [@TraitClause0]: IndexMut<Self, Idx, Clause0_Clause0_Output>,
+    [@TraitClause0]: IndexMut<Self, Idx, Clause0_Clause1_Output>,
 
 // Full name: core::ops::range::Range
 #[lang_item("Range")]
@@ -84,12 +101,18 @@ where
 
 // Full name: core::slice::index::private_slice_index::Sealed
 pub trait Sealed<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+}
 
 // Full name: core::slice::index::SliceIndex
 #[lang_item("SliceIndex")]
 pub trait SliceIndex<Self, T, Self_Output>
 {
-    parent_clause0 : [@TraitClause0]: Sealed<Self>
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: Sealed<Self>
+    parent_clause2 : [@TraitClause2]: MetaSized<T>
+    parent_clause3 : [@TraitClause3]: MetaSized<Self_Output>
     fn get<'_0> = core::slice::index::SliceIndex::get<'_0_0, Self, T, Self_Output>[Self]
     fn get_mut<'_0> = core::slice::index::SliceIndex::get_mut<'_0_0, Self, T, Self_Output>[Self]
     fn get_unchecked = core::slice::index::SliceIndex::get_unchecked<Self, T, Self_Output>[Self]
@@ -112,6 +135,9 @@ where
     [@TraitClause1]: Sized<I>,
     [@TraitClause2]: SliceIndex<I, Slice<T>, Clause2_Output>,
 {
+    parent_clause0 = MetaSized<Slice<T>>
+    parent_clause1 = @TraitClause1::parent_clause0
+    parent_clause2 = @TraitClause2::parent_clause3
     fn index<'_0> = {impl Index<I, Clause2_Output> for Slice<T>}::index<'_0_0, T, I, Clause2_Output>[@TraitClause0, @TraitClause1, @TraitClause2]
 }
 
@@ -129,12 +155,16 @@ where
     [@TraitClause1]: Sized<I>,
     [@TraitClause2]: SliceIndex<I, Slice<T>, Clause2_Output>,
 {
-    parent_clause0 = {impl Index<I, Clause2_Output> for Slice<T>}<T, I, Clause2_Output>[@TraitClause0, @TraitClause1, @TraitClause2]
+    parent_clause0 = MetaSized<Slice<T>>
+    parent_clause1 = {impl Index<I, Clause2_Output> for Slice<T>}<T, I, Clause2_Output>[@TraitClause0, @TraitClause1, @TraitClause2]
+    parent_clause2 = @TraitClause1::parent_clause0
     fn index_mut<'_0> = {impl IndexMut<I, Clause2_Output> for Slice<T>}::index_mut<'_0_0, T, I, Clause2_Output>[@TraitClause0, @TraitClause1, @TraitClause2]
 }
 
 // Full name: core::slice::index::private_slice_index::{impl Sealed for Range<usize>[Sized<usize>]}
-impl Sealed for Range<usize>[Sized<usize>] {}
+impl Sealed for Range<usize>[Sized<usize>] {
+    parent_clause0 = MetaSized<Range<usize>[Sized<usize>]>
+}
 
 pub fn core::slice::index::SliceIndex::get<'_0, Self, T, Clause0_Output>(@1: Self, @2: &'_0 (T)) -> Option<&'_0 (Clause0_Output)>[Sized<&'_0 (Clause0_Output)>]
 where
@@ -195,7 +225,10 @@ impl<T> SliceIndex<Slice<T>, Slice<T>> for Range<usize>[Sized<usize>]
 where
     [@TraitClause0]: Sized<T>,
 {
-    parent_clause0 = {impl Sealed for Range<usize>[Sized<usize>]}
+    parent_clause0 = MetaSized<Range<usize>[Sized<usize>]>
+    parent_clause1 = {impl Sealed for Range<usize>[Sized<usize>]}
+    parent_clause2 = MetaSized<Slice<T>>
+    parent_clause3 = MetaSized<Slice<T>>
     fn get<'_0> = {impl SliceIndex<Slice<T>, Slice<T>> for Range<usize>[Sized<usize>]}::get<'_0_0, T>[@TraitClause0]
     fn get_mut<'_0> = {impl SliceIndex<Slice<T>, Slice<T>> for Range<usize>[Sized<usize>]}::get_mut<'_0_0, T>[@TraitClause0]
     fn get_unchecked = {impl SliceIndex<Slice<T>, Slice<T>> for Range<usize>[Sized<usize>]}::get_unchecked<T>[@TraitClause0]
@@ -653,7 +686,7 @@ pub fn array_subslice_mut_<'_0>(@1: &'_0 mut (Array<u32, 32 : usize>), @2: usize
     @8 := Range { start: move (@9), end: move (@10) }
     storage_dead(@10)
     storage_dead(@9)
-    @6 := {impl IndexMut<I, Clause2_Clause0_Output> for Array<T, const N : usize>}::index_mut<'_, u32, Range<usize>[Sized<usize>], Slice<u32>, 32 : usize>[Sized<u32>, Sized<Range<usize>[Sized<usize>]>, {impl IndexMut<I, Clause2_Output> for Slice<T>}<u32, Range<usize>[Sized<usize>], Slice<u32>>[Sized<u32>, Sized<Range<usize>[Sized<usize>]>, {impl SliceIndex<Slice<T>, Slice<T>> for Range<usize>[Sized<usize>]}<u32>[Sized<u32>]]](move (@7), move (@8))
+    @6 := {impl IndexMut<I, Clause2_Clause1_Output> for Array<T, const N : usize>}::index_mut<'_, u32, Range<usize>[Sized<usize>], Slice<u32>, 32 : usize>[Sized<u32>, Sized<Range<usize>[Sized<usize>]>, {impl IndexMut<I, Clause2_Output> for Slice<T>}<u32, Range<usize>[Sized<usize>], Slice<u32>>[Sized<u32>, Sized<Range<usize>[Sized<usize>]>, {impl SliceIndex<Slice<T>, Slice<T>> for Range<usize>[Sized<usize>]}<u32>[Sized<u32>]]](move (@7), move (@8))
     storage_dead(@8)
     storage_dead(@7)
     @5 := &mut *(@6)
@@ -1363,7 +1396,7 @@ pub fn range_all()
     @6 := &mut x@1
     storage_live(@7)
     @7 := Range { start: const (1 : usize), end: const (3 : usize) }
-    @5 := {impl IndexMut<I, Clause2_Clause0_Output> for Array<T, const N : usize>}::index_mut<'_, u32, Range<usize>[Sized<usize>], Slice<u32>, 4 : usize>[Sized<u32>, Sized<Range<usize>[Sized<usize>]>, {impl IndexMut<I, Clause2_Output> for Slice<T>}<u32, Range<usize>[Sized<usize>], Slice<u32>>[Sized<u32>, Sized<Range<usize>[Sized<usize>]>, {impl SliceIndex<Slice<T>, Slice<T>> for Range<usize>[Sized<usize>]}<u32>[Sized<u32>]]](move (@6), move (@7))
+    @5 := {impl IndexMut<I, Clause2_Clause1_Output> for Array<T, const N : usize>}::index_mut<'_, u32, Range<usize>[Sized<usize>], Slice<u32>, 4 : usize>[Sized<u32>, Sized<Range<usize>[Sized<usize>]>, {impl IndexMut<I, Clause2_Output> for Slice<T>}<u32, Range<usize>[Sized<usize>], Slice<u32>>[Sized<u32>, Sized<Range<usize>[Sized<usize>]>, {impl SliceIndex<Slice<T>, Slice<T>> for Range<usize>[Sized<usize>]}<u32>[Sized<u32>]]](move (@6), move (@7))
     storage_dead(@7)
     storage_dead(@6)
     @4 := &mut *(@5)