Add more definitions to the Lean library and add deboguing features

backends/lean/Base/Primitives/ArraySlice.lean

@@ -582,4 +582,7 @@ def core.slice.Slice.copy_from_slice {T : Type} (_ : core.marker.Copy T)
   if s.len = src.len then ok src
   else fail panic
 
+/- [core::array::TryFromSliceError] -/
+def core.array.TryFromSliceError := ()
+
 end Primitives

backends/lean/Base/Primitives/Core.lean

@@ -111,3 +111,43 @@ def core.convert.IntoFrom {T : Type} {U : Type} (fromInst : core.convert.From U
 def core.convert.FromSame (T : Type) : core.convert.From T T := {
   from_ := fun x => ok (core.convert.FromSame.from_ x)
 }
+
+/- [core::result::Result] -/
+inductive core.result.Result (T : Type) (E : Type) :=
+| Ok : T → core.result.Result T E
+| Err : E → core.result.Result T E
+
+/- [core::fmt::Error] -/
+@[reducible] def core.fmt.Error := Unit
+
+structure core.convert.TryFrom (Self T : Type) where
+  Error : Type
+  try_from : T → Result (core.result.Result Self Error)
+
+structure core.convert.TryInto (Self T : Type) where
+  Error : Type
+  try_into : Self → Result (core.result.Result T Error)
+
+@[reducible, simp]
+def core.convert.TryIntoFrom.try_into {T U : Type} (fromInst : core.convert.TryFrom U T)
+  (x : T) : Result (core.result.Result U fromInst.Error) :=
+  fromInst.try_from x
+
+@[reducible]
+def core.convert.TryIntoFrom {T U : Type} (fromInst : core.convert.TryFrom U T) :
+  core.convert.TryInto T U := {
+  Error := fromInst.Error
+  try_into := core.convert.TryIntoFrom.try_into fromInst
+}
+
+/- TODO: -/
+axiom Formatter : Type
+
+structure core.fmt.Debug (T : Type) where
+  fmt : T → Formatter → Result (Formatter × Formatter → Formatter)
+
+def core.result.Result.unwrap {T E : Type}
+  (_ : core.fmt.Debug T) (e : core.result.Result T E) : Primitives.Result T :=
+  match e with
+  | .Ok x => ok x
+  | .Err _ => fail .panic

src/Config.ml

@@ -45,6 +45,9 @@ let if_backend (f : unit -> 'a) (default : 'a) : 'a =
   | None -> default
   | Some _ -> f ()
 
+(** Print all the external definitions which are not listed in the builtin functions *)
+let print_unknown_externals = ref false
+
 (** {1 Interpreter} *)
 
 (** Activate the sanity checks, and in particular the invariant checks

src/Errors.ml

@@ -57,6 +57,16 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option)
 let craise (file : string) (line : int) (span : Meta.span) (msg : string) =
   craise_opt_span file line (Some span) msg
 
+(** Lazy assert *)
+let classert_opt_span (file : string) (line : int) (b : bool)
+    (span : Meta.span option) (msg : string Lazy.t) =
+  if not b then craise_opt_span file line span (Lazy.force msg)
+
+(** Lazy assert *)
+let classert (file : string) (line : int) (b : bool) (span : Meta.span)
+    (msg : string Lazy.t) =
+  classert_opt_span file line b (Some span) msg
+
 let cassert_opt_span (file : string) (line : int) (b : bool)
     (span : Meta.span option) (msg : string) =
   if not b then craise_opt_span file line span msg

src/Main.ml

@@ -57,6 +57,37 @@ Usage: %s [OPTIONS] FILE
 |}
     Sys.argv.(0)
 
+let matches_name (c : crate) (name : Types.name)
+    (m : 'a ExtractName.NameMatcherMap.t) : bool =
+  let open Charon.NameMatcher in
+  let open ExtractBuiltin in
+  let mctx : ctx =
+    {
+      type_decls = c.type_decls;
+      global_decls = c.global_decls;
+      fun_decls = c.fun_decls;
+      trait_decls = c.trait_decls;
+      trait_impls = c.trait_impls;
+    }
+  in
+  NameMatcherMap.mem mctx name m
+
+let matches_name_with_generics (c : crate) (name : Types.name)
+    (generics : Types.generic_args) (m : 'a ExtractName.NameMatcherMap.t) : bool
+    =
+  let open Charon.NameMatcher in
+  let open ExtractBuiltin in
+  let mctx : ctx =
+    {
+      type_decls = c.type_decls;
+      global_decls = c.global_decls;
+      fun_decls = c.fun_decls;
+      trait_decls = c.trait_decls;
+      trait_impls = c.trait_impls;
+    }
+  in
+  Option.is_some (NameMatcherMap.find_with_generics_opt mctx name generics m)
+
 let () =
   (* Measure start time *)
   let start_time = Unix.gettimeofday () in
@@ -129,6 +160,10 @@ let () =
         Arg.Set use_nested_tuple_projectors,
         " Use nested projectors for tuples (e.g., (0, 1, 2).snd.fst instead of \
          (0, 1, 2).1)." );
+      ( "-print-unknown-externals",
+        Arg.Set print_unknown_externals,
+        " Print all the external definitions which are not listed in the \
+         builtin functions" );
     ]
   in
 
@@ -190,8 +225,6 @@ let () =
     if cond then fail_with_error msg
   in
 
-  if !print_llbc then main_log#set_level EL.Debug;
-
   (* Sanity check (now that the arguments are parsed!) *)
   check_arg_implies
     (not !extract_template_decreases_clauses)
@@ -300,7 +333,9 @@ let () =
   | Ok m ->
       (* Logging *)
       log#linfo (lazy ("Imported: " ^ filename));
-      log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
+      if !print_llbc then
+        log#linfo (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"))
+      else log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
 
       (* Check the Charon CLI options *)
       check_no_doc m.options.hide_marker_traits
@@ -323,6 +358,144 @@ let () =
            definitions";
         fail true);
 
+      (* Print the external definitions which are not listed in the builtin functions *)
+      if !print_unknown_externals then (
+        let open TranslateCore in
+        let { type_decls; fun_decls; global_decls; trait_decls; trait_impls; _ }
+            =
+          m
+        in
+        (* Filter the definitions *)
+        let type_decls =
+          Types.TypeDeclId.Map.filter
+            (fun _ (d : Types.type_decl) ->
+              let names_map = ExtractBuiltin.builtin_types_map () in
+              (not d.item_meta.is_local)
+              && not (matches_name m d.item_meta.name names_map))
+            type_decls
+        in
+        let fun_decls =
+          LlbcAst.FunDeclId.Map.filter
+            (fun _ (d : LlbcAst.fun_decl) ->
+              let names_map = ExtractBuiltin.builtin_funs_map () in
+              (not d.item_meta.is_local)
+              && (not (matches_name m d.item_meta.name names_map))
+              (* We also ignore the trait method declarations *)
+              &&
+              match d.kind with
+              | TraitDeclItem _ -> false
+              | _ -> true)
+            fun_decls
+        in
+        let global_decls =
+          LlbcAst.GlobalDeclId.Map.filter
+            (fun _ (d : LlbcAst.global_decl) ->
+              let funs_map = ExtractBuiltin.builtin_globals_map in
+              (not d.item_meta.is_local)
+              && not (matches_name m d.item_meta.name funs_map))
+            global_decls
+        in
+        let trait_decls =
+          LlbcAst.TraitDeclId.Map.filter
+            (fun _ (d : LlbcAst.trait_decl) ->
+              let names_map = ExtractBuiltin.builtin_trait_decls_map () in
+              (not d.item_meta.is_local)
+              && not (matches_name m d.item_meta.name names_map))
+            trait_decls
+        in
+        let trait_impls =
+          List.filter_map
+            (fun (d : LlbcAst.trait_impl) ->
+              let names_map = ExtractBuiltin.builtin_trait_impls_map () in
+              match
+                LlbcAst.TraitDeclId.Map.find_opt d.impl_trait.trait_decl_id
+                  m.trait_decls
+              with
+              | None -> None (* Just ignore it *)
+              | Some trait_decl ->
+                  if
+                    (not d.item_meta.is_local)
+                    && not
+                         (matches_name_with_generics m trait_decl.item_meta.name
+                            d.impl_trait.decl_generics names_map)
+                  then Some (d, trait_decl)
+                  else None)
+            (LlbcAst.TraitImplId.Map.values trait_impls)
+        in
+        (* Print *)
+        let fmt_env = Print.Crate.crate_to_fmt_env m in
+        let type_decls =
+          List.map
+            (fun (d : Types.type_decl) ->
+              let pattern =
+                TranslateCore.name_with_crate_to_pattern_string m
+                  d.item_meta.name
+              in
+              "Type decl (pattern: [" ^ pattern ^ "]]):\n"
+              ^ Print.type_decl_to_string fmt_env d)
+            (Types.TypeDeclId.Map.values type_decls)
+        in
+        let fun_decls =
+          List.map
+            (fun (d : LlbcAst.fun_decl) ->
+              let pattern =
+                TranslateCore.name_with_crate_to_pattern_string m
+                  d.item_meta.name
+              in
+              let d =
+                (* FIXME: there is a bug in the formatter when splitting the predicates
+                   and trait clauses between the inherited ones and the others (the
+                   index is sometimes out of bounds).
+                   See: https://github.com/AeneasVerif/charon/issues/482
+                *)
+                try Print.Ast.fun_decl_to_string fmt_env "" "  " d
+                with _ -> "UNKNOWN"
+              in
+              "Fun decl (pattern: [" ^ pattern ^ "]]):\n" ^ d)
+            (LlbcAst.FunDeclId.Map.values fun_decls)
+        in
+        let global_decls =
+          List.map
+            (fun (d : LlbcAst.global_decl) ->
+              let pattern =
+                TranslateCore.name_with_crate_to_pattern_string m
+                  d.item_meta.name
+              in
+              "Global decl (pattern: [" ^ pattern ^ "]]):\n"
+              ^ Print.Ast.global_decl_to_string fmt_env "" "  " d)
+            (LlbcAst.GlobalDeclId.Map.values global_decls)
+        in
+        let trait_decls =
+          List.map
+            (fun (d : LlbcAst.trait_decl) ->
+              let pattern =
+                TranslateCore.name_with_crate_to_pattern_string m
+                  d.item_meta.name
+              in
+              "Trait decl (pattern: [" ^ pattern ^ "]]):\n"
+              ^ Print.Ast.trait_decl_to_string fmt_env "" "  " d)
+            (LlbcAst.TraitDeclId.Map.values trait_decls)
+        in
+        let trait_impls =
+          List.map
+            (fun ((d, trait_decl) : LlbcAst.trait_impl * LlbcAst.trait_decl) ->
+              let pattern =
+                TranslateCore.name_with_generics_crate_to_pattern_string m
+                  trait_decl.item_meta.name trait_decl.generics
+                  d.impl_trait.decl_generics
+              in
+              "Trait impl (pattern: [" ^ pattern ^ "]]):\n"
+              ^ Print.Ast.trait_impl_to_string fmt_env "" "  " d)
+            trait_impls
+        in
+
+        log#linfo
+          (lazy
+            (String.concat "\n\n"
+               (type_decls @ fun_decls @ global_decls @ trait_decls
+              @ trait_impls)));
+        ());
+
       (* There may be exceptions to catch *)
       (try
          (* Apply the pre-passes *)

src/TranslateCore.ml

@@ -76,6 +76,43 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx)
   in
   name_with_generics_to_simple_name mctx ~prefix n p g
 
+let name_with_crate_to_pattern_string (ctx : LlbcAst.crate) (n : Types.name) :
+    string =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_decls;
+      global_decls = ctx.global_decls;
+      fun_decls = ctx.fun_decls;
+      trait_decls = ctx.trait_decls;
+      trait_impls = ctx.trait_impls;
+    }
+  in
+  let c : Charon.NameMatcher.to_pat_config =
+    { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let pat = Charon.NameMatcher.name_to_pattern mctx c n in
+  Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat
+
+let name_with_generics_crate_to_pattern_string (ctx : LlbcAst.crate)
+    (n : Types.name) (params : Types.generic_params) (args : Types.generic_args)
+    : string =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_decls;
+      global_decls = ctx.global_decls;
+      fun_decls = ctx.fun_decls;
+      trait_decls = ctx.trait_decls;
+      trait_impls = ctx.trait_impls;
+    }
+  in
+  let c : Charon.NameMatcher.to_pat_config =
+    { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let pat =
+    Charon.NameMatcher.name_with_generics_to_pattern mctx c params n args
+  in
+  Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat
+
 let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string =
   let mctx : Charon.NameMatcher.ctx =
     {

src/extract/ExtractBase.ml

@@ -1680,10 +1680,13 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx)
     let clause_trait = clause.trait.binder_value in
     (* *)
     let trait_id = clause_trait.trait_decl_id in
-    let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
-    let args = clause_trait.decl_generics in
-    trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
-      impl_trait_decl.item_meta.name params args
+    (* The declaration may be missing because of an error *)
+    match TraitDeclId.Map.find_opt trait_id ctx.crate.trait_decls with
+    | None -> [ "clause" ]
+    | Some impl_trait_decl ->
+        let args = clause_trait.decl_generics in
+        trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
+          impl_trait_decl.item_meta.name params args
   in
   String.concat "" clause