Merge pull request #1214 from soteria-tools/update-rustc

Bump rustc to 2026-04-18

Author: Nadrieril

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.lock

@@ -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/Cargo.toml

@@ -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/rust-toolchain

@@ -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/elaboration.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/rustc_trait_elaboration/src/predicates.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.