From ba21ef7f26f7ce3a4ed8208c7624aa5c7d476d0e Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 30 Apr 2026 10:57:11 +0200 Subject: [PATCH 1/5] Option for producing names and expected types compatible with core_models lean library. --- src/extract/ExtractName.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/extract/ExtractName.ml b/src/extract/ExtractName.ml index 294499309..675cb947c 100644 --- a/src/extract/ExtractName.ml +++ b/src/extract/ExtractName.ml @@ -143,7 +143,10 @@ let pattern_to_extract_name (_span : Meta.span option) (name : pattern) : let c = { tgt = TkName } in let visitor = pattern_to_extract_name_visitor in let name = visitor#visit_pattern () name in - List.map (pattern_elem_to_string c) name + let names = List.map (pattern_elem_to_string c) name in + match names with + | "core" :: rest when !Config.core_models_lib -> "core_models" :: rest + | _ -> names let name_matcher_expr_to_extract_name (_span : Meta.span option) (name : expr) : string = From 41508c69b8c80a89b1c5f6a8516fc19d09b95e20 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 30 Apr 2026 14:25:53 +0200 Subject: [PATCH 2/5] Prefix with crate name for impl names. --- src/extract/ExtractBase.ml | 1 + src/extract/ExtractName.ml | 10 ++++++++-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml index bb20060ca..121006532 100644 --- a/src/extract/ExtractBase.ml +++ b/src/extract/ExtractBase.ml @@ -1922,6 +1922,7 @@ let ctx_compute_trait_impl_name_raw (ctx : extraction_ctx) if !core_models_lib && not trait_impl.item_meta.is_local then match trait_impl.item_meta.name with | PeIdent (crate, _) :: _ -> + let crate = rewrite_crate_for_core_models_lib crate in let already_prefixed = self_name = crate || String.starts_with ~prefix:(crate ^ ".") self_name diff --git a/src/extract/ExtractName.ml b/src/extract/ExtractName.ml index 675cb947c..b99327f35 100644 --- a/src/extract/ExtractName.ml +++ b/src/extract/ExtractName.ml @@ -134,6 +134,12 @@ let pattern_to_extract_name_visitor = else super#visit_EPrimAdt () adt g end +(** Under [-core-models-lib], the [core] Rust crate is renamed to [core_models] + in extracted names so that the user's [core_models] Lean library is + referenced instead of Aeneas's standard library. *) +let rewrite_crate_for_core_models_lib (crate : string) : string = + if !Config.core_models_lib && crate = "core" then "core_models" else crate + (** Helper to convert name patterns to names for extraction. For impl blocks, we simply use the name of the type (without its arguments) @@ -145,8 +151,8 @@ let pattern_to_extract_name (_span : Meta.span option) (name : pattern) : let name = visitor#visit_pattern () name in let names = List.map (pattern_elem_to_string c) name in match names with - | "core" :: rest when !Config.core_models_lib -> "core_models" :: rest - | _ -> names + | head :: rest -> rewrite_crate_for_core_models_lib head :: rest + | [] -> [] let name_matcher_expr_to_extract_name (_span : Meta.span option) (name : expr) : string = From 963a6149926e37645fadcfd16aca750e9a4ac121 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 18 May 2026 14:14:58 +0200 Subject: [PATCH 3/5] remove core -> core_models renaming --- src/extract/ExtractBase.ml | 1 - src/extract/ExtractName.ml | 11 +---------- 2 files changed, 1 insertion(+), 11 deletions(-) diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml index 121006532..bb20060ca 100644 --- a/src/extract/ExtractBase.ml +++ b/src/extract/ExtractBase.ml @@ -1922,7 +1922,6 @@ let ctx_compute_trait_impl_name_raw (ctx : extraction_ctx) if !core_models_lib && not trait_impl.item_meta.is_local then match trait_impl.item_meta.name with | PeIdent (crate, _) :: _ -> - let crate = rewrite_crate_for_core_models_lib crate in let already_prefixed = self_name = crate || String.starts_with ~prefix:(crate ^ ".") self_name diff --git a/src/extract/ExtractName.ml b/src/extract/ExtractName.ml index b99327f35..294499309 100644 --- a/src/extract/ExtractName.ml +++ b/src/extract/ExtractName.ml @@ -134,12 +134,6 @@ let pattern_to_extract_name_visitor = else super#visit_EPrimAdt () adt g end -(** Under [-core-models-lib], the [core] Rust crate is renamed to [core_models] - in extracted names so that the user's [core_models] Lean library is - referenced instead of Aeneas's standard library. *) -let rewrite_crate_for_core_models_lib (crate : string) : string = - if !Config.core_models_lib && crate = "core" then "core_models" else crate - (** Helper to convert name patterns to names for extraction. For impl blocks, we simply use the name of the type (without its arguments) @@ -149,10 +143,7 @@ let pattern_to_extract_name (_span : Meta.span option) (name : pattern) : let c = { tgt = TkName } in let visitor = pattern_to_extract_name_visitor in let name = visitor#visit_pattern () name in - let names = List.map (pattern_elem_to_string c) name in - match names with - | head :: rest -> rewrite_crate_for_core_models_lib head :: rest - | [] -> [] + List.map (pattern_elem_to_string c) name let name_matcher_expr_to_extract_name (_span : Meta.span option) (name : expr) : string = From 2dbc1d51054756cd62cbf5535658d7643bed0dc4 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 3 Jun 2026 11:43:36 +0200 Subject: [PATCH 4/5] Remove any non standard field of under -core-models-option. --- src/PrePasses.ml | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/src/PrePasses.ml b/src/PrePasses.ml index cd2a73db0..09bfd942f 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -1209,14 +1209,15 @@ let filter_marker_traits (crate : crate) : crate = in visitor#visit_crate () crate -(** Under [-core-models-lib], remove the [assert_receiver_is_total_eq] method - from the [core::cmp::Eq] trait declaration, from any impls of [Eq], and drop - the corresponding function declarations. This is a Rust-only, - [#[doc(hidden)]] method with an empty default body that Aeneas's own - standard library handles via a hand-tuned override; an external library like - [core_models] doesn't model it, so emitting an impl field for it would not - typecheck against [core_models]'s [Eq] structure. *) -let filter_eq_assert_receiver_method (crate : crate) : crate = +(** Under [-core-models-lib], remove the [Eq] marker method (named + [assert_fields_are_eq] in current rustc, formerly + [assert_receiver_is_total_eq]) from the [core::cmp::Eq] trait declaration, + from any impls of [Eq], and drop the corresponding function declarations. + This is a Rust-only, [#[doc(hidden)]] method with an empty default body that + Aeneas's own standard library handles via a hand-tuned override; an external + library like [core_models] doesn't model it, so emitting an impl field for + it would not typecheck against [core_models]'s [Eq] structure. *) +let filter_eq_assert_fields_method (crate : crate) : crate = if not !Config.core_models_lib then crate else let mctx = NameMatcher.ctx_from_crate crate in @@ -1240,12 +1241,17 @@ let filter_eq_assert_receiver_method (crate : crate) : crate = match eq_id with | None -> crate | Some eq_id -> - let method_name = "assert_receiver_is_total_eq" in + (* The method is named [assert_fields_are_eq] in current rustc; older + versions called it [assert_receiver_is_total_eq]. Match either so the + pass is robust across charon updates. *) + let method_names = + [ "assert_fields_are_eq"; "assert_receiver_is_total_eq" ] + in let eq_decl = TraitDeclId.Map.find eq_id crate.trait_decls in let filtered_method_ids = TraitMethodId.Map.fold (fun mid (m : trait_method binder) acc -> - if m.binder_value.name = method_name then + if List.mem m.binder_value.name method_names then TraitMethodId.Set.add mid acc else acc) eq_decl.methods TraitMethodId.Set.empty @@ -2424,7 +2430,7 @@ let apply_passes (crate : crate) : crate = in let crate = { crate with fun_decls } in let crate = strip_unnecessary_target_suffixes crate in - let crate = filter_eq_assert_receiver_method crate in + let crate = filter_eq_assert_fields_method crate in let crate = filter_marker_traits crate in let crate = filter_type_aliases crate in let crate = replace_static crate in From 72a259f5db4ec8ef9e3df47b5b9247480b96615e Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 4 Jun 2026 11:51:33 +0200 Subject: [PATCH 5/5] Filter allocators when needed under core-models option. --- src/extract/Extract.ml | 56 +++++++++++++++++++++++++---- src/extract/ExtractBuiltin.ml | 21 +++++++++++ src/symbolic/SymbolicToPureTypes.ml | 15 ++++++++ 3 files changed, 85 insertions(+), 7 deletions(-) diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 914fe549a..4f42b718d 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -49,6 +49,7 @@ let texpr_to_string (ctx : extraction_ctx) = let compute_allocator_filter ?(extra_trait_decl_refs : Pure.trait_decl_ref list = []) ?(extra_trait_refs : Pure.trait_ref list = []) + ?(type_args_filter : Pure.type_decl_id -> bool list option = fun _ -> None) (generics : Pure.generic_params) (inputs : Pure.ty list) (output : Pure.ty option) (preds : Pure.predicates) : (bool list * bool list) option = @@ -56,10 +57,37 @@ let compute_allocator_filter let trait_clauses = generics.trait_clauses in if type_params = [] then None else + (* When visiting a type application of an ADT whose own allocator parameter + is being filtered (e.g. [IntoIter T A] -> [IntoIter T]), we must not count + the type variables that only appear in the dropped argument positions as + "used". Otherwise an allocator parameter that only shows up in, say, the + output type [IntoIter] would be wrongly kept. *) + let visit_filtered_ty_args (self : _) (env : unit) (type_id : Pure.type_id) + (generics : Pure.generic_args) : bool = + match type_id with + | TAdtId id -> ( + match type_args_filter id with + | Some keep when List.length keep = List.length generics.types -> + List.iter2 + (fun b ty -> if b then self#visit_ty env ty) + keep generics.types; + List.iter (self#visit_const_generic env) generics.const_generics; + List.iter (self#visit_trait_ref env) generics.trait_refs; + true + | _ -> false) + | _ -> false + in let used = ref Pure.TypeVarId.Set.empty in let body_visitor = - object - inherit [_] Pure.iter_type_decl + object (self) + inherit [_] Pure.iter_type_decl as super + + method! visit_ty env t = + match t with + | Pure.TAdt (type_id, generics) + when visit_filtered_ty_args self env type_id generics -> () + | _ -> super#visit_ty env t + method! visit_type_var_id _ id = used := Pure.TypeVarId.Set.add id !used end in @@ -73,8 +101,15 @@ let compute_allocator_filter let clause_tvars (c : Pure.trait_param) : Pure.TypeVarId.Set.t = let s = ref Pure.TypeVarId.Set.empty in let v = - object - inherit [_] Pure.iter_type_decl + object (self) + inherit [_] Pure.iter_type_decl as super + + method! visit_ty env t = + match t with + | Pure.TAdt (type_id, generics) + when visit_filtered_ty_args self env type_id generics -> () + | _ -> super#visit_ty env t + method! visit_type_var_id _ id = s := Pure.TypeVarId.Set.add id !s end in @@ -140,8 +175,12 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) if not !Config.core_models_lib then ctx else let sg = def.f.signature in + let type_args_filter id = + TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map + in match - compute_allocator_filter sg.generics sg.inputs (Some sg.output) sg.preds + compute_allocator_filter ~type_args_filter sg.generics sg.inputs + (Some sg.output) sg.preds with | None -> ctx | Some (keep_params, keep_trait_clauses) -> @@ -3127,11 +3166,14 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) if not !Config.core_models_lib then ctx else let assoc_tys = List.map (fun (_, _, ty) -> ty) trait_impl.types in + let type_args_filter id = + TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map + in match compute_allocator_filter ~extra_trait_decl_refs:[ trait_impl.impl_trait ] - ~extra_trait_refs:trait_impl.parent_trait_refs trait_impl.generics - assoc_tys None trait_impl.preds + ~extra_trait_refs:trait_impl.parent_trait_refs ~type_args_filter + trait_impl.generics assoc_tys None trait_impl.preds with | None -> ctx | Some (keep_params, keep_trait_clauses) -> diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index 86f5be0e5..f76049e16 100644 --- a/src/extract/ExtractBuiltin.ml +++ b/src/extract/ExtractBuiltin.ml @@ -180,6 +180,27 @@ let mk_builtin_types_map () = let builtin_types_map = mk_memoized mk_builtin_types_map +(** Map from rust type name to its builtin info, restricted to the types that + carry a [keep_params] filter (i.e. types from which Charon's + [hide_allocator] pass leaves a dangling allocator type parameter, such as + [alloc::vec::into_iter::IntoIter]). + + Unlike {!builtin_types_map}, this map is *not* emptied under + [-core-models-lib]: even when the builtin type overrides are disabled, we + still need to drop the dangling allocator type parameter so that the + extracted types match the [core_models] library, which models them without + an allocator (e.g. [IntoIter T] rather than [IntoIter T Global]). *) +let mk_builtin_types_keep_params_map () = + NameMatcherMap.of_list + (List.filter_map + (fun (info : Pure.builtin_type_info) -> + match info.keep_params with + | Some _ -> Some (info.rust_name, info) + | None -> None) + lean_builtin_types) + +let builtin_types_keep_params_map = mk_memoized mk_builtin_types_keep_params_map + let int_and_smaller_list : (string * string) list = let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in let int_names = List.rev [ "i8"; "i16"; "i32"; "i64"; "i128" ] in diff --git a/src/symbolic/SymbolicToPureTypes.ml b/src/symbolic/SymbolicToPureTypes.ml index d35b6d67a..95371ae65 100644 --- a/src/symbolic/SymbolicToPureTypes.ml +++ b/src/symbolic/SymbolicToPureTypes.ml @@ -311,6 +311,21 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : match_name_find_opt ctx def.item_meta.name (ExtractBuiltin.builtin_types_map ()) in + (* Under [-core-models-lib] the builtin type overrides are disabled, so the + lookup above returns [None]. We still need the allocator [keep_params] of + types like [IntoIter] so that the dangling allocator type parameter (left + by Charon's [hide_allocator] pass) is filtered out, matching the + [core_models] library. Recover it from the dedicated, non-disabled map. + This only carries [keep_params]; the extract name still comes from the + standard name mangling (which, for these types, coincides with the builtin + name anyway). *) + let builtin_info = + if Option.is_some builtin_info || not !Config.core_models_lib then + builtin_info + else + match_name_find_opt ctx def.item_meta.name + (ExtractBuiltin.builtin_types_keep_params_map ()) + in { def_id; name;