diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f21d7161ccd..a4ce31d317c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -113,6 +113,14 @@ jobs:
         run: |
           git clone https://github.com/flux-rs/flux-to-lean-demo
 
+      - name: Patch flux-rs dependency if in pull request
+        if: github.event_name == 'pull_request'
+        run: |
+          echo '[patch."https://github.com/flux-rs/flux.git"]' >> flux-to-lean-demo/Cargo.toml
+          echo 'flux-rs = { path = "../lib/flux-rs" }' >> flux-to-lean-demo/Cargo.toml
+          echo 'flux-core = { path = "../lib/flux-core" }' >> flux-to-lean-demo/Cargo.toml
+          echo 'flux-alloc = { path = "../lib/flux-alloc" }' >> flux-to-lean-demo/Cargo.toml
+
       - name: Generate Lean Project
         continue-on-error: true
         working-directory: flux-to-lean-demo
diff --git a/.gitignore b/.gitignore
index 872944f9f99..fd3f296567f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,4 +5,5 @@ target
 log
 sysroot/
 
-.DS_Store
\ No newline at end of file
+.DS_Store
+fixpoint
diff --git a/crates/flux-desugar/src/desugar/lift.rs b/crates/flux-desugar/src/desugar/lift.rs
index c319df27e59..bea5d1e1a66 100644
--- a/crates/flux-desugar/src/desugar/lift.rs
+++ b/crates/flux-desugar/src/desugar/lift.rs
@@ -515,7 +515,7 @@ impl<'genv> RustItemCtxt<'_, 'genv, '_> {
     }
 
     fn lift_const_arg(&mut self, const_arg: &hir::ConstArg) -> fhir::ConstArg {
-        fhir::ConstArg { kind: fhir::ConstArgKind::Infer, span: const_arg.span() }
+        fhir::ConstArg { kind: fhir::ConstArgKind::Infer, span: const_arg.span }
     }
 
     #[track_caller]
diff --git a/crates/flux-driver/src/bin/main.rs b/crates/flux-driver/src/bin/main.rs
index 762644d0172..d05d1159275 100644
--- a/crates/flux-driver/src/bin/main.rs
+++ b/crates/flux-driver/src/bin/main.rs
@@ -2,7 +2,7 @@
 
 extern crate rustc_driver;
 
-use std::{env, io, process::exit};
+use std::{env, io, process::{ExitCode, exit}};
 
 use flux_config::{
     self as config,
@@ -10,7 +10,7 @@ use flux_config::{
 };
 use flux_driver::callbacks::FluxCallbacks;
 use flux_middle::metrics;
-use rustc_driver::{EXIT_SUCCESS, catch_with_exit_code, run_compiler};
+use rustc_driver::{catch_with_exit_code, run_compiler};
 
 mod logger;
 
@@ -49,8 +49,12 @@ fn main() -> io::Result<()> {
     let exit_code = catch_with_exit_code(move || {
         run_compiler(&args, &mut FluxCallbacks);
     });
-    if config::summary() && exit_code == EXIT_SUCCESS {
+    if config::summary() && exit_code == ExitCode::SUCCESS {
         metrics::print_summary(start.elapsed())?;
     };
-    exit(exit_code)
+    exit(if exit_code == ExitCode::SUCCESS {
+        rustc_driver::EXIT_SUCCESS
+    } else {
+        rustc_driver::EXIT_FAILURE
+    })
 }
diff --git a/crates/flux-driver/src/callbacks.rs b/crates/flux-driver/src/callbacks.rs
index 8905c62a981..3cc4fa347c9 100644
--- a/crates/flux-driver/src/callbacks.rs
+++ b/crates/flux-driver/src/callbacks.rs
@@ -23,7 +23,7 @@ use rustc_hir::{
     def_id::{DefId, LOCAL_CRATE, LocalDefId},
 };
 use rustc_interface::interface::Compiler;
-use rustc_middle::{query, ty::TyCtxt};
+use rustc_middle::{queries, ty::TyCtxt, util};
 use rustc_session::config::OutputType;
 use rustc_span::FileName;
 
@@ -37,7 +37,7 @@ impl Callbacks for FluxCallbacks {
         assert!(config.override_queries.is_none());
 
         config.override_queries = Some(|_, local| {
-            local.mir_borrowck = mir_borrowck;
+            local.queries.mir_borrowck = mir_borrowck;
         });
         // this should always be empty otherwise something changed in rustc and all our assumptions
         // about symbol interning are wrong.
@@ -185,11 +185,11 @@ impl<'genv, 'tcx> CrateChecker<'genv, 'tcx> {
         let span = tcx.def_span(def_id);
         let sm = tcx.sess.source_map();
         let FileName::Real(file_name) = sm.span_to_filename(span) else { return true };
-        let mut file_path = file_name.local_path_if_available();
+        let Some(mut file_path) = file_name.local_path() else { return true };
 
         // If the path is absolute try to normalize it to be relative to the working_dir
         if file_path.is_absolute() {
-            let working_dir = tcx.sess.opts.working_dir.local_path_if_available();
+            let Some(working_dir) = sm.working_dir().local_path() else { return true };
             let Ok(p) = file_path.strip_prefix(working_dir) else { return true };
             file_path = p;
         }
@@ -355,7 +355,7 @@ fn force_conv(genv: GlobalEnv, def_id: DefId) -> QueryResult {
 fn mir_borrowck<'tcx>(
     tcx: TyCtxt<'tcx>,
     def_id: LocalDefId,
-) -> query::queries::mir_borrowck::ProvidedValue<'tcx> {
+) -> queries::mir_borrowck::ProvidedValue<'tcx> {
     let bodies_with_facts = rustc_borrowck::consumers::get_bodies_with_borrowck_facts(
         tcx,
         def_id,
@@ -368,8 +368,8 @@ fn mir_borrowck<'tcx>(
             flux_common::mir_storage::store_mir_body(tcx, def_id, body_with_facts);
         }
     }
-    let mut providers = query::Providers::default();
-    rustc_borrowck::provide(&mut providers);
-    let original_mir_borrowck = providers.mir_borrowck;
+    let mut providers = util::Providers::default();
+    rustc_borrowck::provide(&mut providers.queries);
+    let original_mir_borrowck = providers.queries.mir_borrowck;
     original_mir_borrowck(tcx, def_id)
 }
diff --git a/crates/flux-errors/src/lib.rs b/crates/flux-errors/src/lib.rs
index 5d54a93b977..c4e88c6319c 100644
--- a/crates/flux-errors/src/lib.rs
+++ b/crates/flux-errors/src/lib.rs
@@ -13,7 +13,7 @@ pub use rustc_errors::ErrorGuaranteed;
 use rustc_errors::{
     Diagnostic, ErrCode, FatalAbort, FatalError, LazyFallbackBundle, TerminalUrl,
     annotate_snippet_emitter_writer::AnnotateSnippetEmitter,
-    emitter::{Emitter, HumanEmitter, HumanReadableErrorType, OutputTheme, stderr_destination},
+    emitter::{Emitter, HumanReadableErrorType, OutputTheme, stderr_destination},
     json::JsonEmitter,
     translation::Translator,
 };
@@ -100,7 +100,7 @@ fn emitter(
     match sopts.error_format {
         config::ErrorOutputType::HumanReadable { kind, color_config } => {
             match kind {
-                HumanReadableErrorType::AnnotateSnippet { short, unicode } => {
+                HumanReadableErrorType { short, unicode } => {
                     let emitter =
                         AnnotateSnippetEmitter::new(stderr_destination(color_config), translator)
                             .sm(source_map)
@@ -118,23 +118,6 @@ fn emitter(
                             );
                     Box::new(emitter.ui_testing(sopts.unstable_opts.ui_testing))
                 }
-                HumanReadableErrorType::Default { short } => {
-                    let emitter = HumanEmitter::new(stderr_destination(color_config), translator)
-                        .sm(source_map)
-                        .short_message(short)
-                        .diagnostic_width(sopts.diagnostic_width)
-                        .macro_backtrace(macro_backtrace)
-                        .track_diagnostics(track_diagnostics)
-                        .terminal_url(terminal_url)
-                        .theme(OutputTheme::Ascii)
-                        .ignored_directories_in_source_blocks(
-                            sopts
-                                .unstable_opts
-                                .ignore_directory_in_diagnostics_source_blocks
-                                .clone(),
-                        );
-                    Box::new(emitter.ui_testing(sopts.unstable_opts.ui_testing))
-                }
             }
         }
         config::ErrorOutputType::Json { pretty, json_rendered, color_config } => {
diff --git a/crates/flux-macros/src/diagnostics/fluent.rs b/crates/flux-macros/src/diagnostics/fluent.rs
index 51806d4196e..e3a13c9b5ac 100644
--- a/crates/flux-macros/src/diagnostics/fluent.rs
+++ b/crates/flux-macros/src/diagnostics/fluent.rs
@@ -1,15 +1,19 @@
-use std::collections::{HashMap, HashSet};
-use std::fs::read_to_string;
-use std::path::{Path, PathBuf};
+use std::{
+    collections::{HashMap, HashSet},
+    fs::read_to_string,
+    path::{Path, PathBuf},
+};
 
 use annotate_snippets::{Renderer, Snippet};
 use fluent_bundle::{FluentBundle, FluentError, FluentResource};
-use fluent_syntax::ast::{
-    Attribute, Entry, Expression, Identifier, InlineExpression, Message, Pattern, PatternElement,
+use fluent_syntax::{
+    ast::{
+        Attribute, Entry, Expression, Identifier, InlineExpression, Message, Pattern,
+        PatternElement,
+    },
+    parser::ParserError,
 };
-use fluent_syntax::parser::ParserError;
-use proc_macro::tracked_path::path;
-use proc_macro::{Diagnostic, Level, Span};
+use proc_macro::{Diagnostic, Level, Span, tracked::path};
 use proc_macro2::TokenStream;
 use quote::quote;
 use syn::{Ident, LitStr, parse_macro_input};
@@ -158,7 +162,9 @@ pub(crate) fn fluent_messages(input: proc_macro::TokenStream) -> proc_macro::Tok
     for entry in resource.entries() {
         if let Entry::Message(msg) = entry {
             let Message { id: Identifier { name }, attributes, value, .. } = msg;
-            let _ = previous_defns.entry((*name).to_string()).or_insert(resource_span);
+            let _ = previous_defns
+                .entry((*name).to_string())
+                .or_insert(resource_span);
             if name.contains('-') {
                 Diagnostic::spanned(
                     resource_span,
diff --git a/crates/flux-macros/src/lib.rs b/crates/flux-macros/src/lib.rs
index 13c7d5d7a31..e3f98fdd649 100644
--- a/crates/flux-macros/src/lib.rs
+++ b/crates/flux-macros/src/lib.rs
@@ -1,4 +1,10 @@
-#![feature(proc_macro_diagnostic, never_type, proc_macro_span, if_let_guard, track_path)]
+#![feature(
+    proc_macro_diagnostic,
+    never_type,
+    proc_macro_span,
+    if_let_guard,
+    proc_macro_tracked_path
+)]
 
 mod diagnostics;
 mod fold;
diff --git a/crates/flux-metadata/src/decoder.rs b/crates/flux-metadata/src/decoder.rs
index 0ea3f57123b..398231a232c 100644
--- a/crates/flux-metadata/src/decoder.rs
+++ b/crates/flux-metadata/src/decoder.rs
@@ -20,7 +20,8 @@ use rustc_serialize::{
 };
 use rustc_session::StableCrateId;
 use rustc_span::{
-    BytePos, ByteSymbol, DUMMY_SP, SourceFile, Span, SpanDecoder, Symbol, SyntaxContext,
+    BlobDecoder, BytePos, ByteSymbol, DUMMY_SP, SourceFile, Span, SpanDecoder, Symbol,
+    SyntaxContext,
     def_id::{CrateNum, DefIndex},
     hygiene::{HygieneDecodeContext, SyntaxContextKey},
 };
@@ -103,6 +104,42 @@ pub(super) fn decode_crate_metadata(
 
 implement_ty_decoder!(DecodeContext<'a, 'tcx>);
 
+impl BlobDecoder for DecodeContext<'_, '_> {
+    fn decode_symbol(&mut self) -> Symbol {
+        let tag = self.read_u8();
+
+        match tag {
+            SYMBOL_STR => {
+                let s = self.read_str();
+                Symbol::intern(s)
+            }
+            SYMBOL_OFFSET => {
+                // read str offset
+                let pos = self.read_usize();
+
+                // move to str offset and read
+                self.opaque.with_position(pos, |d| {
+                    let s = d.read_str();
+                    Symbol::intern(s)
+                })
+            }
+            SYMBOL_PREDEFINED => {
+                let symbol_index = self.read_u32();
+                Symbol::new(symbol_index)
+            }
+            _ => unreachable!(),
+        }
+    }
+
+    fn decode_byte_symbol(&mut self) -> ByteSymbol {
+        ByteSymbol::intern(self.read_byte_str())
+    }
+
+    fn decode_def_index(&mut self) -> DefIndex {
+        DefIndex::from_u32(self.read_u32())
+    }
+}
+
 impl SpanDecoder for DecodeContext<'_, '_> {
     fn decode_attr_id(&mut self) -> rustc_ast::AttrId {
         self.tcx.sess.psess.attr_id_generator.mk_attr_id()
@@ -113,10 +150,6 @@ impl SpanDecoder for DecodeContext<'_, '_> {
         self.tcx.stable_crate_id_to_crate_num(stable_id)
     }
 
-    fn decode_def_index(&mut self) -> DefIndex {
-        DefIndex::from_u32(self.read_u32())
-    }
-
     fn decode_def_id(&mut self) -> DefId {
         DefId { krate: Decodable::decode(self), index: Decodable::decode(self) }
     }
@@ -165,36 +198,6 @@ impl SpanDecoder for DecodeContext<'_, '_> {
 
         Span::new(lo, hi, ctxt, None)
     }
-
-    fn decode_symbol(&mut self) -> rustc_span::Symbol {
-        let tag = self.read_u8();
-
-        match tag {
-            SYMBOL_STR => {
-                let s = self.read_str();
-                Symbol::intern(s)
-            }
-            SYMBOL_OFFSET => {
-                // read str offset
-                let pos = self.read_usize();
-
-                // move to str offset and read
-                self.opaque.with_position(pos, |d| {
-                    let s = d.read_str();
-                    Symbol::intern(s)
-                })
-            }
-            SYMBOL_PREDEFINED => {
-                let symbol_index = self.read_u32();
-                Symbol::new(symbol_index)
-            }
-            _ => unreachable!(),
-        }
-    }
-
-    fn decode_byte_symbol(&mut self) -> ByteSymbol {
-        ByteSymbol::intern(self.read_byte_str())
-    }
 }
 
 impl<'tcx> TyDecoder<'tcx> for DecodeContext<'_, 'tcx> {
diff --git a/crates/flux-metadata/src/encoder.rs b/crates/flux-metadata/src/encoder.rs
index 0c6d759d862..9ac5f403224 100644
--- a/crates/flux-metadata/src/encoder.rs
+++ b/crates/flux-metadata/src/encoder.rs
@@ -77,8 +77,6 @@ fn file_indices(
     let mut file_index_to_stable_id =
         FxHashMap::with_capacity_and_hasher(files.len(), Default::default());
     use rustc_span::def_id::LOCAL_CRATE;
-    let source_map = tcx.sess.source_map();
-    let working_directory = &tcx.sess.opts.working_dir;
     let local_crate_stable_id = tcx.stable_crate_id(LOCAL_CRATE);
 
     // This portion of the code is adapted from the rustc metadata encoder, while the rest of
@@ -95,9 +93,8 @@ fn file_indices(
             use rustc_span::FileName;
             match file.name {
                 FileName::Real(ref original_file_name) => {
-                    let adapted_file_name = source_map
-                        .path_mapping()
-                        .to_embeddable_absolute_path(original_file_name.clone(), working_directory);
+                    let mut adapted_file_name = original_file_name.clone();
+                    adapted_file_name.update_for_crate_metadata();
 
                     adapted_source_file.name = FileName::Real(adapted_file_name);
                 }
diff --git a/crates/flux-metadata/src/lib.rs b/crates/flux-metadata/src/lib.rs
index 04bd136ef63..0fab410d58d 100644
--- a/crates/flux-metadata/src/lib.rs
+++ b/crates/flux-metadata/src/lib.rs
@@ -489,7 +489,7 @@ fn flux_metadata_extern_location(tcx: TyCtxt, crate_num: CrateNum) -> Option<Pat
     tcx.used_crate_source(crate_num)
         .rmeta
         .as_ref()
-        .map(|(path, _)| path.with_extension("fluxmeta"))
+        .map(|path| path.with_extension("fluxmeta"))
 }
 
 // Tags for encoding Symbol's
diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs
index b715ef46dde..b3b53904831 100644
--- a/crates/flux-middle/src/fhir.rs
+++ b/crates/flux-middle/src/fhir.rs
@@ -1175,7 +1175,7 @@ impl<Id1, Id2> TryFrom<rustc_hir::def::Res<Id1>> for Res<Id2> {
         match res {
             rustc_hir::def::Res::Def(kind, did) => Ok(Res::Def(kind, did)),
             rustc_hir::def::Res::PrimTy(prim_ty) => Ok(Res::PrimTy(prim_ty)),
-            rustc_hir::def::Res::SelfTyAlias { alias_to, forbid_generic: false, is_trait_impl } => {
+            rustc_hir::def::Res::SelfTyAlias { alias_to, is_trait_impl } => {
                 Ok(Res::SelfTyAlias { alias_to, is_trait_impl })
             }
             rustc_hir::def::Res::SelfTyParam { trait_ } => Ok(Res::SelfTyParam { trait_ }),
diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs
index 98daef1b5ff..a47f90d3d15 100644
--- a/crates/flux-middle/src/global_env.rs
+++ b/crates/flux-middle/src/global_env.rs
@@ -697,9 +697,9 @@ impl ErrorEmitter for GlobalEnv<'_, '_> {
 
 fn lean_parent_dir(tcx: TyCtxt) -> PathBuf {
     tcx.sess
-        .opts
-        .working_dir
-        .local_path_if_available()
-        .to_path_buf()
+        .source_map()
+        .working_dir()
+        .local_path()
+        .unwrap()
         .join(config::lean_dir())
 }
diff --git a/crates/flux-middle/src/rty/binder.rs b/crates/flux-middle/src/rty/binder.rs
index f8ba5073f28..e44d0ae5625 100644
--- a/crates/flux-middle/src/rty/binder.rs
+++ b/crates/flux-middle/src/rty/binder.rs
@@ -5,12 +5,12 @@ use flux_common::tracked_span_bug;
 use flux_macros::{TypeFoldable, TypeVisitable};
 use flux_rustc_bridge::{
     ToRustc,
-    ty::{BoundRegion, Region},
+    ty::{BoundRegion, BoundRegionKind, Region},
 };
 use itertools::Itertools;
 use rustc_data_structures::unord::UnordMap;
 use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable};
-use rustc_middle::ty::{BoundRegionKind, TyCtxt};
+use rustc_middle::ty::TyCtxt;
 use rustc_span::Symbol;
 
 use super::{
@@ -263,11 +263,11 @@ impl BoundVariableKind {
     fn to_rustc<'tcx>(
         vars: &[Self],
         tcx: TyCtxt<'tcx>,
-    ) -> &'tcx rustc_middle::ty::List<rustc_middle::ty::BoundVariableKind> {
+    ) -> &'tcx rustc_middle::ty::List<rustc_middle::ty::BoundVariableKind<'tcx>> {
         tcx.mk_bound_variable_kinds_from_iter(vars.iter().flat_map(|kind| {
             match kind {
                 BoundVariableKind::Region(brk) => {
-                    Some(rustc_middle::ty::BoundVariableKind::Region(*brk))
+                    Some(rustc_middle::ty::BoundVariableKind::Region(brk.to_rustc(tcx)))
                 }
                 BoundVariableKind::Refine(..) => None,
             }
diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs
index 2ba4fe566f5..b1feed21bf3 100644
--- a/crates/flux-middle/src/rty/pretty.rs
+++ b/crates/flux-middle/src/rty/pretty.rs
@@ -29,7 +29,7 @@ impl Pretty for BoundRegionKind {
     fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
             BoundRegionKind::Anon => w!(cx, f, "'<annon>"),
-            BoundRegionKind::NamedAnon(sym) => w!(cx, f, "'{sym}"),
+            BoundRegionKind::NamedForPrinting(sym) => w!(cx, f, "'{sym}"),
             BoundRegionKind::Named(def_id) => w!(cx, f, "'{def_id:?}"),
             BoundRegionKind::ClosureEnv => w!(cx, f, "'<env>"),
         }
diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs
index 8b12dcb007d..6c2a37a5a6e 100644
--- a/crates/flux-refineck/src/checker.rs
+++ b/crates/flux-refineck/src/checker.rs
@@ -1649,7 +1649,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
             | CastKind::PointerCoercion(mir::PointerCast::MutToConstPointer)
             | CastKind::PointerCoercion(mir::PointerCast::ClosureFnPointer)
             | CastKind::PointerWithExposedProvenance => self.refine_default(to)?,
-            CastKind::PointerCoercion(mir::PointerCast::ReifyFnPointer) => {
+            CastKind::PointerCoercion(mir::PointerCast::ReifyFnPointer(_)) => {
                 let to = self.refine_default(to)?;
                 if let TyKind::Indexed(BaseTy::FnDef(def_id, args), _) = from.kind()
                     && let TyKind::Indexed(BaseTy::FnPtr(super_sig), _) = to.kind()
diff --git a/crates/flux-refineck/src/ghost_statements/points_to.rs b/crates/flux-refineck/src/ghost_statements/points_to.rs
index 6f9257f3650..089319bf094 100644
--- a/crates/flux-refineck/src/ghost_statements/points_to.rs
+++ b/crates/flux-refineck/src/ghost_statements/points_to.rs
@@ -131,12 +131,12 @@ impl<'a> PointsToAnalysis<'a> {
 
     fn handle_operand(&self, operand: &mir::Operand) -> Option<PlaceIndex> {
         match operand {
-            mir::Operand::Constant(..) => None,
             mir::Operand::Copy(place) | mir::Operand::Move(place) => {
                 // On move, we would ideally flood the place with bottom. But with the current
                 // framework this is not possible (similar to `InterpCx::eval_operand`).
                 self.map.find(place.as_ref())
             }
+            mir::Operand::Constant(..) | mir::Operand::RuntimeChecks(_) => None,
         }
     }
 
diff --git a/crates/flux-rustc-bridge/src/lowering.rs b/crates/flux-rustc-bridge/src/lowering.rs
index 5146646c24e..d8ac1117d10 100644
--- a/crates/flux-rustc-bridge/src/lowering.rs
+++ b/crates/flux-rustc-bridge/src/lowering.rs
@@ -37,7 +37,7 @@ use super::{
 use crate::{
     mir::{BodyRoot, CallKind, ConstOperand},
     ty::{
-        AliasTy, ExistentialTraitRef, GenericArgs, ProjectionPredicate, Region,
+        AliasTy, BoundRegionKind, ExistentialTraitRef, GenericArgs, ProjectionPredicate, Region,
         RegionOutlivesPredicate,
     },
 };
@@ -512,7 +512,6 @@ impl<'sess, 'tcx> MirLoweringCtxt<'_, 'sess, 'tcx> {
                 Ok(Rvalue::ShallowInitBox(self.lower_operand(op)?, ty.lower(self.tcx)?))
             }
             rustc_mir::Rvalue::ThreadLocalRef(_)
-            | rustc_mir::Rvalue::NullaryOp(..)
             | rustc_mir::Rvalue::CopyForDeref(_)
             | rustc_mir::Rvalue::WrapUnsafeBinder(..) => {
                 Err(UnsupportedReason::new(format!("unsupported rvalue `{rvalue:?}`")))
@@ -532,8 +531,8 @@ impl<'sess, 'tcx> MirLoweringCtxt<'_, 'sess, 'tcx> {
             rustc_adjustment::PointerCoercion::ClosureFnPointer(_) => {
                 Some(crate::mir::PointerCast::ClosureFnPointer)
             }
-            rustc_adjustment::PointerCoercion::ReifyFnPointer => {
-                Some(crate::mir::PointerCast::ReifyFnPointer)
+            rustc_adjustment::PointerCoercion::ReifyFnPointer(safety) => {
+                Some(crate::mir::PointerCast::ReifyFnPointer(safety))
             }
             rustc_adjustment::PointerCoercion::UnsafeFnPointer
             | rustc_adjustment::PointerCoercion::ArrayToPointer => None,
@@ -636,6 +635,9 @@ impl<'sess, 'tcx> MirLoweringCtxt<'_, 'sess, 'tcx> {
             rustc_mir::Operand::Copy(place) => Ok(Operand::Copy(lower_place(self.tcx, place)?)),
             rustc_mir::Operand::Move(place) => Ok(Operand::Move(lower_place(self.tcx, place)?)),
             rustc_mir::Operand::Constant(c) => Ok(Operand::Constant(self.lower_constant(c)?)),
+            rustc_mir::Operand::RuntimeChecks(..) => {
+                Err(UnsupportedReason::new(format!("unsupported operand `{op:?}`")))
+            }
         }
     }
 
@@ -700,15 +702,15 @@ impl<'tcx> Lower<'tcx> for rustc_ty::FnSig<'tcx> {
     }
 }
 
-impl<'tcx> Lower<'tcx> for &'tcx rustc_ty::List<rustc_ty::BoundVariableKind> {
+impl<'tcx> Lower<'tcx> for &'tcx rustc_ty::List<rustc_ty::BoundVariableKind<'tcx>> {
     type R = Result<List<BoundVariableKind>, UnsupportedReason>;
 
-    fn lower(self, _tcx: TyCtxt<'tcx>) -> Self::R {
+    fn lower(self, tcx: TyCtxt<'tcx>) -> Self::R {
         let mut vars = vec![];
         for var in self {
             match var {
                 rustc_ty::BoundVariableKind::Region(kind) => {
-                    vars.push(BoundVariableKind::Region(kind));
+                    vars.push(BoundVariableKind::Region(kind.lower(tcx)));
                 }
                 _ => {
                     return Err(UnsupportedReason {
@@ -721,15 +723,30 @@ impl<'tcx> Lower<'tcx> for &'tcx rustc_ty::List<rustc_ty::BoundVariableKind> {
     }
 }
 
-impl<'tcx> Lower<'tcx> for rustc_ty::ValTree<'tcx> {
-    type R = crate::ty::ValTree;
+impl<'tcx> Lower<'tcx> for rustc_ty::BoundRegionKind<'tcx> {
+    type R = BoundRegionKind;
 
     fn lower(self, _tcx: TyCtxt<'tcx>) -> Self::R {
+        match self {
+            rustc_ty::BoundRegionKind::Anon => BoundRegionKind::Anon,
+            rustc_ty::BoundRegionKind::NamedForPrinting(name) => {
+                BoundRegionKind::NamedForPrinting(name)
+            }
+            rustc_ty::BoundRegionKind::Named(def_id) => BoundRegionKind::Named(def_id),
+            rustc_ty::BoundRegionKind::ClosureEnv => BoundRegionKind::ClosureEnv,
+        }
+    }
+}
+
+impl<'tcx> Lower<'tcx> for rustc_ty::ValTree<'tcx> {
+    type R = Result<crate::ty::ValTree, UnsupportedReason>;
+
+    fn lower(self, tcx: TyCtxt<'tcx>) -> Self::R {
         match &*self {
-            rustc_ty::ValTreeKind::Leaf(scalar_int) => crate::ty::ValTree::Leaf(*scalar_int),
-            rustc_ty::ValTreeKind::Branch(trees) => {
-                let trees = trees.iter().map(|tree| tree.lower(_tcx)).collect();
-                crate::ty::ValTree::Branch(trees)
+            rustc_ty::ValTreeKind::Leaf(scalar_int) => Ok(crate::ty::ValTree::Leaf(*scalar_int)),
+            rustc_ty::ValTreeKind::Branch(consts) => {
+                let trees = consts.iter().map(|c| c.lower(tcx)).try_collect()?;
+                Ok(crate::ty::ValTree::Branch(trees))
             }
         }
     }
@@ -744,7 +761,7 @@ impl<'tcx> Lower<'tcx> for rustc_ty::Const<'tcx> {
                 ConstKind::Param(ParamConst { name: param_const.name, index: param_const.index })
             }
             rustc_type_ir::ConstKind::Value(value) => {
-                ConstKind::Value(value.ty.lower(tcx)?, value.valtree.lower(tcx))
+                ConstKind::Value(value.ty.lower(tcx)?, value.valtree.lower(tcx)?)
             }
             rustc_type_ir::ConstKind::Unevaluated(c) => {
                 // TODO: raise unsupported if c.args is not empty?
@@ -948,14 +965,14 @@ impl<'tcx> Lower<'tcx> for rustc_middle::ty::GenericArg<'tcx> {
 impl<'tcx> Lower<'tcx> for rustc_middle::ty::Region<'tcx> {
     type R = Result<Region, UnsupportedReason>;
 
-    fn lower(self, _tcx: TyCtxt<'tcx>) -> Self::R {
+    fn lower(self, tcx: TyCtxt<'tcx>) -> Self::R {
         use rustc_middle::ty;
         match self.kind() {
             ty::ReVar(rvid) => Ok(Region::ReVar(rvid)),
             ty::ReBound(ty::BoundVarIndexKind::Bound(debruijn), bregion) => {
                 Ok(Region::ReBound(
                     debruijn,
-                    Ok(BoundRegion { kind: bregion.kind, var: bregion.var })?,
+                    Ok(BoundRegion { kind: bregion.kind.lower(tcx), var: bregion.var })?,
                 ))
             }
             ty::ReEarlyParam(bregion) => Ok(Region::ReEarlyParam(bregion)),
diff --git a/crates/flux-rustc-bridge/src/mir.rs b/crates/flux-rustc-bridge/src/mir.rs
index fc4fa635852..cfc7c7e579e 100644
--- a/crates/flux-rustc-bridge/src/mir.rs
+++ b/crates/flux-rustc-bridge/src/mir.rs
@@ -12,7 +12,7 @@ use rustc_data_structures::{
     graph::{self, DirectedGraph, StartNode, dominators::Dominators},
     unord::UnordMap,
 };
-use rustc_hir::def_id::DefId;
+use rustc_hir::{self as hir, def_id::DefId};
 use rustc_index::IndexSlice;
 use rustc_macros::{TyDecodable, TyEncodable};
 use rustc_middle::mir::{Promoted, VarDebugInfoContents};
@@ -263,7 +263,7 @@ pub enum PointerCast {
     MutToConstPointer,
     Unsize,
     ClosureFnPointer,
-    ReifyFnPointer,
+    ReifyFnPointer(hir::Safety),
 }
 
 #[derive(Debug)]
@@ -740,7 +740,7 @@ impl fmt::Debug for PointerCast {
             PointerCast::MutToConstPointer => write!(f, "MutToConstPointer"),
             PointerCast::Unsize => write!(f, "Unsize"),
             PointerCast::ClosureFnPointer => write!(f, "ClosureFnPointer"),
-            PointerCast::ReifyFnPointer => write!(f, "ReifyFnPointer"),
+            PointerCast::ReifyFnPointer(safety) => write!(f, "ReifyFnPointer({safety})"),
         }
     }
 }
diff --git a/crates/flux-rustc-bridge/src/ty/mod.rs b/crates/flux-rustc-bridge/src/ty/mod.rs
index 81c5d2d913f..a19ae0b04ff 100644
--- a/crates/flux-rustc-bridge/src/ty/mod.rs
+++ b/crates/flux-rustc-bridge/src/ty/mod.rs
@@ -12,12 +12,12 @@ use rustc_abi;
 pub use rustc_abi::{FIRST_VARIANT, FieldIdx, VariantIdx};
 use rustc_hir::{Safety, def_id::DefId};
 use rustc_index::{IndexSlice, IndexVec};
-use rustc_macros::{TyDecodable, TyEncodable, extension};
+use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable, extension};
 pub use rustc_middle::{
     mir::Mutability,
     ty::{
-        BoundRegionKind, BoundVar, ConstVid, DebruijnIndex, EarlyParamRegion, FloatTy, IntTy,
-        LateParamRegion, LateParamRegionKind, ParamTy, RegionVid, ScalarInt, UintTy,
+        BoundVar, ConstVid, DebruijnIndex, EarlyParamRegion, FloatTy, IntTy, LateParamRegion,
+        LateParamRegionKind, ParamTy, RegionVid, ScalarInt, UintTy,
     },
 };
 use rustc_middle::{
@@ -43,7 +43,22 @@ pub struct EarlyBinder<T>(pub T);
 #[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
 pub struct Binder<T>(T, List<BoundVariableKind>);
 
-#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)]
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, Encodable, Decodable)]
+pub enum BoundRegionKind {
+    /// An anonymous region parameter for a given fn (&T)
+    Anon,
+    /// An anonymous region parameter with a `Symbol` name.
+    ///
+    /// Used to give late-bound regions names for things like pretty printing.
+    NamedForPrinting(Symbol),
+    /// Late-bound regions that appear in the AST.
+    Named(DefId),
+    /// Anonymous region for the implicit env pointer parameter
+    /// to a closure
+    ClosureEnv,
+}
+
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, Encodable, Decodable)]
 pub enum BoundVariableKind {
     Region(BoundRegionKind),
 }
@@ -54,17 +69,32 @@ impl BoundVariableKind {
     fn to_rustc<'tcx>(
         vars: &[Self],
         tcx: TyCtxt<'tcx>,
-    ) -> &'tcx rustc_middle::ty::List<rustc_middle::ty::BoundVariableKind> {
+    ) -> &'tcx rustc_middle::ty::List<rustc_middle::ty::BoundVariableKind<'tcx>> {
         tcx.mk_bound_variable_kinds_from_iter(vars.iter().flat_map(|kind| {
             match kind {
                 BoundVariableKind::Region(brk) => {
-                    Some(rustc_middle::ty::BoundVariableKind::Region(*brk))
+                    Some(rustc_middle::ty::BoundVariableKind::Region(brk.to_rustc(tcx)))
                 }
             }
         }))
     }
 }
 
+impl<'tcx> ToRustc<'tcx> for BoundRegionKind {
+    type T = rustc_middle::ty::BoundRegionKind<'tcx>;
+
+    fn to_rustc(&self, _tcx: TyCtxt<'tcx>) -> Self::T {
+        match *self {
+            BoundRegionKind::Anon => rustc_middle::ty::BoundRegionKind::Anon,
+            BoundRegionKind::NamedForPrinting(name) => {
+                rustc_middle::ty::BoundRegionKind::NamedForPrinting(name)
+            }
+            BoundRegionKind::Named(def_id) => rustc_middle::ty::BoundRegionKind::Named(def_id),
+            BoundRegionKind::ClosureEnv => rustc_middle::ty::BoundRegionKind::ClosureEnv,
+        }
+    }
+}
+
 #[derive(Debug, Hash, Eq, PartialEq, TyEncodable, TyDecodable)]
 pub struct GenericParamDef {
     pub def_id: DefId,
@@ -316,9 +346,9 @@ impl<'tcx> ToRustc<'tcx> for ValTree {
     fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
         match self {
             ValTree::Leaf(scalar) => rustc_middle::ty::ValTree::from_scalar_int(tcx, *scalar),
-            ValTree::Branch(trees) => {
-                let trees = trees.iter().map(|tree| tree.to_rustc(tcx));
-                rustc_middle::ty::ValTree::from_branches(tcx, trees)
+            ValTree::Branch(consts) => {
+                let consts = consts.iter().map(|c| c.to_rustc(tcx));
+                rustc_middle::ty::ValTree::from_branches(tcx, consts)
             }
         }
     }
@@ -353,7 +383,7 @@ pub struct UnevaluatedConst {
 #[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
 pub enum ValTree {
     Leaf(ScalarInt),
-    Branch(List<ValTree>),
+    Branch(List<Const>),
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
@@ -454,10 +484,10 @@ pub struct BoundRegion {
 }
 
 impl<'tcx> ToRustc<'tcx> for BoundRegion {
-    type T = rustc_middle::ty::BoundRegion;
+    type T = rustc_middle::ty::BoundRegion<'tcx>;
 
-    fn to_rustc(&self, _tcx: TyCtxt<'tcx>) -> Self::T {
-        rustc_middle::ty::BoundRegion { var: self.var, kind: self.kind }
+    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
+        rustc_middle::ty::BoundRegion { var: self.var, kind: self.kind.to_rustc(tcx) }
     }
 }
 
@@ -989,7 +1019,7 @@ impl_slice_internable!(
     GenericParamDef,
     BoundVariableKind,
     Clause,
-    ValTree,
+    Const,
     Binder<ExistentialPredicate>,
 );
 
@@ -1170,7 +1200,7 @@ pub fn region_to_string(region: Region) -> String {
                     format!("{debruijn:?}{region:?}")
                 }
                 BoundRegionKind::ClosureEnv => "'<env>".to_string(),
-                BoundRegionKind::NamedAnon(sym) => format!("{sym}"),
+                BoundRegionKind::NamedForPrinting(sym) => format!("{sym}"),
             }
         }
         Region::ReEarlyParam(region) => region.name.to_string(),
diff --git a/lib/flux-alloc/src/vec/mod.rs b/lib/flux-alloc/src/vec/mod.rs
index 3ecaad6d9da..66dc5eacd99 100644
--- a/lib/flux-alloc/src/vec/mod.rs
+++ b/lib/flux-alloc/src/vec/mod.rs
@@ -24,7 +24,10 @@ impl<T> Vec<T> {
 impl<T, A: Allocator> Vec<T, A> {
     #[spec(fn(self: &mut Vec<T, A>[@n], T) ensures self: Vec<T, A>[n+1])]
     fn push(v: &mut Vec<T, A>, value: T);
+}
 
+#[extern_spec]
+impl<T, A: Allocator> Vec<T, A> {
     #[spec(fn(&Vec<T, A>[@n]) -> usize[n])]
     fn len(v: &Vec<T, A>) -> usize;
 
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 028feb5f21d..29e64d0631c 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2025-11-25"
+channel = "nightly-2026-02-09"
 components = ["rust-src", "rustc-dev", "llvm-tools", "rustfmt", "clippy"]
diff --git a/tests/tests/neg/surface/vec01.rs b/tests/tests/neg/surface/vec01.rs
index 312a2465aee..09b85145554 100644
--- a/tests/tests/neg/surface/vec01.rs
+++ b/tests/tests/neg/surface/vec01.rs
@@ -47,7 +47,10 @@ impl<T> Vec<T> {
 impl<T, A: Allocator> Vec<T, A> {
     #[flux::sig(fn(self: &strg Vec<T, A>[@n], T) ensures self: Vec<T, A>[n+1])]
     fn push(v: &mut Vec<T, A>, value: T);
+}
 
+#[extern_spec]
+impl<T, A: Allocator> Vec<T, A> {
     #[flux::sig(fn(&Vec<T, A>[@n]) -> usize[n])]
     fn len(v: &Vec<T, A>) -> usize;
 }