From b88521ef6993dd92bb8112218edc4256f880da61 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Mon, 31 Mar 2025 17:31:51 +0200
Subject: [PATCH 1/4] Update rustc pin

---
 .envrc                                        |   1 +
 cli/driver/src/callbacks_wrapper.rs           |  16 +-
 cli/driver/src/driver.rs                      |   5 +-
 cli/driver/src/exporter.rs                    | 180 +++++++--------
 cli/driver/src/features.rs                    |  22 +-
 engine/lib/concrete_ident/concrete_ident.ml   |   5 +-
 .../lib/concrete_ident/concrete_ident_view.ml |   5 +-
 engine/lib/import_thir.ml                     |  94 ++++----
 engine/lib/span.ml                            |   6 +-
 engine/names/extract/build.rs                 |   5 +-
 flake.lock                                    |   6 +-
 frontend/exporter/src/body.rs                 |   2 +-
 frontend/exporter/src/constant_utils.rs       |   2 +-
 .../exporter/src/constant_utils/uneval.rs     |  18 +-
 frontend/exporter/src/lib.rs                  |   3 +-
 frontend/exporter/src/rustc_utils.rs          |   5 +-
 frontend/exporter/src/sinto.rs                |   6 -
 frontend/exporter/src/traits.rs               |   3 +-
 frontend/exporter/src/traits/resolution.rs    |   8 +-
 frontend/exporter/src/traits/utils.rs         |  10 +
 frontend/exporter/src/types/def_id.rs         |  11 +-
 frontend/exporter/src/types/hir.rs            | 218 ++++++++++--------
 frontend/exporter/src/types/mir.rs            |  64 ++---
 frontend/exporter/src/types/new/full_def.rs   |   8 +-
 .../exporter/src/types/new/item_attributes.rs |   7 +-
 .../exporter/src/types/new/variant_infos.rs   |   2 +-
 frontend/exporter/src/types/span.rs           |   4 +-
 frontend/exporter/src/types/thir.rs           |  21 +-
 frontend/exporter/src/types/ty.rs             |  14 +-
 rust-toolchain.toml                           |   2 +-
 ...oolchain__attribute-opaque into-fstar.snap |   2 +-
 .../snapshots/toolchain__dyn into-fstar.snap  |   2 +-
 .../toolchain__include-flag into-coq.snap     |   2 +-
 .../toolchain__literals into-coq.snap         |   2 +-
 .../toolchain__literals into-fstar.snap       |   2 +-
 .../toolchain__naming into-fstar.snap         |   2 +-
 .../toolchain__side-effects into-fstar.snap   |  15 +-
 .../toolchain__side-effects into-ssprove.snap |  48 ++--
 .../toolchain__traits into-fstar.snap         |  22 +-
 39 files changed, 445 insertions(+), 405 deletions(-)

diff --git a/.envrc b/.envrc
index 3550a30f2..de26198b8 100644
--- a/.envrc
+++ b/.envrc
@@ -1 +1,2 @@
+watch_file rust-toolchain.toml
 use flake
diff --git a/cli/driver/src/callbacks_wrapper.rs b/cli/driver/src/callbacks_wrapper.rs
index 39aebabc1..0d30ef2ef 100644
--- a/cli/driver/src/callbacks_wrapper.rs
+++ b/cli/driver/src/callbacks_wrapper.rs
@@ -1,7 +1,9 @@
 use hax_types::cli_options::{Command, Options, ENV_VAR_OPTIONS_FRONTEND};
 
+use rustc_ast::Crate;
 use rustc_driver::{Callbacks, Compilation};
-use rustc_interface::{interface, Queries};
+use rustc_interface::interface;
+use rustc_middle::ty::TyCtxt;
 use rustc_span::symbol::Symbol;
 
 /// Wraps a [Callbacks] structure, and injects some cache-related
@@ -34,22 +36,22 @@ impl<'a> Callbacks for CallbacksWrapper<'a> {
     fn after_crate_root_parsing<'tcx>(
         &mut self,
         compiler: &interface::Compiler,
-        queries: &'tcx Queries<'tcx>,
+        krate: &mut Crate,
     ) -> Compilation {
-        self.sub.after_crate_root_parsing(compiler, queries)
+        self.sub.after_crate_root_parsing(compiler, krate)
     }
     fn after_expansion<'tcx>(
         &mut self,
         compiler: &interface::Compiler,
-        queries: &'tcx Queries<'tcx>,
+        tcx: TyCtxt<'tcx>,
     ) -> Compilation {
-        self.sub.after_expansion(compiler, queries)
+        self.sub.after_expansion(compiler, tcx)
     }
     fn after_analysis<'tcx>(
         &mut self,
         compiler: &interface::Compiler,
-        queries: &'tcx Queries<'tcx>,
+        tcx: TyCtxt<'tcx>,
     ) -> Compilation {
-        self.sub.after_analysis(compiler, queries)
+        self.sub.after_analysis(compiler, tcx)
     }
 }
diff --git a/cli/driver/src/driver.rs b/cli/driver/src/driver.rs
index ced7479ab..1118158a7 100644
--- a/cli/driver/src/driver.rs
+++ b/cli/driver/src/driver.rs
@@ -14,6 +14,7 @@ extern crate rustc_data_structures;
 extern crate rustc_driver;
 extern crate rustc_errors;
 extern crate rustc_feature;
+extern crate rustc_hashes;
 extern crate rustc_hir;
 extern crate rustc_hir_analysis;
 extern crate rustc_index;
@@ -39,7 +40,7 @@ use features::*;
 use hax_types::cli_options::{BackendOptions, Command, ENV_VAR_OPTIONS_FRONTEND};
 
 use rustc_driver::{Callbacks, Compilation};
-use rustc_interface::{interface, Queries};
+use rustc_interface::interface;
 use rustc_span::symbol::Symbol;
 
 fn rustc_sysroot() -> String {
@@ -174,7 +175,7 @@ fn main() {
 
     let exit_code = rustc_driver::catch_with_exit_code({
         let rustc_args = rustc_args.clone();
-        move || rustc_driver::RunCompiler::new(&rustc_args, &mut callbacks).run()
+        move || rustc_driver::run_compiler(&rustc_args, &mut callbacks)
     });
 
     std::process::exit(
diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs
index 423399b17..4f5a6be54 100644
--- a/cli/driver/src/exporter.rs
+++ b/cli/driver/src/exporter.rs
@@ -3,7 +3,7 @@ use hax_frontend_exporter::SInto;
 use hax_types::cli_options::{Backend, PathOrDash, ENV_VAR_OPTIONS_FRONTEND};
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::interface;
-use rustc_interface::{interface::Compiler, Queries};
+use rustc_interface::interface::Compiler;
 use rustc_middle::middle::region::Scope;
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::{
@@ -76,7 +76,7 @@ fn precompute_local_thir_bodies(
     }
 
     use itertools::Itertools;
-    tcx.hir().body_owners()
+    tcx.hir_body_owners()
         .filter(|ldid| {
             match tcx.def_kind(ldid.to_def_id()) {
                 InlineConst | AnonConst => {
@@ -93,10 +93,20 @@ fn precompute_local_thir_bodies(
             }
         })
         .sorted_by_key(|ldid| const_level_of(tcx, *ldid))
-        .filter(move |ldid| tcx.hir().maybe_body_owned_by(*ldid).is_some())
+        .filter(move |ldid| tcx.hir_maybe_body_owned_by(*ldid).is_some())
         .map(move |ldid| {
             tracing::debug!("⏳ Type-checking THIR body for {:#?}", ldid);
-            let span = tcx.hir().span(tcx.local_def_id_to_hir_id(ldid));
+            let hir_id = tcx.local_def_id_to_hir_id(ldid);
+            // The `type_of` anon constants isn't available directly, it needs to be fed by some
+            // other query. This hack ensures this happens, otherwise `thir_body` returns an error.
+            // See https://rust-lang.zulipchat.com/#narrow/channel/182449-t-compiler.2Fhelp/topic/Change.20in.20THIR.20of.20anonymous.20constants.3F/near/509764021 .
+            for (parent_id, parent) in tcx.hir_parent_iter(hir_id) {
+                if let rustc_hir::Node::Item(..) = parent {
+                    let _ = tcx.check_well_formed(parent_id.owner.def_id);
+                    break;
+                }
+            }
+            let span = tcx.hir().span(hir_id);
             let (thir, expr) = match tcx.thir_body(ldid) {
                 Ok(x) => x,
                 Err(e) => {
@@ -145,9 +155,8 @@ fn convert_thir<'tcx, Body: hax_frontend_exporter::IsBody>(
     }
 
     let result = tcx
-        .hir()
-        .items()
-        .map(|id| tcx.hir().item(id).sinto(&state))
+        .hir_free_items()
+        .map(|id| tcx.hir_item(id).sinto(&state))
         .collect();
     let impl_infos = hax_frontend_exporter::impl_def_ids_to_impled_types_and_bounds(&state)
         .into_iter()
@@ -184,102 +193,87 @@ impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
 }
 
 impl Callbacks for ExtractionCallbacks {
-    fn after_crate_root_parsing<'tcx>(
-        &mut self,
-        compiler: &Compiler,
-        queries: &'tcx Queries<'tcx>,
-    ) -> Compilation {
-        let parse_ast = queries.parse().unwrap();
-        let parse_ast = parse_ast.borrow();
-        Compilation::Continue
-    }
-    fn after_expansion<'tcx>(
-        &mut self,
-        compiler: &Compiler,
-        queries: &'tcx Queries<'tcx>,
-    ) -> Compilation {
+    fn after_expansion<'tcx>(&mut self, compiler: &Compiler, tcx: TyCtxt<'tcx>) -> Compilation {
         use std::ops::{Deref, DerefMut};
 
-        queries.global_ctxt().unwrap().enter(|tcx| {
-            use hax_frontend_exporter::ThirBody;
-            use hax_types::cli_options::Command;
-            use rustc_session::config::CrateType;
-            use serde::{Deserialize, Serialize};
-            use std::fs::File;
-            use std::io::BufWriter;
+        use hax_frontend_exporter::ThirBody;
+        use hax_types::cli_options::Command;
+        use rustc_session::config::CrateType;
+        use serde::{Deserialize, Serialize};
+        use std::fs::File;
+        use std::io::BufWriter;
 
-            use std::path::PathBuf;
+        use std::path::PathBuf;
 
-            let opts = &compiler.sess.opts;
-            let externs: Vec<_> = opts
-                .externs
-                .iter()
-                .flat_map(|(_, ext)| match &ext.location {
-                    rustc_session::config::ExternLocation::ExactPaths(set) => set
-                        .iter()
-                        .map(|cp| cp.canonicalized())
-                        .collect::<Vec<_>>()
-                        .into_iter(),
-                    _ => vec![].into_iter(),
-                })
-                .map(|path| path.with_extension("haxmeta"))
-                .collect();
+        let opts = &compiler.sess.opts;
+        let externs: Vec<_> = opts
+            .externs
+            .iter()
+            .flat_map(|(_, ext)| match &ext.location {
+                rustc_session::config::ExternLocation::ExactPaths(set) => set
+                    .iter()
+                    .map(|cp| cp.canonicalized())
+                    .collect::<Vec<_>>()
+                    .into_iter(),
+                _ => vec![].into_iter(),
+            })
+            .map(|path| path.with_extension("haxmeta"))
+            .collect();
 
-            let cg_metadata = opts.cg.metadata[0].clone();
-            let crate_name = opts.crate_name.clone().unwrap();
+        let cg_metadata = opts.cg.metadata[0].clone();
+        let crate_name = opts.crate_name.clone().unwrap();
 
-            let output_dir = compiler.sess.io.output_dir.clone().unwrap();
-            let haxmeta_path = output_dir.join(format!("{crate_name}-{cg_metadata}.haxmeta",));
+        let output_dir = compiler.sess.io.output_dir.clone().unwrap();
+        let haxmeta_path = output_dir.join(format!("{crate_name}-{cg_metadata}.haxmeta",));
 
-            let mut file = BufWriter::new(File::create(&haxmeta_path).unwrap());
+        let mut file = BufWriter::new(File::create(&haxmeta_path).unwrap());
 
-            use hax_types::driver_api::{with_kind_type, HaxMeta};
-            with_kind_type!(
-                self.body_types.clone(),
-                <Body>|| {
-                    let (spans, def_ids, impl_infos, items, cache_map) =
-                        convert_thir(&self.clone().into(), tcx);
-                    let files: HashSet<PathBuf> = HashSet::from_iter(
-                        items
-                            .iter()
-                            .flat_map(|item| item.span.filename.to_path().map(|path| path.to_path_buf()))
-                    );
-                    let haxmeta: HaxMeta<Body> = HaxMeta {
-                        crate_name,
-                        cg_metadata,
-                        externs,
-                        impl_infos,
-                        items,
-                        comments: files.into_iter()
-                            .flat_map(|path|hax_frontend_exporter::comments::comments_of_file(path).ok())
-                            .flatten()
-                            .collect(),
-                        def_ids,
-                        hax_version: hax_types::HAX_VERSION.into(),
-                    };
-                    haxmeta.write(&mut file, cache_map);
-                }
-            );
+        use hax_types::driver_api::{with_kind_type, HaxMeta};
+        with_kind_type!(
+            self.body_types.clone(),
+            <Body>|| {
+                let (spans, def_ids, impl_infos, items, cache_map) =
+                    convert_thir(&self.clone().into(), tcx);
+                let files: HashSet<PathBuf> = HashSet::from_iter(
+                    items
+                        .iter()
+                        .flat_map(|item| item.span.filename.to_path().map(|path| path.to_path_buf()))
+                );
+                let haxmeta: HaxMeta<Body> = HaxMeta {
+                    crate_name,
+                    cg_metadata,
+                    externs,
+                    impl_infos,
+                    items,
+                    comments: files.into_iter()
+                        .flat_map(|path|hax_frontend_exporter::comments::comments_of_file(path).ok())
+                        .flatten()
+                        .collect(),
+                    def_ids,
+                    hax_version: hax_types::HAX_VERSION.into(),
+                };
+                haxmeta.write(&mut file, cache_map);
+            }
+        );
 
-            let manifest_dir = std::env::var("CARGO_MANIFEST_DIR").unwrap();
-            let manifest_dir = std::path::Path::new(&manifest_dir);
+        let manifest_dir = std::env::var("CARGO_MANIFEST_DIR").unwrap();
+        let manifest_dir = std::path::Path::new(&manifest_dir);
 
-            let data = hax_types::driver_api::EmitHaxMetaMessage {
-                manifest_dir: manifest_dir.to_path_buf(),
-                working_dir: opts
-                    .working_dir
-                    .to_path(rustc_span::FileNameDisplayPreference::Local)
-                    .to_path_buf(),
-                path: haxmeta_path,
-            };
-            eprintln!(
-                "{}{}",
-                hax_types::driver_api::HAX_DRIVER_STDERR_PREFIX,
-                &serde_json::to_string(&hax_types::driver_api::HaxDriverMessage::EmitHaxMeta(data))
-                    .unwrap()
-            );
+        let data = hax_types::driver_api::EmitHaxMetaMessage {
+            manifest_dir: manifest_dir.to_path_buf(),
+            working_dir: opts
+                .working_dir
+                .to_path(rustc_span::FileNameDisplayPreference::Local)
+                .to_path_buf(),
+            path: haxmeta_path,
+        };
+        eprintln!(
+            "{}{}",
+            hax_types::driver_api::HAX_DRIVER_STDERR_PREFIX,
+            &serde_json::to_string(&hax_types::driver_api::HaxDriverMessage::EmitHaxMeta(data))
+                .unwrap()
+        );
 
-            Compilation::Stop
-        })
+        Compilation::Stop
     }
 }
diff --git a/cli/driver/src/features.rs b/cli/driver/src/features.rs
index 01bf54f0a..2b5686fb0 100644
--- a/cli/driver/src/features.rs
+++ b/cli/driver/src/features.rs
@@ -1,7 +1,8 @@
 use std::collections::HashSet;
 
 use rustc_driver::{Callbacks, Compilation};
-use rustc_interface::{interface, Queries};
+use rustc_interface::interface;
+use rustc_middle::ty::TyCtxt;
 use rustc_span::symbol::Symbol;
 
 use crate::callbacks_wrapper::CallbacksWrapper;
@@ -86,16 +87,14 @@ impl Features {
             fn after_expansion<'tcx>(
                 &mut self,
                 compiler: &interface::Compiler,
-                queries: &'tcx Queries<'tcx>,
+                tcx: TyCtxt<'tcx>,
             ) -> Compilation {
-                queries.global_ctxt().unwrap().enter(|tcx| {
-                    self.features = tcx.features().into();
-                    self.features.registered_tools = tcx
-                        .registered_tools(())
-                        .iter()
-                        .map(|x| x.name.to_ident_string())
-                        .collect();
-                });
+                self.features = tcx.features().into();
+                self.features.registered_tools = tcx
+                    .registered_tools(())
+                    .iter()
+                    .map(|x| x.name.to_ident_string())
+                    .collect();
                 rustc_driver::Compilation::Stop
             }
         }
@@ -103,14 +102,13 @@ impl Features {
             features: Features::default(),
         };
         let exit_code = rustc_driver::catch_with_exit_code(|| {
-            rustc_driver::RunCompiler::new(
+            rustc_driver::run_compiler(
                 rustc_args,
                 &mut CallbacksWrapper {
                     sub: &mut callbacks,
                     options: options.clone(),
                 },
             )
-            .run()
         });
         if exit_code != 0 {
             std::process::exit(exit_code);
diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml
index a7f4deb06..6bab423c9 100644
--- a/engine/lib/concrete_ident/concrete_ident.ml
+++ b/engine/lib/concrete_ident/concrete_ident.ml
@@ -675,7 +675,7 @@ let map_path_strings ~(f : string -> string) (did : t) : t =
     |> List.map ~f:(fun (chunk : Types.disambiguated_def_path_item) ->
            let data =
              match chunk.data with
-             | TypeNs s -> Types.TypeNs (f s)
+             | TypeNs s -> Types.TypeNs (Option.map ~f s)
              | ValueNs s -> ValueNs (f s)
              | MacroNs s -> MacroNs (f s)
              | LifetimeNs s -> LifetimeNs (f s)
@@ -699,7 +699,8 @@ let matches_namespace (ns : Types.namespace) (did : t) : bool =
     @ List.map
         ~f:(fun (chunk : Types.disambiguated_def_path_item) ->
           match chunk.data with
-          | TypeNs s | ValueNs s | MacroNs s | LifetimeNs s -> Some s
+          | TypeNs s -> s
+          | ValueNs s | MacroNs s | LifetimeNs s -> Some s
           | _ -> None)
         did.path
   in
diff --git a/engine/lib/concrete_ident/concrete_ident_view.ml b/engine/lib/concrete_ident/concrete_ident_view.ml
index fad6f7a61..83b0f7960 100644
--- a/engine/lib/concrete_ident/concrete_ident_view.ml
+++ b/engine/lib/concrete_ident/concrete_ident_view.ml
@@ -20,7 +20,8 @@ module Assert = struct
 
   let type_ns (did : Explicit_def_id.t) =
     match List.last (Explicit_def_id.to_def_id did).path with
-    | Some { data = TypeNs data; disambiguator } ->
+    (* This can be `None` for the anonymous types generated for `-> impl Trait` in traits. *)
+    | Some { data = TypeNs (Some data); disambiguator } ->
         DisambiguatedString.{ data; disambiguator }
     | _ -> broken_invariant "last path chunk to exist and be of type TypeNs" did
 
@@ -180,7 +181,7 @@ let of_def_id (did : Explicit_def_id.t) : t =
     :: List.map
          ~f:(fun (m : Explicit_def_id.t) ->
            match (Explicit_def_id.to_def_id m).path |> List.last_exn with
-           | Types.{ disambiguator; data = TypeNs data } ->
+           | Types.{ disambiguator; data = TypeNs (Some data) } ->
                DisambiguatedString.{ data; disambiguator }
            | _ ->
                broken_invariant
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 573378a5a..587b45fb8 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -74,6 +74,11 @@ let c_uint_ty (ty : Thir.uint_ty) : int_kind =
 let csafety (safety : Types.safety) : safety_kind =
   match safety with Safe -> Safe | Unsafe -> Unsafe W.unsafe
 
+let c_header_safety (safety : Types.header_safety) : safety_kind =
+  match safety with
+  | SafeTargetFeatures -> Safe
+  | Normal safety -> csafety safety
+
 let c_mutability (witness : 'a) : bool -> 'a Ast.mutability = function
   | true -> Mutable witness
   | false -> Immutable
@@ -103,35 +108,28 @@ let c_logical_op : Thir.logical_op -> logical_op = function
   | And -> And
   | Or -> Or
 
-let c_attr (attr : Thir.attribute) : attr =
-  let kind =
-    match attr.kind with
-    | DocComment (kind, body) ->
-        let kind =
-          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
-        in
-        DocComment { kind; body }
-    | Normal
-        {
-          item =
-            { args = Eq (_, Hir { symbol; _ }); path = "doc"; tokens = None; _ };
-          tokens = None;
-        } ->
-        DocComment { kind = DCKLine; body = symbol }
-        (* Looks for `#[doc = "something"]` *)
-    | Normal { item = { args; path; tokens = subtokens; _ }; tokens } ->
-        let args_tokens =
-          match args with Delimited { tokens; _ } -> Some tokens | _ -> None
-        in
-        let tokens =
-          let ( || ) = Option.first_some in
-          Option.value ~default:"" (args_tokens || tokens || subtokens)
-        in
-        Tool { path; tokens }
-  in
-  { kind; span = Span.of_thir attr.span }
+let c_attr (attr : Thir.attribute) : attr option =
+  match attr with
+  | Parsed (DocComment { kind; comment; span; _ }) ->
+      let kind =
+        match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
+      in
+      let kind = DocComment { kind; body = comment } in
+      Some { kind; span = Span.of_thir span }
+  | Unparsed { args = Eq { expr = { symbol; _ }; _ }; path = "doc"; span; _ } ->
+      (* Looks for `#[doc = "something"]` *)
+      let kind = DocComment { kind = DCKLine; body = symbol } in
+      Some { kind; span = Span.of_thir span }
+  | Unparsed { args; path; span; _ } ->
+      let args_tokens =
+        match args with Delimited { tokens; _ } -> Some tokens | _ -> None
+      in
+      let tokens = Option.value ~default:"" args_tokens in
+      let kind = Tool { path; tokens } in
+      Some { kind; span = Span.of_thir span }
+  | _ -> None
 
-let c_attrs : Thir.attribute list -> attrs = List.map ~f:c_attr
+let c_attrs : Thir.attribute list -> attrs = List.filter_map ~f:c_attr
 
 let c_item_attrs (attrs : Thir.item_attributes) : attrs =
   (* TODO: This is a quite coarse approximation, we need to reflect
@@ -692,9 +690,12 @@ end) : EXPR = struct
           in
           let constructor = def_id ~value:true info.variant in
           let base =
-            Option.map
-              ~f:(fun base -> (c_expr base.base, W.construct_base))
-              base
+            match base with
+            | None' -> None
+            | Base base -> Some (c_expr base.base, W.construct_base)
+            | DefaultFields _ ->
+                unimplemented ~issue_id:1386 [ e.span ]
+                  "Default field values: not supported"
           in
           let fields =
             List.map
@@ -835,7 +836,7 @@ end) : EXPR = struct
           Literal { lit = { node = lit; span }; neg }
       | Adt { fields; info } ->
           let fields = List.map ~f:constant_field_expr fields in
-          Adt { fields; info; base = None; user_ty = None }
+          Adt { fields; info; base = None'; user_ty = None }
       | Array { fields } ->
           Array { fields = List.map ~f:constant_expr_to_expr fields }
       | Tuple { fields } ->
@@ -1347,8 +1348,9 @@ let c_trait_item (item : Thir.trait_item) : trait_item =
 let is_automatically_derived (attrs : Thir.attribute list) =
   List.exists (* We need something better here, see issue #108 *)
     ~f:(function
-      | { kind = Normal { item = { path; _ }; _ }; _ } ->
-          String.equal path "automatically_derived"
+      (* This will break once these attributes get properly parsed. It will
+          then be very easy to parse them correctly *)
+      | Unparsed { path; _ } -> String.equal path "automatically_derived"
       | _ -> false)
     attrs
 
@@ -1487,7 +1489,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
   in
   (* TODO: things might be unnamed (e.g. constants) *)
   match (item.kind : Thir.item_kind) with
-  | Const (_, generics, body) ->
+  | Const (_, _, generics, body) ->
       mk
       @@ Fn
            {
@@ -1497,14 +1499,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              params = [];
              safety = Safe;
            }
-  | Static (_, true, _) ->
+  | Static (_, _, true, _) ->
       unimplemented ~issue_id:1343 [ item.span ]
         "Mutable static items are not supported."
-  | Static (_ty, false, body) ->
+  | Static (_, _ty, false, body) ->
       let name = Concrete_ident.of_def_id ~value:true (assert_item_def_id ()) in
       let generics = { params = []; constraints = [] } in
       mk (Fn { name; generics; body = c_body body; params = []; safety = Safe })
-  | TyAlias (ty, generics) ->
+  | TyAlias (_, ty, generics) ->
       mk
       @@ TyAlias
            {
@@ -1513,7 +1515,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              generics = c_generics generics;
              ty = c_ty item.span ty;
            }
-  | Fn (generics, { body; params; header = { safety; _ }; _ }) ->
+  | Fn { generics; def = { body; params; header = { safety; _ }; _ }; _ } ->
       mk
       @@ Fn
            {
@@ -1521,15 +1523,15 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              generics = c_generics generics;
              body = c_body body;
              params = c_fn_params item.span params;
-             safety = csafety safety;
+             safety = c_header_safety safety;
            }
-  | (Enum (_, generics, _) | Struct (_, generics)) when erased ->
+  | (Enum (_, _, generics, _) | Struct (_, _, generics)) when erased ->
       let generics = c_generics generics in
       let is_struct = match item.kind with Struct _ -> true | _ -> false in
       let def_id = assert_item_def_id () in
       let name = Concrete_ident.of_def_id ~value:false def_id in
       mk @@ Type { name; generics; variants = []; is_struct }
-  | Enum (variants, generics, repr) ->
+  | Enum (_, variants, generics, repr) ->
       let def_id = assert_item_def_id () in
       let generics = c_generics generics in
       let is_struct = false in
@@ -1587,7 +1589,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
         mk_one (Type { name; generics; variants; is_struct }) :: discs
       in
       if is_primitive then cast_fun :: result else result
-  | Struct (v, generics) ->
+  | Struct (_, v, generics) ->
       let generics = c_generics generics in
       let def_id = assert_item_def_id () in
       let is_struct = true in
@@ -1614,7 +1616,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
       let variants = [ v ] in
       let name = Concrete_ident.of_def_id ~value:false def_id in
       mk @@ Type { name; generics; variants; is_struct }
-  | Trait (No, safety, generics, _bounds, items) ->
+  | Trait (No, safety, _, generics, _bounds, items) ->
       let items =
         List.filter
           ~f:(fun { attributes; _ } -> not (should_skip attributes))
@@ -1634,7 +1636,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
       let items = List.map ~f:c_trait_item items in
       let safety = csafety safety in
       mk @@ Trait { name; generics; items; safety }
-  | Trait (Yes, _, _, _, _) ->
+  | Trait (Yes, _, _, _, _, _) ->
       unimplemented ~issue_id:930 [ item.span ] "Auto trait"
   | Impl { of_trait = None; generics; items; _ } ->
       let items =
@@ -1675,7 +1677,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
                         (c_generics item.generics);
                     body = c_body body;
                     params;
-                    safety = csafety safety;
+                    safety = c_header_safety safety;
                   }
             | Const (_ty, e) ->
                 Fn
diff --git a/engine/lib/span.ml b/engine/lib/span.ml
index 3719c7815..a57c9c78e 100644
--- a/engine/lib/span.ml
+++ b/engine/lib/span.ml
@@ -15,7 +15,7 @@ module Imported = struct
 
   and file_name =
     | Real of real_file_name
-    | QuoteExpansion of string
+    | CfgSpec of string
     | Anon of string
     | MacroExpansion of string
     | ProcMacroSourceCode of string
@@ -36,7 +36,7 @@ module Imported = struct
           | LocalPath x -> LocalPath x
           | Remapped { local_path; virtual_name } ->
               Remapped { local_path; virtual_name })
-    | QuoteExpansion x -> QuoteExpansion x
+    | CfgSpec x -> CfgSpec x
     | Anon x -> Anon x
     | MacroExpansion x -> MacroExpansion x
     | ProcMacroSourceCode x -> ProcMacroSourceCode x
@@ -62,7 +62,7 @@ module Imported = struct
           | LocalPath x -> LocalPath x
           | Remapped { local_path; virtual_name } ->
               Remapped { local_path; virtual_name })
-    | QuoteExpansion x -> QuoteExpansion x
+    | CfgSpec x -> CfgSpec x
     | Anon x -> Anon x
     | MacroExpansion x -> MacroExpansion x
     | ProcMacroSourceCode x -> ProcMacroSourceCode x
diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs
index 1ffdc56b6..44d18d8a1 100644
--- a/engine/names/extract/build.rs
+++ b/engine/names/extract/build.rs
@@ -55,7 +55,7 @@ fn disambiguator_to_str(disambiguator: u32) -> String {
 
 fn def_path_item_to_str(path_item: DefPathItem) -> String {
     match path_item {
-        DefPathItem::TypeNs(s)
+        DefPathItem::TypeNs(Some(s))
         | DefPathItem::ValueNs(s)
         | DefPathItem::MacroNs(s)
         | DefPathItem::LifetimeNs(s) => s,
@@ -67,8 +67,7 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String {
         DefPathItem::Closure => "Closure".into(),
         DefPathItem::Ctor => "Ctor".into(),
         DefPathItem::AnonConst => "AnonConst".into(),
-        DefPathItem::OpaqueTy => "OpaqueTy".into(),
-        DefPathItem::AnonAdt => "AnonAdt".into(),
+        DefPathItem::TypeNs(None) | DefPathItem::OpaqueTy => "OpaqueTy".into(),
     }
 }
 
diff --git a/flake.lock b/flake.lock
index b36d4c753..b4290dff0 100644
--- a/flake.lock
+++ b/flake.lock
@@ -127,11 +127,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1736735482,
-        "narHash": "sha256-QOA4jCDyyUM9Y2Vba+HSZ/5LdtCMGaTE/7NkkUzBr50=",
+        "lastModified": 1743388531,
+        "narHash": "sha256-OBcNE+2/TD1AMgq8HKMotSQF8ZPJEFGZdRoBJ7t/HIc=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "cf960a1938ee91200fe0d2f7b2582fde2429d562",
+        "rev": "011de3c895927300651d9c2cb8e062adf17aa665",
         "type": "github"
       },
       "original": {
diff --git a/frontend/exporter/src/body.rs b/frontend/exporter/src/body.rs
index 77c27e0c1..654093ea9 100644
--- a/frontend/exporter/src/body.rs
+++ b/frontend/exporter/src/body.rs
@@ -60,7 +60,7 @@ mod module {
         // be local. It is safe to do so, because if we have access to HIR objects,
         // it necessarily means we are exploring a local item (we don't have
         // access to the HIR of external objects, only their MIR).
-        Body::body(s.base().tcx.hir().body_owner_def_id(id), s)
+        Body::body(s.base().tcx.hir_body_owner_def_id(id), s)
     }
 
     mod implementations {
diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs
index 61658e851..98310e42e 100644
--- a/frontend/exporter/src/constant_utils.rs
+++ b/frontend/exporter/src/constant_utils.rs
@@ -168,7 +168,7 @@ impl From<ConstantExpr> for Expr {
             Adt { info, fields } => ExprKind::Adt(AdtExpr {
                 info,
                 fields: fields.into_iter().map(|field| field.into()).collect(),
-                base: None,
+                base: AdtExprBase::None,
                 user_ty: None,
             }),
             // TODO: propagate the generics and trait refs (see #636)
diff --git a/frontend/exporter/src/constant_utils/uneval.rs b/frontend/exporter/src/constant_utils/uneval.rs
index f1e6e035b..9c90d21ef 100644
--- a/frontend/exporter/src/constant_utils/uneval.rs
+++ b/frontend/exporter/src/constant_utils/uneval.rs
@@ -184,7 +184,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx>
                 },
             },
 
-            ty::ConstKind::Value(ty, valtree) => valtree_to_constant_expr(s, valtree, ty, span),
+            ty::ConstKind::Value(val) => valtree_to_constant_expr(s, val.valtree, val.ty, span),
             ty::ConstKind::Error(_) => fatal!(s[span], "ty::ConstKind::Error"),
             ty::ConstKind::Expr(e) => fatal!(s[span], "ty::ConstKind::Expr {:#?}", e),
 
@@ -203,15 +203,15 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
     ty: rustc_middle::ty::Ty<'tcx>,
     span: rustc_span::Span,
 ) -> ConstantExpr {
-    let kind = match (valtree, ty.kind()) {
+    let kind = match (&*valtree, ty.kind()) {
         (_, ty::Ref(_, inner_ty, _)) => {
             ConstantExprKind::Borrow(valtree_to_constant_expr(s, valtree, *inner_ty, span))
         }
-        (ty::ValTree::Branch(valtrees), ty::Str) => {
+        (ty::ValTreeKind::Branch(valtrees), ty::Str) => {
             let bytes = valtrees
                 .iter()
-                .map(|x| match x {
-                    ty::ValTree::Leaf(leaf) => leaf.to_u8(),
+                .map(|x| match &***x {
+                    ty::ValTreeKind::Leaf(leaf) => leaf.to_u8(),
                     _ => fatal!(
                         s[span],
                         "Expected a flat list of leaves while translating \
@@ -221,7 +221,7 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
                 .collect();
             ConstantExprKind::Literal(ConstantLiteral::byte_str(bytes))
         }
-        (ty::ValTree::Branch(_), ty::Array(..) | ty::Tuple(..) | ty::Adt(..)) => {
+        (ty::ValTreeKind::Branch(_), ty::Array(..) | ty::Tuple(..) | ty::Adt(..)) => {
             let contents: rustc_middle::ty::DestructuredConst = s
                 .base()
                 .tcx
@@ -255,7 +255,7 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
                 _ => unreachable!(),
             }
         }
-        (ty::ValTree::Leaf(x), ty::RawPtr(_, _)) => {
+        (ty::ValTreeKind::Leaf(x), ty::RawPtr(_, _)) => {
             use crate::rustc_type_ir::inherent::Ty;
             let raw_address = x.to_bits_unchecked();
             let uint_ty = UintTy::Usize;
@@ -265,8 +265,8 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
                 source: ConstantExprKind::Literal(lit).decorate(usize_ty, span.sinto(s)),
             }
         }
-        (ty::ValTree::Leaf(x), _) => {
-            ConstantExprKind::Literal(scalar_int_to_constant_literal(s, x, ty))
+        (ty::ValTreeKind::Leaf(x), _) => {
+            ConstantExprKind::Literal(scalar_int_to_constant_literal(s, *x, ty))
         }
         _ => supposely_unreachable_fatal!(
             s[span], "valtree_to_expr";
diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs
index 5a48765c7..fe3b58896 100644
--- a/frontend/exporter/src/lib.rs
+++ b/frontend/exporter/src/lib.rs
@@ -24,11 +24,12 @@ cfg_feature_rustc! {
     extern crate rustc_abi;
     extern crate rustc_ast;
     extern crate rustc_ast_pretty;
-    extern crate rustc_attr;
+    extern crate rustc_attr_data_structures;
     extern crate rustc_apfloat;
     extern crate rustc_const_eval;
     extern crate rustc_data_structures;
     extern crate rustc_driver;
+    extern crate rustc_hashes;
     extern crate rustc_errors;
     extern crate rustc_hir;
     extern crate rustc_hir_analysis;
diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs
index 87c0660fe..1d7f51bfc 100644
--- a/frontend/exporter/src/rustc_utils.rs
+++ b/frontend/exporter/src/rustc_utils.rs
@@ -15,7 +15,7 @@ impl<'tcx, T: ty::TypeFoldable<ty::TyCtxt<'tcx>>> ty::Binder<'tcx, T> {
 #[tracing::instrument(skip(s))]
 pub(crate) fn get_variant_information<'s, S: UnderOwnerState<'s>>(
     adt_def: &ty::AdtDef<'s>,
-    variant_index: rustc_target::abi::VariantIdx,
+    variant_index: rustc_abi::VariantIdx,
     s: &S,
 ) -> VariantInformations {
     fn is_named<'s, I: std::iter::Iterator<Item = &'s ty::FieldDef> + Clone>(it: I) -> bool {
@@ -96,9 +96,8 @@ pub(crate) fn attribute_from_scope<'tcx, S: ExprState<'tcx>>(
     let scope_tree = tcx.region_scope_tree(owner);
     let hir_id = scope.hir_id(scope_tree);
     let tcx = s.base().tcx;
-    let map = tcx.hir();
     let attributes = hir_id
-        .map(|hir_id| map.attrs(hir_id).sinto(s))
+        .map(|hir_id| tcx.hir_attrs(hir_id).sinto(s))
         .unwrap_or_default();
     (hir_id, attributes)
 }
diff --git a/frontend/exporter/src/sinto.rs b/frontend/exporter/src/sinto.rs
index 84342c983..fc58f735f 100644
--- a/frontend/exporter/src/sinto.rs
+++ b/frontend/exporter/src/sinto.rs
@@ -90,12 +90,6 @@ impl<S, D: Clone, T: SInto<S, D>> SInto<S, Vec<D>> for Vec<T> {
         self.iter().map(|x| x.sinto(s)).collect()
     }
 }
-#[cfg(feature = "rustc")]
-impl<S> SInto<S, Vec<u8>> for rustc_data_structures::sync::Lrc<[u8]> {
-    fn sinto(&self, _s: &S) -> Vec<u8> {
-        (**self).to_vec()
-    }
-}
 
 macro_rules! sinto_clone {
     ($t:ty) => {
diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
index 1ff95dc12..a187ffdaf 100644
--- a/frontend/exporter/src/traits.rs
+++ b/frontend/exporter/src/traits.rs
@@ -7,6 +7,7 @@ mod utils;
 #[cfg(feature = "rustc")]
 pub use utils::{
     erase_and_norm, implied_predicates, predicates_defined_on, required_predicates, self_predicate,
+    ToPolyTraitRef,
 };
 
 #[cfg(feature = "rustc")]
@@ -131,7 +132,6 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
     clause: rustc_middle::ty::Clause<'tcx>,
     span: rustc_span::Span,
 ) -> Option<(Clause, ImplExpr, Span)> {
-    use rustc_middle::ty::ToPolyTraitRef;
     let tcx = s.base().tcx;
     let impl_trait_ref = tcx
         .impl_trait_ref(impl_did)
@@ -248,7 +248,6 @@ fn solve_item_traits_inner<'tcx, S: UnderOwnerState<'tcx>>(
     generics: ty::GenericArgsRef<'tcx>,
     predicates: ty::GenericPredicates<'tcx>,
 ) -> Vec<ImplExpr> {
-    use crate::rustc_middle::ty::ToPolyTraitRef;
     let tcx = s.base().tcx;
     let typing_env = s.typing_env();
     predicates
diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs
index 776f0cd04..3d6a56c1e 100644
--- a/frontend/exporter/src/traits/resolution.rs
+++ b/frontend/exporter/src/traits/resolution.rs
@@ -13,7 +13,7 @@ use rustc_trait_selection::traits::ImplSource;
 
 use crate::{self_predicate, traits::utils::erase_and_norm};
 
-use super::utils::{implied_predicates, required_predicates};
+use super::utils::{implied_predicates, required_predicates, ToPolyTraitRef};
 
 #[derive(Debug, Clone)]
 pub enum PathChunk<'tcx> {
@@ -552,7 +552,7 @@ pub fn shallow_resolve_trait_ref<'tcx>(
         Ok(Some(selection)) => selection,
         Ok(None) => return Err(CodegenObligationError::Ambiguity),
         Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented),
-        Err(_) => return Err(CodegenObligationError::FulfillmentError),
+        Err(_) => return Err(CodegenObligationError::Ambiguity),
     };
 
     // Currently, we use a fulfillment context to completely resolve
@@ -567,7 +567,7 @@ pub fn shallow_resolve_trait_ref<'tcx>(
 
     let errors = ocx.select_all_or_error();
     if !errors.is_empty() {
-        return Err(CodegenObligationError::FulfillmentError);
+        return Err(CodegenObligationError::Ambiguity);
     }
 
     let impl_source = infcx.resolve_vars_if_possible(impl_source);
@@ -575,7 +575,7 @@ pub fn shallow_resolve_trait_ref<'tcx>(
 
     if impl_source.has_infer() {
         // Unused lifetimes on an impl get replaced with inference vars, but never resolved.
-        return Err(CodegenObligationError::FulfillmentError);
+        return Err(CodegenObligationError::Ambiguity);
     }
 
     Ok(impl_source)
diff --git a/frontend/exporter/src/traits/utils.rs b/frontend/exporter/src/traits/utils.rs
index a5d1971b0..7a77bcff7 100644
--- a/frontend/exporter/src/traits/utils.rs
+++ b/frontend/exporter/src/traits/utils.rs
@@ -170,3 +170,13 @@ where
             .unwrap_or(x),
     )
 }
+
+pub trait ToPolyTraitRef<'tcx> {
+    fn to_poly_trait_ref(&self) -> PolyTraitRef<'tcx>;
+}
+
+impl<'tcx> ToPolyTraitRef<'tcx> for PolyTraitPredicate<'tcx> {
+    fn to_poly_trait_ref(&self) -> PolyTraitRef<'tcx> {
+        self.map_bound_ref(|trait_pred| trait_pred.trait_ref)
+    }
+}
diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs
index d5e59b04a..fac5dddb0 100644
--- a/frontend/exporter/src/types/def_id.rs
+++ b/frontend/exporter/src/types/def_id.rs
@@ -273,10 +273,10 @@ impl std::convert::From<DefId> for Path {
     fn from(v: DefId) -> Vec<String> {
         std::iter::once(&v.krate)
             .chain(v.path.iter().filter_map(|item| match &item.data {
-                DefPathItem::TypeNs(s)
-                | DefPathItem::ValueNs(s)
-                | DefPathItem::MacroNs(s)
-                | DefPathItem::LifetimeNs(s) => Some(s),
+                DefPathItem::TypeNs(s) => s.as_ref(),
+                DefPathItem::ValueNs(s) | DefPathItem::MacroNs(s) | DefPathItem::LifetimeNs(s) => {
+                    Some(s)
+                }
                 _ => None,
             }))
             .cloned()
@@ -308,7 +308,7 @@ pub enum DefPathItem {
     ForeignMod,
     Use,
     GlobalAsm,
-    TypeNs(Symbol),
+    TypeNs(Option<Symbol>),
     ValueNs(Symbol),
     MacroNs(Symbol),
     LifetimeNs(Symbol),
@@ -316,7 +316,6 @@ pub enum DefPathItem {
     Ctor,
     AnonConst,
     OpaqueTy,
-    AnonAdt,
 }
 
 #[derive_group(Serializers)]
diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs
index e7ac483c9..e4b5a747b 100644
--- a/frontend/exporter/src/types/hir.rs
+++ b/frontend/exporter/src/types/hir.rs
@@ -103,22 +103,31 @@ pub struct FnSig {
     pub span: Span,
 }
 
+#[derive(AdtInto, JsonSchema)]
+#[args(<S>, from: hir::HeaderSafety, state: S as _s)]
+#[derive_group(Serializers)]
+#[derive(Clone, Debug, Hash, PartialEq, Eq, PartialOrd, Ord)]
+pub enum HeaderSafety {
+    SafeTargetFeatures,
+    Normal(Safety),
+}
+
 /// Reflects [`hir::FnHeader`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema)]
 #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: hir::FnHeader, state: S as tcx)]
 pub struct FnHeader {
-    pub safety: Safety,
+    pub safety: HeaderSafety,
     pub constness: Constness,
     pub asyncness: IsAsync,
-    pub abi: Abi,
+    pub abi: ExternAbi,
 }
 
-/// Reflects [`rustc_target::spec::abi::Abi`]
+/// Reflects [`rustc_abi::ExternAbi`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_target::spec::abi::Abi, state: S as s)]
-pub enum Abi {
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_abi::ExternAbi, state: S as s)]
+pub enum ExternAbi {
     Rust,
     C {
         unwind: bool,
@@ -146,19 +155,17 @@ impl<'x: 'tcx, 'tcx, S: UnderOwnerState<'tcx>> SInto<S, Ty> for hir::Ty<'x> {
         // be local. It is safe to do so, because if we have access to a HIR ty,
         // it necessarily means we are exploring a local item (we don't have
         // access to the HIR of external objects, only their MIR).
-        let ctx =
-            rustc_hir_analysis::collect::ItemCtxt::new(s.base().tcx, s.owner_id().expect_local());
-        ctx.lower_ty(self).sinto(s)
+        rustc_hir_analysis::lower_ty(s.base().tcx, self).sinto(s)
     }
 }
 
 /// Reflects [`hir::UseKind`]
 #[derive(AdtInto)]
-#[args(<S>, from: hir::UseKind, state: S as _s)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: hir::UseKind, state: S as _s)]
 #[derive_group(Serializers)]
 #[derive(Clone, Debug, JsonSchema)]
 pub enum UseKind {
-    Single,
+    Single(Ident),
     Glob,
     ListStem,
 }
@@ -221,7 +228,7 @@ pub struct Generics<Body: IsBody> {
 impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, ImplItem<Body>> for hir::ImplItemRef {
     fn sinto(&self, s: &S) -> ImplItem<Body> {
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        let impl_item = tcx.hir().impl_item(self.id);
+        let impl_item = tcx.hir_impl_item(self.id);
         let s = with_owner_id(s.base(), (), (), impl_item.owner_id.to_def_id());
         impl_item.sinto(&s)
     }
@@ -267,7 +274,6 @@ pub struct AnonConst<Body: IsBody> {
 pub struct ConstArg<Body: IsBody> {
     pub hir_id: HirId,
     pub kind: ConstArgKind<Body>,
-    pub is_desugared_from_effects: bool,
 }
 
 /// Reflects [`hir::ConstArgKind`]
@@ -277,6 +283,8 @@ pub struct ConstArg<Body: IsBody> {
 pub enum ConstArgKind<Body: IsBody> {
     Path(QPath),
     Anon(AnonConst<Body>),
+    #[todo]
+    Infer(String),
 }
 
 /// Reflects [`hir::GenericParamKind`]
@@ -321,7 +329,7 @@ pub struct GenericParam<Body: IsBody> {
             }),
         hir::ParamName::Fresh =>
             ParamName::Fresh,
-        hir::ParamName::Error =>
+        hir::ParamName::Error { .. } =>
             ParamName::Error,
     })]
     pub name: ParamName,
@@ -329,7 +337,7 @@ pub struct GenericParam<Body: IsBody> {
     pub pure_wrt_drop: bool,
     pub kind: GenericParamKind<Body>,
     pub colon_span: Option<Span>,
-    #[value(s.base().tcx.hir().attrs(*hir_id).sinto(s))]
+    #[value(s.base().tcx.hir_attrs(*hir_id).sinto(s))]
     attributes: Vec<Attribute>,
 }
 
@@ -488,7 +496,7 @@ pub struct HirFieldDef {
     pub hir_id: HirId,
     pub def_id: GlobalIdent,
     pub ty: Ty,
-    #[value(s.base().tcx.hir().attrs(*hir_id).sinto(s))]
+    #[value(s.base().tcx.hir_attrs(*hir_id).sinto(s))]
     attributes: Vec<Attribute>,
 }
 
@@ -515,7 +523,7 @@ pub struct Variant<Body: IsBody> {
     })]
     pub discr: DiscriminantDefinition,
     pub span: Span,
-    #[value(s.base().tcx.hir().attrs(*hir_id).sinto(s))]
+    #[value(s.base().tcx.hir_attrs(*hir_id).sinto(s))]
     pub attributes: Vec<Attribute>,
 }
 
@@ -532,10 +540,9 @@ pub struct UsePath {
     #[value(self.segments.iter().last().and_then(|segment| {
             match s.base().tcx.hir_node_by_def_id(segment.hir_id.owner.def_id) {
                 hir::Node::Item(hir::Item {
-                    ident,
-                    kind: hir::ItemKind::Use(_, _),
+                    kind: hir::ItemKind::Use(_, hir::UseKind::Single(ident)),
                     ..
-                }) if ident.name.to_ident_string() != "" => Some(ident.name.to_ident_string()),
+                }) => Some(ident.name.to_ident_string()),
                 _ => None,
             }
         }))]
@@ -611,24 +618,36 @@ pub struct PathSegment {
 #[derive_group(Serializers)]
 #[derive(Clone, Debug, JsonSchema)]
 pub enum ItemKind<Body: IsBody> {
-    ExternCrate(Option<Symbol>),
+    ExternCrate(Option<Symbol>, Ident),
     Use(UsePath, UseKind),
-    Static(Ty, Mutability, Body),
-    Const(Ty, Generics<Body>, Body),
+    Static(Ident, Ty, Mutability, Body),
+    Const(Ident, Ty, Generics<Body>, Body),
     #[custom_arm(
-            hir::ItemKind::Fn(sig, generics, body) => {
-                ItemKind::Fn(generics.sinto(s), make_fn_def::<Body, _>(sig, body, s))
+        hir::ItemKind::Fn{ ident, sig, generics, body, .. } => {
+            ItemKind::Fn {
+                ident: ident.sinto(s),
+                generics: generics.sinto(s),
+                def: make_fn_def::<Body, _>(sig, body, s),
             }
-        )]
-    Fn(Generics<Body>, FnDef<Body>),
-    Macro(MacroDef, MacroKind),
-    Mod(Vec<Item<Body>>),
+        }
+    )]
+    Fn {
+        ident: Ident,
+        generics: Generics<Body>,
+        def: FnDef<Body>,
+    },
+
+    Macro(Ident, MacroDef, MacroKind),
+    Mod(Ident, Vec<Item<Body>>),
     ForeignMod {
-        abi: Abi,
+        abi: ExternAbi,
         items: Vec<ForeignItem<Body>>,
     },
-    GlobalAsm(InlineAsm),
+    GlobalAsm {
+        asm: InlineAsm,
+    },
     TyAlias(
+        Ident,
         #[map({
             let s = &State {
                 base: Base {ty_alias_mode: true, ..s.base()},
@@ -643,6 +662,7 @@ pub enum ItemKind<Body: IsBody> {
         Generics<Body>,
     ),
     Enum(
+        Ident,
         EnumDef<Body>,
         Generics<Body>,
         #[value({
@@ -651,16 +671,17 @@ pub enum ItemKind<Body: IsBody> {
         })]
         ReprOptions,
     ),
-    Struct(VariantData, Generics<Body>),
-    Union(VariantData, Generics<Body>),
+    Struct(Ident, VariantData, Generics<Body>),
+    Union(Ident, VariantData, Generics<Body>),
     Trait(
         IsAuto,
         Safety,
+        Ident,
         Generics<Body>,
         GenericBounds,
         Vec<TraitItem<Body>>,
     ),
-    TraitAlias(Generics<Body>, GenericBounds),
+    TraitAlias(Ident, Generics<Body>, GenericBounds),
     Impl(Impl<Body>),
 }
 
@@ -679,7 +700,7 @@ pub enum TraitItemKind<Body: IsBody> {
         }
     )]
     /// Reflects a required [`hir::TraitItemKind::Fn`]
-    RequiredFn(FnSig, Vec<Ident>),
+    RequiredFn(FnSig, Vec<Option<Ident>>),
     #[custom_arm(
         hir::TraitItemKind::Fn(sig, hir::TraitFn::Provided(body)) => {
             TraitItemKind::ProvidedFn(sig.sinto(tcx), make_fn_def::<Body, _>(sig, body, tcx))
@@ -724,7 +745,7 @@ impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto<S, TraitItem<Body>> for hir
     fn sinto(&self, s: &S) -> TraitItem<Body> {
         let s = with_owner_id(s.base(), (), (), self.id.owner_id.to_def_id());
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        tcx.hir().trait_item(self.id).sinto(&s)
+        tcx.hir_trait_item(self.id).sinto(&s)
     }
 }
 
@@ -734,7 +755,7 @@ impl<'a, 'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, Vec<Item<Body>>>
         let tcx = s.base().tcx;
         self.item_ids
             .iter()
-            .map(|id| tcx.hir().item(*id).sinto(s))
+            .map(|id| tcx.hir_item(*id).sinto(s))
             .collect()
     }
 }
@@ -745,7 +766,7 @@ impl<'a, 'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, Vec<Item<Body>>>
 #[derive(Clone, Debug, JsonSchema)]
 #[derive_group(Serializers)]
 pub enum ForeignItemKind<Body: IsBody> {
-    Fn(FnSig, Vec<Ident>, Generics<Body>),
+    Fn(FnSig, Vec<Option<Ident>>, Generics<Body>),
     Static(Ty, Mutability, Safety),
     Type,
 }
@@ -767,7 +788,7 @@ pub struct ForeignItem<Body: IsBody> {
 impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto<S, ForeignItem<Body>> for hir::ForeignItemRef {
     fn sinto(&self, s: &S) -> ForeignItem<Body> {
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        tcx.hir().foreign_item(self.id).sinto(s)
+        tcx.hir_foreign_item(self.id).sinto(s)
     }
 }
 
@@ -889,7 +910,25 @@ pub struct Item<Body: IsBody> {
 #[cfg(feature = "rustc")]
 impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto<S, Item<Body>> for hir::Item<'tcx> {
     fn sinto(&self, s: &S) -> Item<Body> {
-        let name: String = self.ident.name.to_ident_string();
+        use hir::ItemKind::*;
+        // TODO: Not all items have an identifier; return `Option` here, or even better: use the
+        // ident in the `ItemKind`.
+        let name = match self.kind {
+            ExternCrate(_, i)
+            | Use(_, hir::UseKind::Single(i))
+            | Static(i, ..)
+            | Const(i, ..)
+            | Fn { ident: i, .. }
+            | Macro(i, ..)
+            | Mod(i, ..)
+            | TyAlias(i, ..)
+            | Enum(i, ..)
+            | Struct(i, ..)
+            | Union(i, ..)
+            | Trait(_, _, i, ..)
+            | TraitAlias(i, ..) => i.name.to_ident_string(),
+            Use(..) | ForeignMod { .. } | GlobalAsm { .. } | Impl { .. } => String::new(),
+        };
         let s = &with_owner_id(s.base(), (), (), self.owner_id.to_def_id());
         let owner_id: DefId = self.owner_id.sinto(s);
         let def_id = Path::from(owner_id.clone())
@@ -910,7 +949,7 @@ impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto<S, Item<Body>> for hir::Item<
 impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto<S, Item<Body>> for hir::ItemId {
     fn sinto(&self, s: &S) -> Item<Body> {
         let tcx: rustc_middle::ty::TyCtxt = s.base().tcx;
-        tcx.hir().item(*self).sinto(s)
+        tcx.hir_item(*self).sinto(s)
     }
 }
 
@@ -918,42 +957,59 @@ impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto<S, Item<Body>> for hir::ItemI
 pub type Ident = (Symbol, Span);
 
 #[cfg(feature = "rustc")]
-impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Ident> for rustc_span::symbol::Ident {
+impl<'tcx, S: BaseState<'tcx>> SInto<S, Ident> for rustc_span::symbol::Ident {
     fn sinto(&self, s: &S) -> Ident {
         (self.name.sinto(s), self.span.sinto(s))
     }
 }
 
-/// Reflects [`rustc_ast::ast::AttrStyle`]
+/// Reflects [`rustc_ast::AttrStyle`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<S>, from: rustc_ast::ast::AttrStyle, state: S as _s)]
+#[args(<S>, from: rustc_ast::AttrStyle, state: S as _s)]
 pub enum AttrStyle {
     Outer,
     Inner,
 }
 
-/// Reflects [`rustc_ast::ast::Attribute`]
+/// Reflects [`rustc_ast::Attribute`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::Attribute, state: S as gstate)]
-pub struct Attribute {
-    pub kind: AttrKind,
-    #[map(x.as_usize())]
-    pub id: usize,
-    pub style: AttrStyle,
-    pub span: Span,
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_hir::Attribute, state: S as gstate)]
+pub enum Attribute {
+    Parsed(AttributeKind),
+    Unparsed(AttrItem),
+}
+
+/// Reflects [`rustc_attr_data_structures::AttributeKind`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::AttributeKind, state: S as tcx)]
+#[derive_group(Serializers)]
+#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+pub enum AttributeKind {
+    DocComment {
+        style: AttrStyle,
+        kind: CommentKind,
+        span: Span,
+        comment: Symbol,
+    },
+    #[todo]
+    Other(String),
 }
 
-/// Reflects [`rustc_attr::InlineAttr`]
+/// Reflects [`rustc_attr_data_structures::InlineAttr`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr::InlineAttr, state: S as _s)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::InlineAttr, state: S as _s)]
 pub enum InlineAttr {
     None,
     Hint,
     Always,
     Never,
+    Force {
+        attr_span: Span,
+        reason: Option<Symbol>,
+    },
 }
 
 /// Reflects [`rustc_ast::ast::BindingMode`]
@@ -1027,35 +1083,20 @@ pub enum CommentKind {
     Block,
 }
 
-/// Reflects [`rustc_ast::ast::AttrArgs`]
+/// Reflects [`rustc_hir::AttrArgs`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgs, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_hir::AttrArgs, state: S as tcx)]
 #[derive_group(Serializers)]
 #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
 pub enum AttrArgs {
     Empty,
     Delimited(DelimArgs),
-
-    Eq(Span, AttrArgsEq),
-    // #[todo]
-    // Todo(String),
+    Eq { eq_span: Span, expr: MetaItemLit },
 }
 
-/// Reflects [`rustc_ast::ast::AttrArgsEq`]
+/// Reflects [`rustc_ast::MetaItemLit`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgsEq, state: S as tcx)]
-#[derive_group(Serializers)]
-#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-pub enum AttrArgsEq {
-    Hir(MetaItemLit),
-    #[todo]
-    Ast(String),
-    // Ast(P<Expr>),
-}
-
-/// Reflects [`rustc_ast::ast::MetaItemLit`]
-#[derive(AdtInto)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::MetaItemLit, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::MetaItemLit, state: S as tcx)]
 #[derive_group(Serializers)]
 #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
 pub struct MetaItemLit {
@@ -1065,16 +1106,15 @@ pub struct MetaItemLit {
     pub span: Span,
 }
 
-/// Reflects [`rustc_ast::ast::AttrItem`]
-#[derive(AdtInto)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrItem, state: S as tcx)]
+/// Reflects [`rustc_hir::AttrItem`]
 #[derive_group(Serializers)]
-#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_hir::AttrItem, state: S as gstate)]
 pub struct AttrItem {
-    #[map(rustc_ast_pretty::pprust::path_to_string(x))]
+    #[map(x.to_string())]
     pub path: String,
     pub args: AttrArgs,
-    pub tokens: Option<TokenStream>,
+    pub span: Span,
 }
 
 #[cfg(feature = "rustc")]
@@ -1085,26 +1125,6 @@ impl<S> SInto<S, String> for rustc_ast::tokenstream::LazyAttrTokenStream {
     }
 }
 
-/// Reflects [`rustc_ast::ast::NormalAttr`]
-#[derive(AdtInto)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::NormalAttr, state: S as tcx)]
-#[derive_group(Serializers)]
-#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-pub struct NormalAttr {
-    pub item: AttrItem,
-    pub tokens: Option<TokenStream>,
-}
-
-/// Reflects [`rustc_ast::AttrKind`]
-#[derive(AdtInto)]
-#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::AttrKind, state: S as tcx)]
-#[derive_group(Serializers)]
-#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-pub enum AttrKind {
-    Normal(NormalAttr),
-    DocComment(CommentKind, Symbol),
-}
-
 sinto_todo!(rustc_hir, GenericArgs<'a> as HirGenericArgs);
 sinto_todo!(rustc_hir, InlineAsm<'a>);
 sinto_todo!(rustc_hir, MissingLifetimeKind);
diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs
index c10d35db8..5e68f1c61 100644
--- a/frontend/exporter/src/types/mir.rs
+++ b/frontend/exporter/src/types/mir.rs
@@ -812,31 +812,29 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
             let cur_ty = current_ty;
             let cur_kind = current_kind.clone();
             use rustc_middle::ty::TyKind;
-            let mk_field =
-                |index: &rustc_target::abi::FieldIdx,
-                 variant_idx: Option<rustc_target::abi::VariantIdx>| {
-                    ProjectionElem::Field(match cur_ty.kind() {
-                        TyKind::Adt(adt_def, _) => {
-                            assert!(
-                                ((adt_def.is_struct() || adt_def.is_union())
-                                    && variant_idx.is_none())
-                                    || (adt_def.is_enum() && variant_idx.is_some())
-                            );
-                            ProjectionElemFieldKind::Adt {
-                                typ: adt_def.did().sinto(s),
-                                variant: variant_idx.map(|id| id.sinto(s)),
-                                index: index.sinto(s),
-                            }
-                        }
-                        TyKind::Tuple(_types) => ProjectionElemFieldKind::Tuple(index.sinto(s)),
-                        ty_kind => {
-                            supposely_unreachable_fatal!(
-                                s, "ProjectionElemFieldBadType";
-                                {index, ty_kind, variant_idx, &cur_ty, &cur_kind}
-                            );
+            let mk_field = |index: &rustc_abi::FieldIdx,
+                            variant_idx: Option<rustc_abi::VariantIdx>| {
+                ProjectionElem::Field(match cur_ty.kind() {
+                    TyKind::Adt(adt_def, _) => {
+                        assert!(
+                            ((adt_def.is_struct() || adt_def.is_union()) && variant_idx.is_none())
+                                || (adt_def.is_enum() && variant_idx.is_some())
+                        );
+                        ProjectionElemFieldKind::Adt {
+                            typ: adt_def.did().sinto(s),
+                            variant: variant_idx.map(|id| id.sinto(s)),
+                            index: index.sinto(s),
                         }
-                    })
-                };
+                    }
+                    TyKind::Tuple(_types) => ProjectionElemFieldKind::Tuple(index.sinto(s)),
+                    ty_kind => {
+                        supposely_unreachable_fatal!(
+                            s, "ProjectionElemFieldBadType";
+                            {index, ty_kind, variant_idx, &cur_ty, &cur_kind}
+                        );
+                    }
+                })
+            };
             let elem_kind: ProjectionElem = match elems {
                 [Downcast(_, variant_idx), Field(index, ty), rest @ ..] => {
                     elems = rest;
@@ -924,6 +922,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
                         // and `fn(‘static ())` (according to @compiler-errors on Zulip).
                         Subtype { .. } => panic!("unexpected Subtype"),
                         Downcast { .. } => panic!("unexpected Downcast"),
+                        UnwrapUnsafeBinder { .. } => panic!("unsupported feature: unsafe binders"),
                     }
                 }
                 [] => break,
@@ -1012,8 +1011,9 @@ pub enum CoercionSource {
 pub enum NullOp {
     SizeOf,
     AlignOf,
-    OffsetOf(Vec<(usize, FieldIdx)>),
+    OffsetOf(Vec<(VariantIdx, FieldIdx)>),
     UbChecks,
+    ContractChecks,
 }
 
 #[derive_group(Serializers)]
@@ -1030,7 +1030,7 @@ pub enum Rvalue {
     Repeat(Operand, ConstantExpr),
     Ref(Region, BorrowKind, Place),
     ThreadLocalRef(DefId),
-    RawPtr(Mutability, Place),
+    RawPtr(RawPtrKind, Place),
     Len(Place),
     Cast(CastKind, Operand, Ty),
     BinaryOp(BinOp, (Operand, Operand)),
@@ -1040,6 +1040,16 @@ pub enum Rvalue {
     Aggregate(AggregateKind, IndexVec<FieldIdx, Operand>),
     ShallowInitBox(Operand, Ty),
     CopyForDeref(Place),
+    WrapUnsafeBinder(Operand, Ty),
+}
+
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_middle::mir::RawPtrKind, state: S as _s)]
+pub enum RawPtrKind {
+    Mut,
+    Const,
+    FakeForPtrMetadata,
 }
 
 #[derive_group(Serializers)]
@@ -1055,7 +1065,7 @@ make_idx_wrapper!(rustc_middle::mir, BasicBlock);
 make_idx_wrapper!(rustc_middle::mir, SourceScope);
 make_idx_wrapper!(rustc_middle::mir, Local);
 make_idx_wrapper!(rustc_middle::ty, UserTypeAnnotationIndex);
-make_idx_wrapper!(rustc_target::abi, FieldIdx);
+make_idx_wrapper!(rustc_abi, FieldIdx);
 
 /// Reflects [`rustc_middle::mir::UnOp`]
 #[derive_group(Serializers)]
diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs
index ebacfad24..46f56a1bb 100644
--- a/frontend/exporter/src/types/new/full_def.rs
+++ b/frontend/exporter/src/types/new/full_def.rs
@@ -127,9 +127,9 @@ pub enum FullDefKind<Body> {
         #[value(get_param_env(s, s.owner_id()))]
         param_env: ParamEnv,
         /// `Some` if the item is in the local crate.
-        #[value(s.base().tcx.hir().get_if_local(s.owner_id()).map(|node| {
+        #[value(s.base().tcx.hir_get_if_local(s.owner_id()).map(|node| {
             let rustc_hir::Node::Item(item) = node else { unreachable!() };
-            let rustc_hir::ItemKind::TyAlias(ty, _generics) = &item.kind else { unreachable!() };
+            let rustc_hir::ItemKind::TyAlias(_, ty, _generics) = &item.kind else { unreachable!() };
             let mut s = State::from_under_owner(s);
             s.base.ty_alias_mode = true;
             ty.sinto(&s)
@@ -539,7 +539,7 @@ fn get_def_attrs<'tcx>(
     tcx: ty::TyCtxt<'tcx>,
     def_id: RDefId,
     def_kind: RDefKind,
-) -> &'tcx [rustc_ast::ast::Attribute] {
+) -> &'tcx [rustc_hir::Attribute] {
     use RDefKind::*;
     match def_kind {
         // These kinds cause `get_attrs_unchecked` to panic.
@@ -555,7 +555,7 @@ fn get_mod_children<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> Vec<RDefId>
         Some(ldid) => match tcx.hir_node_by_def_id(ldid) {
             rustc_hir::Node::Crate(m)
             | rustc_hir::Node::Item(&rustc_hir::Item {
-                kind: rustc_hir::ItemKind::Mod(m),
+                kind: rustc_hir::ItemKind::Mod(_, m),
                 ..
             }) => m
                 .item_ids
diff --git a/frontend/exporter/src/types/new/item_attributes.rs b/frontend/exporter/src/types/new/item_attributes.rs
index aeebd92c0..c12949902 100644
--- a/frontend/exporter/src/types/new/item_attributes.rs
+++ b/frontend/exporter/src/types/new/item_attributes.rs
@@ -39,12 +39,11 @@ impl ItemAttributes {
         }
         use rustc_hir::hir_id::HirId;
         let tcx = s.base().tcx;
-        let hir = tcx.hir();
-        let attrs_of = |id| tcx.hir().attrs(HirId::from(id)).sinto(s);
+        let attrs_of = |id| tcx.hir_attrs(HirId::from(id)).sinto(s);
         ItemAttributes {
             attributes: attrs_of(oid),
-            parent_attributes: hir
-                .parent_owner_iter(HirId::from(oid))
+            parent_attributes: tcx
+                .hir_parent_owner_iter(HirId::from(oid))
                 .map(|(oid, _)| oid)
                 .flat_map(attrs_of)
                 .collect(),
diff --git a/frontend/exporter/src/types/new/variant_infos.rs b/frontend/exporter/src/types/new/variant_infos.rs
index d43f1b8d5..bdeb2402d 100644
--- a/frontend/exporter/src/types/new/variant_infos.rs
+++ b/frontend/exporter/src/types/new/variant_infos.rs
@@ -21,7 +21,7 @@ pub enum VariantKind {
     },
 }
 
-sinto_as_usize!(rustc_target::abi, VariantIdx);
+sinto_as_usize!(rustc_abi, VariantIdx);
 
 /// Describe a variant
 #[derive_group(Serializers)]
diff --git a/frontend/exporter/src/types/span.rs b/frontend/exporter/src/types/span.rs
index 97a447175..b04a26a88 100644
--- a/frontend/exporter/src/types/span.rs
+++ b/frontend/exporter/src/types/span.rs
@@ -115,7 +115,7 @@ pub enum RealFileName {
 }
 
 #[cfg(feature = "rustc")]
-impl<S> SInto<S, u64> for rustc_data_structures::stable_hasher::Hash64 {
+impl<S> SInto<S, u64> for rustc_hashes::Hash64 {
     fn sinto(&self, _: &S) -> u64 {
         self.as_u64()
     }
@@ -128,7 +128,7 @@ impl<S> SInto<S, u64> for rustc_data_structures::stable_hasher::Hash64 {
 #[derive(Clone, Debug, JsonSchema, PartialEq, Eq, Hash, PartialOrd, Ord)]
 pub enum FileName {
     Real(RealFileName),
-    QuoteExpansion(u64),
+    CfgSpec(u64),
     Anon(u64),
     MacroExpansion(u64),
     ProcMacroSourceCode(u64),
diff --git a/frontend/exporter/src/types/thir.rs b/frontend/exporter/src/types/thir.rs
index f16449d51..44a9e90c3 100644
--- a/frontend/exporter/src/types/thir.rs
+++ b/frontend/exporter/src/types/thir.rs
@@ -33,6 +33,15 @@ pub struct FruInfo {
     pub field_types: Vec<Ty>,
 }
 
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema)]
+#[args(<'tcx, S: ExprState<'tcx>>, from: thir::AdtExprBase<'tcx>, state: S as gstate)]
+pub enum AdtExprBase {
+    None,
+    Base(FruInfo),
+    DefaultFields(Vec<Ty>),
+}
+
 /// A field expression: a field name along with a value
 #[derive_group(Serializers)]
 #[derive(Clone, Debug, JsonSchema)]
@@ -48,7 +57,7 @@ pub struct AdtExpr {
     pub info: VariantInformations,
     pub user_ty: Option<CanonicalUserType>,
     pub fields: Vec<FieldExpr>,
-    pub base: Option<FruInfo>,
+    pub base: AdtExprBase,
 }
 
 #[cfg(feature = "rustc")]
@@ -136,7 +145,7 @@ sinto_as_usize!(rustc_middle::middle::region, FirstStatementIndex);
 #[derive(AdtInto, Clone, Debug, JsonSchema)]
 #[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_middle::middle::region::Scope, state: S as gstate)]
 pub struct Scope {
-    pub id: ItemLocalId,
+    pub local_id: ItemLocalId,
     pub data: ScopeData,
 }
 
@@ -226,9 +235,9 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> for thir::Expr<'tcx> {
                         supposely_unreachable_fatal!(s[span], "PhantomDataNotAdt"; {kind, ty})
                     };
                     let adt_def = AdtExpr {
-                        info: get_variant_information(def, rustc_target::abi::FIRST_VARIANT, s),
+                        info: get_variant_information(def, rustc_abi::FIRST_VARIANT, s),
                         user_ty: None,
-                        base: None,
+                        base: AdtExprBase::None,
                         fields: vec![],
                     };
                     return Expr {
@@ -348,7 +357,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Pat> for thir::Pat<'tcx> {
                 rustc_middle::ty::TyKind::Adt(adt_def, args) => (thir::PatKind::Variant {
                     adt_def: *adt_def,
                     args,
-                    variant_index: rustc_target::abi::VariantIdx::from_usize(0),
+                    variant_index: rustc_abi::VariantIdx::from_usize(0),
                     subpatterns: subpatterns.clone(),
                 })
                 .sinto(s),
@@ -566,7 +575,7 @@ pub struct Param {
     pub self_kind: Option<ImplicitSelfKind>,
     pub hir_id: Option<HirId>,
     #[value(hir_id.map(|id| {
-        s.base().tcx.hir().attrs(id).sinto(s)
+        s.base().tcx.hir_attrs(id).sinto(s)
     }).unwrap_or(vec![]))]
     /// attributes on this parameter
     pub attributes: Vec<Attribute>,
diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs
index abf4ac155..b144f1b42 100644
--- a/frontend/exporter/src/types/ty.rs
+++ b/frontend/exporter/src/types/ty.rs
@@ -382,7 +382,17 @@ pub struct EarlyParamRegion {
 #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegion, state: S as gstate)]
 pub struct LateParamRegion {
     pub scope: DefId,
-    pub bound_region: BoundRegionKind,
+    pub kind: LateParamRegionKind,
+}
+
+/// Reflects [`ty::LateParamRegionKind`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegionKind, state: S as gstate)]
+pub enum LateParamRegionKind {
+    Anon(u32),
+    Named(DefId, Symbol),
+    ClosureEnv,
 }
 
 /// Reflects [`ty::RegionKind`]
@@ -978,7 +988,7 @@ pub struct TyFnSig {
     pub output: Ty,
     pub c_variadic: bool,
     pub safety: Safety,
-    pub abi: Abi,
+    pub abi: ExternAbi,
 }
 
 /// Reflects [`ty::PolyFnSig`]
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 29460b76d..232e120f8 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2024-11-23"
+channel = "nightly-2025-03-29"
 components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ]
diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
index c3f6323aa..4f728c82f 100644
--- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
@@ -133,7 +133,7 @@ class t_T (v_Self: Type0) = {
 val impl_T_for_u8:t_T u8
 
 class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_13225137425257751668:Core.Clone.t_Clone v_U;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_11075708886900110455:Core.Clone.t_Clone v_U;
   f_f_pre:v_U -> Type0;
   f_f_post:v_U -> v_Self -> Type0;
   f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)
diff --git a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap
index f5e736e6c..595596d31 100644
--- a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap	
@@ -55,7 +55,7 @@ let print
             Alloc.Alloc.t_Global)
     : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.impl_2__new_v1 (mk_usize 2)
+    Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
           (mk_usize 1)
           (let list = [""; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
index 5217515b8..b46940c46 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
@@ -58,7 +58,7 @@ Class t_Trait `{v_Self : Type} : Type :=
 Arguments t_Trait:clear implicits.
 Arguments t_Trait (_).
 
-Instance t_Trait_629521404 : t_Trait ((t_Foo)) :=
+Instance t_Trait_373159623 : t_Trait ((t_Foo)) :=
   {
   }.
 
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index d2dadf182..f812ecbe3 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap	
@@ -72,7 +72,7 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_s
   impl_Int__to_u8 (f_add (x) (f_mul (x) (x))).
 
 Definition panic_with_msg (_ : unit) : unit :=
-  never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))).
+  never_to_any (panic_fmt (impl_4__new_const (["with msg"%string]))).
 
 Record t_Foo : Type :=
   {
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index 129cc883a..bb16a1fc7 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
@@ -64,7 +64,7 @@ let math_integers (x: Hax_lib.Int.t_Int)
   Hax_lib.Int.impl_Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
 
 let panic_with_msg (_: Prims.unit) : Prims.unit =
-  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (mk_usize 1
+  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_4__new_const (mk_usize 1
             )
             (let list = ["with msg"] in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index 7d3a1ea1a..949b7e6aa 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -34,7 +34,7 @@ open FStar.Mul
 
 let debug (label value: u32) : Prims.unit =
   let _:Prims.unit =
-    Std.Io.Stdio.e_print (Core.Fmt.impl_2__new_v1 (mk_usize 3)
+    Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 3)
           (mk_usize 2)
           (let list = ["["; "] a="; "\n"] in
             FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index a92a71909..b46c2ad35 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -53,10 +53,7 @@ let f (x: u8) : Core.Result.t_Result u16 u16 =
     Core.Result.Result_Ok (f_my_from #u16 #u8 #FStar.Tactics.Typeclasses.solve x)
     <:
     Core.Result.t_Result u16 u16
-  | Core.Result.Result_Err err ->
-    Core.Result.Result_Err (Core.Convert.f_from #u16 #u8 #FStar.Tactics.Typeclasses.solve err)
-    <:
-    Core.Result.t_Result u16 u16
+  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result u16 u16
 '''
 "Side_effects.Issue_1089_.fst" = '''
 module Side_effects.Issue_1089_
@@ -292,10 +289,7 @@ let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
     : Core.Result.t_Result i8 u32 =
   match y <: Core.Result.t_Result i8 u16 with
   | Core.Result.Result_Ok hoist17 -> Core.Result.Result_Ok hoist17 <: Core.Result.t_Result i8 u32
-  | Core.Result.Result_Err err ->
-    Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
-    <:
-    Core.Result.t_Result i8 u32
+  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
 
 /// Test question mark on `Option`s with some control flow
 let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
@@ -470,10 +464,7 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 =
         Core.Result.Result_Ok (Core.Num.impl_u32__wrapping_add (mk_u32 3) x)
         <:
         Core.Result.t_Result u32 u32
-      | Core.Result.Result_Err err ->
-        Core.Result.Result_Err (Core.Convert.f_from #u32 #u8 #FStar.Tactics.Typeclasses.solve err)
-        <:
-        Core.Result.t_Result u32 u32
+      | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result u32 u32
     else
       Core.Result.Result_Ok (Core.Num.impl_u32__wrapping_add (mk_u32 3) x)
       <:
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
index ec29f9d97..b9b278d64 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap	
@@ -165,7 +165,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -266,7 +266,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -305,14 +305,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    then Result_Err (ret_both (12 : int8))
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -567,7 +567,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -668,7 +668,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -707,14 +707,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    then Result_Err (ret_both (12 : int8))
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -969,7 +969,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -1070,7 +1070,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -1109,14 +1109,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    then Result_Err (ret_both (12 : int8))
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -1371,7 +1371,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -1472,7 +1472,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -1511,14 +1511,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    then Result_Err (ret_both (12 : int8))
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -1773,7 +1773,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -1874,7 +1874,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -1913,14 +1913,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    then Result_Err (ret_both (12 : int8))
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -2175,7 +2175,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -2276,7 +2276,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -2315,14 +2315,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    then Result_Err (ret_both (12 : int8))
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 58770603e..b16d00eee 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -35,11 +35,11 @@ open FStar.Mul
 class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }
 
 class t_ParBlocksSizeUser (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_17750095326162477464:t_BlockSizeUser v_Self
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_12386035071644742916:t_BlockSizeUser v_Self
 }
 
 class t_BlockBackend (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_7661532914804666209:t_ParBlocksSizeUser v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_5078033630945970482:t_ParBlocksSizeUser v_Self;
   f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
   f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
   f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global
@@ -55,7 +55,7 @@ open FStar.Mul
 class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }
 
 class t_Foo (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_13496126865352171029:t_Bar v_Self f_U;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_13709452385921529338:t_Bar v_Self f_U;
   f_U:Type0
 }
 '''
@@ -425,11 +425,11 @@ let associated_function_caller
   ()
 
 class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_1779568480311729828:t_Trait v_Self
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_5670955395916535991:t_Trait v_Self
     v_TypeArg
     v_ConstArg;
   f_AssocType:Type0;
-  f_AssocType_13704321474071752218:t_Trait f_AssocType v_TypeArg v_ConstArg
+  f_AssocType_6891123870612467806:t_Trait f_AssocType v_TypeArg v_ConstArg
 }
 '''
 "Traits.Interlaced_consts_types.fst" = '''
@@ -506,11 +506,11 @@ open FStar.Mul
 
 class t_Trait1 (v_Self: Type0) = {
   f_T:Type0;
-  f_T_2186006717281159153:t_Trait1 f_T
+  f_T_6736093233391770582:t_Trait1 f_T
 }
 
 class t_Trait2 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4351024728553910126:t_Trait1 v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_15807083732906695011:t_Trait1 v_Self;
   f_U:Type0
 }
 '''
@@ -567,7 +567,7 @@ open Core
 open FStar.Mul
 
 class t_SuperTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_9529721400157967266:Core.Clone.t_Clone v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_16027770981543256320:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> Type0;
   f_function_of_super_trait_post:v_Self -> u32 -> Type0;
   f_function_of_super_trait:x0: v_Self
@@ -579,7 +579,7 @@ class t_SuperTrait (v_Self: Type0) = {
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_SuperTrait i32 =
   {
-    _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve;
+    _super_16027770981543256320 = FStar.Tactics.Typeclasses.solve;
     f_function_of_super_trait_pre = (fun (self: i32) -> true);
     f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true);
     f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl_i32__abs self <: i32) <: u32
@@ -651,7 +651,7 @@ let uuse_iimpl_trait (_: Prims.unit) : Prims.unit =
 
 class t_Foo (v_Self: Type0) = {
   f_AssocType:Type0;
-  f_AssocType_16668910951696008497:t_SuperTrait f_AssocType;
+  f_AssocType_6638784903434849583:t_SuperTrait f_AssocType;
   f_N:usize;
   f_assoc_f_pre:Prims.unit -> Type0;
   f_assoc_f_post:Prims.unit -> Prims.unit -> Type0;
@@ -688,7 +688,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x
 let impl_Foo_for_tuple_: t_Foo Prims.unit =
   {
     f_AssocType = i32;
-    f_AssocType_16668910951696008497 = FStar.Tactics.Typeclasses.solve;
+    f_AssocType_6638784903434849583 = FStar.Tactics.Typeclasses.solve;
     f_N = mk_usize 32;
     f_assoc_f_pre = (fun (_: Prims.unit) -> true);
     f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);

From d89c6e6d00530dd919eb0c79d18b2f8aa821df09 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 1 Apr 2025 17:15:04 +0200
Subject: [PATCH 2/4] Use `Steal::is_stolen`

---
 cli/driver/src/exporter.rs | 48 +++++++++++++++++++++-----------------
 1 file changed, 26 insertions(+), 22 deletions(-)

diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs
index 4f5a6be54..088b8da3a 100644
--- a/cli/driver/src/exporter.rs
+++ b/cli/driver/src/exporter.rs
@@ -77,20 +77,18 @@ fn precompute_local_thir_bodies(
 
     use itertools::Itertools;
     tcx.hir_body_owners()
-        .filter(|ldid| {
-            match tcx.def_kind(ldid.to_def_id()) {
-                InlineConst | AnonConst => {
-                    fn is_fn(tcx: TyCtxt<'_>, did: rustc_span::def_id::DefId) -> bool {
-                        use rustc_hir::def::DefKind;
-                        matches!(
-                            tcx.def_kind(did),
-                            DefKind::Fn | DefKind::AssocFn | DefKind::Ctor(..) | DefKind::Closure
-                        )
-                    }
-                    !is_fn(tcx, tcx.local_parent(*ldid).to_def_id())
-                },
-                _ => true
+        .filter(|ldid| match tcx.def_kind(ldid.to_def_id()) {
+            InlineConst | AnonConst => {
+                fn is_fn(tcx: TyCtxt<'_>, did: rustc_span::def_id::DefId) -> bool {
+                    use rustc_hir::def::DefKind;
+                    matches!(
+                        tcx.def_kind(did),
+                        DefKind::Fn | DefKind::AssocFn | DefKind::Ctor(..) | DefKind::Closure
+                    )
+                }
+                !is_fn(tcx, tcx.local_parent(*ldid).to_def_id())
             }
+            _ => true,
         })
         .sorted_by_key(|ldid| const_level_of(tcx, *ldid))
         .filter(move |ldid| tcx.hir_maybe_body_owned_by(*ldid).is_some())
@@ -117,15 +115,21 @@ fn precompute_local_thir_bodies(
                     return (ldid, dummy_thir_body(tcx, span, guar));
                 }
             };
-            let thir = match std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
-                thir.borrow().clone()
-            })) {
-                Ok(x) => x,
-                Err(e) => {
-                    let guar = tcx.dcx().span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hax/issues/27.\nPlease comment this issue if you see this error message!", ldid));
-                    return (ldid, dummy_thir_body(tcx, span, guar));
-                }
-            };
+            if thir.is_stolen() {
+                let guar = tcx.dcx().span_err(
+                    span,
+                    format!(
+                        "The THIR body of item {:?} was stolen.\n\
+                        This is not supposed to happen.\n\
+                        This is a bug in Hax's frontend.\n\
+                        This is discussed in issue https://github.com/hacspec/hax/issues/27.\n\
+                        Please comment this issue if you see this error message!",
+                        ldid
+                    ),
+                );
+                return (ldid, dummy_thir_body(tcx, span, guar));
+            }
+            let thir = thir.borrow().clone();
             tracing::debug!("✅ Type-checked THIR body for {:#?}", ldid);
             (ldid, (Rc::new(thir), expr))
         })

From b27f69500a24d857bc4f81fcfdefb10a8d3b6f6f Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Thu, 10 Apr 2025 11:25:44 +0200
Subject: [PATCH 3/4] Fix core lib names for latest rustc pin.

---
 .../phase_reconstruct_question_marks.ml       | 23 +++++++++++++------
 .../phases/phase_simplify_question_marks.ml   | 23 +++++++++++++------
 proof-libs/fstar/core/Core.Cmp.fsti           |  6 ++---
 proof-libs/fstar/core/Core.Fmt.fsti           |  4 ++--
 .../toolchain__side-effects into-fstar.snap   | 15 +++++++++---
 5 files changed, 49 insertions(+), 22 deletions(-)

diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml
index 2487644f4..f41c74949 100644
--- a/engine/lib/phases/phase_reconstruct_question_marks.ml
+++ b/engine/lib/phases/phase_reconstruct_question_marks.ml
@@ -51,13 +51,22 @@ module%inlined_contents Make (FA : Features.T) = struct
       `std::ops::FromResidual` for the type [Result<_, _>], and
       extract its parent [From] impl expr *)
       let expect_residual_impl_result (impl : impl_expr) : impl_expr option =
-        match impl.kind with
-        | ImplApp
-            {
-              impl = { kind = Concrete { trait; _ }; _ };
-              args = [ _; _; _; from_impl ];
-            }
-          when Concrete_ident.eq_name Core__result__Impl_27 trait ->
+        match impl with
+        | {
+         kind = ImplApp { args = [ _; _; _; from_impl ]; _ };
+         goal =
+           {
+             trait;
+             args =
+               [
+                 GType (TApp { ident = arg1; _ });
+                 GType (TApp { ident = arg2; _ });
+               ];
+           };
+        }
+          when Concrete_ident.eq_name Core__ops__try_trait__FromResidual trait
+               && Global_ident.eq_name Core__result__Result arg1
+               && Global_ident.eq_name Core__result__Result arg2 ->
             Some from_impl
         | _ -> None
 
diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml
index bd6a62875..e205911c5 100644
--- a/engine/lib/phases/phase_simplify_question_marks.ml
+++ b/engine/lib/phases/phase_simplify_question_marks.ml
@@ -51,13 +51,22 @@ module%inlined_contents Make (FA : Features.T) = struct
       `std::ops::FromResidual` for the type [Result<_, _>], and
       extract its parent [From] impl expr *)
       let expect_residual_impl_result (impl : impl_expr) : impl_expr option =
-        match impl.kind with
-        | ImplApp
-            {
-              impl = { kind = Concrete { trait; _ }; _ };
-              args = [ _; _; _; from_impl ];
-            }
-          when Concrete_ident.eq_name Core__result__Impl_27 trait ->
+        match impl with
+        | {
+         kind = ImplApp { args = [ _; _; _; from_impl ]; _ };
+         goal =
+           {
+             trait;
+             args =
+               [
+                 GType (TApp { ident = arg1; _ });
+                 GType (TApp { ident = arg2; _ });
+               ];
+           };
+        }
+          when Concrete_ident.eq_name Core__ops__try_trait__FromResidual trait
+               && Global_ident.eq_name Core__result__Result arg1
+               && Global_ident.eq_name Core__result__Result arg2 ->
             Some from_impl
         | _ -> None
 
diff --git a/proof-libs/fstar/core/Core.Cmp.fsti b/proof-libs/fstar/core/Core.Cmp.fsti
index d942fd213..51c3a1d59 100644
--- a/proof-libs/fstar/core/Core.Cmp.fsti
+++ b/proof-libs/fstar/core/Core.Cmp.fsti
@@ -28,15 +28,15 @@ type t_Ordering =
 
 
 class t_PartialOrd (v_Self: Type) (v_Rhs:Type) = {
-  _super_8303539986193044559: t_PartialEq v_Self v_Rhs;
+  _super_7951719793721949255: t_PartialEq v_Self v_Rhs;
   f_partial_cmp_pre: v_Self -> v_Rhs -> Type0;
   f_partial_cmp_post: v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering -> Type0;
   f_partial_cmp:v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering;
 }
 
 class t_Ord (v_Self: Type) = {
-  _super_8438227699474489191: t_Eq v_Self;
-  _super_17497397511932837737: t_PartialOrd v_Self v_Self;
+  _super_641474646876120386: t_Eq v_Self;
+  _super_12012119932897234219: t_PartialOrd v_Self v_Self;
   f_cmp_pre: v_Self -> v_Self -> Type0;
   f_cmp_post: v_Self -> v_Self -> t_Ordering -> Type0;
   f_cmp:v_Self -> v_Self -> t_Ordering;
diff --git a/proof-libs/fstar/core/Core.Fmt.fsti b/proof-libs/fstar/core/Core.Fmt.fsti
index 8c62b1661..11c57fbfc 100644
--- a/proof-libs/fstar/core/Core.Fmt.fsti
+++ b/proof-libs/fstar/core/Core.Fmt.fsti
@@ -19,8 +19,8 @@ class t_Debug t_Self = {
 }
 
 val t_Arguments: Type0
-val impl_2__new_v1 (sz1: usize) (sz2: usize) (pieces: t_Slice string) (args: t_Slice Core.Fmt.Rt.t_Argument): t_Arguments
+val impl_4__new_v1 (sz1: usize) (sz2: usize) (pieces: t_Slice string) (args: t_Slice Core.Fmt.Rt.t_Argument): t_Arguments
 val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Formatter & t_Result
-val impl_2__new_const (u:usize) (args: t_Slice string): t_Arguments
+val impl_4__new_const (u:usize) (args: t_Slice string): t_Arguments
 
 
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index b46c2ad35..a92a71909 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -53,7 +53,10 @@ let f (x: u8) : Core.Result.t_Result u16 u16 =
     Core.Result.Result_Ok (f_my_from #u16 #u8 #FStar.Tactics.Typeclasses.solve x)
     <:
     Core.Result.t_Result u16 u16
-  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result u16 u16
+  | Core.Result.Result_Err err ->
+    Core.Result.Result_Err (Core.Convert.f_from #u16 #u8 #FStar.Tactics.Typeclasses.solve err)
+    <:
+    Core.Result.t_Result u16 u16
 '''
 "Side_effects.Issue_1089_.fst" = '''
 module Side_effects.Issue_1089_
@@ -289,7 +292,10 @@ let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
     : Core.Result.t_Result i8 u32 =
   match y <: Core.Result.t_Result i8 u16 with
   | Core.Result.Result_Ok hoist17 -> Core.Result.Result_Ok hoist17 <: Core.Result.t_Result i8 u32
-  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
+  | Core.Result.Result_Err err ->
+    Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
+    <:
+    Core.Result.t_Result i8 u32
 
 /// Test question mark on `Option`s with some control flow
 let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
@@ -464,7 +470,10 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 =
         Core.Result.Result_Ok (Core.Num.impl_u32__wrapping_add (mk_u32 3) x)
         <:
         Core.Result.t_Result u32 u32
-      | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result u32 u32
+      | Core.Result.Result_Err err ->
+        Core.Result.Result_Err (Core.Convert.f_from #u32 #u8 #FStar.Tactics.Typeclasses.solve err)
+        <:
+        Core.Result.t_Result u32 u32
     else
       Core.Result.Result_Ok (Core.Num.impl_u32__wrapping_add (mk_u32 3) x)
       <:

From f89ffecd6f200cc072994d98d11336f3c44ae6b7 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Thu, 10 Apr 2025 11:45:07 +0200
Subject: [PATCH 4/4] Updated test snapshots.

---
 .../toolchain__side-effects into-ssprove.snap | 48 +++++++++----------
 1 file changed, 24 insertions(+), 24 deletions(-)

diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
index b9b278d64..ec29f9d97 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap	
@@ -165,7 +165,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -266,7 +266,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -305,14 +305,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then Result_Err (ret_both (12 : int8))
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -567,7 +567,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -668,7 +668,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -707,14 +707,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then Result_Err (ret_both (12 : int8))
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -969,7 +969,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -1070,7 +1070,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -1109,14 +1109,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then Result_Err (ret_both (12 : int8))
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -1371,7 +1371,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -1472,7 +1472,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -1511,14 +1511,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then Result_Err (ret_both (12 : int8))
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -1773,7 +1773,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -1874,7 +1874,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -1913,14 +1913,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then Result_Err (ret_both (12 : int8))
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).
@@ -2175,7 +2175,7 @@ Hint Unfold int16_t_MyFrom.
 
 Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
   f x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := Result_Err (ret_both (1 : int8)) in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 
@@ -2276,7 +2276,7 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] hoist17 := y in
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
     Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
@@ -2315,14 +2315,14 @@ Fail Next Obligation.
 
 Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) :=
   question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int8] _ := ifb x >.? (ret_both (40 : int32))
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
     then letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb hoist34 := x >.? (ret_both (90 : int32)) in
     ifb hoist34
-    then Result_Err (ret_both (12 : int8))
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
     else ()
     else () in
     Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32).