Upload precompiled oleans for release

.github/workflows/release.yml

@@ -118,6 +118,12 @@ jobs:
             "$script"
           fi
 
+      - name: Upload Lean oleans
+        uses: softprops/action-gh-release@v2
+        with:
+          tag_name: ${{ needs.prepare.outputs.tag_name }}
+          files: dist_staging/backends/lean/.lake/aeneas-*.tar.gz
+
       - name: Re-package Tarball
         run: |
           set -eo pipefail

backends/lean/lakefile.lean

@@ -5,7 +5,8 @@ open Lake DSL
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @ "v4.30.0-rc2"
 
-package «aeneas» {}
+package «aeneas» where
+  preferReleaseBuild := true
 
 @[default_target] lean_lib «Aeneas» {}
 

scripts/ci-precompile-lean.sh

@@ -13,5 +13,9 @@ fi
 # required for plugin loading.
 CI="" lake build
 
+# Pack prebuilt oleans into an archive for Lake's automatic olean download.
+# Users who pin to a release tag get these instead of compiling from source.
+lake pack
+
 # Delete heavy dependency sources to keep the release archive small.
 rm -rf .lake/packages

src/Config.ml

@@ -598,3 +598,14 @@ let max_recdepth = ref 2048
 (** If [false], evaluate [drop(p)] as [p := bottom]. Otherwise, evaluate it as a
     no-op (which means that we do not borrow-check the drops). *)
 let drop_as_no_op = ref true
+
+(** For Lean only: disable the Rust core library overrides defined in
+    [ExtractBuiltinLean.ml].
+
+    With this flag, references to items such as [core::clone::Clone<[T; N]>] are
+    extracted using the standard name-mangling scheme rather than the hand-tuned
+    names like [core.array.CloneArray.clone], and the associated shape overrides
+    ([keep_params], [can_fail], etc.) are ignored. This is useful when
+    extracting against a separate Lean library that mirrors the Rust core API
+    under the standard names. *)
+let core_models_lib = ref false

src/Main.ml

@@ -211,6 +211,14 @@ let () =
          collisions with field projectors. Example: the `len` method in `impl \
          Struct { fn len(&self) -> usize { ... } }` would be named \
          `Struct.impl.len`." );
+      ( "-core-models-lib",
+        Arg.Set core_models_lib,
+        " For Lean: disable the Rust core library overrides from \
+         ExtractBuiltinLean.ml. Items like the `Clone` impl for arrays are \
+         extracted using the standard name-mangling scheme rather than \
+         hand-tuned names such as `core.array.CloneArray.clone`, and the \
+         associated shape overrides (keep_params, can_fail, etc.) are ignored."
+      );
       ( "-all-computable",
         Arg.Set all_computable,
         " For Lean: do not insert `noncomputable section` at the top of the \
@@ -457,6 +465,9 @@ let () =
   if !lean_gen_lakefile && not (backend () = Lean) then
     fail_with_error
       "The -lean-default-lakefile option is valid only for the Lean backend";
+  if !core_models_lib && not (backend () = Lean) then
+    fail_with_error
+      "The -core-models-lib option is valid only for the Lean backend";
   if !set_max_heartbeats && not (backend () = Lean) then
     fail_with_error
       "The -max-heartbeats option is valid only for the Lean backend";

src/PrePasses.ml

@@ -1209,6 +1209,135 @@ let filter_marker_traits (crate : crate) : crate =
     in
     visitor#visit_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
+    let pat = NameMatcher.parse_pattern "core::cmp::Eq" in
+    let match_config =
+      {
+        NameMatcher.map_vars_to_vars = true;
+        match_with_trait_decl_refs = Config.match_patterns_with_trait_decl_refs;
+      }
+    in
+    let eq_id =
+      TraitDeclId.Map.fold
+        (fun id (decl : trait_decl) acc ->
+          if
+            acc = None
+            && NameMatcher.match_name mctx match_config pat decl.item_meta.name
+          then Some id
+          else acc)
+        crate.trait_decls None
+    in
+    match eq_id with
+    | None -> crate
+    | Some eq_id ->
+        (* 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 List.mem m.binder_value.name method_names then
+                TraitMethodId.Set.add mid acc
+              else acc)
+            eq_decl.methods TraitMethodId.Set.empty
+        in
+        if TraitMethodId.Set.is_empty filtered_method_ids then crate
+        else
+          let trait_decls =
+            TraitDeclId.Map.update eq_id
+              (function
+                | None -> None
+                | Some (d : trait_decl) ->
+                    Some
+                      {
+                        d with
+                        methods =
+                          TraitMethodId.Map.filter
+                            (fun mid _ ->
+                              not
+                                (TraitMethodId.Set.mem mid filtered_method_ids))
+                            d.methods;
+                      })
+              crate.trait_decls
+          in
+          (* Collect fun_decl_ids backing the filtered methods of every [Eq]
+             trait impl, and strip those methods from the impl's method map. *)
+          let dropped_fun_decl_ids = ref FunDeclId.Set.empty in
+          let trait_impls =
+            TraitImplId.Map.map
+              (fun (impl : trait_impl) ->
+                if impl.impl_trait.id <> eq_id then impl
+                else
+                  let methods =
+                    TraitMethodId.Map.filter
+                      (fun mid (m : fun_decl_ref binder) ->
+                        if TraitMethodId.Set.mem mid filtered_method_ids then begin
+                          dropped_fun_decl_ids :=
+                            FunDeclId.Set.add m.binder_value.id
+                              !dropped_fun_decl_ids;
+                          false
+                        end
+                        else true)
+                      impl.methods
+                  in
+                  { impl with methods })
+              crate.trait_impls
+          in
+          let fun_decls =
+            FunDeclId.Map.filter
+              (fun id _ -> not (FunDeclId.Set.mem id !dropped_fun_decl_ids))
+              crate.fun_decls
+          in
+          let declarations =
+            List.filter_map
+              (fun (g : declaration_group) ->
+                match g with
+                | FunGroup (NonRecGroup id) ->
+                    if FunDeclId.Set.mem id !dropped_fun_decl_ids then None
+                    else Some g
+                | FunGroup (RecGroup ids) ->
+                    let ids =
+                      List.filter
+                        (fun id ->
+                          not (FunDeclId.Set.mem id !dropped_fun_decl_ids))
+                        ids
+                    in
+                    if ids = [] then None else Some (FunGroup (RecGroup ids))
+                | MixedGroup g -> (
+                    let is_dropped (id : item_id) =
+                      match id with
+                      | IdFun id -> FunDeclId.Set.mem id !dropped_fun_decl_ids
+                      | _ -> false
+                    in
+                    match g with
+                    | NonRecGroup id ->
+                        if is_dropped id then None else Some (MixedGroup g)
+                    | RecGroup ids ->
+                        let ids =
+                          List.filter (fun id -> not (is_dropped id)) ids
+                        in
+                        if ids = [] then None
+                        else Some (MixedGroup (RecGroup ids)))
+                | _ -> Some g)
+              crate.declarations
+          in
+          { crate with trait_decls; trait_impls; fun_decls; declarations }
+
 (* Remove the type aliases from the type declarations and declaration groups *)
 let filter_type_aliases (crate : crate) : crate =
   let type_decl_is_alias (ty : type_decl) =
@@ -2304,6 +2433,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_fields_method crate in
   let crate = filter_marker_traits crate in
   let crate = filter_type_aliases crate in
   let crate = replace_static crate in

src/Translate.ml

@@ -13,6 +13,12 @@ open Parallel
 (** The local logger *)
 let log = TranslateCore.log
 
+(** When [-core-models-lib] is on, non-local items are skipped from the main
+    extracted files (the user is expected to provide them via a separate Lean
+    library, e.g. [core_models] for [core::*] items). *)
+let skip_for_core_models_lib (is_local : bool) : bool =
+  !Config.core_models_lib && not is_local
+
 (** The result of running the symbolic interpreter on a function:
     - the list of symbolic values used for the input values
     - the generated symbolic AST *)
@@ -758,6 +764,12 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
     assert (List.for_all (fun b -> b) builtin)
+  else if
+    List.exists
+      (fun (d : Pure.type_decl) ->
+        skip_for_core_models_lib d.item_meta.is_local)
+      defs
+  then ()
   else if List.exists dont_extract defs then
     (* Check if we have to ignore declarations *)
     (* Sanity check *)
@@ -838,6 +850,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     && match_name_find_opt ctx.trans_ctx global.item_meta.name
          (builtin_globals_map ())
        = None
+    && not (skip_for_core_models_lib global.item_meta.is_local)
   in
   if extract then (
     (* We don't wrap global declaration groups between calls to functions
@@ -967,6 +980,12 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
     assert (List.for_all (fun b -> b) builtin)
+  else if
+    List.exists
+      (fun (trans : pure_fun_translation) ->
+        skip_for_core_models_lib trans.f.item_meta.is_local)
+      pure_ls
+  then ()
   else
     (* Utility to check a function has a decrease clause *)
     let has_decreases_clause (def : Pure.fun_decl) : bool =
@@ -1070,7 +1089,10 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
       (TraitDeclId.Map.find_opt trait_decl_id ctx.trans_trait_decls)
   in
   (* Check if the trait declaration is builtin, in which case we ignore it *)
-  if not (trait_decl_is_builtin ctx trait_decl_id) then (
+  if
+    (not (trait_decl_is_builtin ctx trait_decl_id))
+    && not (skip_for_core_models_lib trait_decl.item_meta.is_local)
+  then (
     let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
     if extract_decl then (
       Extract.extract_trait_decl ctx fmt trait_decl;
@@ -1088,7 +1110,10 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     [%silent_unwrap_opt_span] None
       (TraitImplId.Map.find_opt trait_impl_id ctx.trans_trait_impls)
   in
-  if not (trait_impl_is_builtin ctx trait_impl_id) then (
+  if
+    (not (trait_impl_is_builtin ctx trait_impl_id))
+    && not (skip_for_core_models_lib trait_impl.item_meta.is_local)
+  then (
     Extract.extract_trait_impl ctx fmt ~is_rec trait_impl;
     EmitJson.record_trait_impl_if_enabled ctx trait_impl)
 
@@ -1343,12 +1368,19 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       Printf.fprintf out "Module %s.\n" fi.module_name
   | Lean ->
       Printf.fprintf out "import Aeneas\n";
+      if !Config.core_models_lib then Printf.fprintf out "import CoreModels\n";
       (* Add the custom imports *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_imports;
       (* Add the custom includes *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes;
       (* Always open the Primitives namespace *)
-      Printf.fprintf out "open Aeneas Aeneas.Std Result ControlFlow Error\n";
+      if !Config.core_models_lib then begin
+        Printf.fprintf out "open CoreModels Aeneas\n";
+        Printf.fprintf out "open Aeneas.Std hiding namespace core alloc\n";
+        Printf.fprintf out "open Result ControlFlow Error\n"
+      end
+      else
+        Printf.fprintf out "open Aeneas Aeneas.Std Result ControlFlow Error\n";
       (* It happens that we generate duplicated namespaces, like `betree.betree`.
          We deactivate the linter for this, because otherwise it leads to too much
          noise. *)