Bump rustc to 2026-04-18

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.207"
+let supported_charon_version = "0.1.208"

charon-ml/src/generated/Generated_Meta.ml

@@ -57,6 +57,9 @@ and attribute =
   | AttrVariantsSuffix of string
       (** Same as [VariantsPrefix], but appends to the name instead of
           pre-pending. *)
+  | AttrTransparent
+      (** The structure is treated as a transparent wrapper around its sole
+          field. Written [#[charon::transparent]]. *)
   | AttrDocComment of string  (** A doc-comment such as [/// ...]. *)
   | AttrUnknown of raw_attribute  (** A non-charon-specific attribute. *)
 

charon-ml/src/generated/Generated_OfJson.ml

@@ -1954,6 +1954,7 @@ and attribute_of_json (ctx : of_json_ctx) (js : json) :
     | `Assoc [ ("VariantsSuffix", variants_suffix) ] ->
         let* variants_suffix = string_of_json ctx variants_suffix in
         Ok (AttrVariantsSuffix variants_suffix)
+    | `String "Transparent" -> Ok AttrTransparent
     | `Assoc [ ("DocComment", doc_comment) ] ->
         let* doc_comment = string_of_json ctx doc_comment in
         Ok (AttrDocComment doc_comment)

charon-ml/src/generated/Generated_OfPostcard.ml

@@ -1714,10 +1714,11 @@ and attribute_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
      | 4 ->
          let* x_0 = string_of_postcard ctx st in
          Ok (AttrVariantsSuffix x_0)
-     | 5 ->
+     | 5 -> Ok AttrTransparent
+     | 6 ->
          let* x_0 = string_of_postcard ctx st in
          Ok (AttrDocComment x_0)
-     | 6 ->
+     | 7 ->
          let* x_0 = raw_attribute_of_postcard ctx st in
          Ok (AttrUnknown x_0)
      | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag))

charon/Cargo.toml

@@ -25,7 +25,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] }
 
 [package]
 name = "charon"
-version = "0.1.207"
+version = "0.1.208"
 authors.workspace = true
 edition.workspace = true
 license.workspace = true

charon/rust-toolchain

@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2026-02-22"
+channel = "nightly-2026-04-18"
 components = [ "rustc-dev", "llvm-tools-preview", "rust-src", "miri" ]
 targets = [ "x86_64-unknown-linux-gnu", "x86_64-apple-darwin", "x86_64-pc-windows-msvc", "aarch64-apple-darwin", "i686-unknown-linux-gnu", "powerpc64-unknown-linux-gnu", "riscv64gc-unknown-none-elf" ]

charon/rustc_trait_elaboration/src/elaboration.rs

@@ -120,10 +120,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
         let initial_self_pred = initial_self_pred(tcx, owner_id);
         let mut out = Self {
             elab_ctx,
-            typing_env: TypingEnv {
-                param_env: tcx.param_env(owner_id),
-                typing_mode: TypingMode::PostAnalysis,
-            },
+            typing_env: TypingEnv::new(tcx.param_env(owner_id), TypingMode::PostAnalysis),
             candidates: Default::default(),
             implicit_self_clause: initial_self_pred.is_some(),
             item_refs_cache: Default::default(),
@@ -219,25 +216,32 @@ impl<'tcx> PredicateSearcher<'tcx> {
         let elab_ctx = self.elab_ctx;
         let tcx = self.elab_ctx.tcx;
         // Note: We skip a binder but rebind it just after.
-        let TyKind::Alias(AliasTyKind::Projection, alias_ty) = ty.skip_binder().kind() else {
+        let TyKind::Alias(
+            alias @ ty::AliasTy {
+                kind: AliasTyKind::Projection { def_id, .. },
+                args,
+                ..
+            },
+        ) = ty.skip_binder().kind()
+        else {
             return;
         };
-        let trait_ref = ty.rebind(alias_ty.trait_ref(tcx)).upcast(tcx);
+        let trait_ref = ty.rebind(alias.trait_ref(tcx)).upcast(tcx);
 
         // The predicate we're looking for is is `<T as Trait>::Type: OtherTrait`. We try to solve
         // `T as Trait` and add all the bounds on `Trait::Type` to our context.
         let proof = self.resolve(&trait_ref);
         if matches!(proof.kind, TraitProofKind::Error(_)) {
             return;
         }
-        let item_ref = self.resolve_item_reference(alias_ty.def_id, alias_ty.args, true);
+        let item_ref = self.resolve_item_reference(*def_id, args, true);
 
         // The bounds that hold on the associated type.
-        let item_bounds = ItemPredicates::implied(self.elab_ctx, alias_ty.def_id);
+        let item_bounds = ItemPredicates::implied(self.elab_ctx, *def_id);
         let item_bounds = item_bounds
             .iter_trait_clauses()
             // Substitute the item generics
-            .map(|(_, tref)| EarlyBinder::bind(tref).instantiate(tcx, alias_ty.args))
+            .map(|(_, tref)| EarlyBinder::bind(tref).instantiate(tcx, args))
             .enumerate();
 
         // Add all the bounds on the corresponding associated item.
@@ -345,8 +349,8 @@ impl<'tcx> PredicateSearcher<'tcx> {
                         let ty =
                             Ty::new_projection(tcx, assoc.def_id, erased_tref.skip_binder().args);
                         let ty = crate::erase_and_norm(tcx, self.typing_env, ty);
-                        if let TyKind::Alias(_, alias_ty) = ty.kind()
-                            && alias_ty.def_id == assoc.def_id
+                        if let TyKind::Alias(alias_ty) = ty.kind()
+                            && alias_ty.kind.def_id() == assoc.def_id
                         {
                             // Couldn't normalize the type to anything different than itself;
                             // this must be a built-in associated type such as

charon/rustc_trait_elaboration/src/predicates.rs

@@ -212,10 +212,10 @@ impl<'tcx> ItemPredicates<'tcx> {
             let options = elab_ctx.bounds_options();
             let def_kind = tcx.def_kind(def_id);
             let mut predicates = match def_kind {
-                AssocConst
+                AssocConst { .. }
                 | AssocFn
                 | AssocTy
-                | Const
+                | Const { .. }
                 | Enum
                 | Fn
                 | ForeignTy
@@ -398,6 +398,13 @@ fn inherits_parent_clauses<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> bool {
     use DefKind::*;
     matches!(
         tcx.def_kind(def_id),
-        AnonConst | AssocConst | AssocFn | AssocTy | Closure | Ctor(..) | InlineConst | Variant
+        AnonConst
+            | AssocConst { .. }
+            | AssocFn
+            | AssocTy
+            | Closure
+            | Ctor(..)
+            | InlineConst
+            | Variant
     )
 }

charon/src/ast/meta.rs

@@ -127,6 +127,9 @@ pub enum Attribute {
     VariantsPrefix(String),
     /// Same as `VariantsPrefix`, but appends to the name instead of pre-pending.
     VariantsSuffix(String),
+    /// The structure is treated as a transparent wrapper around its sole field.
+    /// Written `#[charon::transparent]`.
+    Transparent,
     /// A doc-comment such as `/// ...`.
     DocComment(String),
     /// A non-charon-specific attribute.

charon/src/ast/names.rs

@@ -90,6 +90,7 @@ pub enum ImplElem {
     Debug, Default, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut,
 )]
 #[serde(transparent)]
+#[cfg_attr(feature = "charon_on_charon", charon::transparent)]
 pub struct Name {
     pub name: Vec<PathElem>,
 }

charon/src/ast/types/vars.rs

@@ -28,6 +28,7 @@ use crate::{ast::*, impl_from_enum};
     DriveMut,
 )]
 #[serde(transparent)]
+#[cfg_attr(feature = "charon_on_charon", charon::transparent)]
 #[drive(skip)]
 pub struct DeBruijnId {
     pub index: usize,

charon/src/bin/charon-driver/hax/constant_utils/uneval.rs

@@ -42,6 +42,7 @@ pub(crate) fn scalar_int_to_constant_literal<'tcx, S: UnderOwnerState<'tcx>>(
             let v = x.to_bits_unchecked();
             bits_and_type_to_float_constant_literal(v, kind.sinto(s))
         }
+        ty::Pat(inner, _) => scalar_int_to_constant_literal(s, x, *inner),
         _ => {
             let ty_sinto: Ty = ty.sinto(s);
             supposely_unreachable_fatal!(
@@ -133,7 +134,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx>
                 {
                     val.sinto(s)
                 } else {
-                    use rustc_middle::query::Key;
+                    use rustc_middle::query::QueryKey;
                     let span = tcx
                         .def_ident_span(ucv.def)
                         .unwrap_or_else(|| ucv.def.default_span(tcx));
@@ -192,7 +193,7 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
             ConstantExprKind::Literal(ConstantLiteral::byte_str(bytes))
         }
         (ty::ValTreeKind::Branch(fields), ty::Array(..) | ty::Slice(..) | ty::Tuple(..)) => {
-            let fields = fields.iter().copied().map(|field| field.sinto(s)).collect();
+            let fields = fields.iter().map(|field| field.sinto(s)).collect();
             match ty.kind() {
                 ty::Array(..) | ty::Slice(..) => ConstantExprKind::Array { fields },
                 ty::Tuple(_) => ConstantExprKind::Tuple { fields },
@@ -371,9 +372,12 @@ fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>(
                 ConstantExprKind::Literal(lit)
             }
         }
+        ty::Pat(..) => {
+            let op = ecx.project_field(&op, FieldIdx::from_u16(0))?;
+            *op_to_const(s, span, ecx, op)?.contents
+        }
         ty::Dynamic(..)
         | ty::Foreign(..)
-        | ty::Pat(..)
         | ty::UnsafeBinder(..)
         | ty::CoroutineClosure(..)
         | ty::Coroutine(..)

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

@@ -1,6 +1,7 @@
 use crate::hax::prelude::*;
 use rustc_hir::def::DefKind as RDefKind;
 use rustc_middle::{mir, ty};
+use rustc_type_ir::Interner;
 
 pub fn inst_binder<'tcx, T>(
     tcx: ty::TyCtxt<'tcx>,
@@ -88,10 +89,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> HasParamEnv<'tcx> for S {
         }
     }
     fn typing_env(&self) -> ty::TypingEnv<'tcx> {
-        ty::TypingEnv {
-            param_env: self.param_env(),
-            typing_mode: ty::TypingMode::PostAnalysis,
-        }
+        ty::TypingEnv::new(self.param_env(), ty::TypingMode::PostAnalysis)
     }
 }
 
@@ -221,7 +219,9 @@ pub fn assoc_tys_for_trait<'tcx>(
                     tcx.generics_of(assoc.def_id).own_params.is_empty()
                         && tcx.predicates_of(assoc.def_id).predicates.is_empty()
                 })
-                .map(|assoc| ty::AliasTy::new(tcx, assoc.def_id, tref.args)),
+                .map(|assoc| {
+                    ty::AliasTy::new(tcx, tcx.alias_ty_kind_from_def_id(assoc.def_id), tref.args)
+                }),
         );
         for clause in tcx
             .explicit_super_predicates_of(tref.def_id)
@@ -260,7 +260,7 @@ pub fn dyn_self_ty<'tcx>(
         .map(|alias_ty| {
             let proj = ty::ProjectionPredicate {
                 projection_term: alias_ty.into(),
-                term: ty::Ty::new_alias(tcx, ty::Projection, alias_ty).into(),
+                term: ty::Ty::new_alias(tcx, alias_ty).into(),
             };
             let proj = ty::ExistentialProjection::erase_self_ty(tcx, proj);
             ty::Binder::dummy(ty::ExistentialPredicate::Projection(proj))

charon/src/bin/charon-driver/hax/types/def_id.rs

@@ -38,7 +38,9 @@ pub enum DefKind {
     AssocTy,
     TyParam,
     Fn,
-    Const,
+    Const {
+        is_type_const: bool,
+    },
     ConstParam,
     Static {
         safety: Safety,
@@ -47,7 +49,9 @@ pub enum DefKind {
     },
     Ctor(CtorOf, CtorKind),
     AssocFn,
-    AssocConst,
+    AssocConst {
+        is_type_const: bool,
+    },
     Macro(MacroKinds),
     ExternCrate,
     Use,
@@ -267,9 +271,9 @@ impl DefId {
     pub fn visibility<'tcx>(&self, tcx: ty::TyCtxt<'tcx>) -> Option<bool> {
         use DefKind::*;
         match self.kind {
-            AssocConst
+            AssocConst { .. }
             | AssocFn
-            | Const
+            | Const { .. }
             | Enum
             | Field
             | Fn
@@ -393,11 +397,9 @@ pub enum DefPathItem {
     LifetimeNs(Symbol),
     Closure,
     Ctor,
-    LateAnonConst,
     AnonConst,
     #[disable_mapping]
     PromotedConst,
-    DesugaredAnonymousLifetime,
     OpaqueTy,
     OpaqueLifetime(Symbol),
     AnonAssocTy(Symbol),

charon/src/bin/charon-driver/hax/types/mod.rs

@@ -13,7 +13,7 @@ use crate::hax::sinto_todo;
 
 sinto_reexport!(rustc_span::Span);
 
-pub use rustc_span::source_map::Spanned;
+pub use rustc_span::Spanned;
 impl<'s, S: UnderOwnerState<'s>, T: SInto<S, U>, U> SInto<S, Spanned<U>> for Spanned<T> {
     fn sinto<'a>(&self, s: &S) -> Spanned<U> {
         Spanned {

charon/src/bin/charon-driver/hax/types/new/full_def.rs

@@ -1204,7 +1204,7 @@ impl<'tcx> FullDef<'tcx> {
             let tcx = s.base().tcx;
             for impl_def_id in tcx.inherent_impls(rust_def_id) {
                 children.extend(
-                    tcx.associated_items(impl_def_id)
+                    tcx.associated_items(*impl_def_id)
                         .in_definition_order()
                         .filter_map(|assoc| Some((assoc.opt_name()?, assoc.def_id).sinto(s))),
                 );

charon/src/bin/charon-driver/hax/types/new/item_ref.rs

@@ -192,7 +192,7 @@ impl ItemRef {
         let tref = ty::TraitRef::new(tcx, def_id, generics);
         rustc_utils::assoc_tys_for_trait(tcx, typing_env, tref)
             .into_iter()
-            .map(|alias_ty| ty::Ty::new_alias(tcx, ty::Projection, alias_ty))
+            .map(|alias_ty| ty::Ty::new_alias(tcx, alias_ty))
             .map(|ty| normalize(tcx, typing_env, ty))
             .map(|ty| ty.sinto(s))
             .collect()