Bump rustc to nightly-2026-05-31

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.208"
+let supported_charon_version = "0.1.209"

charon-ml/src/PrintFmt.ml

@@ -1355,7 +1355,7 @@ and pp_aggregate (env : fmt_env) (agg : aggregate_kind) (fmt : Format.formatter)
 
 and pp_rvalue (env : fmt_env) (fmt : Format.formatter) (rv : rvalue) : unit =
   match rv with
-  | Use op -> pp_operand env fmt op
+  | Use (op, _) -> pp_operand env fmt op
   | RvRef (p, bk, op) -> begin
       let p = place_to_string env p in
       let borrow_kind =

charon-ml/src/generated/Generated_Expressions.ml

@@ -245,7 +245,7 @@ and projection_elem =
     the aggregate kind to operands TODO: we should prefix the type variants with
     "R" or "Rv", this would avoid collisions *)
 and rvalue =
-  | Use of operand  (** Lifts an operand as an rvalue. *)
+  | Use of operand * with_retag  (** Lifts an operand as an rvalue. *)
   | RvRef of place * borrow_kind * operand
       (** Takes a reference to the given place. The [Operand] refers to the init
           value of the metadata, it is [()] if no metadata
@@ -317,6 +317,10 @@ and unop =
   | Neg of overflow_mode  (** This can overflow, for [-i::MIN]. *)
   | Cast of cast_kind
       (** Casts are rvalues in MIR, but we treat them as unops. *)
+
+(** Used for [[Rvalue::Use]] to indicate whether the operand should be retagged
+    (this is used for Rust's aliasing model). *)
+and with_retag = NoRetag | YesRetag
 [@@deriving
   show,
   eq,

charon-ml/src/generated/Generated_OfJson.ml

@@ -1108,9 +1108,10 @@ and region_param_of_json (ctx : of_json_ctx) (js : json) :
 and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("Use", use) ] ->
-        let* use = operand_of_json ctx use in
-        Ok (Use use)
+    | `Assoc [ ("Use", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = operand_of_json ctx x_0 in
+        let* x_1 = with_retag_of_json ctx x_1 in
+        Ok (Use (x_0, x_1))
     | `Assoc
         [
           ( "Ref",
@@ -1546,6 +1547,14 @@ and variant_id_of_json (ctx : of_json_ctx) (js : json) :
     | x -> VariantId.id_of_json ctx x
     | _ -> Error "")
 
+and with_retag_of_json (ctx : of_json_ctx) (js : json) :
+    (with_retag, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `String "No" -> Ok NoRetag
+    | `String "Yes" -> Ok YesRetag
+    | _ -> Error "")
+
 module Ullbc = struct
   open UllbcAst
 

charon-ml/src/generated/Generated_OfPostcard.ml

@@ -1030,7 +1030,8 @@ and rvalue_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
      match __tag with
      | 0 ->
          let* x_0 = operand_of_postcard ctx st in
-         Ok (Use x_0)
+         let* x_1 = with_retag_of_postcard ctx st in
+         Ok (Use (x_0, x_1))
      | 1 ->
          let* place = place_of_postcard ctx st in
          let* kind = borrow_kind_of_postcard ctx st in
@@ -1389,6 +1390,15 @@ and variant_id_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
     (variant_id, string) result =
   combine_error_msgs st __FUNCTION__ (VariantId.id_of_postcard ctx st)
 
+and with_retag_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
+    (with_retag, string) result =
+  combine_error_msgs st __FUNCTION__
+    (let* __tag = int_of_postcard ctx st in
+     match __tag with
+     | 0 -> Ok NoRetag
+     | 1 -> Ok YesRetag
+     | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag))
+
 module Ullbc = struct
   open UllbcAst
 

charon/Cargo.toml

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

charon/rust-toolchain

@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2026-04-18"
+channel = "nightly-2026-05-31"
 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/ctx.rs

@@ -103,7 +103,7 @@ impl<'tcx> PredicateCache<'tcx> {
             return predicates;
         }
         let predicates = compute();
-        let _ = self.values.insert(def_id, predicates.clone());
+        self.values.insert_unique(def_id, predicates.clone());
         predicates
     }
 }

charon/rustc_trait_elaboration/src/elaboration.rs

@@ -242,7 +242,11 @@ impl<'tcx> PredicateSearcher<'tcx> {
         let item_bounds = item_bounds
             .iter_trait_clauses()
             // Substitute the item generics
-            .map(|(_, tref)| EarlyBinder::bind(tref).instantiate(tcx, args))
+            .map(|(_, tref)| {
+                EarlyBinder::bind(tref)
+                    .instantiate(tcx, args)
+                    .skip_normalization()
+            })
             .enumerate();
 
         // Add all the bounds on the corresponding associated item.
@@ -351,7 +355,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
                     .filter_map(|assoc| {
                         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);
+                        let ty = crate::erase_and_norm(tcx, self.typing_env, Unnormalized::new(ty));
                         if let TyKind::Alias(alias_ty) = ty.kind()
                             && alias_ty.kind.def_id() == assoc.def_id
                         {
@@ -489,7 +493,11 @@ impl<'tcx> PredicateSearcher<'tcx> {
         predicates
             .iter_trait_clauses()
             // Substitute the item generics
-            .map(|(_, trait_ref)| EarlyBinder::bind(trait_ref).instantiate(tcx, generics))
+            .map(|(_, trait_ref)| {
+                EarlyBinder::bind(trait_ref)
+                    .instantiate(tcx, generics)
+                    .skip_normalization()
+            })
             // Resolve
             .map(|trait_ref| self.resolve(&trait_ref))
             .collect()

charon/rustc_trait_elaboration/src/item_ref.rs

@@ -77,7 +77,7 @@ impl<'tcx> PredicateSearcher<'tcx> {
         let tcx = self.elab_ctx.tcx;
         let typing_env = self.typing_env;
         // Normalize the generics.
-        let mut generics = normalize(tcx, typing_env, generics);
+        let mut generics = normalize(tcx, typing_env, ty::Unnormalized::new_wip(generics));
 
         if tcx.is_typeck_child(def_id) {
             // Rustc gives closures/inline consts extra generic for inference that we don't care about.
@@ -92,7 +92,9 @@ impl<'tcx> PredicateSearcher<'tcx> {
             let self_pred = self_predicate(tcx, tr_def_id);
             // Substitute to be in the context of the current item.
             let generics = generics.truncate_to(tcx, tcx.generics_of(tr_def_id));
-            let self_pred = ty::EarlyBinder::bind(self_pred).instantiate(tcx, generics);
+            let self_pred = ty::EarlyBinder::bind(self_pred)
+                .instantiate(tcx, generics)
+                .skip_norm_wip();
             let num_trait_req_clauses =
                 ItemPredicates::required_recursively(elab_ctx, tr_def_id).len();
             Some((self.resolve(&self_pred), num_trait_req_clauses))

charon/rustc_trait_elaboration/src/predicates.rs

@@ -390,7 +390,9 @@ impl<'tcx> ItemPredicates<'tcx> {
     /// Substitute all the predicates with these args.
     pub fn instantiate(mut self, tcx: TyCtxt<'tcx>, args: ty::GenericArgsRef<'tcx>) -> Self {
         for predicate in self.iter_mut() {
-            predicate.clause = ty::EarlyBinder::bind(predicate.clause).instantiate(tcx, args);
+            predicate.clause = ty::EarlyBinder::bind(predicate.clause)
+                .instantiate(tcx, args)
+                .skip_norm_wip();
         }
         self
     }

charon/rustc_trait_elaboration/src/utils.rs

@@ -29,20 +29,25 @@
 use rustc_middle::ty::*;
 
 /// Normalize a value.
-pub fn normalize<'tcx, T>(tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, value: T) -> T
+pub fn normalize<'tcx, T>(
+    tcx: TyCtxt<'tcx>,
+    typing_env: TypingEnv<'tcx>,
+    unnormalized: Unnormalized<'tcx, T>,
+) -> T
 where
     T: TypeFoldable<TyCtxt<'tcx>> + Clone,
 {
     use rustc_infer::infer::TyCtxtInferExt;
     use rustc_middle::traits::ObligationCause;
     use rustc_trait_selection::traits::query::normalize::QueryNormalizeExt;
+    let value = unnormalized.clone().skip_normalization();
     let (infcx, param_env) = tcx.infer_ctxt().build_with_typing_env(typing_env);
     infcx
         .at(&ObligationCause::dummy(), param_env)
-        .query_normalize(value.clone())
+        .query_normalize(value)
         // We ignore the generated outlives relations. Unsure what we should do with them.
         .map(|x| x.value)
-        .unwrap_or(value)
+        .unwrap_or(unnormalized.skip_normalization())
 }
 
 /// Erase free regions from the given value. Largely copied from `tcx.erase_and_anonymize_regions`, but also
@@ -92,14 +97,19 @@ where
 
 // Normalize and erase lifetimes, erasing more lifetimes than normal because we might be already
 // inside a binder and rustc doesn't like that.
-pub fn erase_and_norm<'tcx, T>(tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, x: T) -> T
+pub fn erase_and_norm<'tcx, T>(
+    tcx: TyCtxt<'tcx>,
+    typing_env: TypingEnv<'tcx>,
+    x: Unnormalized<'tcx, T>,
+) -> T
 where
     T: TypeFoldable<TyCtxt<'tcx>> + Copy,
 {
+    let fallback = x.skip_normalization();
     erase_free_regions(
         tcx,
         tcx.try_normalize_erasing_regions(typing_env, x)
-            .unwrap_or(x),
+            .unwrap_or(fallback),
     )
 }
 
@@ -115,7 +125,11 @@ pub fn normalize_bound_val<'tcx, T>(
 where
     T: TypeFoldable<TyCtxt<'tcx>> + Copy,
 {
-    Binder::dummy(erase_and_norm(tcx, typing_env, x.skip_binder()))
+    Binder::dummy(erase_and_norm(
+        tcx,
+        typing_env,
+        Unnormalized::new_wip(x.skip_binder()),
+    ))
 }
 
 pub trait ToPolyTraitRef<'tcx> {

charon/src/ast/expressions.rs

@@ -671,6 +671,15 @@ pub struct ConstantExpr {
     pub ty: Ty,
 }
 
+/// Used for [`Rvalue::Use`] to indicate whether the operand should be retagged (this is used
+/// for Rust's aliasing model).
+#[derive(Debug, Hash, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
+#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Retag"))]
+pub enum WithRetag {
+    No,
+    Yes,
+}
+
 /// TODO: we could factor out [Rvalue] and function calls (for LLBC, not ULLBC).
 /// We can also factor out the unops, binops with the function calls.
 /// TODO: move the aggregate kind to operands
@@ -690,7 +699,7 @@ pub struct ConstantExpr {
 )]
 pub enum Rvalue {
     /// Lifts an operand as an rvalue.
-    Use(Operand),
+    Use(Operand, #[drive(skip)] WithRetag),
     /// Takes a reference to the given place.
     /// The `Operand` refers to the init value of the metadata, it is `()` if no metadata
     #[cfg_attr(feature = "charon_on_charon", charon::rename("RvRef"))]

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

@@ -28,7 +28,6 @@ fn run_compiler_with_callbacks(
 fn set_mir_options(config: &mut Config) {
     config.opts.unstable_opts.always_encode_mir = true;
     config.opts.unstable_opts.mir_opt_level = Some(0);
-    config.opts.unstable_opts.mir_emit_retag = true;
     config.opts.unstable_opts.mir_preserve_ub = true;
     let disabled_mir_passes = ["CheckAlignment"];
     for pass in disabled_mir_passes {
@@ -42,12 +41,14 @@ fn set_mir_options(config: &mut Config) {
 
 /// Enable rustc's parallel front-end.
 fn set_parallel_frontend(config: &mut Config) {
-    if config.opts.unstable_opts.threads <= 1 {
+    if config.opts.unstable_opts.threads.is_none_or(|t| t <= 1) {
         // Match rustc's `-Zthreads=0` behavior.
         const RUSTC_MAX_THREADS_CAP: usize = 256;
-        config.opts.unstable_opts.threads = std::thread::available_parallelism()
-            .map_or(1, |n| n.get())
-            .min(RUSTC_MAX_THREADS_CAP);
+        config.opts.unstable_opts.threads = Some(
+            std::thread::available_parallelism()
+                .map_or(1, |n| n.get())
+                .min(RUSTC_MAX_THREADS_CAP),
+        );
     }
 }
 

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

@@ -109,6 +109,7 @@ pub fn eval_ty_constant<'tcx, S: UnderOwnerState<'tcx>>(
         .ok()?
         .ok()?;
     let ty = tcx.type_of(uv.def).instantiate(tcx, uv.args);
+    let ty = normalize(tcx, typing_env, ty);
     Some(ty::Const::new_value(tcx, val, ty))
 }
 
@@ -172,7 +173,7 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
     ty: rustc_middle::ty::Ty<'tcx>,
     span: rustc_span::Span,
 ) -> ConstantExpr {
-    let ty = normalize(s.base().tcx, s.typing_env(), ty);
+    let ty = normalize(s.base().tcx, s.typing_env(), ty::Unnormalized::new_wip(ty));
 
     let kind = match (&*valtree, ty.kind()) {
         (_, ty::Ref(_, inner_ty, _)) => {