Update to nightly-2025-10-01

creusot/src/analysis.rs

@@ -514,7 +514,7 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
                 | Ref(_, _, _)
                 | FnDef(_, _)
                 | FnPtr(..)
-                | Dynamic(_, _, _)
+                | Dynamic(_, _)
                 | CoroutineClosure(_, _)
                 | Coroutine(_, _)
                 | CoroutineWitness(_, _)

creusot/src/backend.rs

@@ -2,7 +2,7 @@ use crate::{
     contracts_items::{is_spec, is_trusted},
     ctx::{HasTyCtxt, ItemType, TranslatedItem, TranslationCtx},
     naming::ModulePath,
-    util::path_of_span,
+    util::{impl_subject, path_of_span},
 };
 use creusot_args::options::SpanMode;
 use indexmap::IndexMap;
@@ -165,7 +165,7 @@ impl<'tcx> Why3Generator<'tcx> {
             let parent_id = key.parent?; // The last segment is CrateRoot. Skip it.
 
             if key.disambiguated_data.data == rustc_hir::definitions::DefPathData::Impl {
-                return Some(display_impl_subject(&tcx.impl_subject(id).skip_binder()));
+                return Some(display_impl_subject(tcx, id));
             }
             id.index = parent_id;
         }
@@ -182,10 +182,10 @@ impl<'tcx> HasTyCtxt<'tcx> for Why3Generator<'tcx> {
     }
 }
 
-fn display_impl_subject(i: &rustc_middle::ty::ImplSubject<'_>) -> String {
-    match i {
-        rustc_middle::ty::ImplSubject::Trait(trait_ref) => trait_ref.to_string(),
-        rustc_middle::ty::ImplSubject::Inherent(ty) => ty.to_string(),
+fn display_impl_subject(tcx: TyCtxt, id: DefId) -> String {
+    match impl_subject(tcx, id) {
+        Ok(trait_ref) => trait_ref.to_string(),
+        Err(ty) => ty.to_string(),
     }
 }
 

creusot/src/backend/clone_map.rs

@@ -170,12 +170,12 @@ pub(crate) trait Namer<'tcx> {
             .without_search_path()
     }
 
-    // TODO: get rid of this. `erase_regions` should be the responsibility of the callers.
+    // TODO: get rid of this. `erase_and_anonymize_regions` should be the responsibility of the callers.
     // NOTE: should `Namer::ty()` be asserting with `has_erasable_regions` instead?
     fn raw_dependency(&self, dep: Dependency<'tcx>) -> &Kind;
 
     fn dependency(&self, dep: Dependency<'tcx>) -> &Kind {
-        self.raw_dependency(dep.erase_regions(self.tcx()))
+        self.raw_dependency(dep.erase_and_anonymize_regions(self.tcx()))
     }
 
     fn resolve_dependency(&self, dep: Dependency<'tcx>) -> Dependency<'tcx> {

creusot/src/backend/clone_map/elaborator.rs

@@ -452,7 +452,7 @@ fn expand_type<'tcx>(
             translate_tydecl(ctx, &names, (def_id, subst), typing_env)
         }
         TyKind::Tuple(_) => translate_tuple_ty(ctx, &names, ty),
-        TyKind::Dynamic(traits, _, _) => {
+        TyKind::Dynamic(traits, _) => {
             if is_logically_dyn_compatible(ctx.tcx(), traits.iter()) {
                 vec![Decl::TyDecl(TyDecl::Opaque {
                     ty_name: names.ty(ty).to_ident(),

creusot/src/backend/dependency.rs

@@ -47,8 +47,8 @@ impl<'tcx> Dependency<'tcx> {
     }
 
     // FIXME: this function should not be necessary, dependencies should not be created non-normalized
-    pub(crate) fn erase_regions(self, tcx: TyCtxt<'tcx>) -> Self {
-        tcx.erase_regions(self)
+    pub(crate) fn erase_and_anonymize_regions(self, tcx: TyCtxt<'tcx>) -> Self {
+        tcx.erase_and_anonymize_regions(self)
     }
 
     pub(crate) fn base_ident(self, ctx: &TranslationCtx<'tcx>) -> Option<Symbol> {
@@ -74,7 +74,7 @@ impl<'tcx> Dependency<'tcx> {
                         .replace(|c: char| !(c.is_ascii_alphanumeric() || c == '\''), "_"),
                 ))),
                 TyKind::Tuple(_) => Some(Symbol::intern("tuple")),
-                TyKind::Dynamic(_, _, _) => {
+                TyKind::Dynamic(_, _) => {
                     Some(Symbol::intern(&type_string(ctx.tcx, String::new(), ty)))
                 }
                 _ => None,
@@ -193,7 +193,7 @@ fn type_string_walk(tcx: TyCtxt, prefix: &mut String, ty: Ty) {
             None => push_(prefix, "x"),
             Some(name) => push_(prefix, &to_alphanumeric(name.as_str())),
         },
-        Dynamic(traits, _, _) => {
+        Dynamic(traits, _) => {
             prefix.push_str("dyn");
             for tr in traits.iter() {
                 let ty::ExistentialPredicate::Trait(tr) = tr.skip_binder() else { continue };

creusot/src/backend/optimization/constant_propagation.rs

@@ -139,7 +139,6 @@ impl<'tcx> LocalUsage<'_, 'tcx> {
             RValue::Constructor(_, _, es) => es.iter().for_each(|e| self.visit_operand(e)),
             RValue::Cast(e, _, _) => self.visit_operand(e),
             RValue::Tuple(es) => es.iter().for_each(|e| self.visit_operand(e)),
-            RValue::Len(e) => self.visit_operand(e),
             RValue::Array(es) => es.iter().for_each(|e| self.visit_operand(e)),
             RValue::Repeat(l, r) => {
                 self.visit_operand(l);
@@ -327,7 +326,6 @@ impl<'tcx> SimplePropagator<'tcx> {
             RValue::Constructor(_, _, es) => es.iter_mut().for_each(|e| self.visit_operand(e)),
             RValue::Cast(e, _, _) => self.visit_operand(e),
             RValue::Tuple(es) => es.iter_mut().for_each(|e| self.visit_operand(e)),
-            RValue::Len(e) => self.visit_operand(e),
             RValue::Array(es) => es.iter_mut().for_each(|e| self.visit_operand(e)),
             RValue::Repeat(l, r) => {
                 self.visit_operand(l);

creusot/src/backend/program.rs

@@ -51,7 +51,7 @@ use rustc_middle::{
     ty::{self, AdtDef, GenericArgs, GenericArgsRef, Ty, TyCtxt, TyKind},
 };
 use rustc_span::{DUMMY_SP, Span};
-use rustc_type_ir::{DynKind, IntTy};
+use rustc_type_ir::IntTy;
 use std::{collections::HashMap, fmt::Debug, iter::once};
 use why3::{
     Ident, Name,
@@ -739,7 +739,7 @@ impl<'tcx> RValue<'tcx> {
             RValue::Cast(e, source, target)
                 if let Some(source) = source.builtin_deref(false)
                     && let Some(target) = target.builtin_deref(false)
-                    && let TyKind::Dynamic(_, _, _) = target.kind() =>
+                    && let TyKind::Dynamic(_, _) = target.kind() =>
             {
                 let cast = lower.names.dyn_cast(source, target);
                 Exp::var(cast).app(vec![e.into_why(lower, istmts)])
@@ -818,8 +818,6 @@ impl<'tcx> RValue<'tcx> {
                     _ => unsupported_cast(lower.ctx, span, source, target),
                 }
             }
-            RValue::Len(op) => Exp::qvar(lower.names.in_pre(PreMod::Slice, "length"))
-                .app([op.into_why(lower, istmts)]),
             RValue::Array(fields) => {
                 let id = Ident::fresh_local("__arr_temp");
                 let ty = lower.ty(ty);
@@ -1435,5 +1433,5 @@ pub fn ptr_cast_kind<'tcx>(
 /// If `true`, this is definitely an unsized type, so pointers to it must be fat.
 /// If `false`, nothing is known for sure.
 pub fn is_unsized(ty: &Ty) -> bool {
-    matches!(ty.kind(), TyKind::Str | TyKind::Slice(_) | TyKind::Dynamic(_, _, DynKind::Dyn))
+    matches!(ty.kind(), TyKind::Str | TyKind::Slice(_) | TyKind::Dynamic(_, _))
 }

creusot/src/backend/ty.rs

@@ -74,7 +74,7 @@ pub(crate) fn translate_ty<'tcx, N: Namer<'tcx>>(
         | Adt(..)
         | Tuple(_)
         | Param(_)
-        | Dynamic(_, _, _)
+        | Dynamic(_, _)
         | Alias(AliasTyKind::Opaque | AliasTyKind::Projection, _) => {
             MlT::TConstructor(names.ty(ty))
         }

creusot/src/backend/ty_inv.rs

@@ -76,7 +76,7 @@ pub(crate) fn is_tyinv_trivial<'tcx>(
             | TyKind::FnDef(_, _)
             | TyKind::FnPtr(..)
             | TyKind::RawPtr(_, _)
-            | TyKind::Dynamic(_, _, _) => (),
+            | TyKind::Dynamic(_, _) => (),
             _ => ctx.dcx().span_fatal(span, format!("Unsupported type: {ty}")),
         }
     }

creusot/src/callbacks.rs

@@ -118,7 +118,7 @@ impl Callbacks for ToWhy {
 fn mir_borrowck<'tcx, 'a>(
     tcx: TyCtxt<'tcx>,
     def_id: LocalDefId,
-) -> Result<&'a mir::ConcreteOpaqueTypes<'tcx>, ErrorGuaranteed> {
+) -> Result<&'a mir::DefinitionSiteHiddenTypes<'tcx>, ErrorGuaranteed> {
     let opts = ConsumerOptions::RegionInferenceContext;
     let bodies_with_facts =
         rustc_borrowck::consumers::get_bodies_with_borrowck_facts(tcx, def_id, opts);

creusot/src/naming.rs

@@ -7,7 +7,7 @@ use rustc_middle::ty::TyCtxt;
 use rustc_span::Symbol;
 use std::{iter::once, path::PathBuf};
 
-use crate::very_stable_hash::get_very_stable_hash;
+use crate::{util::impl_subject, very_stable_hash::get_very_stable_hash};
 
 // TODO: clean up this module. There are a bunch of redundancies.
 //
@@ -191,9 +191,8 @@ fn ident_path_segments_(tcx: TyCtxt, def_id: DefId) -> Vec<Segment> {
             Some(parent_id) => parent_id,
         };
         match key.disambiguated_data.data {
-            DefPathData::Impl => {
-                segs.push(Segment::Impl(get_very_stable_hash(&tcx.impl_subject(id), &tcx).as_u64()))
-            }
+            DefPathData::Impl => segs
+                .push(Segment::Impl(get_very_stable_hash(&impl_subject(tcx, id), &tcx).as_u64())),
             _ => segs.push(Segment::Other(key.disambiguated_data)),
         }
         id.index = parent_id;

creusot/src/translation/fmir.rs

@@ -139,7 +139,6 @@ pub enum RValue<'tcx> {
     Constructor(DefId, GenericArgsRef<'tcx>, Box<[Operand<'tcx>]>),
     Cast(Operand<'tcx>, Ty<'tcx>, Ty<'tcx>),
     Tuple(Box<[Operand<'tcx>]>),
-    Len(Operand<'tcx>),
     Array(Box<[Operand<'tcx>]>),
     Repeat(Operand<'tcx>, Operand<'tcx>),
     Ptr(Place<'tcx>),
@@ -189,7 +188,6 @@ impl RValue<'_> {
             RValue::Constructor(_, _, _) => true,
             RValue::Cast(_, _, _) => false,
             RValue::Tuple(_) => true,
-            RValue::Len(_) => true,
             RValue::Array(_) => true,
             RValue::Repeat(_, _) => true,
             RValue::Snapshot(_) => true,
@@ -721,9 +719,6 @@ pub(crate) fn super_visit_rvalue<'tcx, V: FmirVisitor<'tcx>>(visitor: &mut V, rv
                 visitor.visit_operand(op);
             }
         }
-        RValue::Len(op) => {
-            visitor.visit_operand(op);
-        }
         RValue::Array(ops) => {
             for op in ops {
                 visitor.visit_operand(op);

creusot/src/translation/function/statement.rs

@@ -155,10 +155,6 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                     ),
                 }
             }
-            &Rvalue::Len(pl) => {
-                let e = Operand::Copy(self.translate_place(pl, span));
-                RValue::Len(e)
-            }
             Rvalue::Cast(CastKind::IntToInt | CastKind::PtrToPtr, op, cast_ty) => {
                 let op_ty = op.ty(self.body, self.tcx());
                 RValue::Cast(self.translate_operand(op, span), op_ty, *cast_ty)

creusot/src/translation/specification.rs

@@ -217,7 +217,7 @@ pub(crate) fn inherited_extern_spec<'tcx>(
 
         let assoc = ctx.opt_associated_item(def_id)?;
         let trait_ref = ctx.impl_trait_ref(assoc.container_id(ctx.tcx))?;
-        let id = assoc.trait_item_def_id?;
+        let id = assoc.trait_item_def_id()?;
 
         if ctx.extern_spec(id).is_none() {
             return None;

creusot/src/translation/traits.rs

@@ -169,7 +169,7 @@ pub(crate) fn evaluate_additional_predicates<'tcx>(
 ) -> Result<(), Vec<FulfillmentError<'tcx>>> {
     let mut fulfill_cx = <dyn TraitEngine<'tcx, _>>::new(infcx);
     for predicate in p {
-        let predicate = infcx.tcx.erase_regions(predicate);
+        let predicate = infcx.tcx.erase_and_anonymize_regions(predicate);
         let cause = ObligationCause::dummy_with_span(sp);
         let obligation = Obligation { cause, param_env, recursion_depth: 0, predicate };
         fulfill_cx.register_predicate_obligation(infcx, obligation);
@@ -326,7 +326,7 @@ impl<'tcx> TraitResolved<'tcx> {
                 );
                 let substs = substs.rebase_onto(tcx, trait_ref.def_id, args);
 
-                let leaf_substs = tcx.erase_regions(substs);
+                let leaf_substs = tcx.erase_and_anonymize_regions(substs);
 
                 TraitResolved::Instance {
                     def: (leaf_def.item.def_id, leaf_substs),
@@ -348,7 +348,7 @@ impl<'tcx> TraitResolved<'tcx> {
                 TraitResolved::UnknownFound
             }
             ImplSource::Builtin(_, _) => {
-                if matches!(substs.type_at(0).kind(), rustc_middle::ty::Dynamic(_, _, _)) {
+                if matches!(substs.type_at(0).kind(), rustc_middle::ty::Dynamic(_, _)) {
                     // These types are not supported, but we want to display a proper error message because
                     // they are rather common in real Rust code, and this is not the right place to emit
                     // such an error message.

creusot/src/util.rs

@@ -18,7 +18,7 @@ use rustc_span::{Span, Symbol};
 use creusot_args::options::SpanMode;
 
 pub(crate) fn erased_identity_for_item(tcx: TyCtxt, did: DefId) -> GenericArgsRef {
-    tcx.erase_regions(GenericArgs::identity_for_item(tcx, did))
+    tcx.erase_and_anonymize_regions(GenericArgs::identity_for_item(tcx, did))
 }
 
 pub(crate) fn parent_module(tcx: TyCtxt, mut id: DefId) -> DefId {
@@ -142,6 +142,16 @@ fn hashed_symbol(data: DefPathData) -> Option<Symbol> {
     }
 }
 
+pub fn impl_subject<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    id: DefId,
+) -> Result<ty::TraitRef<'tcx>, ty::Ty<'tcx>> {
+    match tcx.impl_trait_ref(id) {
+        Some(trait_ref) => Ok(trait_ref.skip_binder()),
+        None => Err(tcx.type_of(id).skip_binder()),
+    }
+}
+
 pub fn eq_nameless_generic_args<'tcx>(
     args1: ty::GenericArgsRef<'tcx>,
     args2: ty::GenericArgsRef<'tcx>,

creusot/src/validate/purity.rs

@@ -208,7 +208,7 @@ impl<'a, 'tcx> Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> {
             ExprKind::Call { fun, ref args, .. } => {
                 if let &FnDef(func_did, subst) = self.thir[fun].ty.kind() {
                     // try to specialize the called function if it is a trait method.
-                    let subst = self.ctx.erase_regions(subst);
+                    let subst = self.ctx.erase_and_anonymize_regions(subst);
                     let (func_did, _) =
                         TraitResolved::resolve_item(self.ctx.tcx, self.typing_env, func_did, subst)
                             .to_opt(func_did, subst)

creusot/src/very_stable_hash.rs

@@ -64,6 +64,20 @@ impl<CTX, T: VeryStableHash<CTX>> VeryStableHash<CTX> for Option<T> {
     }
 }
 
+impl<CTX, T: VeryStableHash<CTX>, E: VeryStableHash<CTX>> VeryStableHash<CTX> for Result<T, E> {
+    fn very_stable_hash(&self, tcx: &CTX, hcx: &mut StableHasher) {
+        std::mem::discriminant(self).hash(hcx);
+        match self {
+            Ok(x) => {
+                x.very_stable_hash(tcx, hcx);
+            }
+            Err(e) => {
+                e.very_stable_hash(tcx, hcx);
+            }
+        }
+    }
+}
+
 impl<CTX, T: VeryStableHash<CTX>> VeryStableHash<CTX> for Vec<T> {
     fn very_stable_hash(&self, tcx: &CTX, hcx: &mut StableHasher) {
         self.as_slice().very_stable_hash(tcx, hcx);
@@ -176,10 +190,9 @@ impl<'tcx> VeryStableHash<TyCtxt<'tcx>> for ty::TyKind<'tcx> {
                 binder.very_stable_hash(tcx, hcx);
                 sig.very_stable_hash(tcx, hcx);
             }
-            Dynamic(trait_ty, region, kind) => {
+            Dynamic(trait_ty, region) => {
                 trait_ty.very_stable_hash(tcx, hcx);
                 region.very_stable_hash(tcx, hcx);
-                kind.very_stable_hash(tcx, hcx);
             }
             Closure(def_id, substs) => {
                 def_id.very_stable_hash(tcx, hcx);
@@ -224,16 +237,6 @@ impl<'tcx> VeryStableHash<TyCtxt<'tcx>> for ty::TraitRef<'tcx> {
     }
 }
 
-impl<'tcx> VeryStableHash<TyCtxt<'tcx>> for ty::ImplSubject<'tcx> {
-    fn very_stable_hash(&self, tcx: &TyCtxt<'tcx>, hcx: &mut StableHasher) {
-        std::mem::discriminant(self).hash(hcx);
-        match self {
-            ty::ImplSubject::Inherent(ty) => ty.very_stable_hash(tcx, hcx),
-            ty::ImplSubject::Trait(trait_ref) => trait_ref.very_stable_hash(tcx, hcx),
-        }
-    }
-}
-
 impl<'tcx> VeryStableHash<TyCtxt<'tcx>> for ty::ExistentialTraitRef<'tcx> {
     fn very_stable_hash(&self, tcx: &TyCtxt<'tcx>, hcx: &mut StableHasher) {
         self.def_id.very_stable_hash(tcx, hcx);
@@ -331,12 +334,6 @@ impl<'tcx, CTX, T: VeryStableHash<CTX>> VeryStableHash<CTX> for ty::EarlyBinder<
     }
 }
 
-impl<CTX> VeryStableHash<CTX> for ty::DynKind {
-    fn very_stable_hash(&self, _tcx: &CTX, hcx: &mut StableHasher) {
-        std::mem::discriminant(self).hash(hcx);
-    }
-}
-
 impl<CTX> VeryStableHash<CTX> for ty::AliasTyKind {
     fn very_stable_hash(&self, _tcx: &CTX, hcx: &mut StableHasher) {
         std::mem::discriminant(self).hash(hcx);

rust-toolchain

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2025-09-04"
+channel = "nightly-2025-10-01"
 components = [ "rustfmt", "rustc-dev", "llvm-tools" ]