From 367b7a966e4dfc4bc233b96f9f1bdc4973232a42 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Thu, 28 Nov 2024 16:36:37 +0000
Subject: [PATCH 01/11] Generate better error messages to report mixed mut rec
 groups

---
 src/interp/Interpreter.ml | 82 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 80 insertions(+), 2 deletions(-)

diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml
index 6fc0d3a1..a926ac14 100644
--- a/src/interp/Interpreter.ml
+++ b/src/interp/Interpreter.ml
@@ -11,6 +11,7 @@ open LlbcAst
 open Contexts
 open SynthesizeSymbolic
 open Errors
+open Meta
 module SA = SymbolicAst
 
 (** The local logger *)
@@ -23,8 +24,85 @@ let compute_contexts (m : crate) : decls_ctx =
   let global_decls = m.global_decls in
   let trait_decls = m.trait_decls in
   let trait_impls = m.trait_impls in
-  let type_decls_groups, _, _, _, _ =
-    split_declarations_to_group_maps m.declarations
+  let fmt_env : Print.fmt_env =
+    {
+      type_decls;
+      fun_decls;
+      global_decls;
+      trait_decls;
+      trait_impls;
+      regions = [];
+      generics = empty_generic_params;
+      locals = [];
+    }
+  in
+  let type_decls_groups =
+    match split_declarations_to_group_maps m.declarations with
+    | Ok (type_decls_groups, _, _, _, _) -> type_decls_groups
+    | Error mixed_groups ->
+        let any_decl_id_to_string (id : any_decl_id) : string =
+          let get_meta :
+                'a. ('a -> item_meta) -> 'a option -> (span * name) option =
+           fun get x ->
+            match x with
+            | None -> None
+            | Some d ->
+                let meta = get d in
+                Some (meta.span, meta.name)
+          in
+          let kind, info =
+            match id with
+            | IdType id ->
+                ( "type decl",
+                  get_meta
+                    (fun (d : type_decl) -> d.item_meta)
+                    (TypeDeclId.Map.find_opt id type_decls) )
+            | IdFun id ->
+                ( "fun decl",
+                  get_meta
+                    (fun (d : fun_decl) -> d.item_meta)
+                    (FunDeclId.Map.find_opt id fun_decls) )
+            | IdGlobal id ->
+                ( "global decl",
+                  get_meta
+                    (fun (d : global_decl) -> d.item_meta)
+                    (GlobalDeclId.Map.find_opt id global_decls) )
+            | IdTraitDecl id ->
+                ( "trait decl",
+                  get_meta
+                    (fun (d : trait_decl) -> d.item_meta)
+                    (TraitDeclId.Map.find_opt id trait_decls) )
+            | IdTraitImpl id ->
+                ( "trait impl",
+                  get_meta
+                    (fun (d : trait_impl) -> d.item_meta)
+                    (TraitImplId.Map.find_opt id trait_impls) )
+          in
+          let s =
+            match info with
+            | None -> show_any_decl_id id
+            | Some (span, name) ->
+                kind ^ "(" ^ span_to_string span ^ "): "
+                ^ Print.name_to_string fmt_env name
+          in
+          "- " ^ s
+        in
+        let msgs =
+          List.map
+            (fun (g : mixed_declaration_group) ->
+              let decls =
+                List.map any_decl_id_to_string (g_declaration_group_to_list g)
+              in
+              String.concat "\n" decls)
+            mixed_groups
+        in
+        let msgs =
+          String.concat "\n\n" (List.map (fun s -> "Group:\n" ^ s) msgs)
+        in
+        craise_opt_span __FILE__ __LINE__ None
+          ("Detected groups of mixed mutually recursive definitions (such as a \
+            type mutually recursive with a function, or a function mutually \
+            recursive with a trait implementation):\n\n" ^ msgs)
   in
   let type_infos =
     TypesAnalysis.analyze_type_declarations type_decls type_decls_list

From 86987dafa17b7e45175de2b744c6049fe9699ffe Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 00:26:11 +0000
Subject: [PATCH 02/11] Improve further the errors for mixed declaration groups

---
 src/interp/Interpreter.ml          |  71 ++++---------
 src/interp/InterpreterExpansion.ml |   2 +-
 src/interp/InterpreterLoopsCore.ml |   3 -
 src/llbc/LlbcAstUtils.ml           | 154 +++++++++++++++++++++++++++++
 src/llbc/TypesAnalysis.ml          |   2 +-
 src/pure/PureMicroPasses.ml        |   2 +-
 src/symbolic/SymbolicToPure.ml     |   2 +-
 src/utils/Utils.ml                 |   3 +
 8 files changed, 182 insertions(+), 57 deletions(-)

diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml
index a926ac14..69a45da9 100644
--- a/src/interp/Interpreter.ml
+++ b/src/interp/Interpreter.ml
@@ -11,7 +11,6 @@ open LlbcAst
 open Contexts
 open SynthesizeSymbolic
 open Errors
-open Meta
 module SA = SymbolicAst
 
 (** The local logger *)
@@ -36,66 +35,38 @@ let compute_contexts (m : crate) : decls_ctx =
       locals = [];
     }
   in
+  (* Split the declaration groups between the declaration kinds (types, functions, etc.) *)
   let type_decls_groups =
     match split_declarations_to_group_maps m.declarations with
     | Ok (type_decls_groups, _, _, _, _) -> type_decls_groups
     | Error mixed_groups ->
+        (* We detected mixed groups: print a nice error message *)
         let any_decl_id_to_string (id : any_decl_id) : string =
-          let get_meta :
-                'a. ('a -> item_meta) -> 'a option -> (span * name) option =
-           fun get x ->
-            match x with
-            | None -> None
-            | Some d ->
-                let meta = get d in
-                Some (meta.span, meta.name)
-          in
-          let kind, info =
-            match id with
-            | IdType id ->
-                ( "type decl",
-                  get_meta
-                    (fun (d : type_decl) -> d.item_meta)
-                    (TypeDeclId.Map.find_opt id type_decls) )
-            | IdFun id ->
-                ( "fun decl",
-                  get_meta
-                    (fun (d : fun_decl) -> d.item_meta)
-                    (FunDeclId.Map.find_opt id fun_decls) )
-            | IdGlobal id ->
-                ( "global decl",
-                  get_meta
-                    (fun (d : global_decl) -> d.item_meta)
-                    (GlobalDeclId.Map.find_opt id global_decls) )
-            | IdTraitDecl id ->
-                ( "trait decl",
-                  get_meta
-                    (fun (d : trait_decl) -> d.item_meta)
-                    (TraitDeclId.Map.find_opt id trait_decls) )
-            | IdTraitImpl id ->
-                ( "trait impl",
-                  get_meta
-                    (fun (d : trait_impl) -> d.item_meta)
-                    (TraitImplId.Map.find_opt id trait_impls) )
-          in
+          let kind = any_decl_id_to_kind_name id in
+          let meta = LlbcAstUtils.crate_get_item_meta m id in
           let s =
-            match info with
+            match meta with
             | None -> show_any_decl_id id
-            | Some (span, name) ->
-                kind ^ "(" ^ span_to_string span ^ "): "
-                ^ Print.name_to_string fmt_env name
+            | Some meta ->
+                kind ^ "(" ^ span_to_string meta.span ^ "): "
+                ^ Print.name_to_string fmt_env meta.name
           in
           "- " ^ s
         in
-        let msgs =
-          List.map
-            (fun (g : mixed_declaration_group) ->
-              let decls =
-                List.map any_decl_id_to_string (g_declaration_group_to_list g)
-              in
-              String.concat "\n" decls)
-            mixed_groups
+        let group_to_msg (g : mixed_declaration_group) : string =
+          let ids = g_declaration_group_to_list g in
+          let decls = List.map any_decl_id_to_string ids in
+          let local_requires =
+            LlbcAstUtils.find_local_transitive_dep m (AnyDeclIdSet.of_list ids)
+          in
+          let local_requires = List.map span_to_string local_requires in
+          "# Group:\n" ^ String.concat "\n" decls
+          ^ "\n\n\
+             The declarations in this group are (transitively) used at the \
+             following location(s):\n"
+          ^ String.concat "\n" local_requires
         in
+        let msgs = List.map group_to_msg mixed_groups in
         let msgs =
           String.concat "\n\n" (List.map (fun s -> "Group:\n" ^ s) msgs)
         in
diff --git a/src/interp/InterpreterExpansion.ml b/src/interp/InterpreterExpansion.ml
index 3758d342..9c6355ef 100644
--- a/src/interp/InterpreterExpansion.ml
+++ b/src/interp/InterpreterExpansion.ml
@@ -649,7 +649,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
                       > 1 variants (option \
                       [greedy_expand_symbolics_with_borrows] of [config]): "
                     ^ name_to_string ctx def.item_meta.name)
-              | Alias _ | Opaque | Error _ ->
+              | Alias _ | Opaque | TError _ ->
                   craise __FILE__ __LINE__ span
                     "Attempted to greedily expand an alias or opaque type"
               | Union _ ->
diff --git a/src/interp/InterpreterLoopsCore.ml b/src/interp/InterpreterLoopsCore.ml
index a71cab4f..e1c9b46e 100644
--- a/src/interp/InterpreterLoopsCore.ml
+++ b/src/interp/InterpreterLoopsCore.ml
@@ -23,9 +23,6 @@ exception Distinct of string
 
 type ctx_or_update = (eval_ctx, updt_env_kind) result
 
-(** Union Find *)
-module UF = UnionFind.Make (UnionFind.StoreMap)
-
 (** A small utility.
 
     Remark: we use projection markers, meaning we compute maps from/to
diff --git a/src/llbc/LlbcAstUtils.ml b/src/llbc/LlbcAstUtils.ml
index a407a323..c962fe40 100644
--- a/src/llbc/LlbcAstUtils.ml
+++ b/src/llbc/LlbcAstUtils.ml
@@ -2,6 +2,8 @@ open Types
 open LlbcAst
 include Charon.LlbcAstUtils
 open Collections
+open Utils
+open Meta
 
 module FunIdOrderedType : OrderedType with type t = fun_id = struct
   type t = fun_id
@@ -66,3 +68,155 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_builtin : bool) :
 let crate_has_opaque_non_builtin_decls (k : crate) (filter_builtin : bool) :
     bool =
   crate_get_opaque_non_builtin_decls k filter_builtin <> ([], [])
+
+(** For error reporting: compute which local definitions (transitively) depend
+    on a set of external definitions. This allows us to pinpoint to the user
+    which parts of the code are responsible for an error stemming from a
+    dependency. *)
+let find_local_transitive_dep (m : crate) (marked_externals : AnyDeclIdSet.t) :
+    span list =
+  (* Compute the edges from: (decl_id, span) to (decl_id) *)
+  let edges = ref [] in
+  let visitor =
+    object
+      inherit [_] iter_statement as super
+
+      method! visit_statement decl_span_info st =
+        let decl_span_info =
+          Option.map (fun (decl_id, _) -> (decl_id, st.span)) decl_span_info
+        in
+        super#visit_statement decl_span_info st
+
+      method! visit_type_decl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdType id) :: !edges)
+          decl_span_info
+
+      method! visit_fun_decl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdFun id) :: !edges)
+          decl_span_info
+
+      method! visit_global_decl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdGlobal id) :: !edges)
+          decl_span_info
+
+      method! visit_trait_decl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdTraitDecl id) :: !edges)
+          decl_span_info
+
+      method! visit_trait_impl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdTraitImpl id) :: !edges)
+          decl_span_info
+    end
+  in
+  (* Visit each kind of definition *)
+  TypeDeclId.Map.iter
+    (fun _ (d : type_decl) ->
+      let decl_span_info = Some (IdType d.def_id, d.item_meta.span) in
+      visitor#visit_type_decl decl_span_info d)
+    m.type_decls;
+  FunDeclId.Map.iter
+    (fun _ (d : fun_decl) ->
+      let decl_span_info = Some (IdFun d.def_id, d.item_meta.span) in
+      visitor#visit_fun_sig decl_span_info d.signature;
+      Option.iter
+        (fun (body : expr_body) ->
+          visitor#visit_statement decl_span_info body.body)
+        d.body)
+    m.fun_decls;
+  (* We don't need to visit the globals (it is redundant with visiting the functions) *)
+  TraitDeclId.Map.iter
+    (fun _ (d : trait_decl) ->
+      let decl_span_info = Some (IdTraitDecl d.def_id, d.item_meta.span) in
+      visitor#visit_trait_decl decl_span_info d)
+    m.trait_decls;
+  TraitImplId.Map.iter
+    (fun _ (d : trait_impl) ->
+      let decl_span_info = Some (IdTraitImpl d.def_id, d.item_meta.span) in
+      visitor#visit_trait_impl decl_span_info d)
+    m.trait_impls;
+  (* We're using a union-find data-structure.
+
+     All external dependencies which are in the set [external] or which
+     transitively depend on declarations in this set are put in the same
+     equivalence class.
+  *)
+  let ids =
+    List.map (fun id -> IdType id) (TypeDeclId.Map.keys m.type_decls)
+    @ List.map (fun id -> IdFun id) (FunDeclId.Map.keys m.fun_decls)
+    @ List.map (fun id -> IdGlobal id) (GlobalDeclId.Map.keys m.global_decls)
+    @ List.map (fun id -> IdTraitDecl id) (TraitDeclId.Map.keys m.trait_decls)
+    @ List.map (fun id -> IdTraitImpl id) (TraitImplId.Map.keys m.trait_impls)
+  in
+  let uf_store = UF.new_store () in
+  let external_ids =
+    AnyDeclIdMap.of_list
+      (List.filter_map
+         (fun id ->
+           let meta = crate_get_item_meta m id in
+           match meta with
+           | None -> None
+           | Some meta ->
+               if meta.is_local then None else Some (id, UF.make uf_store id))
+         ids)
+  in
+  (* Merge the classes of the marked externals *)
+  let marked_class =
+    match AnyDeclIdSet.elements marked_externals with
+    | id0 :: ids ->
+        let c0 = AnyDeclIdMap.find id0 external_ids in
+        List.iter
+          (fun id ->
+            let c = AnyDeclIdMap.find id external_ids in
+            let _ = UF.union uf_store c0 c in
+            ())
+          ids;
+        c0
+    | _ -> raise (Failure "Unreachable")
+  in
+  (* Merge the classes by using the edges *)
+  List.iter
+    (fun ((id0, _), id1) ->
+      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
+      | Some meta0, Some meta1 ->
+          if (not meta0.is_local) && not meta1.is_local then
+            let c0 = AnyDeclIdMap.find id0 external_ids in
+            let c1 = AnyDeclIdMap.find id1 external_ids in
+            let _ = UF.union uf_store c0 c1 in
+            ()
+          else ()
+      | _ -> ())
+    !edges;
+  (* We now compute a map from external id in the set to set of local
+     declarations (and spans) which depend on this external id *)
+  List.iter
+    (fun ((id0, _), id1) ->
+      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
+      | Some meta0, Some meta1 ->
+          if (not meta0.is_local) && not meta1.is_local then
+            let c0 = AnyDeclIdMap.find id0 external_ids in
+            let c1 = AnyDeclIdMap.find id1 external_ids in
+            let _ = UF.union uf_store c0 c1 in
+            ()
+          else ()
+      | _ -> ())
+    !edges;
+  (* The spans at which we transitively refer to a marked external definition *)
+  let spans = ref Charon.MetaUtils.SpanSet.empty in
+  List.iter
+    (fun ((id0, span), id1) ->
+      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
+      | Some meta0, Some meta1 ->
+          if meta0.is_local && not meta1.is_local then
+            let c1 = AnyDeclIdMap.find id1 external_ids in
+            if UF.eq uf_store marked_class c1 then
+              spans := Charon.MetaUtils.SpanSet.add span !spans
+            else ()
+      | _ -> ())
+    !edges;
+  (* Return the spans *)
+  Charon.MetaUtils.SpanSet.elements !spans
diff --git a/src/llbc/TypesAnalysis.ml b/src/llbc/TypesAnalysis.ml
index 5e317418..effadd42 100644
--- a/src/llbc/TypesAnalysis.ml
+++ b/src/llbc/TypesAnalysis.ml
@@ -385,7 +385,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
             "type aliases should have been removed earlier"
       | Union _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unions are not supported"
-      | Opaque | Error _ ->
+      | Opaque | TError _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unreachable"
     in
     (* Substitute the regions in the fields *)
diff --git a/src/pure/PureMicroPasses.ml b/src/pure/PureMicroPasses.ml
index 49157705..25ce368d 100644
--- a/src/pure/PureMicroPasses.ml
+++ b/src/pure/PureMicroPasses.ml
@@ -1385,7 +1385,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 in
                 let fields =
                   match adt_decl.kind with
-                  | Enum _ | Alias _ | Opaque | Error _ ->
+                  | Enum _ | Alias _ | Opaque | TError _ ->
                       craise __FILE__ __LINE__ def.item_meta.span "Unreachable"
                   | Union _ ->
                       craise __FILE__ __LINE__ def.item_meta.span
diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml
index 81bac9aa..01172a1c 100644
--- a/src/symbolic/SymbolicToPure.ml
+++ b/src/symbolic/SymbolicToPure.ml
@@ -595,7 +595,7 @@ let translate_type_decl_kind (span : Meta.span) (kind : T.type_decl_kind) :
   | Alias _ ->
       craise __FILE__ __LINE__ span
         "type aliases should have been removed earlier"
-  | T.Union _ | T.Opaque | T.Error _ -> Opaque
+  | T.Union _ | T.Opaque | T.TError _ -> Opaque
 
 (** Compute which input parameters should be implicit or explicit.
 
diff --git a/src/utils/Utils.ml b/src/utils/Utils.ml
index 987ac317..4389d512 100644
--- a/src/utils/Utils.ml
+++ b/src/utils/Utils.ml
@@ -1 +1,4 @@
 include Charon.Utils
+
+(** Union Find *)
+module UF = UnionFind.Make (UnionFind.StoreMap)

From 0dccfdb780a95bc9426191914ac356e56b402e34 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 00:28:51 +0000
Subject: [PATCH 03/11] Improve the messages further

---
 src/interp/Interpreter.ml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml
index 69a45da9..e3fd2a9b 100644
--- a/src/interp/Interpreter.ml
+++ b/src/interp/Interpreter.ml
@@ -60,11 +60,15 @@ let compute_contexts (m : crate) : decls_ctx =
             LlbcAstUtils.find_local_transitive_dep m (AnyDeclIdSet.of_list ids)
           in
           let local_requires = List.map span_to_string local_requires in
-          "# Group:\n" ^ String.concat "\n" decls
-          ^ "\n\n\
-             The declarations in this group are (transitively) used at the \
-             following location(s):\n"
-          ^ String.concat "\n" local_requires
+          let local_requires =
+            if local_requires <> [] then
+              "\n\n\
+               The declarations in this group are (transitively) used at the \
+               following location(s):\n"
+              ^ String.concat "\n" local_requires
+            else ""
+          in
+          "# Group:\n" ^ String.concat "\n" decls ^ local_requires
         in
         let msgs = List.map group_to_msg mixed_groups in
         let msgs =

From ac72c0cdbec91067295691f264a870b0cc078de2 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 00:29:21 +0000
Subject: [PATCH 04/11] Update the Charon pin

---
 charon-pin |  2 +-
 flake.lock | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/charon-pin b/charon-pin
index 261dfbd6..014d9cb2 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-04d97dd849d7a69239e28aa64859d3a4f86b4162
+3cc56758495403a4b767aa0839ba0bd225c214dc
diff --git a/flake.lock b/flake.lock
index 425abdcc..88d2ef02 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1732711803,
-        "narHash": "sha256-wG+PavPKAM4w4E5Wvwu2EeTZb06Z/17u16b26Atz9js=",
+        "lastModified": 1732839662,
+        "narHash": "sha256-1BKExMo7n30CuHo6rEmgp24q/j3lF+dJPN9J4TUKeSs=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "04d97dd849d7a69239e28aa64859d3a4f86b4162",
+        "rev": "3cc56758495403a4b767aa0839ba0bd225c214dc",
         "type": "github"
       },
       "original": {
@@ -285,11 +285,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1732674798,
-        "narHash": "sha256-oM1gjCv9R4zxDFO3as9wqQ4FI3+pDA9MKZ72L7tTIII=",
+        "lastModified": 1732802692,
+        "narHash": "sha256-kFrxb45qj52TT/OFUFyTdmvXkn/KXDUL0/DOtjHEQvs=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "1d569430326b0a7807ccffdb2a188b814091976c",
+        "rev": "34971069ec33755b2adf2481851f66d8ec9a6bfa",
         "type": "github"
       },
       "original": {

From f5729988e8ee596f8249c6dd9d63f376ba291132 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 00:41:33 +0000
Subject: [PATCH 05/11] Update the Charon pin

---
 charon-pin | 2 +-
 flake.lock | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/charon-pin b/charon-pin
index 014d9cb2..af46f201 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-3cc56758495403a4b767aa0839ba0bd225c214dc
+d2ec320a28a6c570f1c9669f00a773c3365c22d0
diff --git a/flake.lock b/flake.lock
index 88d2ef02..5d5cbfd1 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1732839662,
-        "narHash": "sha256-1BKExMo7n30CuHo6rEmgp24q/j3lF+dJPN9J4TUKeSs=",
+        "lastModified": 1732840875,
+        "narHash": "sha256-xl6Ym8Sx4HLsFdaqkdPynAa7kQyhEcEf1K3p5uvocsA=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "3cc56758495403a4b767aa0839ba0bd225c214dc",
+        "rev": "d2ec320a28a6c570f1c9669f00a773c3365c22d0",
         "type": "github"
       },
       "original": {

From 13c6928f8aee5d653892b1024c218c26b6833ead Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 11:06:41 +0000
Subject: [PATCH 06/11] Update find_local_transitive_dep to properly update
 spans

---
 src/llbc/LlbcAstUtils.ml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/llbc/LlbcAstUtils.ml b/src/llbc/LlbcAstUtils.ml
index c962fe40..9fcb6e71 100644
--- a/src/llbc/LlbcAstUtils.ml
+++ b/src/llbc/LlbcAstUtils.ml
@@ -87,6 +87,28 @@ let find_local_transitive_dep (m : crate) (marked_externals : AnyDeclIdSet.t) :
         in
         super#visit_statement decl_span_info st
 
+      method! visit_variant decl_span_info (variant : variant) =
+        let decl_span_info =
+          Option.map
+            (fun (decl_id, _) -> (decl_id, variant.span))
+            decl_span_info
+        in
+        super#visit_variant decl_span_info variant
+
+      method! visit_trait_clause decl_span_info (clause : trait_clause) =
+        let decl_span_info =
+          match (decl_span_info, clause.span) with
+          | Some (decl_id, _), Some span -> Some (decl_id, span)
+          | _ -> decl_span_info
+        in
+        super#visit_trait_clause decl_span_info clause
+
+      method! visit_field decl_span_info (field : field) =
+        let decl_span_info =
+          Option.map (fun (decl_id, _) -> (decl_id, field.span)) decl_span_info
+        in
+        super#visit_field decl_span_info field
+
       method! visit_type_decl_id decl_span_info id =
         Option.iter
           (fun info -> edges := (info, IdType id) :: !edges)

From 983a24c05b1b5d486d4cfdd04782be66186e3e94 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 11:42:50 +0000
Subject: [PATCH 07/11] Move some definitions and helpers to Charon-ML

---
 README.md                 |   2 +-
 src/dune                  |   2 +-
 src/interp/Interpreter.ml |  12 +--
 src/llbc/LlbcAstUtils.ml  | 176 --------------------------------------
 src/utils/Utils.ml        |   3 -
 5 files changed, 8 insertions(+), 187 deletions(-)

diff --git a/README.md b/README.md
index 08bb3686..cf17368c 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,7 @@ You can then install the dependencies with the following command:
 
 ```
 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \
-  unionFind ocamlgraph menhir ocamlformat
+  ocamlgraph menhir ocamlformat
 ```
 
 Moreover, Aeneas uses the [Charon](https://github.com/AeneasVerif/charon) project and library.
diff --git a/src/dune b/src/dune
index cfb0ff59..a66dec34 100644
--- a/src/dune
+++ b/src/dune
@@ -14,7 +14,7 @@
  (public_name aeneas) ;; The name as revealed to the projects importing this library
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries charon core_unix unionFind ocamlgraph str)
+ (libraries charon core_unix ocamlgraph str)
  (modules
   AssociatedTypes
   BorrowCheck
diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml
index e3fd2a9b..d3107073 100644
--- a/src/interp/Interpreter.ml
+++ b/src/interp/Interpreter.ml
@@ -53,7 +53,7 @@ let compute_contexts (m : crate) : decls_ctx =
           in
           "- " ^ s
         in
-        let group_to_msg (g : mixed_declaration_group) : string =
+        let group_to_msg (i : int) (g : mixed_declaration_group) : string =
           let ids = g_declaration_group_to_list g in
           let decls = List.map any_decl_id_to_string ids in
           let local_requires =
@@ -68,12 +68,12 @@ let compute_contexts (m : crate) : decls_ctx =
               ^ String.concat "\n" local_requires
             else ""
           in
-          "# Group:\n" ^ String.concat "\n" decls ^ local_requires
-        in
-        let msgs = List.map group_to_msg mixed_groups in
-        let msgs =
-          String.concat "\n\n" (List.map (fun s -> "Group:\n" ^ s) msgs)
+          "# Group "
+          ^ string_of_int (i + 1)
+          ^ ":\n" ^ String.concat "\n" decls ^ local_requires
         in
+        let msgs = List.mapi group_to_msg mixed_groups in
+        let msgs = String.concat "\n\n" msgs in
         craise_opt_span __FILE__ __LINE__ None
           ("Detected groups of mixed mutually recursive definitions (such as a \
             type mutually recursive with a function, or a function mutually \
diff --git a/src/llbc/LlbcAstUtils.ml b/src/llbc/LlbcAstUtils.ml
index 9fcb6e71..a407a323 100644
--- a/src/llbc/LlbcAstUtils.ml
+++ b/src/llbc/LlbcAstUtils.ml
@@ -2,8 +2,6 @@ open Types
 open LlbcAst
 include Charon.LlbcAstUtils
 open Collections
-open Utils
-open Meta
 
 module FunIdOrderedType : OrderedType with type t = fun_id = struct
   type t = fun_id
@@ -68,177 +66,3 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_builtin : bool) :
 let crate_has_opaque_non_builtin_decls (k : crate) (filter_builtin : bool) :
     bool =
   crate_get_opaque_non_builtin_decls k filter_builtin <> ([], [])
-
-(** For error reporting: compute which local definitions (transitively) depend
-    on a set of external definitions. This allows us to pinpoint to the user
-    which parts of the code are responsible for an error stemming from a
-    dependency. *)
-let find_local_transitive_dep (m : crate) (marked_externals : AnyDeclIdSet.t) :
-    span list =
-  (* Compute the edges from: (decl_id, span) to (decl_id) *)
-  let edges = ref [] in
-  let visitor =
-    object
-      inherit [_] iter_statement as super
-
-      method! visit_statement decl_span_info st =
-        let decl_span_info =
-          Option.map (fun (decl_id, _) -> (decl_id, st.span)) decl_span_info
-        in
-        super#visit_statement decl_span_info st
-
-      method! visit_variant decl_span_info (variant : variant) =
-        let decl_span_info =
-          Option.map
-            (fun (decl_id, _) -> (decl_id, variant.span))
-            decl_span_info
-        in
-        super#visit_variant decl_span_info variant
-
-      method! visit_trait_clause decl_span_info (clause : trait_clause) =
-        let decl_span_info =
-          match (decl_span_info, clause.span) with
-          | Some (decl_id, _), Some span -> Some (decl_id, span)
-          | _ -> decl_span_info
-        in
-        super#visit_trait_clause decl_span_info clause
-
-      method! visit_field decl_span_info (field : field) =
-        let decl_span_info =
-          Option.map (fun (decl_id, _) -> (decl_id, field.span)) decl_span_info
-        in
-        super#visit_field decl_span_info field
-
-      method! visit_type_decl_id decl_span_info id =
-        Option.iter
-          (fun info -> edges := (info, IdType id) :: !edges)
-          decl_span_info
-
-      method! visit_fun_decl_id decl_span_info id =
-        Option.iter
-          (fun info -> edges := (info, IdFun id) :: !edges)
-          decl_span_info
-
-      method! visit_global_decl_id decl_span_info id =
-        Option.iter
-          (fun info -> edges := (info, IdGlobal id) :: !edges)
-          decl_span_info
-
-      method! visit_trait_decl_id decl_span_info id =
-        Option.iter
-          (fun info -> edges := (info, IdTraitDecl id) :: !edges)
-          decl_span_info
-
-      method! visit_trait_impl_id decl_span_info id =
-        Option.iter
-          (fun info -> edges := (info, IdTraitImpl id) :: !edges)
-          decl_span_info
-    end
-  in
-  (* Visit each kind of definition *)
-  TypeDeclId.Map.iter
-    (fun _ (d : type_decl) ->
-      let decl_span_info = Some (IdType d.def_id, d.item_meta.span) in
-      visitor#visit_type_decl decl_span_info d)
-    m.type_decls;
-  FunDeclId.Map.iter
-    (fun _ (d : fun_decl) ->
-      let decl_span_info = Some (IdFun d.def_id, d.item_meta.span) in
-      visitor#visit_fun_sig decl_span_info d.signature;
-      Option.iter
-        (fun (body : expr_body) ->
-          visitor#visit_statement decl_span_info body.body)
-        d.body)
-    m.fun_decls;
-  (* We don't need to visit the globals (it is redundant with visiting the functions) *)
-  TraitDeclId.Map.iter
-    (fun _ (d : trait_decl) ->
-      let decl_span_info = Some (IdTraitDecl d.def_id, d.item_meta.span) in
-      visitor#visit_trait_decl decl_span_info d)
-    m.trait_decls;
-  TraitImplId.Map.iter
-    (fun _ (d : trait_impl) ->
-      let decl_span_info = Some (IdTraitImpl d.def_id, d.item_meta.span) in
-      visitor#visit_trait_impl decl_span_info d)
-    m.trait_impls;
-  (* We're using a union-find data-structure.
-
-     All external dependencies which are in the set [external] or which
-     transitively depend on declarations in this set are put in the same
-     equivalence class.
-  *)
-  let ids =
-    List.map (fun id -> IdType id) (TypeDeclId.Map.keys m.type_decls)
-    @ List.map (fun id -> IdFun id) (FunDeclId.Map.keys m.fun_decls)
-    @ List.map (fun id -> IdGlobal id) (GlobalDeclId.Map.keys m.global_decls)
-    @ List.map (fun id -> IdTraitDecl id) (TraitDeclId.Map.keys m.trait_decls)
-    @ List.map (fun id -> IdTraitImpl id) (TraitImplId.Map.keys m.trait_impls)
-  in
-  let uf_store = UF.new_store () in
-  let external_ids =
-    AnyDeclIdMap.of_list
-      (List.filter_map
-         (fun id ->
-           let meta = crate_get_item_meta m id in
-           match meta with
-           | None -> None
-           | Some meta ->
-               if meta.is_local then None else Some (id, UF.make uf_store id))
-         ids)
-  in
-  (* Merge the classes of the marked externals *)
-  let marked_class =
-    match AnyDeclIdSet.elements marked_externals with
-    | id0 :: ids ->
-        let c0 = AnyDeclIdMap.find id0 external_ids in
-        List.iter
-          (fun id ->
-            let c = AnyDeclIdMap.find id external_ids in
-            let _ = UF.union uf_store c0 c in
-            ())
-          ids;
-        c0
-    | _ -> raise (Failure "Unreachable")
-  in
-  (* Merge the classes by using the edges *)
-  List.iter
-    (fun ((id0, _), id1) ->
-      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
-      | Some meta0, Some meta1 ->
-          if (not meta0.is_local) && not meta1.is_local then
-            let c0 = AnyDeclIdMap.find id0 external_ids in
-            let c1 = AnyDeclIdMap.find id1 external_ids in
-            let _ = UF.union uf_store c0 c1 in
-            ()
-          else ()
-      | _ -> ())
-    !edges;
-  (* We now compute a map from external id in the set to set of local
-     declarations (and spans) which depend on this external id *)
-  List.iter
-    (fun ((id0, _), id1) ->
-      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
-      | Some meta0, Some meta1 ->
-          if (not meta0.is_local) && not meta1.is_local then
-            let c0 = AnyDeclIdMap.find id0 external_ids in
-            let c1 = AnyDeclIdMap.find id1 external_ids in
-            let _ = UF.union uf_store c0 c1 in
-            ()
-          else ()
-      | _ -> ())
-    !edges;
-  (* The spans at which we transitively refer to a marked external definition *)
-  let spans = ref Charon.MetaUtils.SpanSet.empty in
-  List.iter
-    (fun ((id0, span), id1) ->
-      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
-      | Some meta0, Some meta1 ->
-          if meta0.is_local && not meta1.is_local then
-            let c1 = AnyDeclIdMap.find id1 external_ids in
-            if UF.eq uf_store marked_class c1 then
-              spans := Charon.MetaUtils.SpanSet.add span !spans
-            else ()
-      | _ -> ())
-    !edges;
-  (* Return the spans *)
-  Charon.MetaUtils.SpanSet.elements !spans
diff --git a/src/utils/Utils.ml b/src/utils/Utils.ml
index 4389d512..987ac317 100644
--- a/src/utils/Utils.ml
+++ b/src/utils/Utils.ml
@@ -1,4 +1 @@
 include Charon.Utils
-
-(** Union Find *)
-module UF = UnionFind.Make (UnionFind.StoreMap)

From 5753a1c39720fd4aee6943c50f20f17164c525d4 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 11:44:23 +0000
Subject: [PATCH 08/11] Update the Charon pin

---
 charon-pin |  2 +-
 flake.lock | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/charon-pin b/charon-pin
index af46f201..b36be8ad 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-d2ec320a28a6c570f1c9669f00a773c3365c22d0
+93727aba2ea5b2e45b4d4cf3239a7f57b7bae5e4
diff --git a/flake.lock b/flake.lock
index 5d5cbfd1..1910fdd0 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1732840875,
-        "narHash": "sha256-xl6Ym8Sx4HLsFdaqkdPynAa7kQyhEcEf1K3p5uvocsA=",
+        "lastModified": 1732880518,
+        "narHash": "sha256-KhhIrCtZbgT9yGwGuAQd2yMnBvc8u3bHE2HiuT0nMF0=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "d2ec320a28a6c570f1c9669f00a773c3365c22d0",
+        "rev": "93727aba2ea5b2e45b4d4cf3239a7f57b7bae5e4",
         "type": "github"
       },
       "original": {
@@ -285,11 +285,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1732802692,
-        "narHash": "sha256-kFrxb45qj52TT/OFUFyTdmvXkn/KXDUL0/DOtjHEQvs=",
+        "lastModified": 1732847586,
+        "narHash": "sha256-SnHHSBNZ+aj8mRzYxb6yXBl9ei3K3j5agC/D8Vjw/no=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "34971069ec33755b2adf2481851f66d8ec9a6bfa",
+        "rev": "97210ddff72fe139815f4c1ac5da74b5b0dde2d7",
         "type": "github"
       },
       "original": {

From ad919748172da8b053461f3db5c7d5af0ccf8175 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 11:51:25 +0000
Subject: [PATCH 09/11] Update the Charon pin

---
 charon-pin | 2 +-
 flake.lock | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/charon-pin b/charon-pin
index b36be8ad..4012c5f5 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-93727aba2ea5b2e45b4d4cf3239a7f57b7bae5e4
+d1c45e6f82963997ec45907f96497676e7d94caf
diff --git a/flake.lock b/flake.lock
index 1910fdd0..c7b3cbe8 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1732880518,
-        "narHash": "sha256-KhhIrCtZbgT9yGwGuAQd2yMnBvc8u3bHE2HiuT0nMF0=",
+        "lastModified": 1732881016,
+        "narHash": "sha256-O7GWCiwVb8xCxfLG/XF50XhqZ/txNbYhfRogjToVbdY=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "93727aba2ea5b2e45b4d4cf3239a7f57b7bae5e4",
+        "rev": "d1c45e6f82963997ec45907f96497676e7d94caf",
         "type": "github"
       },
       "original": {

From cc4a605445ece74f019eadbb02f2a887b0ce76e6 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 11:57:12 +0000
Subject: [PATCH 10/11] Update the nix file

---
 flake.nix | 1 -
 1 file changed, 1 deletion(-)

diff --git a/flake.nix b/flake.nix
index aa24a78e..fc2b2999 100644
--- a/flake.nix
+++ b/flake.nix
@@ -65,7 +65,6 @@
             yojson
             zarith
             ocamlgraph
-            unionFind
           ]);
           afterBuild = ''
             echo charon.packages.${system}.tests

From 7881c3c553d916e5b11a21da9b3ad4f3944eb95b Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 29 Nov 2024 11:57:43 +0000
Subject: [PATCH 11/11] Update the Charon pin

---
 charon-pin | 2 +-
 flake.lock | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/charon-pin b/charon-pin
index 4012c5f5..57f50f86 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-d1c45e6f82963997ec45907f96497676e7d94caf
+1172606b471b5d9913f95cfbf944d3b943736667
diff --git a/flake.lock b/flake.lock
index c7b3cbe8..ce28af39 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1732881016,
-        "narHash": "sha256-O7GWCiwVb8xCxfLG/XF50XhqZ/txNbYhfRogjToVbdY=",
+        "lastModified": 1732881390,
+        "narHash": "sha256-BHsHEnl6S5YXU1UMHR/wryH1CNvNaN/kxg43VwOsWFc=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "d1c45e6f82963997ec45907f96497676e7d94caf",
+        "rev": "1172606b471b5d9913f95cfbf944d3b943736667",
         "type": "github"
       },
       "original": {