Upgrade toolchain to nightly-2026-04-21

creusot-install/src/main.rs

@@ -1,4 +1,3 @@
-#![feature(exit_status_error, try_blocks)]
 use anyhow::{Context as _, anyhow, bail};
 use clap::*;
 use creusot_setup::{self as setup, Binary, CreusotPaths, tools_versions_urls::*};

creusot-std/src/ghost.rs

@@ -262,6 +262,9 @@ macro_rules! define_objective {
         /// `Unique<T>` (and therefore `Box<T>`, `Vec<T>`, ...) are therefore objective.
         #[trusted]
         pub auto trait Objective {}
+
+        #[trusted]
+        impl !Objective for NotObjective {}
     };
 }
 
@@ -276,7 +279,3 @@ define_objective! {}
 /// This negative implementation primarily targets `Perm<PermCell<T>>` and
 /// `Perm<*const T>`.
 pub(crate) struct NotObjective {}
-
-#[cfg(creusot)]
-#[trusted]
-impl !Objective for NotObjective {}

creusot-std/src/lib.rs

@@ -47,38 +47,30 @@
 #![cfg_attr(feature = "nightly", allow(incomplete_features, internal_features))]
 #![cfg_attr(
     feature = "nightly",
+    feature(step_trait, allocator_api, unboxed_closures, tuple_trait, edition_panic)
+)]
+#![cfg_attr(
+    creusot,
     feature(
         core_intrinsics,
         const_destruct,
         fn_traits,
-        fmt_internals,
         fmt_arguments_from_str,
         fmt_helpers_for_derive,
-        step_trait,
         try_trait_v2,
-        allocator_api,
-        unboxed_closures,
-        tuple_trait,
         panic_internals,
-        never_type,
         ptr_metadata,
         hint_must_use,
         pointer_is_aligned_to,
-        edition_panic,
-        new_range_api,
         range_bounds_is_empty,
         bound_copied,
-        decl_macro,
         auto_traits,
+        new_range_api_legacy,
         negative_impls,
-        clone_from_ref,
     )
 )]
 #![cfg_attr(all(doc, feature = "nightly"), feature(intra_doc_pointers))]
-#![cfg_attr(
-    all(feature = "nightly", feature = "std"),
-    feature(print_internals, libstd_sys_internals, rt,)
-)]
+#![cfg_attr(all(creusot, feature = "std"), feature(print_internals, libstd_sys_internals, rt,))]
 #![cfg_attr(not(feature = "std"), no_std)]
 
 extern crate alloc;

creusot/src/analysis.rs

@@ -21,7 +21,7 @@ use rustc_index::{Idx as _, bit_set::MixedBitSet};
 use rustc_macros::{TyDecodable, TyEncodable};
 use rustc_middle::{
     mir::{self, BasicBlock, Local, Location, Place, traversal},
-    ty::{self, TyCtxt, TypingEnv},
+    ty::{self, TyCtxt, TypingEnv, Unnormalized},
 };
 use rustc_mir_dataflow::{
     Analysis as _, ResultsCursor,
@@ -275,7 +275,7 @@ impl<'a, 'tcx> HasMoveData<'tcx> for Analysis<'a, 'tcx> {
 fn local_typing_env(tcx: TyCtxt<'_>, def_id: DefId) -> TypingEnv<'_> {
     let param_env = tcx.param_env(def_id);
     let typing_mode = ty::TypingMode::post_borrowck_analysis(tcx, def_id.as_local().unwrap());
-    TypingEnv { typing_mode, param_env }
+    TypingEnv::new(param_env, typing_mode)
 }
 
 impl<'a, 'tcx> Analysis<'a, 'tcx> {
@@ -446,7 +446,7 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
                 continue;
             }
             let ty = pl.ty(&self.body().local_decls, self.tcx());
-            let ty = self.tcx().normalize_erasing_regions(self.typing_env, ty);
+            let ty = self.tcx().normalize_erasing_regions(self.typing_env, Unnormalized::new(ty));
             use TyKind::*;
             match ty.ty.kind() {
                 Adt(adt_def, subst) => {
@@ -517,7 +517,7 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
                 | Foreign(_)
                 | Str
                 | RawPtr(_, _)
-                | Alias(_, _)
+                | Alias(_)
                 | Param(_)
                 | Bound(_, _)
                 | Placeholder(_)
@@ -915,7 +915,7 @@ pub(crate) fn run_with_specs<'tcx>(
     let tree = fmir::ScopeTree::build(&body.body, &body_locals.locals);
     let clos_subst = tcx.is_closure_like(def_id).then(|| {
         let loc = body_locals.vars.get_index(1).unwrap();
-        let ty_env = tcx.type_of(def_id).instantiate_identity();
+        let ty_env = tcx.type_of(def_id).instantiate_identity().skip_normalization();
         let TyKind::Closure(_, subst) = ty_env.kind() else { unreachable!() };
         let self_ = Term::var(*loc.0, loc.1.ty);
         let self_ = match subst.as_closure().kind() {
@@ -996,10 +996,8 @@ impl<'tcx> BodyLocals<'tcx> {
                 } else {
                     (Ident::fresh(ctx.crate_name(), &format!("_{}", idx)), LocalKind::Temp)
                 };
-                (
-                    (ident, fmir::LocalDecl { span: d.source_info.span, ty: d.ty, kind }),
-                    (loc, ident),
-                )
+                let ty = ctx.erase_and_anonymize_regions(d.ty);
+                ((ident, fmir::LocalDecl { span: d.source_info.span, ty, kind }), (loc, ident))
             })
             .unzip();
         BodyLocals { vars, locals }

creusot/src/analysis/borrows.rs

@@ -70,8 +70,6 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
 
     /// Kill any borrows that conflict with `place`.
     fn kill_borrows_on_place(&self, trans: &mut impl GenKill<BorrowIndex>, place: Place<'tcx>) {
-        debug!("kill_borrows_on_place: place={:?}", place);
-
         let other_borrows_of_local = self
             .borrow_set
             .local_map()

creusot/src/backend/clone_map.rs

@@ -20,6 +20,7 @@ use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::ty::{
     GenericArgsRef, List, Ty, TyCtxt, TyKind, TypeFoldable, TypeVisitableExt, TypingEnv,
+    Unnormalized,
 };
 use rustc_span::Span;
 use why3::{
@@ -131,9 +132,11 @@ pub(crate) trait Namer<'tcx> {
         self.dependency(Dependency::PrivateResolve(struct_id, subst)).ident()
     }
 
-    // TODO: get rid of this. It feels like it should be unnecessary
+    /// Ideally we'd like to avoid caring about normalization in the backend,
+    /// but we still need this for normalizing field types after instantiation.
+    /// Also for normalizing RPITs but that seems easier to get rid of if we ever care to.
     fn normalize<T: TypeFoldable<TyCtxt<'tcx>>>(&self, ty: T) -> T {
-        self.tcx().normalize_erasing_regions(self.typing_env(), ty)
+        self.tcx().normalize_erasing_regions(self.typing_env(), Unnormalized::new(ty))
     }
 
     fn import_prelude_module(&self, module: PreMod) {

creusot/src/backend/clone_map/elaborator.rs

@@ -31,7 +31,7 @@ use rustc_middle::ty::{
     self, AliasTyKind, Const, GenericArg, GenericArgsRef, TraitRef, Ty, TyCtxt, TyKind, TypingEnv,
 };
 use rustc_span::{DUMMY_SP, Span, Symbol};
-use rustc_type_ir::{ClosureKind, ConstKind, EarlyBinder};
+use rustc_type_ir::{AliasTy, ClosureKind, ConstKind, EarlyBinder};
 use std::{
     assert_matches,
     cell::RefCell,
@@ -119,9 +119,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
 
         let name = names.dependency(dep).ident();
 
-        let mut pre_sig = EarlyBinder::bind(ctx.sig(def_id).clone())
-            .instantiate(ctx.tcx, subst)
-            .normalize(ctx, typing_env);
+        let mut pre_sig = ctx.sig(def_id).clone().instantiate_and_normalize(ctx, subst, typing_env);
 
         if ctx.def_kind(def_id) == DefKind::Closure {
             // Inline the body of closures
@@ -221,9 +219,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
         }
 
         let typing_env = self.typing_env;
-        let pre_sig = EarlyBinder::bind(ctx.sig(def_id).clone())
-            .instantiate(ctx.tcx, subst)
-            .normalize(ctx, typing_env);
+        let pre_sig = ctx.sig(def_id).clone().instantiate_and_normalize(ctx, subst, typing_env);
 
         let bound: Box<[Ident]> = pre_sig.inputs.iter().map(|(ident, _, _)| ident.0).collect();
         let trait_resol = TraitResolved::resolve_item(self.tcx(), typing_env, def_id, subst);
@@ -265,8 +261,9 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
                 let args_tup = Term::var(args_id, subst.type_at(0));
 
                 let res_id = Ident::fresh_local("res").into();
-                let res_ty = ctx.instantiate_bound_regions_with_erased(
-                    ctx.fn_sig(did_f).instantiate(ctx.tcx, subst_f).output(),
+                let res_ty = ctx.normalize_erasing_late_bound_regions(
+                    names.typing_env(),
+                    ctx.fn_sig(did_f).instantiate(ctx.tcx, subst_f).skip_normalization().output(),
                 );
                 let res = Term::var(res_id, res_ty);
 
@@ -330,7 +327,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
             .tcx()
             .layout_of(ty::PseudoCanonicalInput { typing_env: self.typing_env, value: ty })
             .is_err();
-        if size_unknown && self.ctx.is_nonzero_sized(ty) {
+        if size_unknown && self.ctx.is_nonzero_sized(self.typing_env, ty) {
             Some(Decl::Axiom(Axiom {
                 name: Ident::fresh_local(format!("nonzero_{}", name.name().to_string())),
                 rewrite: false,
@@ -373,9 +370,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
 
         let mut names = self.namer(dep);
         let name = names.dependency(dep).ident();
-        let mut pre_sig = EarlyBinder::bind(ctx.sig(def_id).clone())
-            .instantiate(ctx.tcx, subst)
-            .normalize(ctx, typing_env);
+        let mut pre_sig = ctx.sig(def_id).clone().instantiate_and_normalize(ctx, subst, typing_env);
         sig_add_type_invariant_spec(ctx, typing_env, names.source_id(), &mut pre_sig, def_id);
         let sig = lower_logic_sig(ctx, &names, name, pre_sig, def_id);
 
@@ -466,10 +461,13 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
                 ty_name: names.ty(ty).to_ident(),
                 ty_params: Box::new([]),
             })],
-            TyKind::Alias(AliasTyKind::Opaque | AliasTyKind::Projection, _) => {
-                let (def_id, subst) = dep.did().unwrap();
+            &TyKind::Alias(AliasTy {
+                kind: AliasTyKind::Opaque { def_id } | AliasTyKind::Projection { def_id },
+                args,
+                ..
+            }) => {
                 vec![Decl::TyDecl(TyDecl::Opaque {
-                    ty_name: names.def_ty(def_id, subst).to_ident(),
+                    ty_name: names.def_ty(def_id, args).to_ident(),
                     ty_params: Box::new([]),
                 })]
             }
@@ -959,10 +957,7 @@ fn post_fndef<'tcx>(
     if is_logic(ctx.tcx, did) {
         return None;
     }
-
-    let mut sig = EarlyBinder::bind(ctx.sig(did).clone())
-        .instantiate(ctx.tcx, subst)
-        .normalize(ctx, names.typing_env());
+    let mut sig = ctx.sig(did).clone().instantiate_and_normalize(ctx, subst, names.typing_env());
     sig_add_type_invariant_spec(ctx, names.typing_env(), names.source_id(), &mut sig, did);
     let mut post = sig.contract.ensures_conj(ctx.tcx);
     post.subst(&HashMap::from([(name::result(), res.kind)]));
@@ -1044,9 +1039,7 @@ fn pre_fndef<'tcx>(
         // precondition if called in a program via a generic.
         return None;
     }
-    let mut sig = EarlyBinder::bind(ctx.sig(did).clone())
-        .instantiate(ctx.tcx, subst)
-        .normalize(ctx, names.typing_env());
+    let mut sig = ctx.sig(did).clone().instantiate_and_normalize(ctx, subst, names.typing_env());
     sig_add_type_invariant_spec(ctx, names.typing_env(), names.source_id(), &mut sig, did);
     let pre = sig.contract.requires_conj(ctx.tcx);
     let pattern = Pattern::tuple(
@@ -1286,7 +1279,7 @@ fn term<'tcx>(
         Intrinsic::MetadataMatches => metadata_matches_term(ctx, names, subst, bound),
         _ => {
             let term = EarlyBinder::bind(ctx.term(def_id).unwrap().rename(bound));
-            Some(normalize(ctx, typing_env, term.instantiate(ctx.tcx, subst)))
+            Some(normalize(ctx, typing_env, term.instantiate(ctx.tcx, subst).skip_normalization()))
         }
     }
 }

creusot/src/backend/closures.rs

@@ -25,7 +25,9 @@ fn closure_captures<'tcx>(
     tcx: TyCtxt<'tcx>,
     def_id: LocalDefId,
 ) -> impl Iterator<Item = (FieldIdx, &'tcx CapturedPlace<'tcx>, Ty<'tcx>)> {
-    let TyKind::Closure(_, subst) = tcx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) =
+        tcx.type_of(def_id).instantiate_identity().skip_normalization().kind()
+    else {
         unreachable!()
     };
     tcx.closure_captures(def_id)
@@ -41,7 +43,9 @@ pub(crate) fn closure_hist_inv<'tcx>(
     self_: Term<'tcx>,
     future: Term<'tcx>,
 ) -> Term<'tcx> {
-    let TyKind::Closure(_, subst) = ctx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) =
+        ctx.type_of(def_id).instantiate_identity().skip_normalization().kind()
+    else {
         unreachable!()
     };
     let closure_kind = subst.as_closure().kind();
@@ -82,7 +86,9 @@ pub(crate) fn closure_pre<'tcx>(
     args: Term<'tcx>,
 ) -> Term<'tcx> {
     let typing_env = ctx.typing_env(def_id.into());
-    let TyKind::Closure(_, subst) = ctx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) =
+        ctx.type_of(def_id).instantiate_identity().skip_normalization().kind()
+    else {
         unreachable!()
     };
     let closure_kind = subst.as_closure().kind();
@@ -145,7 +151,9 @@ pub(crate) fn closure_post<'tcx>(
     args: Term<'tcx>,
     result_state: Option<Term<'tcx>>,
 ) -> Term<'tcx> {
-    let TyKind::Closure(_, subst) = ctx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) =
+        ctx.type_of(def_id).instantiate_identity().skip_normalization().kind()
+    else {
         unreachable!()
     };
     let closure_kind = subst.as_closure().kind();

creusot/src/backend/dependency.rs

@@ -3,7 +3,7 @@ use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::ty::{GenericArgKind, GenericArgsRef, List, Ty, TyCtxt, TyKind};
 use rustc_span::Symbol;
-use rustc_type_ir::AliasTyKind;
+use rustc_type_ir::{AliasTy, AliasTyKind};
 
 use crate::{
     contracts_items::Intrinsic,
@@ -38,9 +38,11 @@ impl<'tcx> Dependency<'tcx> {
             Dependency::Type(t) => match t.kind() {
                 TyKind::Adt(def, substs) => Some((def.did(), substs)),
                 TyKind::Closure(id, substs) => Some((*id, substs)),
-                TyKind::Alias(AliasTyKind::Opaque | AliasTyKind::Projection, aty) => {
-                    Some((aty.def_id, aty.args))
-                }
+                &TyKind::Alias(AliasTy {
+                    kind: AliasTyKind::Opaque { def_id } | AliasTyKind::Projection { def_id },
+                    args,
+                    ..
+                }) => Some((def_id, args)),
                 _ => None,
             },
             _ => None,
@@ -76,7 +78,7 @@ impl<'tcx> Dependency<'tcx> {
                 _ if Intrinsic::SizeOfLogic.is(ctx, did) => {
                     Some(Symbol::intern(&type_string(ctx.tcx, "size_of".into(), subst.type_at(0))))
                 }
-                DefKind::Const | DefKind::AssocConst | DefKind::ConstParam => ctx
+                DefKind::Const { .. } | DefKind::AssocConst { .. } | DefKind::ConstParam => ctx
                     .opt_item_name(did)
                     .map(|name| Symbol::intern(&lowercase_prefix("const_", name.as_str()))),
                 _ => {
@@ -88,7 +90,10 @@ impl<'tcx> Dependency<'tcx> {
                         && let Some(trait_ref) = ctx.impl_opt_trait_ref(parent)
                     {
                         // AssocFn in a trait impl: get the instantiated Self type
-                        first_ty_arg(trait_ref.instantiate(ctx.tcx, subst).args)
+                        // Skip normalization: we are generating names so it doesn't really matter
+                        first_ty_arg(
+                            trait_ref.instantiate(ctx.tcx, subst).skip_normalization().args,
+                        )
                     } else {
                         // AssocFn in a trait or in an inherent impl: Self is the first argument in `subst`
                         // And for plain fn, also display the first type argument in its name.

creusot/src/backend/logic.rs

@@ -23,7 +23,7 @@ mod vcgen;
 
 pub(crate) fn translate_logic(ctx: &Why3Generator, def_id: DefId) -> Option<FileModule> {
     let names = Dependencies::new(ctx, def_id);
-    let pre_sig = ctx.sig(def_id).clone().normalize(ctx, ctx.typing_env(def_id));
+    let pre_sig = ctx.sig(def_id).clone().normalize_contract(ctx, ctx.typing_env(def_id));
 
     let namespace_ty = names.namespace_ty();