Bump rustc to 2026-02-19

charon/hax-frontend/src/constant_utils/uneval.rs

@@ -114,9 +114,8 @@ pub fn eval_ty_constant<'tcx, S: UnderOwnerState<'tcx>>(
 impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx> {
     #[tracing::instrument(level = "trace", skip(s))]
     fn sinto(&self, s: &S) -> ConstantExpr {
-        use rustc_middle::query::Key;
         let tcx = s.base().tcx;
-        let span = self.default_span(tcx);
+        let span = rustc_span::DUMMY_SP;
         match self.kind() {
             ty::ConstKind::Param(p) => {
                 let ty = p.find_const_ty_from_env(s.param_env());
@@ -135,10 +134,9 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx>
                     val.sinto(s)
                 } else {
                     use crate::rustc_middle::query::Key;
-                    let span = span.substitute_dummy(
-                        tcx.def_ident_span(ucv.def)
-                            .unwrap_or_else(|| ucv.def.default_span(tcx)),
-                    );
+                    let span = tcx
+                        .def_ident_span(ucv.def)
+                        .unwrap_or_else(|| ucv.def.default_span(tcx));
                     let item = translate_item_ref(s, ucv.def, ucv.args);
                     let kind = ConstantExprKind::NamedGlobal(item);
                     let ty = tcx.type_of(ucv.def).instantiate(tcx, ucv.args);
@@ -182,9 +180,9 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
         (ty::ValTreeKind::Branch(valtrees), ty::Str) => {
             let bytes = valtrees
                 .iter()
-                .map(|x| match &***x {
-                    ty::ValTreeKind::Leaf(leaf) => leaf.to_u8(),
-                    _ => fatal!(
+                .map(|x| match x.try_to_leaf() {
+                    Some(leaf) => leaf.to_u8(),
+                    None => fatal!(
                         s[span],
                         "Expected a flat list of leaves while translating \
                             a str literal, got a arbitrary valtree."
@@ -193,43 +191,34 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
                 .collect();
             ConstantExprKind::Literal(ConstantLiteral::byte_str(bytes))
         }
-        (
-            ty::ValTreeKind::Branch(_),
-            ty::Array(..) | ty::Slice(..) | ty::Tuple(..) | ty::Adt(..),
-        ) => {
-            let contents: rustc_middle::ty::DestructuredConst = s
-                .base()
-                .tcx
-                .destructure_const(ty::Const::new_value(s.base().tcx, valtree, ty));
-            let fields = contents.fields.iter().copied();
+        (ty::ValTreeKind::Branch(fields), ty::Array(..) | ty::Slice(..) | ty::Tuple(..)) => {
+            let fields = fields.iter().copied().map(|field| field.sinto(s)).collect();
             match ty.kind() {
-                ty::Array(..) | ty::Slice(..) => ConstantExprKind::Array {
-                    fields: fields.map(|field| field.sinto(s)).collect(),
-                },
-                ty::Tuple(_) => ConstantExprKind::Tuple {
-                    fields: fields.map(|field| field.sinto(s)).collect(),
-                },
-                ty::Adt(def, _) => {
-                    let variant_idx = contents
-                        .variant
-                        .s_expect(s, "destructed const of adt without variant idx");
-                    let variant_def = &def.variant(variant_idx);
-
-                    ConstantExprKind::Adt {
-                        kind: get_variant_kind(def, variant_idx, s),
-                        fields: fields
-                            .into_iter()
-                            .zip(&variant_def.fields)
-                            .map(|(value, field)| ConstantFieldExpr {
-                                field: field.did.sinto(s),
-                                value: value.sinto(s),
-                            })
-                            .collect(),
-                    }
-                }
+                ty::Array(..) | ty::Slice(..) => ConstantExprKind::Array { fields },
+                ty::Tuple(_) => ConstantExprKind::Tuple { fields },
                 _ => unreachable!(),
             }
         }
+        (ty::ValTreeKind::Branch(_), ty::Adt(def, _)) => {
+            let contents: rustc_middle::ty::DestructuredAdtConst =
+                ty::Value { valtree, ty }.destructure_adt_const();
+
+            let fields = contents.fields.iter().copied();
+            let variant_idx = contents.variant;
+            let variant_def = &def.variant(variant_idx);
+
+            ConstantExprKind::Adt {
+                kind: get_variant_kind(def, variant_idx, s),
+                fields: fields
+                    .into_iter()
+                    .zip(&variant_def.fields)
+                    .map(|(value, field)| ConstantFieldExpr {
+                        field: field.did.sinto(s),
+                        value: value.sinto(s),
+                    })
+                    .collect(),
+            }
+        }
         (ty::ValTreeKind::Leaf(x), ty::RawPtr(_, _)) => {
             use crate::rustc_type_ir::inherent::Ty;
             let raw_address = x.to_bits_unchecked();

charon/hax-frontend/src/types/mir.rs

@@ -75,8 +75,7 @@ pub mod mir_kinds {
                 id: DefId,
                 f: impl FnOnce(&Body<'tcx>) -> T,
             ) -> Option<T> {
-                tcx.is_ctfe_mir_available(id)
-                    .then(|| f(tcx.mir_for_ctfe(id)))
+                (!tcx.is_trivial_const(id)).then(|| f(tcx.mir_for_ctfe(id)))
             }
         }
 

charon/hax-frontend/src/types/ty.rs

@@ -72,7 +72,7 @@ pub struct ExistentialProjection {
 /// Reflects [`ty::BoundTyKind`]
 
 #[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTyKind, state: S as s)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTyKind<'tcx>, state: S as s)]
 pub enum BoundTyKind {
     Anon,
     #[custom_arm(&FROM_TYPE::Param(def_id) => TO_TYPE::Param(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
@@ -82,7 +82,7 @@ pub enum BoundTyKind {
 /// Reflects [`ty::BoundTy`]
 
 #[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTy, state: S as s)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTy<'tcx>, state: S as s)]
 pub struct BoundTy {
     pub var: BoundVar,
     pub kind: BoundTyKind,
@@ -93,10 +93,10 @@ sinto_as_usize!(rustc_middle::ty, BoundVar);
 /// Reflects [`ty::BoundRegionKind`]
 
 #[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegionKind, state: S as s)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegionKind<'tcx>, state: S as s)]
 pub enum BoundRegionKind {
     Anon,
-    NamedAnon(Symbol),
+    NamedForPrinting(Symbol),
     #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
     Named(DefId, Symbol),
     ClosureEnv,
@@ -105,7 +105,7 @@ pub enum BoundRegionKind {
 /// Reflects [`ty::BoundRegion`]
 
 #[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegion, state: S as s)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegion<'tcx>, state: S as s)]
 pub struct BoundRegion {
     pub var: BoundVar,
     pub kind: BoundRegionKind,
@@ -126,7 +126,7 @@ pub struct Placeholder<T> {
 }
 
 impl<'tcx, S: UnderOwnerState<'tcx>, T: SInto<S, U>, U> SInto<S, Placeholder<U>>
-    for ty::Placeholder<T>
+    for ty::Placeholder<ty::TyCtxt<'tcx>, T>
 {
     fn sinto(&self, s: &S) -> Placeholder<U> {
         Placeholder {
@@ -1291,7 +1291,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Predicate> for ty::Predicate<'tcx>
 
 /// Reflects [`ty::BoundVariableKind`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundVariableKind, state: S as tcx)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundVariableKind<'tcx>, state: S as tcx)]
 #[derive(Clone, Debug, Hash, PartialEq, Eq)]
 pub enum BoundVariableKind {
     Ty(BoundTyKind),
@@ -1445,7 +1445,7 @@ impl ClosureArgs {
         struct RegionUnEraserVisitor<'tcx> {
             tcx: ty::TyCtxt<'tcx>,
             depth: u32,
-            bound_vars: Vec<ty::BoundVariableKind>,
+            bound_vars: Vec<ty::BoundVariableKind<'tcx>>,
         }
 
         impl<'tcx> ty::TypeFolder<ty::TyCtxt<'tcx>> for RegionUnEraserVisitor<'tcx> {

charon/rust-toolchain

@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2025-11-23"
+channel = "nightly-2026-02-07"
 components = [ "rustc-dev", "llvm-tools-preview", "rust-src", "miri" ]
 targets = [ "x86_64-apple-darwin", "i686-unknown-linux-gnu", "powerpc64-unknown-linux-gnu", "riscv64gc-unknown-none-elf" ]

charon/src/ast/types_utils.rs

@@ -689,6 +689,10 @@ impl Ty {
         Self::mk_tuple(vec![])
     }
 
+    pub fn mk_bool() -> Ty {
+        TyKind::Literal(LiteralTy::Bool).into()
+    }
+
     pub fn mk_usize() -> Ty {
         TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)).into()
     }

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

@@ -54,7 +54,7 @@ fn set_skip_borrowck() {
 }
 fn skip_borrowck_if_set(providers: &mut Providers) {
     if SKIP_BORROWCK.load(Ordering::SeqCst) {
-        providers.mir_borrowck = |tcx, _def_id| {
+        providers.queries.mir_borrowck = |tcx, _def_id| {
             // Empty result, which is what is used for custom_mir bodies.
             Ok(tcx.arena.alloc(Default::default()))
         }

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

@@ -99,17 +99,17 @@ fn get_mir_for_def_id_and_level<'tcx>(
                     | hax::DefKind::InlineConst
             );
             let mir_available = tcx.is_mir_available(rust_def_id);
-            let ctfe_mir_available = tcx.is_ctfe_mir_available(rust_def_id);
-            // For globals, prefer ctfe_mir when both are available.
-            let body = if mir_available && !(is_global && ctfe_mir_available) {
-                tcx.optimized_mir(rust_def_id).clone()
-            } else if ctfe_mir_available {
-                tcx.mir_for_ctfe(rust_def_id).clone()
+
+            if mir_available && !is_global {
+                Some(tcx.optimized_mir(rust_def_id).clone())
+            } else if (is_global && !tcx.is_trivial_const(rust_def_id))
+                || tcx.is_const_fn(rust_def_id)
+            {
+                Some(tcx.mir_for_ctfe(rust_def_id).clone())
             } else {
-                trace!("no mir available");
-                return None;
-            };
-            Some(body)
+                trace!("mir not available for {:?}", rust_def_id);
+                None
+            }
         }
         hax::DefIdBase::Promoted(rust_def_id, promoted_id) => {
             Some(hax::get_promoted_mir(tcx, rust_def_id, promoted_id))