Update rustc to latest nightly

cli/driver/src/driver.rs

@@ -1,6 +1,5 @@
 #![feature(rustc_private)]
 #![feature(box_patterns)]
-#![feature(concat_idents)]
 #![feature(trait_alias)]
 #![allow(unused_imports)]
 #![allow(unused_variables)]

engine/backends/coq/coq/coq_backend.ml

@@ -1085,6 +1085,7 @@ open Phase_utils
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Reject.RawOrMutPointer
   |> Phases.And_mut_defsite
   |> Phases.Reconstruct_asserts

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -554,6 +554,7 @@ open Phase_utils
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.Unsafe(Features.Rust)
+    |> Phases.Drop_metasized
     |> Phases.Reject.RawOrMutPointer
     |> Phases.And_mut_defsite
     |> Phases.Reconstruct_asserts

engine/backends/fstar/fstar_backend.ml

@@ -1910,6 +1910,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.RawOrMutPointer(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Transform_hax_lib_inline
   |> Phases.Specialize
   |> Phases.Drop_sized_trait

engine/backends/proverif/proverif_backend.ml

@@ -885,6 +885,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.Unsafe(Features.Rust)
+  |> Phases.Drop_metasized
   |> Phases.Reject.RawOrMutPointer
   |> Phases.Transform_hax_lib_inline
   |> Phases.Simplify_question_marks

engine/lib/import_thir.ml

@@ -1101,8 +1101,6 @@ end) : EXPR = struct
         match non_traits with
         | [] -> TDyn { witness = W.dyn; goals }
         | _ -> assertion_failure [ span ] "type Dyn with non trait predicate")
-    | Dynamic (_, _, DynStar) ->
-        unimplemented ~issue_id:931 [ span ] "type DynStar"
     | Coroutine _ ->
         unimplemented ~issue_id:924 [ span ]
           "Got type `Coroutine`: coroutines are not supported by hax"
@@ -1513,7 +1511,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
            {
@@ -1523,14 +1521,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 (false, _, _ty, 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 (_, generics, ty) ->
       mk
       @@ TyAlias
            {
@@ -1549,13 +1547,13 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              params = c_fn_params item.span params;
              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 (_, generics, variants, repr) ->
       let def_id = assert_item_def_id () in
       let generics = c_generics generics in
       let is_struct = false in
@@ -1613,7 +1611,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 (_, generics, v) ->
       let generics = c_generics generics in
       let def_id = assert_item_def_id () in
       let is_struct = true in
@@ -1808,7 +1806,9 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
           {
             path = List.map ~f:(fun x -> fst x.ident) segments;
             is_external =
-              List.exists ~f:(function Err -> true | _ -> false) res;
+              List.exists
+                ~f:(function None | Some Err -> true | _ -> false)
+                res;
             (* TODO: this should represent local/external? *)
             rename;
           }

engine/lib/phases/phase_drop_metasized.ml

@@ -0,0 +1,192 @@
+(** This phase gets rid of the MetaSized bound. See https://github.com/cryspen/hax/pull/1534. *)
+
+open! Prelude
+
+module%inlined_contents Make (F : Features.T) = struct
+  open Ast
+  module FA = F
+  module FB = FA
+
+  include
+    Phase_utils.MakeBase (F) (FB)
+      (struct
+        let phase_id = [%auto_phase_name auto]
+      end)
+
+  module UA = Ast_utils.Make (F)
+
+  module Implem : ImplemT.T = struct
+    let metadata = metadata
+
+    module S = struct
+      include Features.SUBTYPE.Id
+    end
+
+    [%%inline_defs dmutability + dsafety_kind]
+
+    let rec dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr option =
+      let* kind = dimpl_expr_kind span i.kind in
+      let* goal = dtrait_goal span i.goal in
+      Some B.{ kind; goal }
+
+    and dtrait_goal (span : span) (r : A.trait_goal) : B.trait_goal option =
+      let*? _ = not (Concrete_ident.eq_name Core__marker__MetaSized r.trait) in
+      Some
+        B.{ trait = r.trait; args = List.map ~f:(dgeneric_value span) r.args }
+
+    and dimpl_expr_exn message span i =
+      match dimpl_expr span i with
+      | None -> Error.assertion_failure span message
+      | Some impl -> impl
+
+    and dimpl_ident (span : span) (r : A.impl_ident) : B.impl_ident option =
+      let* goal = dtrait_goal span r.goal in
+      Some B.{ goal; name = r.name }
+
+    and dty (span : span) (ty : A.ty) : B.ty =
+      match ty with
+      | TAssociatedType { impl; item } ->
+          let impl =
+            dimpl_expr_exn "MetaSized has no associated type" span impl
+          in
+          TAssociatedType { impl; item }
+      | [%inline_arms "dty.*" - TAssociatedType] -> auto
+
+    and dprojection_predicate (span : span) (r : A.projection_predicate) :
+        B.projection_predicate =
+      {
+        impl = dimpl_expr_exn "MetaSized cannot be projected" span r.impl;
+        assoc_item = r.assoc_item;
+        typ = dty span r.typ;
+      }
+
+    and dimpl_expr_kind (span : span) (i : A.impl_expr_kind) :
+        B.impl_expr_kind option =
+      match i with
+      | Parent { impl; ident } ->
+          let* impl = dimpl_expr span impl in
+          let* ident = dimpl_ident span ident in
+          Some (B.Parent { impl; ident })
+      | Projection { impl; item; ident } ->
+          let impl = dimpl_expr_exn "MetaSized have no projection" span impl in
+          let* ident = dimpl_ident span ident in
+          Some (B.Projection { impl; item; ident })
+      | ImplApp { impl; args } ->
+          let* impl = dimpl_expr span impl in
+          let args = List.filter_map ~f:(dimpl_expr span) args in
+          Some (B.ImplApp { impl; args })
+      | Builtin tr ->
+          let* tr = dtrait_goal span tr in
+          Some (B.Builtin tr)
+      | Concrete tr ->
+          let* tr = dtrait_goal span tr in
+          Some (B.Concrete tr)
+      | [%inline_arms
+          "dimpl_expr_kind.*" - Parent - Projection - ImplApp - Builtin
+          - Concrete] ->
+          map (fun x ->
+              Some
+                (let result : B.impl_expr_kind = x in
+                 result))
+
+    and dexpr' (span : span) (expr : A.expr') : B.expr' =
+      match expr with
+      | App { f; args; generic_args; bounds_impls; trait } ->
+          let dgeneric_values = List.map ~f:(dgeneric_value span) in
+          App
+            {
+              f = dexpr f;
+              args = List.map ~f:dexpr args;
+              generic_args = dgeneric_values generic_args;
+              bounds_impls = List.filter_map ~f:(dimpl_expr span) bounds_impls;
+              trait =
+                Option.map
+                  ~f:
+                    (dimpl_expr_exn "MetaSized have no method" span
+                    *** dgeneric_values)
+                  trait;
+            }
+      | [%inline_arms "dexpr'.*" - App] -> auto
+    [@@inline_ands
+      bindings_of dty - dimpl_expr - dexpr' - dprojection_predicate
+      - dimpl_expr_kind - dty - dimpl_ident]
+
+    let rec dimpl_item' (span : span) (ii : A.impl_item') : B.impl_item' =
+      match ii with
+      | IIType { typ; parent_bounds } ->
+          IIType
+            {
+              typ = dty span typ;
+              parent_bounds =
+                List.filter_map
+                  ~f:(fun (impl, ident) ->
+                    let* impl = dimpl_expr span impl in
+                    let* ident = dimpl_ident span ident in
+                    Some (impl, ident))
+                  parent_bounds;
+            }
+          (* | _ -> Obj.magic () *)
+      | [%inline_arms "dimpl_item'.*" - IIType] -> auto
+
+    and dtrait_item' (span : span) (ti : A.trait_item') : B.trait_item' =
+      match ti with
+      | TIType idents -> TIType (List.filter_map ~f:(dimpl_ident span) idents)
+      | [%inline_arms "dtrait_item'.*" - TIType] -> auto
+
+    and dgeneric_constraint (span : span)
+        (generic_constraint : A.generic_constraint) :
+        B.generic_constraint option =
+      match generic_constraint with
+      | GCLifetime (lf, witness) ->
+          Some (B.GCLifetime (lf, S.lifetime span witness))
+      | GCType impl_ident ->
+          let* impl = dimpl_ident span impl_ident in
+          Some (B.GCType impl)
+      | GCProjection projection ->
+          Some (B.GCProjection (dprojection_predicate span projection))
+
+    and dgenerics (span : span) (g : A.generics) : B.generics =
+      {
+        params = List.map ~f:(dgeneric_param span) g.params;
+        constraints =
+          List.filter_map ~f:(dgeneric_constraint span) g.constraints;
+      }
+
+    and ditem' (span : span) (item : A.item') : B.item' =
+      match item with
+      | Impl
+          {
+            generics;
+            self_ty;
+            of_trait = trait_id, trait_generics;
+            items;
+            parent_bounds;
+            safety;
+          } ->
+          B.Impl
+            {
+              generics = dgenerics span generics;
+              self_ty = dty span self_ty;
+              of_trait =
+                (trait_id, List.map ~f:(dgeneric_value span) trait_generics);
+              items = List.map ~f:dimpl_item items;
+              parent_bounds =
+                List.filter_map
+                  ~f:(fun (impl, ident) ->
+                    let* impl = dimpl_expr span impl in
+                    let* ident = dimpl_ident span ident in
+                    Some (impl, ident))
+                  parent_bounds;
+              safety = dsafety_kind span safety;
+            }
+      | [%inline_arms "ditem'.*" - Impl] -> auto
+    [@@inline_ands
+      "Item.*" - ditem' - dimpl_item' - dtrait_item' - dgeneric_constraint
+      - dgenerics]
+
+    [%%inline_defs ditems]
+  end
+
+  include Implem
+end
+[@@add "subtype.ml"]

engine/lib/phases/phase_drop_metasized.mli

@@ -0,0 +1,15 @@
+(** This phase gets rid of the MetaSized bound. See https://github.com/cryspen/hax/pull/1534. *)
+
+open! Prelude
+
+module Make (F : Features.T) : sig
+  include module type of struct
+    module FA = F
+    module FB = FA
+    module A = Ast.Make (F)
+    module B = Ast.Make (FB)
+    module ImplemT = Phase_utils.MakePhaseImplemT (A) (B)
+  end
+
+  include ImplemT.T
+end

frontend/exporter/Cargo.toml

@@ -1,10 +1,10 @@
 [package]
 name = "hax-frontend-exporter"
+edition = "2024"
 version.workspace = true
 authors.workspace = true
 license.workspace = true
 homepage.workspace = true
-edition.workspace = true
 repository.workspace = true
 readme.workspace = true
 description = "Provides mirrors of the algebraic data types used in the Rust compilers, removing indirections and inlining various pieces of information."

frontend/exporter/src/constant_utils/uneval.rs

@@ -154,7 +154,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx>
         let span = self.default_span(s.base().tcx);
         match self.kind() {
             ty::ConstKind::Param(p) => {
-                let ty = p.find_ty_from_env(s.param_env());
+                let ty = p.find_const_ty_from_env(s.param_env());
                 let kind = ConstantExprKind::ConstRef { id: p.sinto(s) };
                 kind.decorate(ty.sinto(s), span.sinto(s))
             }
@@ -279,7 +279,7 @@ fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>(
     // Helper for struct-likes.
     let read_fields = |of: rustc_const_eval::interpret::OpTy<'tcx>, field_count| {
         (0..field_count).map(move |i| {
-            let field_op = ecx.project_field(&of, i)?;
+            let field_op = ecx.project_field(&of, rustc_abi::FieldIdx::from_usize(i))?;
             op_to_const(s, span, &ecx, field_op)
         })
     };

frontend/exporter/src/lib.rs

@@ -1,9 +1,8 @@
 #![allow(rustdoc::private_intra_doc_links)]
-#![cfg_attr(feature = "rustc", feature(concat_idents))]
 #![cfg_attr(feature = "rustc", feature(if_let_guard))]
-#![cfg_attr(feature = "rustc", feature(let_chains))]
 #![cfg_attr(feature = "rustc", feature(macro_metavar_expr))]
 #![cfg_attr(feature = "rustc", feature(rustc_private))]
+#![cfg_attr(feature = "rustc", feature(sized_hierarchy))]
 #![cfg_attr(feature = "rustc", feature(trait_alias))]
 #![cfg_attr(feature = "rustc", feature(type_changing_struct_update))]
 

frontend/exporter/src/sinto.rs

@@ -1,9 +1,15 @@
 use crate::prelude::{derive_group, JsonSchema};
 
+#[cfg(not(feature = "rustc"))]
 pub trait SInto<S, To> {
     fn sinto(&self, s: &S) -> To;
 }
 
+#[cfg(feature = "rustc")]
+pub trait SInto<S, To>: std::marker::PointeeSized {
+    fn sinto(&self, s: &S) -> To;
+}
+
 #[macro_export]
 macro_rules! sinto_todo {
     ($($mod:ident)::+, $type:ident$(<$($lts:lifetime),*$(,)?>)? as $renamed:ident) => {