Merge pull request #258 from Nadrieril/bump-charon

18 files changed, 113 insertions, 105 deletions

diff --git a/charon-pin b/charon-pin
index ad45dea7..2621304e 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.
-2e74074eaa0528f3203dc1c160ccdba0f44b563a
+5c2ae3744ce702d07920d0f536a272aadd396ed9
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 6c6b7f0e..1fbce7fd 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1258,7 +1258,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
-     if !extract_external_name_patterns && not def.is_local then
+     if !extract_external_name_patterns && not def.item_meta.is_local then
        Some def.llbc_name
      else None
    in
@@ -1433,7 +1433,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
     [ comment_pre ^ loop_comment ]
   in
   let name =
-    if !extract_external_name_patterns && not def.is_local then
+    if !extract_external_name_patterns && not def.item_meta.is_local then
       Some def.llbc_name
     else None
   in
@@ -1924,7 +1924,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
   let name =
-    if !extract_external_name_patterns && not global.is_local then
+    if !extract_external_name_patterns && not global.item_meta.is_local then
       Some global.llbc_name
     else None
   in
@@ -2389,7 +2389,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
-     if !extract_external_name_patterns && not decl.is_local then
+     if !extract_external_name_patterns && not decl.item_meta.is_local then
        Some decl.llbc_name
      else None
    in
@@ -2703,7 +2703,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name, generics =
-     if !extract_external_name_patterns && not impl.is_local then
+     if !extract_external_name_patterns && not impl.item_meta.is_local then
        let decl_id = impl.impl_trait.trait_decl_id in
        let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
        let decl_ref = impl.llbc_impl_trait in
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index fb65bd5e..57131dad 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -253,8 +253,9 @@ let empty_names_map : names_map =
   }
 
 (** Small helper to update an LLBC name if the rename attribute has been set *)
-let rename_llbc_name (item_meta : Meta.item_meta) (llbc_name : llbc_name) =
-  match item_meta.rename with
+let rename_llbc_name (attr_info : Meta.attr_info) (llbc_name : llbc_name) :
+    llbc_name =
+  match attr_info.rename with
   | Some rename ->
       let name_prefix = List.tl (List.rev llbc_name) in
       List.rev (T.PeIdent (rename, Disambiguator.zero) :: name_prefix)
@@ -1393,8 +1394,8 @@ let ctx_compute_simple_type_name = ctx_compute_simple_name
 
 (** Helper *)
 let ctx_compute_type_name_no_suffix (ctx : extraction_ctx)
-    (item_meta : Meta.item_meta) (name : llbc_name) : string =
-  let name = rename_llbc_name item_meta name in
+    (item_meta : Types.item_meta) (name : llbc_name) : string =
+  let name = rename_llbc_name item_meta.attr_info name in
   flatten_name (ctx_compute_simple_type_name item_meta.span ctx name)
 
 (** Provided a basename, compute a type name.
@@ -1403,7 +1404,7 @@ let ctx_compute_type_name_no_suffix (ctx : extraction_ctx)
     for instance field and variant names when we need to add the name of the type as a
     prefix.
  *)
-let ctx_compute_type_name (item_meta : Meta.item_meta) (ctx : extraction_ctx)
+let ctx_compute_type_name (item_meta : Types.item_meta) (ctx : extraction_ctx)
     (name : llbc_name) =
   let name = ctx_compute_type_name_no_suffix ctx item_meta name in
   match backend () with
@@ -1424,7 +1425,7 @@ let ctx_compute_type_name (item_meta : Meta.item_meta) (ctx : extraction_ctx)
     to tuples, meaning generating names by using indices shouldn't be too
     much of a problem.
  *)
-let ctx_compute_field_name (def : type_decl) (field_meta : Meta.item_meta)
+let ctx_compute_field_name (def : type_decl) (field_meta : Meta.attr_info)
     (ctx : extraction_ctx) (def_name : llbc_name) (field_id : FieldId.id)
     (field_name : string option) : string =
   (* If the user did not provide a name, use the field index. *)
@@ -1435,7 +1436,7 @@ let ctx_compute_field_name (def : type_decl) (field_meta : Meta.item_meta)
   let field_name_s = Option.value field_meta.rename ~default:field_name_s in
   (* Prefix the name with the name of the type, if necessary (some backends don't
      support field name collisions) *)
-  let def_name = rename_llbc_name def.item_meta def_name in
+  let def_name = rename_llbc_name def.item_meta.attr_info def_name in
   let name =
     if !Config.record_fields_short_names then
       if field_name = None then (* TODO: this is a bit ugly *)
@@ -1457,7 +1458,7 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl)
     (variant : variant) : string =
   (* Replace the name of the variant if the user annotated it with the [rename] attribute. *)
   let variant =
-    Option.value variant.item_meta.rename ~default:variant.variant_name
+    Option.value variant.attr_info.rename ~default:variant.variant_name
   in
   match backend () with
   | FStar | Coq | HOL4 ->
@@ -1547,7 +1548,9 @@ let ctx_compute_fun_name (span : Meta.span) (ctx : extraction_ctx)
 
 let ctx_compute_trait_decl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
     : string =
-  let llbc_name = rename_llbc_name trait_decl.item_meta trait_decl.llbc_name in
+  let llbc_name =
+    rename_llbc_name trait_decl.item_meta.attr_info trait_decl.llbc_name
+  in
   ctx_compute_type_name trait_decl.item_meta ctx llbc_name
 
 let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
@@ -1561,7 +1564,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
      Note that if the user provided a [rename] attribute, we simply use that.
   *)
   let name =
-    match trait_impl.item_meta.rename with
+    match trait_impl.item_meta.attr_info.rename with
     | None ->
         let name =
           let params = trait_impl.llbc_generics in
@@ -1569,7 +1572,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
           let name =
             ctx_prepare_name trait_impl.item_meta.span ctx trait_decl.llbc_name
           in
-          let name = rename_llbc_name trait_impl.item_meta name in
+          let name = rename_llbc_name trait_impl.item_meta.attr_info name in
           trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
         in
         flatten_name name
@@ -1631,7 +1634,7 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx)
     let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
     let args = clause.clause_generics in
     trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix
-      impl_trait_decl.name params args
+      impl_trait_decl.item_meta.name params args
   in
   String.concat "" clause
 
@@ -1814,7 +1817,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
               *)
               (* The name shouldn't be empty, and its last element should
                * be an ident *)
-              let cl = Collections.List.last def.name in
+              let cl = Collections.List.last def.item_meta.name in
               name_from_type_ident (TypesUtils.as_ident cl))
       | TVar _ -> (
           (* TODO: use "t" also for F* *)
@@ -2006,7 +2009,7 @@ let ctx_add_generic_params (span : Meta.span) (current_def_name : Types.name)
 
 let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
-  let name = rename_llbc_name def.item_meta def.llbc_name in
+  let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in
   let name =
     ctx_compute_decreases_proof_name def.item_meta.span ctx def.def_id name
       def.num_loops def.loop_id
@@ -2017,7 +2020,7 @@ let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
 
 let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
-  let name = rename_llbc_name def.item_meta def.llbc_name in
+  let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in
   let name =
     ctx_compute_termination_measure_name def.item_meta.span ctx def.def_id name
       def.num_loops def.loop_id
@@ -2034,13 +2037,15 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
   (* Check if the global corresponds to an assumed global that we should map
      to a custom definition in our standard library (for instance, happens
      with "core::num::usize::MAX") *)
-  match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with
+  match
+    match_name_find_opt ctx.trans_ctx def.item_meta.name builtin_globals_map
+  with
   | Some name ->
       (* Yes: register the custom binding *)
       ctx_add def.item_meta.span decl name ctx
   | None ->
       (* Not the case: "standard" registration *)
-      let name = rename_llbc_name def.item_meta def.name in
+      let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in
       let name = ctx_compute_global_name def.item_meta.span ctx name in
 
       let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
@@ -2068,7 +2073,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
   let item_meta =
     match def.kind with
     | TraitItemImpl (_, trait_decl_id, item_name, _) -> (
-        if Option.is_some def.item_meta.rename then def.item_meta
+        if Option.is_some def.item_meta.attr_info.rename then def.item_meta
         else
           (* Lookup the declaration. TODO: the trait item impl info
              should directly give us the id of the method declaration. *)
@@ -2099,7 +2104,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
                     ~default:def.item_meta))
     | _ -> def.item_meta
   in
-  let llbc_name = rename_llbc_name item_meta def.llbc_name in
+  let llbc_name = rename_llbc_name item_meta.attr_info def.llbc_name in
   ctx_compute_fun_name def.item_meta.span ctx llbc_name def.num_loops
     def.loop_id
 
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index a242e950..129fdd78 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -782,7 +782,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
                   FieldId.mapi
                     (fun fid (field : field) ->
                       ( fid,
-                        ctx_compute_field_name def field.item_meta ctx
+                        ctx_compute_field_name def field.attr_info ctx
                           def.llbc_name fid field.field_name ))
                     fields
                 in
@@ -1425,8 +1425,8 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   (let name =
-     if !Config.extract_external_name_patterns && not def.is_local then
-       Some def.llbc_name
+     if !Config.extract_external_name_patterns && not def.item_meta.is_local
+     then Some def.llbc_name
      else None
    in
    extract_comment_with_raw_span ctx fmt
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index e0a86145..d448c173 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -74,7 +74,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
        way. *)
     let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option =
       let open ExtractBuiltin in
-      NameMatcherMap.find_opt name_matcher_ctx f.name
+      NameMatcherMap.find_opt name_matcher_ctx f.item_meta.name
         (builtin_fun_effects_map ())
     in
 
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 075672fe..afa189e3 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -282,7 +282,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     (lazy
       ("evaluate_function_symbolic_synthesize_backward_from_return:"
      ^ "\n- fname: "
-      ^ Print.EvalCtx.name_to_string ctx fdef.name
+      ^ Print.EvalCtx.name_to_string ctx fdef.item_meta.name
       ^ "\n- back_id: "
       ^ RegionGroupId.to_string back_id
       ^ "\n- loop_id: "
@@ -526,7 +526,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
   let name_to_string () =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
-      fdef.name
+      fdef.item_meta.name
   in
   log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ()));
 
@@ -670,7 +670,7 @@ module Test = struct
         ("test_unit_function: "
         ^ Print.Types.name_to_string
             (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
-            fdef.name));
+            fdef.item_meta.name));
 
     (* Sanity check - *)
     sanity_check __FILE__ __LINE__
@@ -697,7 +697,7 @@ module Test = struct
             ("Unit test failed (concrete execution) on: "
             ^ Print.Types.name_to_string
                 (Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
-                fdef.name)
+                fdef.item_meta.name)
     in
     (* Evaluate the function *)
     let ctx_resl, _ = eval_function_body config body.body ctx in
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 1690aa80..c4e37646 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -647,7 +647,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
                   ("Attempted to greedily expand a symbolic enumeration with > \
                     1 variants (option [greedy_expand_symbolics_with_borrows] \
                     of [config]): "
-                  ^ name_to_string ctx def.name)
+                  ^ name_to_string ctx def.item_meta.name)
             | Alias _ | Opaque ->
                 craise __FILE__ __LINE__ span
                   "Attempted to greedily expand an alias or opaque type");
@@ -656,7 +656,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
               craise __FILE__ __LINE__ span
                 ("Attempted to greedily expand a recursive definition (option \
                   [greedy_expand_symbolics_with_borrows] of [config]): "
-                ^ name_to_string ctx def.name)
+                ^ name_to_string ctx def.item_meta.name)
             else expand_symbolic_value_no_branching config span sv None ctx
         | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
             (* Ok *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 27f503bc..67ac15d9 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1274,7 +1274,7 @@ and eval_transparent_function_call_concrete (config : config) (span : Meta.span)
         | None ->
             craise __FILE__ __LINE__ span
               ("Can't evaluate a call to an opaque function: "
-              ^ name_to_string ctx def.name)
+              ^ name_to_string ctx def.item_meta.name)
         | Some body -> body
       in
       (* TODO: we need to normalize the types if we want to correctly support traits *)
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 1053c9ab..e7b85c30 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -46,13 +46,14 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
        (which don't have a body but must not be considered as opaque) *)
     && (match d.kind with TraitItemDecl _ -> false | _ -> true)
     && ((not filter_assumed)
-       || (not (NameMatcherMap.mem ctx d.name builtin_globals_map))
-          && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ())))
+       || (not (NameMatcherMap.mem ctx d.item_meta.name builtin_globals_map))
+          && not (NameMatcherMap.mem ctx d.item_meta.name (builtin_funs_map ()))
+       )
   in
   let is_opaque_type (d : type_decl) : bool =
     d.kind = Opaque
     && ((not filter_assumed)
-       || not (NameMatcherMap.mem ctx d.name (builtin_types_map ())))
+       || not (NameMatcherMap.mem ctx d.item_meta.name (builtin_types_map ())))
   in
   (* Note that by checking the function bodies we also the globals *)
   ( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls),
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 5cef8b05..6bdf0a01 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -482,7 +482,7 @@ let apply_passes (crate : crate) : crate =
          However, we replace the body of the function, and save an error to
          report to the user the fact that we will ignore the function body *)
       let fmt = Print.Crate.crate_to_fmt_env crate in
-      let name = Print.name_to_string fmt f.name in
+      let name = Print.name_to_string fmt f.item_meta.name in
       save_error __FILE__ __LINE__ (Some f.item_meta.span)
         ("Ignoring the body of '" ^ name ^ "' because of previous error");
       { f with body = None }
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 2ff8c272..d273546a 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -355,14 +355,14 @@ and trait_instance_id =
 type field = {
   field_name : string option;
   field_ty : ty;
-  item_meta : item_meta;
+  attr_info : attr_info;
 }
 [@@deriving show]
 
 type variant = {
   variant_name : string;
   fields : field list;
-  item_meta : item_meta;
+  attr_info : attr_info;
 }
 [@@deriving show]
 
@@ -397,7 +397,6 @@ type predicates = { trait_type_constraints : trait_type_constraint list }
 
 type type_decl = {
   def_id : TypeDeclId.id;
-  is_local : bool;
   llbc_name : llbc_name;
       (** The original name coming from the LLBC declaration *)
   name : string;
@@ -405,7 +404,7 @@ type type_decl = {
           the name used at extraction time will be derived from the
           llbc_name.
        *)
-  item_meta : item_meta;
+  item_meta : T.item_meta;
   generics : generic_params;
   llbc_generics : Types.generic_params;
       (** We use the LLBC generics to generate "pretty" names, for instance
@@ -1097,8 +1096,7 @@ type backend_attributes = {
 
 type fun_decl = {
   def_id : FunDeclId.id;
-  is_local : bool;
-  item_meta : item_meta;
+  item_meta : T.item_meta;
   kind : item_kind;
   backend_attributes : backend_attributes;
   num_loops : int;
@@ -1121,9 +1119,9 @@ type fun_decl = {
 [@@deriving show]
 
 type global_decl = {
-  span : span;
   def_id : GlobalDeclId.id;
-  is_local : bool;
+  span : span;
+  item_meta : T.item_meta;
   llbc_name : llbc_name;  (** The original LLBC name. *)
   name : string;
       (** We use the name only for printing purposes (for debugging):
@@ -1142,10 +1140,9 @@ type global_decl = {
 
 type trait_decl = {
   def_id : trait_decl_id;
-  is_local : bool;
   llbc_name : llbc_name;
   name : string;
-  item_meta : item_meta;
+  item_meta : T.item_meta;
   generics : generic_params;
   llbc_generics : Types.generic_params;
       (** We use the LLBC generics to generate "pretty" names, for instance
@@ -1165,10 +1162,9 @@ type trait_decl = {
 
 type trait_impl = {
   def_id : trait_impl_id;
-  is_local : bool;
   llbc_name : llbc_name;
   name : string;
-  item_meta : item_meta;
+  item_meta : T.item_meta;
   impl_trait : trait_decl_ref;
   llbc_impl_trait : Types.trait_decl_ref;
       (** Same remark as for {!field:llbc_generics}. *)
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 543b2bee..dda6a611 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1499,7 +1499,6 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
             let loop_def : fun_decl =
               {
                 def_id = def.def_id;
-                is_local = def.is_local;
                 item_meta;
                 kind = def.kind;
                 backend_attributes = def.backend_attributes;
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 5a85628c..d38644c1 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -689,7 +689,6 @@ let trait_decl_get_method (trait_decl : trait_decl) (method_name : string) :
 let trait_decl_is_empty (trait_decl : trait_decl) : bool =
   let {
     def_id = _;
-    is_local = _;
     name = _;
     llbc_name = _;
     item_meta = _;
@@ -711,7 +710,6 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
 let trait_impl_is_empty (trait_impl : trait_impl) : bool =
   let {
     def_id = _;
-    is_local = _;
     name = _;
     llbc_name = _;
     item_meta = _;
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index c608c02e..6c5253b8 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -322,8 +322,9 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t)
     List.map
       (fun ((fid, d) : FunDeclId.id * fun_decl) ->
         ( FRegular fid,
-          (Types.name_to_string env d.name, d.signature, Some d.item_meta.span)
-        ))
+          ( Types.name_to_string env d.item_meta.name,
+            d.signature,
+            Some d.item_meta.span ) ))
       (FunDeclId.Map.bindings fun_decls)
   in
   let assumed =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7aa5c558..13c94bdf 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -542,8 +542,8 @@ let translate_generic_params (span : Meta.span) (generics : T.generic_params) :
 let translate_field (span : Meta.span) (f : T.field) : field =
   let field_name = f.field_name in
   let field_ty = translate_sty span f.field_ty in
-  let item_meta = f.item_meta in
-  { field_name; field_ty; item_meta }
+  let attr_info = f.attr_info in
+  { field_name; field_ty; attr_info }
 
 let translate_fields (span : Meta.span) (fl : T.field list) : field list =
   List.map (translate_field span) fl
@@ -551,8 +551,8 @@ let translate_fields (span : Meta.span) (fl : T.field list) : field list =
 let translate_variant (span : Meta.span) (v : T.variant) : variant =
   let variant_name = v.variant_name in
   let fields = translate_fields span v.fields in
-  let item_meta = v.item_meta in
-  { variant_name; fields; item_meta }
+  let attr_info = v.attr_info in
+  { variant_name; fields; attr_info }
 
 let translate_variants (span : Meta.span) (vl : T.variant list) : variant list =
   List.map (translate_variant span) vl
@@ -583,8 +583,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
        ^ "\n"));
   let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
   let def_id = def.T.def_id in
-  let llbc_name = def.name in
-  let name = Print.Types.name_to_string env def.name in
+  let llbc_name = def.item_meta.name in
+  let name = Print.Types.name_to_string env def.item_meta.name in
   (* Can't translate types with regions for now *)
   cassert __FILE__ __LINE__
     (def.generics.regions = [])
@@ -593,11 +593,9 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
     translate_generic_params def.item_meta.span def.generics
   in
   let kind = translate_type_decl_kind def.item_meta.span def.T.kind in
-  let is_local = def.is_local in
   let item_meta = def.item_meta in
   {
     def_id;
-    is_local;
     llbc_name;
     name;
     item_meta;
@@ -1285,7 +1283,8 @@ let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx)
   log#ldebug
     (lazy
       ("translate_fun_sig_from_decl_to_decomposed:" ^ "\n- name: "
-     ^ T.show_name fdef.name ^ "\n- sg:\n" ^ show_decomposed_fun_sig sg ^ "\n"));
+      ^ T.show_name fdef.item_meta.name
+      ^ "\n- sg:\n" ^ show_decomposed_fun_sig sg ^ "\n"));
   sg
 
 let mk_output_ty_from_effect_info (effect_info : fun_effect_info) (ty : ty) : ty
@@ -2184,7 +2183,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                   let decl =
                     FunDeclId.Map.find fid ctx.fun_ctx.llbc_fun_decls
                   in
-                  match Collections.List.last decl.name with
+                  match Collections.List.last decl.item_meta.name with
                   | PeIdent (s, _) -> s
                   | PeImpl _ ->
                       (* We shouldn't get there *)
@@ -2368,7 +2367,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
   log#ldebug
     (lazy
       ("translate_end_abstraction_synth_input:" ^ "\n- function: "
-      ^ name_to_string ctx ctx.fun_decl.name
+      ^ name_to_string ctx ctx.fun_decl.item_meta.name
       ^ "\n- rg_id: "
       ^ T.RegionGroupId.to_string rg_id
       ^ "\n- loop_id: "
@@ -3768,12 +3767,12 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   log#ldebug
     (lazy
       ("SymbolicToPure.translate_fun_decl: "
-      ^ name_to_string ctx def.name
+      ^ name_to_string ctx def.item_meta.name
       ^ "\n"));
 
   (* Translate the declaration *)
   let def_id = def.def_id in
-  let llbc_name = def.name in
+  let llbc_name = def.item_meta.name in
   let name = name_to_string ctx llbc_name in
   (* Translate the signature *)
   let signature = translate_fun_sig_from_decomposed ctx.sg in
@@ -3864,7 +3863,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
         log#ldebug
           (lazy
             ("SymbolicToPure.translate_fun_decl: "
-            ^ name_to_string ctx def.name
+            ^ name_to_string ctx def.item_meta.name
             ^ "\n- inputs: "
             ^ String.concat ", " (List.map show_var ctx.forward_inputs)
             ^ "\n- state: "
@@ -3894,7 +3893,6 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
   let def : fun_decl =
     {
       def_id;
-      is_local = def.is_local;
       item_meta = def.item_meta;
       kind = def.kind;
       backend_attributes;
@@ -3921,8 +3919,10 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
       try Some (translate_type_decl ctx d)
       with CFailure (span, _) ->
         let env = PrintPure.decls_ctx_to_fmt_env ctx in
-        let name = PrintPure.name_to_string env d.name in
-        let name_pattern = TranslateCore.name_to_pattern_string ctx d.name in
+        let name = PrintPure.name_to_string env d.item_meta.name in
+        let name_pattern =
+          TranslateCore.name_to_pattern_string ctx d.item_meta.name
+        in
         save_error __FILE__ __LINE__ span
           ("Could not translate type decl '" ^ name
          ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'");
@@ -3933,8 +3933,6 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     : trait_decl =
   let {
     def_id;
-    is_local;
-    name = llbc_name;
     item_meta;
     generics = llbc_generics;
     parent_clauses = llbc_parent_clauses;
@@ -3945,6 +3943,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
   } : A.trait_decl =
     trait_decl
   in
+  let llbc_name = item_meta.name in
   let type_infos = ctx.type_ctx.type_infos in
   let name =
     Print.Types.name_to_string
@@ -3979,7 +3978,6 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
   in
   {
     def_id;
-    is_local;
     llbc_name;
     name;
     item_meta;
@@ -3998,8 +3996,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     : trait_impl =
   let {
     A.def_id;
-    is_local;
-    name = llbc_name;
     item_meta;
     impl_trait = llbc_impl_trait;
     generics = llbc_generics;
@@ -4011,6 +4007,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   } =
     trait_impl
   in
+  let llbc_name = item_meta.name in
   let type_infos = ctx.type_ctx.type_infos in
   let impl_trait =
     translate_trait_decl_ref trait_impl.item_meta.span
@@ -4046,7 +4043,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   in
   {
     def_id;
-    is_local;
     llbc_name;
     name;
     item_meta;
@@ -4067,8 +4063,6 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
   let {
     A.item_meta;
     def_id;
-    is_local;
-    name = llbc_name;
     generics = llbc_generics;
     ty;
     kind;
@@ -4076,6 +4070,7 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
   } =
     decl
   in
+  let llbc_name = item_meta.name in
   let name =
     Print.Types.name_to_string
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
@@ -4088,7 +4083,7 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
   {
     span = item_meta.span;
     def_id;
-    is_local;
+    item_meta;
     llbc_name;
     name;
     llbc_generics;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0474d233..cadf8cbd 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -25,7 +25,8 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
   (* Debug *)
   log#ldebug
     (lazy
-      ("translate_function_to_symbolics: " ^ name_to_string trans_ctx fdef.name));
+      ("translate_function_to_symbolics: "
+      ^ name_to_string trans_ctx fdef.item_meta.name));
 
   match fdef.body with
   | None -> None
@@ -47,7 +48,9 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx)
     pure_fun_translation_no_loops =
   (* Debug *)
   log#ldebug
-    (lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.name));
+    (lazy
+      ("translate_function_to_pure: "
+      ^ name_to_string trans_ctx fdef.item_meta.name));
 
   (* Compute the symbolic ASTs, if the function is transparent *)
   let symbolic_trans = translate_function_to_symbolics trans_ctx fdef in
@@ -205,8 +208,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
     Some
       (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
   with CFailure (span, _) ->
-    let name = name_to_string trans_ctx fdef.name in
-    let name_pattern = name_to_pattern_string trans_ctx fdef.name in
+    let name = name_to_string trans_ctx fdef.item_meta.name in
+    let name_pattern = name_to_pattern_string trans_ctx fdef.item_meta.name in
     save_error __FILE__ __LINE__ span
       ("Could not translate the function '" ^ name
      ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'");
@@ -245,8 +248,10 @@ let translate_crate_to_pure (crate : crate) :
                  SymbolicToPure.translate_fun_sig_from_decl_to_decomposed
                    trans_ctx fdef )
            with CFailure (span, _) ->
-             let name = name_to_string trans_ctx fdef.name in
-             let name_pattern = name_to_pattern_string trans_ctx fdef.name in
+             let name = name_to_string trans_ctx fdef.item_meta.name in
+             let name_pattern =
+               name_to_pattern_string trans_ctx fdef.item_meta.name
+             in
              save_error __FILE__ __LINE__ span
                ("Could not translate the function signature of '" ^ name
               ^ " because of previous error\nName pattern: '" ^ name_pattern
@@ -268,8 +273,10 @@ let translate_crate_to_pure (crate : crate) :
       (fun d ->
         try Some (SymbolicToPure.translate_trait_decl trans_ctx d)
         with CFailure (span, _) ->
-          let name = name_to_string trans_ctx d.name in
-          let name_pattern = name_to_pattern_string trans_ctx d.name in
+          let name = name_to_string trans_ctx d.item_meta.name in
+          let name_pattern =
+            name_to_pattern_string trans_ctx d.item_meta.name
+          in
           save_error __FILE__ __LINE__ span
             ("Could not translate the trait declaration '" ^ name
            ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"
@@ -284,8 +291,10 @@ let translate_crate_to_pure (crate : crate) :
       (fun d ->
         try Some (SymbolicToPure.translate_trait_impl trans_ctx d)
         with CFailure (span, _) ->
-          let name = name_to_string trans_ctx d.name in
-          let name_pattern = name_to_pattern_string trans_ctx d.name in
+          let name = name_to_string trans_ctx d.item_meta.name in
+          let name_pattern =
+            name_to_pattern_string trans_ctx d.item_meta.name
+          in
           save_error __FILE__ __LINE__ span
             ("Could not translate the trait instance '" ^ name
            ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"
@@ -511,7 +520,9 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
   let open ExtractBuiltin in
   let extract =
     extract
-    && match_name_find_opt ctx.trans_ctx global.name builtin_globals_map = None
+    && match_name_find_opt ctx.trans_ctx global.item_meta.name
+         builtin_globals_map
+       = None
   in
   if extract then
     (* We don't wrap global declaration groups between calls to functions
@@ -522,8 +533,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     let global =
       try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
       with CFailure (span, _) ->
-        let name = name_to_string ctx.trans_ctx global.name in
-        let name_pattern = name_to_pattern_string ctx.trans_ctx global.name in
+        let name = name_to_string ctx.trans_ctx global.item_meta.name in
+        let name_pattern =
+          name_to_pattern_string ctx.trans_ctx global.item_meta.name
+        in
         save_error __FILE__ __LINE__ span
           ("Could not translate the global declaration '" ^ name
          ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'");
diff --git a/flake.lock b/flake.lock
index 19263560..73bd300d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1719218135,
-        "narHash": "sha256-ICbwKLkfAjuIivmruHF6srfn9MBjo/zO+IpLeKtH5d4=",
+        "lastModified": 1719229989,
+        "narHash": "sha256-/Eb1xd65HQeZtO7R/XMXA0ibzig7mffOLNGITuG6rVQ=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "2e74074eaa0528f3203dc1c160ccdba0f44b563a",
+        "rev": "5c2ae3744ce702d07920d0f536a272aadd396ed9",
         "type": "github"
       },
       "original": {
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index df80ccc6..bd281a82 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -1,17 +1,17 @@
 [Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
-[Error] In file Translate.ml, line 813:
+[Error] In file Translate.ml, line 826:
 Mutually recursive trait declarations are not supported
 
 Uncaught exception:
   
   (Failure
-    "In file Translate.ml, line 813:\
-   \nIn file Translate.ml, line 813:\
+    "In file Translate.ml, line 826:\
+   \nIn file Translate.ml, line 826:\
    \nMutually recursive trait declarations are not supported")
 
 Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 47, characters 4-76
 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
-Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 839, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 966, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1515, characters 5-42
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 852, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 979, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1528, characters 5-42
 Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66