From c70fa4a07f77a566ee29f28e1992ed61faeec971 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 1 Jul 2025 17:22:48 +0200 Subject: [PATCH 1/6] Don't overuse the `tcx` arena --- frontend/exporter/src/state.rs | 2 +- frontend/exporter/src/traits.rs | 5 +-- frontend/exporter/src/traits/resolution.rs | 16 ++++---- frontend/exporter/src/traits/utils.rs | 48 ++++++++-------------- frontend/exporter/src/types/hir.rs | 1 - frontend/exporter/src/types/ty.rs | 11 +++++ 6 files changed, 38 insertions(+), 45 deletions(-) diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs index 18a5b749b..bf621c216 100644 --- a/frontend/exporter/src/state.rs +++ b/frontend/exporter/src/state.rs @@ -357,7 +357,7 @@ impl ImplInfos { .impl_trait_ref(did) .map(|trait_ref| trait_ref.instantiate_identity()) .sinto(s), - clauses: predicates_defined_on(tcx, did).predicates.sinto(s), + clauses: predicates_defined_on(tcx, did).as_ref().sinto(s), } } } diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 377bef55c..619c21714 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -7,7 +7,7 @@ mod utils; #[cfg(feature = "rustc")] pub use utils::{ erase_and_norm, implied_predicates, predicates_defined_on, required_predicates, self_predicate, - ToPolyTraitRef, + Predicates, ToPolyTraitRef, }; #[cfg(feature = "rustc")] @@ -358,12 +358,11 @@ pub fn solve_item_implied_traits<'tcx, S: UnderOwnerState<'tcx>>( fn solve_item_traits_inner<'tcx, S: UnderOwnerState<'tcx>>( s: &S, generics: ty::GenericArgsRef<'tcx>, - predicates: ty::GenericPredicates<'tcx>, + predicates: utils::Predicates<'tcx>, ) -> Vec { let tcx = s.base().tcx; let typing_env = s.typing_env(); predicates - .predicates .iter() .map(|(clause, _span)| *clause) .filter_map(|clause| clause.as_trait_clause()) diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index 453a811ae..887225e70 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -11,9 +11,10 @@ use rustc_middle::traits::CodegenObligationError; use rustc_middle::ty::{self, *}; use rustc_trait_selection::traits::ImplSource; -use crate::{self_predicate, traits::utils::erase_and_norm}; - -use super::utils::{implied_predicates, normalize_bound_val, required_predicates, ToPolyTraitRef}; +use super::utils::{ + self, erase_and_norm, implied_predicates, normalize_bound_val, required_predicates, + self_predicate, ToPolyTraitRef, +}; #[derive(Debug, Clone)] pub enum PathChunk<'tcx> { @@ -179,7 +180,6 @@ fn initial_search_predicates<'tcx>( } predicates.extend( required_predicates(tcx, def_id, add_drop) - .predicates .iter() .map(|(clause, _span)| *clause) .filter_map(|clause| { @@ -204,7 +204,6 @@ fn parents_trait_predicates<'tcx>( ) -> Vec> { let self_trait_ref = pred.to_poly_trait_ref(); implied_predicates(tcx, pred.def_id(), add_drop) - .predicates .iter() .map(|(clause, _span)| *clause) // Substitute with the `self` args so that the clause makes sense in the @@ -342,8 +341,8 @@ impl<'tcx> PredicateSearcher<'tcx> { }; // The bounds that hold on the associated type. - let item_bounds = implied_predicates(tcx, alias_ty.def_id, self.add_drop) - .predicates + let item_bounds = implied_predicates(tcx, alias_ty.def_id, self.add_drop); + let item_bounds = item_bounds .iter() .map(|(clause, _span)| *clause) .filter_map(|pred| pred.as_trait_clause()) @@ -642,13 +641,12 @@ impl<'tcx> PredicateSearcher<'tcx> { pub fn resolve_predicates( &mut self, generics: GenericArgsRef<'tcx>, - predicates: GenericPredicates<'tcx>, + predicates: utils::Predicates<'tcx>, // Call back into hax-related code to display a nice warning. warn: &impl Fn(&str), ) -> Result>, String> { let tcx = self.tcx; predicates - .predicates .iter() .map(|(clause, _span)| *clause) .filter_map(|clause| clause.as_trait_clause()) diff --git a/frontend/exporter/src/traits/utils.rs b/frontend/exporter/src/traits/utils.rs index 20adc33e2..9e9cad39f 100644 --- a/frontend/exporter/src/traits/utils.rs +++ b/frontend/exporter/src/traits/utils.rs @@ -29,23 +29,21 @@ use rustc_hir::def::DefKind; use rustc_middle::ty::*; use rustc_span::def_id::DefId; -use rustc_span::DUMMY_SP; +use rustc_span::{Span, DUMMY_SP}; +use std::borrow::Cow; + +pub type Predicates<'tcx> = Cow<'tcx, [(Clause<'tcx>, Span)]>; /// Returns a list of type predicates for the definition with ID `def_id`, including inferred /// lifetime constraints. This is the basic list of predicates we use for essentially all items. -pub fn predicates_defined_on(tcx: TyCtxt<'_>, def_id: DefId) -> GenericPredicates<'_> { - let mut result = tcx.explicit_predicates_of(def_id); +pub fn predicates_defined_on(tcx: TyCtxt<'_>, def_id: DefId) -> Predicates<'_> { + let mut result = Cow::Borrowed(tcx.explicit_predicates_of(def_id).predicates); let inferred_outlives = tcx.inferred_outlives_of(def_id); if !inferred_outlives.is_empty() { - let inferred_outlives_iter = inferred_outlives - .iter() - .map(|(clause, span)| ((*clause).upcast(tcx), *span)); - result.predicates = tcx.arena.alloc_from_iter( - result - .predicates - .into_iter() - .copied() - .chain(inferred_outlives_iter), + result.to_mut().extend( + inferred_outlives + .iter() + .map(|(clause, span)| ((*clause).upcast(tcx), *span)), ); } result @@ -66,7 +64,7 @@ pub fn required_predicates<'tcx>( tcx: TyCtxt<'tcx>, def_id: DefId, add_drop: bool, -) -> GenericPredicates<'tcx> { +) -> Predicates<'tcx> { use DefKind::*; let def_kind = tcx.def_kind(def_id); let mut predicates = match def_kind { @@ -103,9 +101,7 @@ pub fn required_predicates<'tcx>( .map(|ty| Binder::dummy(TraitRef::new(tcx, drop_trait, [ty]))) .map(|tref| tref.upcast(tcx)) .map(|clause| (clause, DUMMY_SP)); - predicates.predicates = tcx - .arena - .alloc_from_iter(predicates.predicates.iter().copied().chain(extra_bounds)); + predicates.to_mut().extend(extra_bounds); } } predicates @@ -134,36 +130,26 @@ pub fn implied_predicates<'tcx>( tcx: TyCtxt<'tcx>, def_id: DefId, add_drop: bool, -) -> GenericPredicates<'tcx> { +) -> Predicates<'tcx> { use DefKind::*; let parent = tcx.opt_parent(def_id); match tcx.def_kind(def_id) { // We consider all predicates on traits to be outputs Trait | TraitAlias => predicates_defined_on(tcx, def_id), AssocTy if matches!(tcx.def_kind(parent.unwrap()), Trait) => { - let mut predicates = GenericPredicates { - parent, - // `skip_binder` is for the GAT `EarlyBinder` - predicates: tcx.explicit_item_bounds(def_id).skip_binder(), - ..GenericPredicates::default() - }; + // `skip_binder` is for the GAT `EarlyBinder` + let mut predicates = Cow::Borrowed(tcx.explicit_item_bounds(def_id).skip_binder()); if add_drop { // Add a `Drop` bound to the assoc item. let drop_trait = tcx.lang_items().drop_trait().unwrap(); let ty = Ty::new_projection(tcx, def_id, GenericArgs::identity_for_item(tcx, def_id)); let tref = Binder::dummy(TraitRef::new(tcx, drop_trait, [ty])); - predicates.predicates = tcx.arena.alloc_from_iter( - predicates - .predicates - .iter() - .copied() - .chain([(tref.upcast(tcx), DUMMY_SP)]), - ); + predicates.to_mut().push((tref.upcast(tcx), DUMMY_SP)); } predicates } - _ => GenericPredicates::default(), + _ => Predicates::default(), } } diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs index e4b5a747b..aefb310a7 100644 --- a/frontend/exporter/src/types/hir.rs +++ b/frontend/exporter/src/types/hir.rs @@ -830,7 +830,6 @@ fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> Gene .instantiate_identity() } else { predicates_defined_on(tcx, s.owner_id()) - .predicates .iter() .map(|(x, _span)| x) .copied() diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index 0438ab5ee..233dba9f0 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -1337,6 +1337,17 @@ pub struct GenericPredicates { pub predicates: Vec<(Clause, Span)>, } +#[cfg(feature = "rustc")] +impl<'tcx, S: UnderOwnerState<'tcx>> SInto + for crate::traits::Predicates<'tcx> +{ + fn sinto(&self, s: &S) -> GenericPredicates { + GenericPredicates { + predicates: self.as_ref().sinto(s), + } + } +} + #[cfg(feature = "rustc")] impl<'tcx, S: UnderOwnerState<'tcx>, T1, T2> SInto> for ty::Binder<'tcx, T1> where From 13ac8f93168518bb4567c98f210986d18e43ab50 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 2 Jul 2025 16:56:58 +0200 Subject: [PATCH 2/6] Add an explicit `Self: Trait` clause to trait assoc items This way, the special `ImplExpr::SelfImpl` is only valid within a trait declaration. --- frontend/exporter/src/traits.rs | 7 ++++--- frontend/exporter/src/traits/resolution.rs | 20 ++++++++++++++---- frontend/exporter/src/traits/utils.rs | 5 +++++ .../toolchain__traits into-fstar.snap | 21 ++++++++++++++----- 4 files changed, 41 insertions(+), 12 deletions(-) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 619c21714..06c53f42f 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -290,7 +290,9 @@ pub fn translate_item_ref<'tcx, S: UnderOwnerState<'tcx>>( let num_trait_generics = trait_ref.generic_args.len(); generic_args.drain(0..num_trait_generics); let num_trait_trait_clauses = trait_ref.impl_exprs.len(); - impl_exprs.drain(0..num_trait_trait_clauses); + // Associated items take a `Self` clause as first clause, we skip that one too. Note: that + // clause is the same as `tinfo`. + impl_exprs.drain(0..num_trait_trait_clauses + 1); } let content = ItemRefContents { @@ -386,7 +388,6 @@ pub fn self_clause_for_item<'tcx, S: UnderOwnerState<'tcx>>( def_id: RDefId, generics: rustc_middle::ty::GenericArgsRef<'tcx>, ) -> Option { - use rustc_middle::ty::EarlyBinder; let tcx = s.base().tcx; let tr_def_id = tcx.trait_of_item(def_id)?; @@ -394,7 +395,7 @@ pub fn self_clause_for_item<'tcx, S: UnderOwnerState<'tcx>>( let self_pred = self_predicate(tcx, tr_def_id); // Substitute to be in the context of the current item. let generics = generics.truncate_to(tcx, tcx.generics_of(tr_def_id)); - let self_pred = EarlyBinder::bind(self_pred).instantiate(tcx, generics); + let self_pred = ty::EarlyBinder::bind(self_pred).instantiate(tcx, generics); // Resolve Some(solve_trait(s, self_pred)) diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index 887225e70..518de605e 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -154,6 +154,7 @@ fn initial_search_predicates<'tcx>( tcx: TyCtxt<'tcx>, def_id: rustc_span::def_id::DefId, add_drop: bool, + include_self_pred: bool, predicates: &mut Vec>, pred_id: &mut usize, ) { @@ -165,11 +166,22 @@ fn initial_search_predicates<'tcx>( use DefKind::*; match tcx.def_kind(def_id) { // These inherit some predicates from their parent. - AssocTy | AssocFn | AssocConst | Closure | Ctor(..) | Variant => { + dk @ (AssocTy | AssocFn | AssocConst | Closure | Ctor(..) | Variant) => { let parent = tcx.parent(def_id); - acc_predicates(tcx, parent, add_drop, predicates, pred_id); + // Hack: we don't support GATs well so for now we let assoc types refer to the + // implicit trait `Self` clause. Other associated items get an explicit `Self: + // Trait` clause passed to them so they don't need that. + let include_self_pred = include_self_pred && matches!(dk, AssocTy); + acc_predicates( + tcx, + parent, + add_drop, + include_self_pred, + predicates, + pred_id, + ); } - Trait | TraitAlias => { + Trait | TraitAlias if include_self_pred => { let self_pred = self_predicate(tcx, def_id).upcast(tcx); predicates.push(AnnotatedTraitPred { origin: BoundPredicateOrigin::SelfPred, @@ -192,7 +204,7 @@ fn initial_search_predicates<'tcx>( } let mut predicates = vec![]; - acc_predicates(tcx, def_id, add_drop, &mut predicates, &mut 0); + acc_predicates(tcx, def_id, add_drop, true, &mut predicates, &mut 0); predicates } diff --git a/frontend/exporter/src/traits/utils.rs b/frontend/exporter/src/traits/utils.rs index 9e9cad39f..3d469eb92 100644 --- a/frontend/exporter/src/traits/utils.rs +++ b/frontend/exporter/src/traits/utils.rs @@ -86,6 +86,11 @@ pub fn required_predicates<'tcx>( // `predicates_defined_on` ICEs on other def kinds. _ => Default::default(), }; + // For associated items in trait definitions, we add an explicit `Self: Trait` clause. + if let Some(trait_def_id) = tcx.trait_of_item(def_id) { + let self_clause = self_predicate(tcx, trait_def_id).upcast(tcx); + predicates.to_mut().insert(0, (self_clause, DUMMY_SP)); + } if add_drop { // Add a `T: Drop` bound for every generic, unless the current trait is `Drop` itself, or // `Sized`. diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 373243c11..550ddad93 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -661,9 +661,18 @@ class t_Foo (v_Self: Type0) = { f_method_f_post:v_Self -> Prims.unit -> Type0; f_method_f:x0: v_Self -> Prims.Pure Prims.unit (f_method_f_pre x0) (fun result -> f_method_f_post x0 result); - f_assoc_type_pre:{| i2: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Type0; - f_assoc_type_post:{| i2: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> Type0; - f_assoc_type:{| i2: Core.Marker.t_Copy f_AssocType |} -> x0: f_AssocType + f_assoc_type_pre: + {| i2: Core.Marker.t_Copy v_5081411602995720689.f_AssocType |} -> + v_5081411602995720689.f_AssocType + -> Type0; + f_assoc_type_post: + {| i2: Core.Marker.t_Copy v_5081411602995720689.f_AssocType |} -> + v_5081411602995720689.f_AssocType -> + Prims.unit + -> Type0; + f_assoc_type: + {| i2: Core.Marker.t_Copy v_5081411602995720689.f_AssocType |} -> + x0: v_5081411602995720689.f_AssocType -> Prims.Pure Prims.unit (f_assoc_type_pre #i2 x0) (fun result -> f_assoc_type_post #i2 x0 result) @@ -672,9 +681,11 @@ class t_Foo (v_Self: Type0) = { class t_Lang (v_Self: Type0) = { f_Var:Type0; f_s_pre:v_Self -> i32 -> Type0; - f_s_post:v_Self -> i32 -> (v_Self & f_Var) -> Type0; + f_s_post:v_Self -> i32 -> (v_Self & v_178762381425797165.f_Var) -> Type0; f_s:x0: v_Self -> x1: i32 - -> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result) + -> Prims.Pure (v_Self & v_178762381425797165.f_Var) + (f_s_pre x0 x1) + (fun result -> f_s_post x0 x1 result) } let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit = From 5c2d83bd8de81112c79109c60dff0066ac272ff7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 1 Jul 2025 13:10:07 +0200 Subject: [PATCH 3/6] Update rustc --- cli/driver/src/driver.rs | 1 - engine/lib/import_thir.ml | 18 +++++----- flake.lock | 6 ++-- .../exporter/src/constant_utils/uneval.rs | 4 +-- frontend/exporter/src/lib.rs | 2 +- frontend/exporter/src/sinto.rs | 6 ++++ frontend/exporter/src/traits/resolution.rs | 4 +-- frontend/exporter/src/types/hir.rs | 16 ++++----- frontend/exporter/src/types/new/full_def.rs | 5 +-- frontend/exporter/src/types/ty.rs | 6 ++-- rust-toolchain.toml | 2 +- ...oolchain__attribute-opaque into-fstar.snap | 2 ++ .../toolchain__attributes into-fstar.snap | 6 ++++ .../snapshots/toolchain__dyn into-fstar.snap | 34 +++++++++--------- .../toolchain__functions into-fstar.snap | 1 + .../toolchain__generics into-fstar.snap | 1 + .../toolchain__include-flag into-coq.snap | 4 +-- .../toolchain__include-flag into-fstar.snap | 4 ++- .../toolchain__interface-only into-fstar.snap | 2 ++ .../toolchain__literals into-coq.snap | 5 ++- .../toolchain__literals into-fstar.snap | 2 +- ..._mut-ref-functionalization into-fstar.snap | 1 + .../toolchain__naming into-fstar.snap | 36 ++++++++++++------- .../toolchain__side-effects into-fstar.snap | 1 + .../toolchain__traits into-fstar.snap | 36 ++++++++++++++++--- 25 files changed, 133 insertions(+), 72 deletions(-) diff --git a/cli/driver/src/driver.rs b/cli/driver/src/driver.rs index a7f1d4e2c..2ec019b8f 100644 --- a/cli/driver/src/driver.rs +++ b/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)] diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 830f4edc7..eecd488eb 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1513,7 +1513,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 +1523,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 +1549,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 +1613,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 +1808,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; } diff --git a/flake.lock b/flake.lock index 08354fcfa..c263241e4 100644 --- a/flake.lock +++ b/flake.lock @@ -127,11 +127,11 @@ ] }, "locked": { - "lastModified": 1748399823, - "narHash": "sha256-kahD8D5hOXOsGbNdoLLnqCL887cjHkx98Izc37nDjlA=", + "lastModified": 1751338093, + "narHash": "sha256-/yd9nPcTfUZPFtwjRbdB5yGLdt3LTPqz6Ja63Joiahs=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "d68a69dc71bc19beb3479800392112c2f6218159", + "rev": "6cfb7821732dac2d3e2dea857a5613d3b856c20c", "type": "github" }, "original": { diff --git a/frontend/exporter/src/constant_utils/uneval.rs b/frontend/exporter/src/constant_utils/uneval.rs index 33d18f07d..8f41b2392 100644 --- a/frontend/exporter/src/constant_utils/uneval.rs +++ b/frontend/exporter/src/constant_utils/uneval.rs @@ -154,7 +154,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto 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) }) }; diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs index fe3b58896..a4c851910 100644 --- a/frontend/exporter/src/lib.rs +++ b/frontend/exporter/src/lib.rs @@ -1,9 +1,9 @@ #![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))] diff --git a/frontend/exporter/src/sinto.rs b/frontend/exporter/src/sinto.rs index fc58f735f..15d65f66b 100644 --- a/frontend/exporter/src/sinto.rs +++ b/frontend/exporter/src/sinto.rs @@ -1,9 +1,15 @@ use crate::prelude::{derive_group, JsonSchema}; +#[cfg(not(feature = "rustc"))] pub trait SInto { fn sinto(&self, s: &S) -> To; } +#[cfg(feature = "rustc")] +pub trait SInto: std::marker::PointeeSized { + fn sinto(&self, s: &S) -> To; +} + #[macro_export] macro_rules! sinto_todo { ($($mod:ident)::+, $type:ident$(<$($lts:lifetime),*$(,)?>)? as $renamed:ident) => { diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index 518de605e..6ac0989e3 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -687,7 +687,7 @@ pub fn shallow_resolve_trait_ref<'tcx>( use rustc_middle::traits::CodegenObligationError; use rustc_middle::ty::TypeVisitableExt; use rustc_trait_selection::traits::{ - Obligation, ObligationCause, ObligationCtxt, SelectionContext, Unimplemented, + Obligation, ObligationCause, ObligationCtxt, SelectionContext, SelectionError, }; // Do the initial selection for the obligation. This yields the // shallow result we are looking for -- that is, what specific impl. @@ -703,7 +703,7 @@ pub fn shallow_resolve_trait_ref<'tcx>( let selection = match selcx.poly_select(&obligation) { Ok(Some(selection)) => selection, Ok(None) => return Err(CodegenObligationError::Ambiguity), - Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented), + Err(SelectionError::Unimplemented) => return Err(CodegenObligationError::Unimplemented), Err(_) => return Err(CodegenObligationError::Ambiguity), }; diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs index aefb310a7..669063f26 100644 --- a/frontend/exporter/src/types/hir.rs +++ b/frontend/exporter/src/types/hir.rs @@ -535,7 +535,7 @@ pub struct Variant { pub struct UsePath { pub span: Span, #[map(x.iter().map(|res| res.sinto(s)).collect())] - pub res: Vec, + pub res: Vec>, pub segments: Vec, #[value(self.segments.iter().last().and_then(|segment| { match s.base().tcx.hir_node_by_def_id(segment.hir_id.owner.def_id) { @@ -620,8 +620,8 @@ pub struct PathSegment { pub enum ItemKind { ExternCrate(Option, Ident), Use(UsePath, UseKind), - Static(Ident, Ty, Mutability, Body), - Const(Ident, Ty, Generics, Body), + Static(Mutability, Ident, Ty, Body), + Const(Ident, Generics, Ty, Body), #[custom_arm( hir::ItemKind::Fn{ ident, sig, generics, body, .. } => { ItemKind::Fn { @@ -648,6 +648,7 @@ pub enum ItemKind { }, TyAlias( Ident, + Generics, #[map({ let s = &State { base: Base {ty_alias_mode: true, ..s.base()}, @@ -659,20 +660,19 @@ pub enum ItemKind { x.sinto(s) })] Ty, - Generics, ), Enum( Ident, - EnumDef, Generics, + EnumDef, #[value({ let tcx = s.base().tcx; tcx.repr_options_of_def(s.owner_id().expect_local()).sinto(s) })] ReprOptions, ), - Struct(Ident, VariantData, Generics), - Union(Ident, VariantData, Generics), + Struct(Ident, Generics, VariantData), + Union(Ident, Generics, VariantData), Trait( IsAuto, Safety, @@ -915,7 +915,7 @@ impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto> for hir::Item< let name = match self.kind { ExternCrate(_, i) | Use(_, hir::UseKind::Single(i)) - | Static(i, ..) + | Static(_, i, ..) | Const(i, ..) | Fn { ident: i, .. } | Macro(i, ..) diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index 951150d21..91a3e49a9 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -217,7 +217,7 @@ pub enum FullDefKind { /// `Some` if the item is in the local crate. #[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(_, _generics, ty) = &item.kind else { unreachable!() }; let mut s = State::from_under_owner(s); s.base.ty_alias_mode = true; ty.sinto(&s) @@ -981,7 +981,8 @@ fn closure_once_shim<'tcx>( #[cfg(feature = "rustc")] fn drop_glue_shim<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> Option> { - let drop_in_place = tcx.require_lang_item(rustc_hir::LangItem::DropInPlace, None); + let drop_in_place = + tcx.require_lang_item(rustc_hir::LangItem::DropInPlace, rustc_span::DUMMY_SP); if !tcx.generics_of(def_id).is_empty() { // Hack: layout code panics if it can't fully normalize types, which can happen e.g. with a // trait associated type. For now we only translate the glue for monomorphic types. diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index 233dba9f0..34e3e0e69 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -544,14 +544,14 @@ impl std::ops::Deref for ItemRef { #[cfg(feature = "rustc")] impl<'tcx, S: UnderOwnerState<'tcx>> SInto for ty::GenericArg<'tcx> { fn sinto(&self, s: &S) -> GenericArg { - self.unpack().sinto(s) + self.kind().sinto(s) } } #[cfg(feature = "rustc")] impl<'tcx, S: UnderOwnerState<'tcx>> SInto> for ty::GenericArgsRef<'tcx> { fn sinto(&self, s: &S) -> Vec { - self.iter().map(|v| v.unpack().sinto(s)).collect() + self.iter().map(|v| v.kind().sinto(s)).collect() } } @@ -1169,7 +1169,7 @@ pub enum Term { impl<'tcx, S: UnderOwnerState<'tcx>> SInto for ty::Term<'tcx> { fn sinto(&self, s: &S) -> Term { use ty::TermKind; - match self.unpack() { + match self.kind() { TermKind::Ty(ty) => Term::Ty(ty.sinto(s)), TermKind::Const(c) => Term::Const(c.sinto(s)), } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index f290a30ed..3a87a82e7 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2025-05-26" +channel = "nightly-2025-06-30" 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 bc99d93be..21d95b115 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -119,6 +119,7 @@ val ff_pre_post (x y: bool) result =. y) class t_T (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_U:Type0; f_c:u8; f_d_pre:Prims.unit -> Type0; @@ -133,6 +134,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_4726684624731801277:Core.Marker.t_MetaSized v_Self; [@@@ FStar.Tactics.Typeclasses.no_method]_super_17240578109911634293:Core.Clone.t_Clone v_U; f_f_pre:v_U -> Type0; f_f_post:v_U -> v_Self -> Type0; diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 4b29f6b9a..7dca84eb7 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -155,6 +155,7 @@ open Core open FStar.Mul class t_T (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_v_pre:v_Self -> Type0; f_v_post:x: v_Self -> x_future: v_Self -> pred: Type0{pred ==> true}; f_v:x0: v_Self -> Prims.Pure v_Self (f_v_pre x0) (fun result -> f_v_post x0 result) @@ -214,6 +215,7 @@ let impl_SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (mk_usize 10)) t_SafeIndex = { f_Output = v_T; + f_Output_6696274936538609082 = FStar.Tactics.Typeclasses.solve; f_index_pre = (fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) -> true); f_index_post = (fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) (out: v_T) -> true); f_index = fun (self: t_Array v_T (mk_usize 10)) (index: t_SafeIndex) -> self.[ index.f_i ] @@ -250,6 +252,7 @@ open Core open FStar.Mul class t_Operation (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_double_pre:x: u8 -> pred: Type0 @@ -306,6 +309,7 @@ let impl_Operation_for_ViaMul: t_Operation t_ViaMul = } class t_TraitWithRequiresAndEnsures (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_method_pre:self_: v_Self -> x: u8 -> pred: Type0{x <. mk_u8 100 ==> pred}; f_method_post:self_: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. mk_u8 88}; f_method:x0: v_Self -> x1: u8 @@ -400,6 +404,7 @@ let mutation_example let impl: Core.Ops.Index.t_Index t_MyArray usize = { f_Output = u8; + f_Output_6696274936538609082 = FStar.Tactics.Typeclasses.solve; f_index_pre = (fun (self_: t_MyArray) (index: usize) -> index <. v_MAX); f_index_post = (fun (self: t_MyArray) (index: usize) (out: u8) -> true); f_index = fun (self: t_MyArray) (index: usize) -> self.[ index ] @@ -588,6 +593,7 @@ open Core open FStar.Mul class t_Foo (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_f_pre:x: u8 -> y: u8 -> pred: Type0 diff --git a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap index 0928d26ad..75edb2282 100644 --- a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap @@ -33,6 +33,7 @@ open Core open FStar.Mul class t_Printable (v_Self: Type0) (v_S: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_stringify_pre:v_Self -> Type0; f_stringify_post:v_Self -> v_S -> Type0; f_stringify:x0: v_Self @@ -54,27 +55,28 @@ let print Alloc.Boxed.t_Box (dyn 1 (fun z -> t_Printable z Alloc.String.t_String)) Alloc.Alloc.t_Global) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = + [ + Core.Fmt.Rt.impl__new_display #Alloc.String.t_String + (f_stringify #(dyn 1 (fun z -> t_Printable z Alloc.String.t_String)) + #Alloc.String.t_String + #FStar.Tactics.Typeclasses.solve + a + <: + Alloc.String.t_String) + ] + in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [ - Core.Fmt.Rt.impl__new_display #Alloc.String.t_String - (f_stringify #(dyn 1 (fun z -> t_Printable z Alloc.String.t_String)) - #Alloc.String.t_String - #FStar.Tactics.Typeclasses.solve - a - <: - Alloc.String.t_String) - <: - Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/test-harness/src/snapshots/toolchain__functions into-fstar.snap b/test-harness/src/snapshots/toolchain__functions into-fstar.snap index df12b8b6e..f456755a4 100644 --- a/test-harness/src/snapshots/toolchain__functions into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__functions into-fstar.snap @@ -38,6 +38,7 @@ type t_CallableViaDeref = | CallableViaDeref : t_CallableViaDeref let impl: Core.Ops.Deref.t_Deref t_CallableViaDeref = { f_Target = Prims.unit -> bool; + f_Target_4695674276362814091 = FStar.Tactics.Typeclasses.solve; f_deref_pre = (fun (self: t_CallableViaDeref) -> true); f_deref_post = (fun (self: t_CallableViaDeref) (out: (Prims.unit -> bool)) -> true); f_deref diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index d42249d1c..c75680dca 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -157,6 +157,7 @@ let call_g (_: Prims.unit) : usize = mk_usize 3 class t_Foo (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_const_add_pre:v_N: usize -> v_Self -> Type0; f_const_add_post:v_N: usize -> v_Self -> usize -> Type0; f_const_add:v_N: usize -> x0: v_Self 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 e0f975a26..b6d4c8c65 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap @@ -51,10 +51,10 @@ Record Foo_record : Type := #[export] Notation "'Foo_Foo_record'" := Build_Foo_record. -Class t_Trait (v_Self : Type) : Type := +Class t_Trait (v_Self : Type) `{t_MetaSized (v_Self)} : Type := { }. -Arguments t_Trait (_). +Arguments t_Trait (_) {_}. Instance t_Trait_572156424 : t_Trait ((t_Foo)) := { diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap index 81212e6dd..45ac83394 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap @@ -34,7 +34,9 @@ open FStar.Mul type t_Foo = | Foo : t_Foo -class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } +class t_Trait (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self +} [@@ FStar.Tactics.Typeclasses.tcinstance] let impl: t_Trait t_Foo = { __marker_trait = () } diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap index 7d30bbb68..b8c5290cc 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -101,6 +101,7 @@ unfold let ff_generic (v_X: usize) (#v_U: Type0) = ff_generic' v_X #v_U class t_T (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_Assoc:Type0; f_d_pre:Prims.unit -> Type0; f_d_post:Prims.unit -> Prims.unit -> Type0; @@ -118,6 +119,7 @@ let impl_T_for_u8: t_T u8 = } class t_T2 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_d_pre:Prims.unit -> Type0; f_d_post:Prims.unit -> Prims.unit -> Type0; f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result) diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index b6ff74d73..45268beae 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -45,8 +45,7 @@ From Core Require Import Core. (* NotImplementedYet *) -From Literals Require Import hax_lib. -Export hax_lib. + Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_str (("0"%string : string)))) (f_lt (x) (impl_Int__e_unsafe_from_str (("16"%string : string)))) = true} : t_u8 := let _ : t_Int := f_lift ((3 : t_usize)) in @@ -73,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 : string)]))). + never_to_any (panic_fmt (impl_1__new_const ([("with msg"%string : string)]))). Record Foo_record : Type := { diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index 55c3c8e73..e93a5afdd 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.Rt.impl_2__new_const (mk_usize + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__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__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap index ac5dff563..38d1d747b 100644 --- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap @@ -269,6 +269,7 @@ let k (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) class t_FooTrait (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_z_pre:v_Self -> Type0; f_z_post:v_Self -> v_Self -> Type0; f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result) diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index cae01d074..9ec3ce4a9 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -33,20 +33,21 @@ open Core open FStar.Mul let debug (label value: u32) : Prims.unit = + let args:(u32 & u32) = label, value <: (u32 & u32) in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 2) = + let list = + [Core.Fmt.Rt.impl__new_display #u32 args._1; Core.Fmt.Rt.impl__new_display #u32 args._2] + in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); + Rust_primitives.Hax.array_of_list 2 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 3) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 3) (mk_usize 2) (let list = ["["; "] a="; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); Rust_primitives.Hax.array_of_list 3 list) - (let list = - [ - Core.Fmt.Rt.impl__new_display #u32 label <: Core.Fmt.Rt.t_Argument; - Core.Fmt.Rt.impl__new_display #u32 value <: Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); - Rust_primitives.Hax.array_of_list 2 list) + args <: Core.Fmt.t_Arguments) in @@ -171,7 +172,9 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T -class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit } +class t_T1 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self +} [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () } @@ -179,13 +182,17 @@ let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () } [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () } -class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit } +class t_T2_for_a (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self +} [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_T2_ee_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) = { __marker_trait = () } -class t_T3_ee_for_a (v_Self: Type0) = { __marker_trait_t_T3_ee_for_a:Prims.unit } +class t_T3_ee_for_a (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self +} [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_T3_ee_e_for_a_for_Foo: t_T3_ee_for_a t_Foo = { __marker_trait = () } @@ -213,7 +220,10 @@ let construct_structs (a b: usize) : Prims.unit = let v_INHERENT_CONSTANT: usize = mk_usize 3 -class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize } +class t_FooTrait (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; + f_ASSOCIATED_CONSTANT:usize +} let constants (#v_T: Type0) 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..0a676481d 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -34,6 +34,7 @@ open Core open FStar.Mul class t_MyFrom (v_Self: Type0) (v_T: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_my_from_pre:v_T -> Type0; f_my_from_post:v_T -> v_Self -> Type0; f_my_from:x0: v_T -> Prims.Pure v_Self (f_my_from_pre x0) (fun result -> f_my_from_post x0 result) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 550ddad93..f0132d6a7 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -32,13 +32,18 @@ module Traits.Block_size open Core open FStar.Mul -class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 } +class t_BlockSizeUser (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; + f_BlockSize:Type0 +} class t_ParBlocksSizeUser (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; [@@@ FStar.Tactics.Typeclasses.no_method]_super_5884559561557426095:t_BlockSizeUser v_Self } class t_BlockBackend (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; [@@@ FStar.Tactics.Typeclasses.no_method]_super_17422710415653782164: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; @@ -52,9 +57,12 @@ module Traits.Default_traits_parameters open Core open FStar.Mul -class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit } +class t_Bar (v_Self: Type0) (v_T: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self +} class t_Foo (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; [@@@ FStar.Tactics.Typeclasses.no_method]_super_7275791365833186636:t_Bar v_Self f_U; f_U:Type0 } @@ -65,7 +73,9 @@ module Traits.For_clauses.Issue_495_.Minimized_3_ open Core open FStar.Mul -class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } +class t_Trait (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self +} [@@ FStar.Tactics.Typeclasses.tcinstance] let impl @@ -148,6 +158,7 @@ open Core open FStar.Mul class t_Foo (v_Self: Type0) (v_T: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_to_t_pre:v_Self -> Type0; f_to_t_post:v_Self -> v_T -> Type0; f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result) @@ -164,9 +175,14 @@ module Traits.Impl_expr_in_goal open Core open FStar.Mul -class t_T1 (v_Self: Type0) = { f_Assoc:Type0 } +class t_T1 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; + f_Assoc:Type0 +} -class t_T2 (v_Self: Type0) = { __marker_trait_t_T2:Prims.unit } +class t_T2 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self +} [@@ FStar.Tactics.Typeclasses.tcinstance] let impl @@ -230,6 +246,7 @@ open Core open FStar.Mul class t_MyTrait (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_my_method_pre:v_Self -> Type0; f_my_method_post:v_Self -> Prims.unit -> Type0; f_my_method:x0: v_Self @@ -263,6 +280,7 @@ open FStar.Mul type t_Type (v_TypeArg: Type0) (v_ConstArg: usize) = { f_field:t_Array v_TypeArg v_ConstArg } class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_method_pre: #v_MethodTypeArg: Type0 -> v_MethodConstArg: usize -> @@ -425,6 +443,7 @@ let associated_function_caller () class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; [@@@ FStar.Tactics.Typeclasses.no_method]_super_15145771689388873921:t_Trait v_Self v_TypeArg v_ConstArg; @@ -442,6 +461,7 @@ type t_Bar (v_FooConst: usize) (v_FooType: Type0) = | Bar : t_Array v_FooType v_FooConst -> t_Bar v_FooConst v_FooType class t_Foo (v_Self: Type0) (v_FooConst: usize) (v_FooType: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_fun_pre: v_FunConst: usize -> #v_FunType: Type0 -> @@ -505,11 +525,13 @@ open Core open FStar.Mul class t_Trait1 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_T:Type0; f_T_7969211799618487585:t_Trait1 f_T } class t_Trait2 (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; [@@@ FStar.Tactics.Typeclasses.no_method]_super_3259985701465885527:t_Trait1 v_Self; f_U:Type0 } @@ -530,6 +552,7 @@ open Core open FStar.Mul class t_PolyOp (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_op_pre:u32 -> u32 -> Type0; f_op_post:u32 -> u32 -> u32 -> Type0; f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result) @@ -567,6 +590,7 @@ open Core open FStar.Mul class t_SuperTrait (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; [@@@ FStar.Tactics.Typeclasses.no_method]_super_15837849249852401974: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; @@ -588,6 +612,7 @@ let impl: t_SuperTrait i32 = type t_Struct = | Struct : t_Struct class t_Bar (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_bar_pre:v_Self -> Type0; f_bar_post:v_Self -> Prims.unit -> Type0; f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result) @@ -650,6 +675,7 @@ let uuse_iimpl_trait (_: Prims.unit) : Prims.unit = () class t_Foo (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_4726684624731801277:Core.Marker.t_MetaSized v_Self; f_AssocType:Type0; f_AssocType_1162045947544099865:t_SuperTrait f_AssocType; f_N:usize; From 95101a5d8c780861bdaa77bf135b069884b03138 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 3 Jul 2025 17:04:33 +0200 Subject: [PATCH 4/6] Don't add `Drop` clauses to some more marker traits --- frontend/exporter/src/traits/utils.rs | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/frontend/exporter/src/traits/utils.rs b/frontend/exporter/src/traits/utils.rs index 3d469eb92..a8e561d8c 100644 --- a/frontend/exporter/src/traits/utils.rs +++ b/frontend/exporter/src/traits/utils.rs @@ -27,6 +27,7 @@ //! benefit of reducing the size of signatures. Moreover, the rules on which bounds are required vs //! implied are subtle. We may change this if this proves to be a problem. use rustc_hir::def::DefKind; +use rustc_hir::LangItem; use rustc_middle::ty::*; use rustc_span::def_id::DefId; use rustc_span::{Span, DUMMY_SP}; @@ -92,11 +93,21 @@ pub fn required_predicates<'tcx>( predicates.to_mut().insert(0, (self_clause, DUMMY_SP)); } if add_drop { - // Add a `T: Drop` bound for every generic, unless the current trait is `Drop` itself, or - // `Sized`. - let drop_trait = tcx.lang_items().drop_trait().unwrap(); - let sized_trait = tcx.lang_items().sized_trait().unwrap(); - if def_id != drop_trait && def_id != sized_trait { + // Add a `T: Drop` bound for every generic, unless the current trait is `Drop` itself, or a + // built-in marker trait that we know doesn't need the bound. + let lang_item = tcx.as_lang_item(def_id); + if !matches!( + lang_item, + Some( + LangItem::Drop + | LangItem::Sized + | LangItem::MetaSized + | LangItem::PointeeSized + | LangItem::DiscriminantKind + | LangItem::PointeeTrait + ) + ) { + let drop_trait = tcx.lang_items().drop_trait().unwrap(); let extra_bounds = tcx .generics_of(def_id) .own_params From 2380f4b40e498cbab61ed59d8874ca32d3705a4e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 3 Jul 2025 22:44:09 +0200 Subject: [PATCH 5/6] Normalize projections before translating them --- frontend/exporter/src/traits.rs | 4 ++-- frontend/exporter/src/traits/utils.rs | 19 ++++++++++++++++++- frontend/exporter/src/types/ty.rs | 12 +++++++++++- .../toolchain__traits into-fstar.snap | 12 ++++++++---- 4 files changed, 39 insertions(+), 8 deletions(-) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 06c53f42f..3c00f1642 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -6,8 +6,8 @@ mod resolution; mod utils; #[cfg(feature = "rustc")] pub use utils::{ - erase_and_norm, implied_predicates, predicates_defined_on, required_predicates, self_predicate, - Predicates, ToPolyTraitRef, + erase_and_norm, erase_free_regions, implied_predicates, normalize, predicates_defined_on, + required_predicates, self_predicate, Predicates, ToPolyTraitRef, }; #[cfg(feature = "rustc")] diff --git a/frontend/exporter/src/traits/utils.rs b/frontend/exporter/src/traits/utils.rs index a8e561d8c..cf0d94162 100644 --- a/frontend/exporter/src/traits/utils.rs +++ b/frontend/exporter/src/traits/utils.rs @@ -169,10 +169,27 @@ pub fn implied_predicates<'tcx>( } } +/// Normalize a value. +pub fn normalize<'tcx, T>(tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, value: T) -> T +where + T: TypeFoldable> + Copy, +{ + use rustc_infer::infer::TyCtxtInferExt; + use rustc_middle::traits::ObligationCause; + use rustc_trait_selection::traits::query::normalize::QueryNormalizeExt; + let (infcx, param_env) = tcx.infer_ctxt().build_with_typing_env(typing_env); + infcx + .at(&ObligationCause::dummy(), param_env) + .query_normalize(value) + // We ignore the generated outlives relations. Unsure what we should do with them. + .map(|x| x.value) + .unwrap_or(value) +} + /// Erase free regions from the given value. Largely copied from `tcx.erase_regions`, but also /// erases bound regions that are bound outside `value`, so we can call this function inside a /// `Binder`. -fn erase_free_regions<'tcx, T>(tcx: TyCtxt<'tcx>, value: T) -> T +pub fn erase_free_regions<'tcx, T>(tcx: TyCtxt<'tcx>, value: T) -> T where T: TypeFoldable>, { diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index 34e3e0e69..bfc1fe3e9 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -804,7 +804,17 @@ impl Alias { alias_ty: &ty::AliasTy<'tcx>, ) -> TyKind { let tcx = s.base().tcx; + let typing_env = s.typing_env(); use rustc_type_ir::AliasTyKind as RustAliasKind; + + // Try to normalize the alias first. + let ty = ty::Ty::new_alias(tcx, *alias_kind, *alias_ty); + let ty = crate::traits::normalize(tcx, typing_env, ty); + let ty::Alias(alias_kind, alias_ty) = ty.kind() else { + let ty: Ty = ty.sinto(s); + return ty.kind().clone(); + }; + let kind = match alias_kind { RustAliasKind::Projection => { let trait_ref = alias_ty.trait_ref(tcx); @@ -820,7 +830,7 @@ impl Alias { // yet we dont have a binder around (could even be several). Binding this correctly // is therefore difficult. Since our trait resolution ignores lifetimes anyway, we // just erase them. See also https://github.com/hacspec/hax/issues/747. - let trait_ref = crate::traits::erase_and_norm(tcx, s.typing_env(), trait_ref); + let trait_ref = crate::traits::erase_free_regions(tcx, trait_ref); AliasKind::Projection { assoc_item: tcx.associated_item(alias_ty.def_id).sinto(s), impl_expr: solve_trait(s, ty::Binder::dummy(trait_ref)), diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index f0132d6a7..3bac0d098 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -666,11 +666,15 @@ let iter_option (#v_T: Type0) (x: Core.Option.t_Option v_T) : Core.Option.t_Into (Core.Option.impl__as_ref #v_T x <: Core.Option.t_Option v_T) let uuse_iimpl_trait (_: Prims.unit) : Prims.unit = - let iter:_ = iter_option #bool (Core.Option.Option_Some false <: Core.Option.t_Option bool) in - let tmp0, out:(_ & Core.Option.t_Option bool) = - Core.Iter.Traits.Iterator.f_next #_ #FStar.Tactics.Typeclasses.solve iter + let iter:Core.Option.t_IntoIter bool = + iter_option #bool (Core.Option.Option_Some false <: Core.Option.t_Option bool) in - let iter:_ = tmp0 in + let tmp0, out:(Core.Option.t_IntoIter bool & Core.Option.t_Option bool) = + Core.Iter.Traits.Iterator.f_next #(Core.Option.t_IntoIter bool) + #FStar.Tactics.Typeclasses.solve + iter + in + let iter:Core.Option.t_IntoIter bool = tmp0 in let _:Core.Option.t_Option bool = out in () From 6194bf2e32aeb5b89b909d0cc783ec9fac1f0bd6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 3 Jul 2025 22:44:46 +0200 Subject: [PATCH 6/6] Resolve assoc ty predicates in builtin `ImplExpr`s --- frontend/exporter/src/sinto.rs | 8 ++++++++ frontend/exporter/src/traits.rs | 2 +- frontend/exporter/src/traits/resolution.rs | 11 +++++++++-- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/frontend/exporter/src/sinto.rs b/frontend/exporter/src/sinto.rs index 15d65f66b..8363ecb78 100644 --- a/frontend/exporter/src/sinto.rs +++ b/frontend/exporter/src/sinto.rs @@ -65,6 +65,14 @@ impl, R: SInto> SInto for (L, R) } } +impl, B: SInto, C: SInto> SInto + for (A, B, C) +{ + fn sinto(&self, s: &S) -> (AA, BB, CC) { + (self.0.sinto(s), self.1.sinto(s), self.2.sinto(s)) + } +} + impl> SInto> for Option { fn sinto(&self, s: &S) -> Option { self.as_ref().map(|x| x.sinto(s)) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 3c00f1642..6879130f6 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -140,7 +140,7 @@ pub enum ImplExprAtom { /// FnOnce`. impl_exprs: Vec, /// The values of the associated types for this trait. - types: Vec<(DefId, Ty)>, + types: Vec<(DefId, Ty, Vec)>, }, /// An error happened while resolving traits. Error(String), diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index 6ac0989e3..a13291898 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -89,7 +89,7 @@ pub enum ImplExprAtom<'tcx> { /// FnOnce`. impl_exprs: Vec>, /// The values of the associated types for this trait. - types: Vec<(DefId, Ty<'tcx>)>, + types: Vec<(DefId, Ty<'tcx>, Vec>)>, }, /// An error happened while resolving traits. Error(String), @@ -495,7 +495,14 @@ impl<'tcx> PredicateSearcher<'tcx> { return None; } } - Some((assoc.def_id, ty)) + let impl_exprs = self + .resolve_item_implied_predicates( + assoc.def_id, + erased_tref.skip_binder().args, + warn, + ) + .ok()?; + Some((assoc.def_id, ty, impl_exprs)) }) .collect(); ImplExprAtom::Builtin {