Cleanup and fix a mistake

13 files changed, 172 insertions, 194 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index d6a5f0fc..1f9c9117 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -509,8 +509,6 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx)
       | Error (types, err) ->
           extract_generic_args meta ctx fmt TypeDeclId.Set.empty
             { generics with types };
-          (* if !Config.fail_hard then craise __FILE__ __LINE__ meta err
-             else *)
           save_error __FILE__ __LINE__ (Some meta) err;
           F.pp_print_string fmt
             "(\"ERROR: ill-formed builtin: invalid number of filtering \
@@ -1876,8 +1874,8 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (global : global_decl) (body : fun_decl) (interface : bool) : unit =
   let meta = body.meta in
-  sanity_check __FILE__ __LINE__ body.is_global_decl_body body.meta;
-  sanity_check __FILE__ __LINE__ (body.signature.inputs = []) body.meta;
+  sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
+  sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
@@ -2232,7 +2230,8 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
   cassert __FILE__ __LINE__
     (trait_impl.provided_methods = [])
     trait_impl.meta
-    ("Overriding provided methods is not supported yet (overriden methods: "
+    ("Overriding trait provided methods in trait implementations is not \
+      supported yet (overriden methods: "
     ^ String.concat ", " (List.map fst trait_impl.provided_methods)
     ^ ")");
   (* Everything is taken care of by {!extract_trait_decl_register_names} *but*
@@ -2622,8 +2621,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
   in
   extract_trait_impl_item ctx fmt fun_name ty
 
-(** Extract a trait implementation  
-*)
+(** Extract a trait implementation *)
 let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (impl : trait_impl) : unit =
   log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name));
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index cad469f9..f194d4e5 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -119,7 +119,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
           method! visit_Call env call =
             (match call.func with
             | FnOpMove _ ->
-                (* Ignoring this: we lookup t he called function upon creating
+                (* Ignoring this: we lookup the called function upon creating
                    the closure *)
                 ()
             | FnOpRegular func -> (
@@ -145,9 +145,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
         end
       in
       (* Sanity check: global bodies don't contain stateful calls *)
-      sanity_check __FILE__ __LINE__
+      cassert __FILE__ __LINE__
         ((not f.is_global_decl_body) || not !stateful)
-        f.meta;
+        f.meta "Global definition containing a stateful call in its body";
       let builtin_info = get_builtin_info f in
       let has_builtin_info = builtin_info <> None in
       group_has_builtin_info := !group_has_builtin_info || has_builtin_info;
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index b32261e6..e593ae75 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -443,8 +443,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta
-    "Only one loan should have been given back";
+  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
   (* Apply the reborrows *)
   apply_registered_reborrows ctx
 
@@ -503,7 +502,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
   let replaced : bool ref = ref false in
   let set_replaced () =
     cassert __FILE__ __LINE__ (not !replaced) meta
-      "Only one loan should have been updated";
+      "Exacly one loan should be updated";
     replaced := true
   in
   let obj =
@@ -589,7 +588,7 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta "Only one loan should be given back";
+  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
   (* Return *)
   ctx
 
@@ -608,7 +607,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   let replaced : bool ref = ref false in
   let set_replaced () =
     cassert __FILE__ __LINE__ (not !replaced) meta
-      "Only one loan should be updated";
+      "Exactly one loan should be updated";
     replaced := true
   in
   let obj =
@@ -673,8 +672,7 @@ let give_back_shared _config (meta : Meta.meta) (bid : BorrowId.id)
   (* Explore the environment *)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check we gave back to exactly one loan *)
-  cassert __FILE__ __LINE__ !replaced meta
-    "Exactly one loan should be given back";
+  cassert __FILE__ __LINE__ !replaced meta "No loan updated";
   (* Return *)
   ctx
 
@@ -1553,8 +1551,8 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
       (* I don't think it is possible to have two-phase borrows involving borrows
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
       craise __FILE__ __LINE__ meta
-        "Can't promote a shared loan to a mutable loan if the loan is inside \
-         an abstraction"
+        "Can't promote a shared loan to a mutable loan if the loan is inside a \
+         region abstraction"
 
 (** Helper function: see {!activate_reserved_mut_borrow}.
 
@@ -1581,7 +1579,7 @@ let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id)
         (* This can't happen for sure *)
         craise __FILE__ __LINE__ meta
           "Can't promote a shared borrow to a mutable borrow if the borrow is \
-           inside an abstraction"
+           inside a region abstraction"
   in
   (* Continue *)
   cf ctx
@@ -1647,7 +1645,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta)
        * returned by abstractions. I'm not sure how we could handle that anyway. *)
       craise __FILE__ __LINE__ meta
         "Can't activate a reserved mutable borrow referencing a loan inside\n\
-        \         an abstraction"
+        \         a region abstraction"
 
 let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
     (destructure_shared_values : bool) (ctx : eval_ctx) (abs0 : abs) : abs =
@@ -2272,12 +2270,11 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind)
 
   (* Sanity check: there is no loan/borrows which appears in both abstractions,
      unless we allow to merge duplicates *)
-  if merge_funs = None then
-    (sanity_check __FILE__ __LINE__
-       (BorrowId.Set.disjoint borrows0 borrows1)
-       meta;
-     sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1))
+  if merge_funs = None then (
+    sanity_check __FILE__ __LINE__
+      (BorrowId.Set.disjoint borrows0 borrows1)
       meta;
+    sanity_check __FILE__ __LINE__ (BorrowId.Set.disjoint loans0 loans1) meta);
 
   (* Merge.
      There are several cases:
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 92d8670a..6e65b11d 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -864,7 +864,7 @@ let update_intersecting_aproj_borrows (meta : Meta.meta)
   let ctx = obj#visit_eval_ctx None ctx in
   (* Check that we updated the context at least once *)
   cassert __FILE__ __LINE__ (Option.is_some !shared) meta
-    "Context was not updated at least once";
+    "Context was not updated";
   (* Return *)
   ctx
 
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 2283e842..a5b3a021 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -256,12 +256,12 @@ module type PrimMatcher = sig
 end
 
 module type Matcher = sig
+  val meta : Meta.meta
+
   (** Match two values.
 
       Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}.
    *)
-  val meta : Meta.meta
-
   val match_typed_values :
     eval_ctx -> eval_ctx -> typed_value -> typed_value -> typed_value
 
@@ -279,6 +279,8 @@ end
     Very annoying: functors only take modules as inputs...
  *)
 module type MatchCheckEquivState = sig
+  val meta : Meta.meta
+
   (** [true] if we check equivalence between contexts, [false] if we match
       a source context with a target context. *)
   val check_equiv : bool
@@ -299,7 +301,6 @@ module type MatchCheckEquivState = sig
   val aid_map : AbstractionId.InjSubst.t ref
   val lookup_shared_value_in_ctx0 : BorrowId.id -> typed_value
   val lookup_shared_value_in_ctx1 : BorrowId.id -> typed_value
-  val meta : Meta.meta
 end
 
 module type CheckEquivMatcher = sig
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index d97b05d0..de00cb93 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -491,8 +491,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
            are not in the prefix anymore *)
         if DummyVarId.Set.mem b0 fixed_ids.dids then (
           (* Still in the prefix: match the values *)
-          cassert __FILE__ __LINE__ (b0 = b1) meta
-            "Bindings are not the same. We are not in the prefix anymore";
+          sanity_check __FILE__ __LINE__ (b0 = b1) meta;
           let b = b0 in
           let v = M.match_typed_values ctx0 ctx1 v0 v1 in
           let var = EBinding (BDummy b, v) in
@@ -514,9 +513,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
 
         (* Variable bindings *must* be in the prefix and consequently their
            ids must be the same *)
-        cassert __FILE__ __LINE__ (b0 = b1) meta
-          "Variable bindings *must* be in the prefix and consequently their\n\
-          \        ids must be the same";
+        sanity_check __FILE__ __LINE__ (b0 = b1) meta;
         (* Match the values *)
         let b = b0 in
         let v = M.match_typed_values ctx0 ctx1 v0 v1 in
@@ -537,8 +534,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets)
         (* Same as for the dummy values: there are two cases *)
         if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
           (* Still in the prefix: the abstractions must be the same *)
-          cassert __FILE__ __LINE__ (abs0 = abs1) meta
-            "The abstractions are not the same";
+          sanity_check __FILE__ __LINE__ (abs0 = abs1) meta;
           (* Continue *)
           abs :: join_prefixes env0' env1')
         else (* Not in the prefix anymore *)
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index bd271ff4..e710ed2b 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -827,13 +827,13 @@ end
 
 (* Very annoying: functors only take modules as inputs... *)
 module type MatchMoveState = sig
+  val meta : Meta.meta
+
   (** The current loop *)
   val loop_id : LoopId.id
 
   (** The moved values *)
   val nvalues : typed_value list ref
-
-  val meta : Meta.meta
 end
 
 (* We use this matcher to move values in environment.
@@ -853,9 +853,9 @@ end
    indeed matches the resulting target environment: it will be re-checked later.
 *)
 module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
-  (** Small utility *)
   let meta = S.meta
 
+  (** Small utility *)
   let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues
 
   let match_etys _ _ ty0 ty1 =
@@ -959,6 +959,8 @@ end
 
 module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher =
 struct
+  let meta = S.meta
+
   module MkGetSetM (Id : Identifiers.Id) = struct
     module Inj = Id.InjSubst
 
@@ -1001,8 +1003,6 @@ struct
         (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1))
   end
 
-  let meta = S.meta
-
   module GetSetRid = MkGetSetM (RegionId)
 
   let match_rid = GetSetRid.match_e "match_rid: " S.rid_map
@@ -1383,15 +1383,15 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
     | EBinding (BDummy b0, v0) :: env0', EBinding (BDummy b1, v1) :: env1' ->
         (* Sanity check: if the dummy value is an old value, the bindings must
            be the same and their values equal (and the borrows/loans/symbolic *)
-        if DummyVarId.Set.mem b0 fixed_ids.dids then
-          ((* Fixed values: the values must be equal *)
-           sanity_check __FILE__ __LINE__ (b0 = b1) meta;
-           sanity_check __FILE__ __LINE__ (v0 = v1) meta;
-           (* The ids present in the left value must be fixed *)
-           let ids, _ = compute_typed_value_ids v0 in
-           sanity_check __FILE__ __LINE__
-             ((not S.check_equiv) || ids_are_fixed ids))
-            meta;
+        if DummyVarId.Set.mem b0 fixed_ids.dids then (
+          (* Fixed values: the values must be equal *)
+          sanity_check __FILE__ __LINE__ (b0 = b1) meta;
+          sanity_check __FILE__ __LINE__ (v0 = v1) meta;
+          (* The ids present in the left value must be fixed *)
+          let ids, _ = compute_typed_value_ids v0 in
+          sanity_check __FILE__ __LINE__
+            ((not S.check_equiv) || ids_are_fixed ids)
+            meta);
         (* We still match the values - allows to compute mappings (which
            are the identity actually) *)
         let _ = M.match_typed_values ctx0 ctx1 v0 v1 in
@@ -1457,9 +1457,16 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
       }
     in
     Some maps
-  with Distinct msg ->
-    log#ldebug (lazy ("match_ctxs: distinct: " ^ msg));
-    None
+  with
+  | Distinct msg ->
+      log#ldebug (lazy ("match_ctxs: distinct: " ^ msg ^ "\n"));
+      None
+  | ValueMatchFailure k ->
+      log#ldebug
+        (lazy
+          ("match_ctxs: distinct: ValueMatchFailure" ^ show_updt_env_kind k
+         ^ "\n"));
+      None
 
 let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets)
     (ctx0 : eval_ctx) (ctx1 : eval_ctx) : bool =
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 93e56106..f2c0bcb1 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -483,7 +483,7 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta)
               (Some (Synth.mk_mplace meta prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
-            craise __FILE__ __LINE__ meta "Found [Bottom] while reading a place"
+            craise __FILE__ __LINE__ meta "Found bottom while reading a place"
         | FailBorrow _ ->
             craise __FILE__ __LINE__ meta "Could not read a borrow"
       in
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 8b6eeb6c..6e86e6a4 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -199,22 +199,22 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
       | VSymbolic s, _ ->
           (* Check that the projection doesn't contain already ended regions,
            * if necessary *)
-          if check_symbolic_no_ended then
-            (let ty1 = s.sv_ty in
-             let rset1 = ctx.ended_regions in
-             let ty2 = ty in
-             let rset2 = regions in
-             log#ldebug
-               (lazy
-                 ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
-                ^ "\n- rset1: "
-                 ^ RegionId.Set.to_string None rset1
-                 ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
-                 ^ RegionId.Set.to_string None rset2
-                 ^ "\n"));
-             sanity_check __FILE__ __LINE__
-               (not (projections_intersect meta ty1 rset1 ty2 rset2)))
-              meta;
+          if check_symbolic_no_ended then (
+            let ty1 = s.sv_ty in
+            let rset1 = ctx.ended_regions in
+            let ty2 = ty in
+            let rset2 = regions in
+            log#ldebug
+              (lazy
+                ("projections_intersect:" ^ "\n- ty1: " ^ ty_to_string ctx ty1
+               ^ "\n- rset1: "
+                ^ RegionId.Set.to_string None rset1
+                ^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
+                ^ RegionId.Set.to_string None rset2
+                ^ "\n"));
+            sanity_check __FILE__ __LINE__
+              (not (projections_intersect meta ty1 rset1 ty2 rset2))
+              meta);
           ASymbolic (AProjBorrows (s, ty))
       | _ ->
           log#lerror
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 11cd89fc..0b39f64a 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -402,8 +402,8 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
     let check_visitor =
       object
         inherit [_] iter_statement as super
-        (* Remember the span of the statement we enter *)
 
+        (* Remember the span of the statement we enter *)
         method! visit_statement _ st = super#visit_statement st.meta st
 
         method! visit_var_id meta id =
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 12b3387a..9fa07029 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1989,6 +1989,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
       (List.concat (List.map (fun { f; loops } -> [ f :: loops ]) transl))
   in
   let subgroups = ReorderDecls.group_reorder_fun_decls all_decls in
+
   log#ldebug
     (lazy
       ("filter_loop_inputs: all_decls:\n\n"
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4830f65a..0c30f44c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -144,6 +144,7 @@ type loop_info = {
 (** Body synthesis context *)
 type bs_ctx = {
   (* TODO: there are a lot of duplications with the various decls ctx *)
+  meta : Meta.meta;  (** The meta information about the current declaration *)
   decls_ctx : C.decls_ctx;
   type_ctx : type_ctx;
   fun_ctx : fun_ctx;
@@ -325,7 +326,7 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
 
 let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
   let env = bs_ctx_to_fmt_env ctx in
-  Print.Values.typed_value_to_string ~meta:(Some ctx.fun_decl.meta) env v
+  Print.Values.typed_value_to_string ~meta:(Some ctx.meta) env v
 
 let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let env = bs_ctx_to_pure_fmt_env ctx in
@@ -349,8 +350,7 @@ let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
 
 let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
   let env = bs_ctx_to_pure_fmt_env ctx in
-  PrintPure.texpression_to_string ~metadata:(Some ctx.fun_decl.meta) env false
-    "" "  " e
+  PrintPure.texpression_to_string ~metadata:(Some ctx.meta) env false "" "  " e
 
 let fun_id_to_string (ctx : bs_ctx) (id : A.fun_id) : string =
   let env = bs_ctx_to_fmt_env ctx in
@@ -364,10 +364,9 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
   let env = bs_ctx_to_pure_fmt_env ctx in
   PrintPure.fun_decl_to_string env def
 
-let typed_pattern_to_string ?(meta : Meta.meta option = None) (ctx : bs_ctx)
-    (p : Pure.typed_pattern) : string =
+let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
   let env = bs_ctx_to_pure_fmt_env ctx in
-  PrintPure.typed_pattern_to_string ~meta env p
+  PrintPure.typed_pattern_to_string ~meta:(Some ctx.meta) env p
 
 let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) :
     fun_effect_info =
@@ -386,7 +385,7 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
   let verbose = false in
   let indent = "" in
   let indent_incr = "  " in
-  Print.Values.abs_to_string ~meta:(Some ctx.fun_decl.meta) env verbose indent
+  Print.Values.abs_to_string ~meta:(Some ctx.meta) env verbose indent
     indent_incr abs
 
 let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
@@ -676,13 +675,13 @@ and translate_fwd_trait_instance_id (meta : Meta.meta) (type_infos : type_infos)
 (** Simply calls [translate_fwd_ty] *)
 let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty =
   let type_infos = ctx.type_ctx.type_infos in
-  translate_fwd_ty ctx.fun_decl.meta type_infos ty
+  translate_fwd_ty ctx.meta type_infos ty
 
 (** Simply calls [translate_fwd_generic_args] *)
 let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
     generic_args =
   let type_infos = ctx.type_ctx.type_infos in
-  translate_fwd_generic_args ctx.fun_decl.meta type_infos generics
+  translate_fwd_generic_args ctx.meta type_infos generics
 
 (** Translate a type, when some regions may have ended.
     
@@ -775,7 +774,7 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos)
 let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
     (inside_mut : bool) (ty : T.ty) : ty option =
   let type_infos = ctx.type_ctx.type_infos in
-  translate_back_ty ctx.fun_decl.meta type_infos keep_region inside_mut ty
+  translate_back_ty ctx.meta type_infos keep_region inside_mut ty
 
 let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
   let const_generics =
@@ -794,14 +793,14 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
   }
 
 let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
-  let meta = ctx.fun_decl.meta in
+  let meta = ctx.meta in
   let ctx = mk_type_check_ctx ctx in
   let _ = PureTypeCheck.check_typed_pattern meta ctx v in
   ()
 
 let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
   if !Config.type_check_pure_code then
-    let meta = ctx.fun_decl.meta in
+    let meta = ctx.meta in
     let ctx = mk_type_check_ctx ctx in
     PureTypeCheck.check_texpression meta ctx e
 
@@ -811,9 +810,7 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
   | FunId fun_id -> FunId fun_id
   | TraitMethod (trait_ref, method_name, fun_decl_id) ->
       let type_infos = ctx.type_ctx.type_infos in
-      let trait_ref =
-        translate_fwd_trait_ref ctx.fun_decl.meta type_infos trait_ref
-      in
+      let trait_ref = translate_fwd_trait_ref ctx.meta type_infos trait_ref in
       TraitMethod (trait_ref, method_name, fun_decl_id)
 
 let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
@@ -823,7 +820,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
   let calls = ctx.calls in
   sanity_check __FILE__ __LINE__
     (not (V.FunCallId.Map.mem call_id calls))
-    ctx.fun_decl.meta;
+    ctx.meta;
   let info = { forward; forward_inputs = args; back_funs } in
   let calls = V.FunCallId.Map.add call_id info calls in
   { ctx with calls }
@@ -847,7 +844,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
   let abstractions = ctx.abstractions in
   sanity_check __FILE__ __LINE__
     (not (V.AbstractionId.Map.mem abs.abs_id abstractions))
-    ctx.fun_decl.meta;
+    ctx.meta;
   let abstractions =
     V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions
   in
@@ -953,22 +950,20 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref)
           in
           { info with is_rec = info.is_rec || Option.is_some lid }
       | FunId (FAssumed _) ->
-          compute_raw_fun_effect_info ctx.fun_decl.meta ctx.fun_ctx.fun_infos
-            fun_id lid gid)
+          compute_raw_fun_effect_info ctx.meta ctx.fun_ctx.fun_infos fun_id lid
+            gid)
   | Some lid -> (
       (* This is necessarily for the current function *)
       match fun_id with
       | FunId (FRegular fid) -> (
-          sanity_check __FILE__ __LINE__
-            (fid = ctx.fun_decl.def_id)
-            ctx.fun_decl.meta;
+          sanity_check __FILE__ __LINE__ (fid = ctx.fun_decl.def_id) ctx.meta;
           (* Lookup the loop *)
           let lid = V.LoopId.Map.find lid ctx.loop_ids_map in
           let loop_info = LoopId.Map.find lid ctx.loops in
           match gid with
           | None -> loop_info.fwd_effect_info
           | Some gid -> RegionGroupId.Map.find gid loop_info.back_effect_infos)
-      | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable")
+      | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable")
 
 (** Translate a function signature to a decomposed function signature.
 
@@ -1514,7 +1509,7 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
   match V.SymbolicValueId.Map.find_opt sv.sv_id ctx.sv_to_var with
   | Some v -> v
   | None ->
-      craise __FILE__ __LINE__ ctx.fun_decl.meta
+      craise __FILE__ __LINE__ ctx.meta
         ("Could not find var for symbolic value: "
         ^ V.SymbolicValueId.to_string sv.sv_id)
 
@@ -1564,7 +1559,7 @@ let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) :
 let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
     (v : V.typed_value) : texpression =
   (* We need to ignore boxes *)
-  let v = unbox_typed_value ctx.fun_decl.meta v in
+  let v = unbox_typed_value ctx.meta v in
   let translate = typed_value_to_texpression ctx ectx in
   (* Translate the type *)
   let ty = ctx_translate_fwd_ty ctx v.ty in
@@ -1578,12 +1573,12 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
         match v.ty with
         | TAdt (TTuple, _) ->
-            sanity_check __FILE__ __LINE__ (variant_id = None) ctx.fun_decl.meta;
-            mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
+            sanity_check __FILE__ __LINE__ (variant_id = None) ctx.meta;
+            mk_simpl_tuple_texpression ctx.meta field_values
         | _ ->
             (* Retrieve the type and the translated generics from the translated
                type (simpler this way) *)
-            let adt_id, generics = ty_as_adt ctx.fun_decl.meta ty in
+            let adt_id, generics = ty_as_adt ctx.meta ty in
             (* Create the constructor *)
             let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in
             let qualif = { id = qualif_id; generics } in
@@ -1594,20 +1589,18 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
             let cons_ty = mk_arrows field_tys ty in
             let cons = { e = cons_e; ty = cons_ty } in
             (* Apply the constructor *)
-            mk_apps ctx.fun_decl.meta cons field_values)
-    | VBottom -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+            mk_apps ctx.meta cons field_values)
+    | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
     | VLoan lc -> (
         match lc with
         | VSharedLoan (_, v) -> translate v
-        | VMutLoan _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
-        )
+        | VMutLoan _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable")
     | VBorrow bc -> (
         match bc with
         | VSharedBorrow bid ->
             (* Lookup the shared value in the context, and continue *)
             let sv =
-              InterpreterBorrowsCore.lookup_shared_value ctx.fun_decl.meta ectx
-                bid
+              InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid
             in
             translate sv
         | VReservedMutBorrow bid ->
@@ -1615,8 +1608,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
              * only in *meta-data*: a value *actually used* in the translation can't come
              * from an unpromoted reserved borrow *)
             let sv =
-              InterpreterBorrowsCore.lookup_shared_value ctx.fun_decl.meta ectx
-                bid
+              InterpreterBorrowsCore.lookup_shared_value ctx.meta ectx bid
             in
             translate sv
         | VMutBorrow (_, v) ->
@@ -1663,7 +1655,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
         | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
-            cassert __FILE__ __LINE__ (field_values = []) ctx.fun_decl.meta
+            cassert __FILE__ __LINE__ (field_values = []) ctx.meta
               "ADTs containing borrows are not supported yet";
             None
         | TTuple ->
@@ -1672,11 +1664,9 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
             else
               (* Note that if there is exactly one field value,
                * [mk_simpl_tuple_rvalue] is the identity *)
-              let rv =
-                mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
-              in
+              let rv = mk_simpl_tuple_texpression ctx.meta field_values in
               Some rv)
-    | ABottom -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+    | ABottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
     | ALoan lc -> aloan_content_to_consumed ctx ectx lc
     | ABorrow bc -> aborrow_content_to_consumed ctx bc
     | ASymbolic aproj -> aproj_to_consumed ctx aproj
@@ -1694,7 +1684,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
     (lc : V.aloan_content) : texpression option =
   match lc with
   | AMutLoan (_, _) | ASharedLoan (_, _, _) ->
-      craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+      craise __FILE__ __LINE__ ctx.meta "Unreachable"
   | AEndedMutLoan { child = _; given_back = _; given_back_meta } ->
       (* Return the meta-value *)
       Some (typed_value_to_texpression ctx ectx given_back_meta)
@@ -1706,7 +1696,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
       None
   | AIgnoredMutLoan (_, _) ->
       (* There can be *inner* not ended mutable loans, but not outer ones *)
-      craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+      craise __FILE__ __LINE__ ctx.meta "Unreachable"
   | AEndedIgnoredMutLoan _ ->
       (* This happens with nested borrows: we need to dive in *)
       raise Unimplemented
@@ -1718,7 +1708,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
     texpression option =
   match bc with
   | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
-      craise __FILE__ __LINE__ _ctx.fun_decl.meta "Unreachable"
+      craise __FILE__ __LINE__ _ctx.meta "Unreachable"
   | AEndedMutBorrow (_, _) ->
       (* We collect consumed values: ignore *)
       None
@@ -1737,7 +1727,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option =
   | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) ->
       sanity_check __FILE__ __LINE__
         (child_aproj = AIgnoredProjBorrows)
-        ctx.fun_decl.meta;
+        ctx.meta;
       (* The symbolic value was updated *)
       Some (symbolic_value_to_texpression ctx mnv)
   | V.AEndedProjLoans (_, _) ->
@@ -1746,7 +1736,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option =
       raise Unimplemented
   | AEndedProjBorrows _ -> (* We consider consumed values *) None
   | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
-      craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+      craise __FILE__ __LINE__ ctx.meta "Unreachable"
 
 (** Convert the abstraction values in an abstraction to consumed values.
 
@@ -1812,20 +1802,20 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
         | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
-            cassert __FILE__ __LINE__ (field_values = []) ctx.fun_decl.meta
+            cassert __FILE__ __LINE__ (field_values = []) ctx.meta
               "ADTs with borrows are not supported yet";
             (ctx, None)
         | TTuple ->
             (* Return *)
             let variant_id = adt_v.variant_id in
-            sanity_check __FILE__ __LINE__ (variant_id = None) ctx.fun_decl.meta;
+            sanity_check __FILE__ __LINE__ (variant_id = None) ctx.meta;
             if field_values = [] then (ctx, None)
             else
               (* Note that if there is exactly one field value, [mk_simpl_tuple_pattern]
                * is the identity *)
               let lv = mk_simpl_tuple_pattern field_values in
               (ctx, Some lv))
-    | ABottom -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+    | ABottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
     | ALoan lc -> aloan_content_to_given_back mp lc ctx
     | ABorrow bc -> aborrow_content_to_given_back mp bc ctx
     | ASymbolic aproj -> aproj_to_given_back mp aproj ctx
@@ -1841,14 +1831,14 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
     (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   match lc with
   | AMutLoan (_, _) | ASharedLoan (_, _, _) ->
-      craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+      craise __FILE__ __LINE__ ctx.meta "Unreachable"
   | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
   | AEndedSharedLoan (_, _) ->
       (* We consider given back values, and thus ignore those *)
       (ctx, None)
   | AIgnoredMutLoan (_, _) ->
       (* There can be *inner* not ended mutable loans, but not outer ones *)
-      craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+      craise __FILE__ __LINE__ ctx.meta "Unreachable"
   | AEndedIgnoredMutLoan _ ->
       (* This happens with nested borrows: we need to dive in *)
       raise Unimplemented
@@ -1860,7 +1850,7 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
     (ctx : bs_ctx) : bs_ctx * typed_pattern option =
   match bc with
   | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
-      craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+      craise __FILE__ __LINE__ ctx.meta "Unreachable"
   | AEndedMutBorrow (msv, _) ->
       (* Return the meta-symbolic-value *)
       let ctx, var = fresh_var_for_symbolic_value msv ctx in
@@ -1882,14 +1872,14 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
         (List.for_all
            (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows)
            child_projs)
-        ctx.fun_decl.meta "Nested borrows are not supported yet";
+        ctx.meta "Nested borrows are not supported yet";
       (ctx, None)
   | AEndedProjBorrows mv ->
       (* Return the meta-value *)
       let ctx, var = fresh_var_for_symbolic_value mv ctx in
       (ctx, Some (mk_typed_pattern_from_var var mp))
   | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
-      craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+      craise __FILE__ __LINE__ ctx.meta "Unreachable"
 
 (** Convert the abstraction values in an abstraction to given back values.
 
@@ -2004,7 +1994,7 @@ and translate_panic (ctx : bs_ctx) : texpression =
   (* Here we use the function return type - note that it is ok because
    * we don't match on panics which happen inside the function body -
    * but it won't be true anymore once we translate individual blocks *)
-  (* If we use a state modune partie nad, we need to add a lambda for the state variable *)
+  (* If we use a state monad, we need to add a lambda for the state variable *)
   (* Note that only forward functions return a state *)
   let effect_info = ctx_get_effect_info ctx in
   (* TODO: we should use a [Fail] function *)
@@ -2013,13 +2003,13 @@ and translate_panic (ctx : bs_ctx) : texpression =
       (* Create the [Fail] value *)
       let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
       let ret_v =
-        mk_result_fail_texpression_with_error_id ctx.fun_decl.meta
-          error_failure_id ret_ty
+        mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+          ret_ty
       in
       ret_v
     else
-      mk_result_fail_texpression_with_error_id ctx.fun_decl.meta
-        error_failure_id output_ty
+      mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+        output_ty
   in
   if ctx.inside_loop && Option.is_some ctx.bid then
     (* We are synthesizing the backward function of a loop body *)
@@ -2075,12 +2065,12 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
     | Some _ ->
         (* Backward function *)
         (* Sanity check *)
-        sanity_check __FILE__ __LINE__ (opt_v = None) ctx.fun_decl.meta;
+        sanity_check __FILE__ __LINE__ (opt_v = None) ctx.meta;
         (* Group the variables in which we stored the values we need to give back.
            See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
         let backward_outputs = Option.get ctx.backward_outputs in
         let field_values = List.map mk_texpression_from_var backward_outputs in
-        mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
+        mk_simpl_tuple_texpression ctx.meta field_values
   in
   (* We may need to return a state
    * - error-monad: Return x
@@ -2090,21 +2080,17 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
   let output =
     if effect_info.stateful then
       let state_rvalue = mk_state_texpression ctx.state_var in
-      mk_simpl_tuple_texpression ctx.fun_decl.meta [ state_rvalue; output ]
+      mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
     else output
   in
   (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
-  mk_result_return_texpression ctx.fun_decl.meta output
+  mk_result_return_texpression ctx.meta output
 
 and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
     (ctx : bs_ctx) : texpression =
-  sanity_check __FILE__ __LINE__
-    (is_continue = ctx.inside_loop)
-    ctx.fun_decl.meta;
+  sanity_check __FILE__ __LINE__ (is_continue = ctx.inside_loop) ctx.meta;
   let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in
-  sanity_check __FILE__ __LINE__
-    (loop_id = Option.get ctx.loop_id)
-    ctx.fun_decl.meta;
+  sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.meta;
 
   (* Lookup the loop information *)
   let loop_id = Option.get ctx.loop_id in
@@ -2128,7 +2114,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
           match ctx.backward_outputs with Some outputs -> outputs | None -> []
         in
         let field_values = List.map mk_texpression_from_var backward_outputs in
-        mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
+        mk_simpl_tuple_texpression ctx.meta field_values
   in
 
   (* We may need to return a state
@@ -2142,12 +2128,12 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
   let output =
     if effect_info.stateful then
       let state_rvalue = mk_state_texpression ctx.state_var in
-      mk_simpl_tuple_texpression ctx.fun_decl.meta [ state_rvalue; output ]
+      mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
     else output
   in
   (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
   mk_emeta (Tag "return_with_loop")
-    (mk_result_return_texpression ctx.fun_decl.meta output)
+    (mk_result_return_texpression ctx.meta output)
 
 and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     texpression =
@@ -2198,8 +2184,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
           let sg = Option.get call.sg in
           let decls_ctx = ctx.decls_ctx in
           let dsg =
-            translate_fun_sig_with_regions_hierarchy_to_decomposed
-              ctx.fun_decl.meta decls_ctx fid call.regions_hierarchy sg
+            translate_fun_sig_with_regions_hierarchy_to_decomposed ctx.meta
+              decls_ctx fid call.regions_hierarchy sg
               (List.map (fun _ -> None) sg.inputs)
           in
           log#ldebug
@@ -2212,7 +2198,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                   ctx_translate_fwd_generic_args ctx all_generics
                 in
                 let tr_self =
-                  translate_fwd_trait_instance_id ctx.fun_decl.meta
+                  translate_fwd_trait_instance_id ctx.meta
                     ctx.type_ctx.type_infos tr_self
                 in
                 (tr_self, all_generics)
@@ -2333,7 +2319,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     | S.Unop E.Neg -> (
         match args with
         | [ arg ] ->
-            let int_ty = ty_as_integer ctx.fun_decl.meta arg.ty in
+            let int_ty = ty_as_integer ctx.meta arg.ty in
             (* Note that negation can lead to an overflow and thus fail (it
              * is thus monadic) *)
             let effect_info =
@@ -2348,7 +2334,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
             let dest = mk_typed_pattern_from_var dest dest_mplace in
             (ctx, Unop (Neg int_ty), effect_info, args, dest)
-        | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable")
+        | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable")
     | S.Unop (E.Cast cast_kind) -> (
         match cast_kind with
         | CastScalar (src_ty, tgt_ty) ->
@@ -2366,18 +2352,16 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             let dest = mk_typed_pattern_from_var dest dest_mplace in
             (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest)
         | CastFnPtr _ ->
-            craise __FILE__ __LINE__ ctx.fun_decl.meta "TODO: function casts")
+            craise __FILE__ __LINE__ ctx.meta "TODO: function casts")
     | S.Binop binop -> (
         match args with
         | [ arg0; arg1 ] ->
-            let int_ty0 = ty_as_integer ctx.fun_decl.meta arg0.ty in
-            let int_ty1 = ty_as_integer ctx.fun_decl.meta arg1.ty in
+            let int_ty0 = ty_as_integer ctx.meta arg0.ty in
+            let int_ty1 = ty_as_integer ctx.meta arg1.ty in
             (match binop with
             (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *)
             | E.Shl | E.Shr -> ()
-            | _ ->
-                sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1)
-                  ctx.fun_decl.meta);
+            | _ -> sanity_check __FILE__ __LINE__ (int_ty0 = int_ty1) ctx.meta);
             let effect_info =
               {
                 can_fail = ExpressionsUtils.binop_can_fail binop;
@@ -2390,7 +2374,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
             let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
             let dest = mk_typed_pattern_from_var dest dest_mplace in
             (ctx, Binop (binop, int_ty0), effect_info, args, dest)
-        | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable")
+        | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable")
   in
   let func = { id = FunOrOp fun_id; generics } in
   let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
@@ -2399,7 +2383,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
   in
   let func_ty = mk_arrows input_tys ret_ty in
   let func = { e = Qualif func; ty = func_ty } in
-  let call = mk_apps ctx.fun_decl.meta func args in
+  let call = mk_apps ctx.meta func args in
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
   (* Put together *)
@@ -2433,7 +2417,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
       ^ "\n- loop_id: "
       ^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id
       ^ "\n- eval_ctx:\n"
-      ^ eval_ctx_to_string ~meta:(Some ctx.fun_decl.meta) ectx
+      ^ eval_ctx_to_string ~meta:(Some ctx.meta) ectx
       ^ "\n- abs:\n" ^ abs_to_string ctx abs ^ "\n"));
 
   (* When we end an input abstraction, this input abstraction gets back
@@ -2447,7 +2431,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
      for a parent backward function.
   *)
   let bid = Option.get ctx.bid in
-  sanity_check __FILE__ __LINE__ (rg_id = bid) ctx.fun_decl.meta;
+  sanity_check __FILE__ __LINE__ (rg_id = bid) ctx.meta;
 
   (* First, introduce the given back variables.
 
@@ -2497,7 +2481,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
       (fun (var, v) ->
         sanity_check __FILE__ __LINE__
           ((var : var).ty = (v : texpression).ty)
-          ctx.fun_decl.meta)
+          ctx.meta)
       variables_values;
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
@@ -2518,7 +2502,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     | S.Fun (fun_id, _) -> fun_id
     | Unop _ | Binop _ ->
         (* Those don't have backward functions *)
-        craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+        craise __FILE__ __LINE__ ctx.meta "Unreachable"
   in
   let effect_info = get_fun_effect_info ctx fun_id None (Some rg_id) in
   (* Retrieve the values consumed upon ending the loans inside this
@@ -2580,7 +2564,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
            ^ "\nfunc type: "
            ^ pure_ty_to_string ctx func.ty
            ^ "\n\nargs:\n" ^ String.concat "\n" args));
-      let call = mk_apps ctx.fun_decl.meta func args in
+      let call = mk_apps ctx.meta func args in
       mk_let effect_info.can_fail output call next_e
 
 and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
@@ -2591,8 +2575,8 @@ and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
   (* We can do this simply by checking that it consumes and gives back nothing *)
   let inputs = abs_to_consumed ctx ectx abs in
   let ctx, outputs = abs_to_given_back None abs ctx in
-  sanity_check __FILE__ __LINE__ (inputs = []) ctx.fun_decl.meta;
-  sanity_check __FILE__ __LINE__ (outputs = []) ctx.fun_decl.meta;
+  sanity_check __FILE__ __LINE__ (inputs = []) ctx.meta;
+  sanity_check __FILE__ __LINE__ (outputs = []) ctx.meta;
 
   (* Translate the next expression *)
   translate_expression e ctx
@@ -2634,7 +2618,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
   (* Retrieve the values consumed upon ending the loans inside this
    * abstraction: as there are no nested borrows, there should be none. *)
   let consumed = abs_to_consumed ctx ectx abs in
-  cassert __FILE__ __LINE__ (consumed = []) ctx.fun_decl.meta
+  cassert __FILE__ __LINE__ (consumed = []) ctx.meta
     "Nested borrows are not supported yet";
   (* Retrieve the values given back upon ending this abstraction - note that
    * we don't provide meta-place information, because those assignments will
@@ -2653,8 +2637,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
           ^ pure_ty_to_string ctx given_back.ty
           ^ "\n- sig input ty: "
           ^ pure_ty_to_string ctx input.ty));
-      sanity_check __FILE__ __LINE__ (given_back.ty = input.ty)
-        ctx.fun_decl.meta)
+      sanity_check __FILE__ __LINE__ (given_back.ty = input.ty) ctx.meta)
     given_back_inputs;
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
@@ -2671,9 +2654,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
     texpression =
   let vloop_id = loop_id in
   let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in
-  sanity_check __FILE__ __LINE__
-    (loop_id = Option.get ctx.loop_id)
-    ctx.fun_decl.meta;
+  sanity_check __FILE__ __LINE__ (loop_id = Option.get ctx.loop_id) ctx.meta;
   let rg_id = Option.get rg_id in
   (* There are two cases depending on the [abs_kind] (whether this is a
      synth input or a regular loop call) *)
@@ -2743,7 +2724,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       match func with
       | None -> next_e
       | Some func ->
-          let call = mk_apps ctx.fun_decl.meta func args in
+          let call = mk_apps ctx.meta func args in
           (* Add meta-information - this is slightly hacky: we look at the
              values consumed by the abstraction (note that those come from
              *before* we applied the fixed-point context) and use them to
@@ -2800,7 +2781,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
   in
   let func_ty = mk_arrow (TLiteral TBool) mk_unit_ty in
   let func = { e = Qualif func; ty = func_ty } in
-  let assertion = mk_apps ctx.fun_decl.meta func args in
+  let assertion = mk_apps ctx.meta func args in
   mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e
 
 and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
@@ -2815,7 +2796,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
       | V.SeLiteral _ ->
           (* We do not *register* symbolic expansions to literal
              values in the symbolic ADT *)
-          craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+          craise __FILE__ __LINE__ ctx.meta "Unreachable"
       | SeMutRef (_, nsv) | SeSharedRef (_, nsv) ->
           (* The (mut/shared) borrow type is extracted to identity: we thus simply
              introduce an reassignment *)
@@ -2828,11 +2809,11 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
             next_e
       | SeAdt _ ->
           (* Should be in the [ExpandAdt] case *)
-          craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable")
+          craise __FILE__ __LINE__ ctx.meta "Unreachable")
   | ExpandAdt branches -> (
       (* We don't do the same thing if there is a branching or not *)
       match branches with
-      | [] -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+      | [] -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
       | [ (variant_id, svl, branch) ]
         when not
                (TypesUtils.ty_is_custom_adt sv.V.sv_ty
@@ -2873,7 +2854,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
           (* Sanity check *)
           sanity_check __FILE__ __LINE__
             (List.for_all (fun br -> br.branch.ty = ty) branches)
-            ctx.fun_decl.meta;
+            ctx.meta;
           (* Return *)
           { e; ty })
   | ExpandBool (true_e, false_e) ->
@@ -2893,7 +2874,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
           ^ pure_ty_to_string ctx true_e.ty
           ^ "\n\nfalse_e.ty: "
           ^ pure_ty_to_string ctx false_e.ty));
-      sanity_check __FILE__ __LINE__ (ty = false_e.ty) ctx.fun_decl.meta;
+      sanity_check __FILE__ __LINE__ (ty = false_e.ty) ctx.meta;
       { e; ty }
   | ExpandInt (int_ty, branches, otherwise) ->
       let translate_branch ((v, branch_e) : V.scalar_value * S.expression) :
@@ -2920,7 +2901,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
       let ty = otherwise.branch.ty in
       sanity_check __FILE__ __LINE__
         (List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches)
-        ctx.fun_decl.meta;
+        ctx.meta;
       { e; ty }
 
 (* Translate and [ExpandAdt] when there is no branching (i.e., one branch).
@@ -2995,14 +2976,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
          * field.
          * We use the [dest] variable in order not to have to recompute
          * the type of the result of the projection... *)
-        let adt_id, generics = ty_as_adt ctx.fun_decl.meta scrutinee.ty in
+        let adt_id, generics = ty_as_adt ctx.meta scrutinee.ty in
         let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression =
           let proj_kind = { adt_id; field_id } in
           let qualif = { id = Proj proj_kind; generics } in
           let proj_e = Qualif qualif in
           let proj_ty = mk_arrow scrutinee.ty dest.ty in
           let proj = { e = proj_e; ty = proj_ty } in
-          mk_app ctx.fun_decl.meta proj scrutinee
+          mk_app ctx.meta proj scrutinee
         in
         let id_var_pairs = FieldId.mapi (fun fid v -> (fid, v)) vars in
         let monadic = false in
@@ -3023,7 +3004,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
       let var =
         match vars with
         | [ v ] -> v
-        | _ -> craise __FILE__ __LINE__ ctx.fun_decl.meta "Unreachable"
+        | _ -> craise __FILE__ __LINE__ ctx.meta "Unreachable"
       in
       (* We simply introduce an assignment - the box type is the
        * identity when extracted ([box a = a]) *)
@@ -3037,7 +3018,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
        * through the functions provided by the API (note that we don't
        * know how to expand values like vectors or arrays, because they have a variable number
        * of fields!) *)
-      craise __FILE__ __LINE__ ctx.fun_decl.meta
+      craise __FILE__ __LINE__ ctx.meta
         "Attempt to expand a non-expandable value"
 
 and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
@@ -3075,9 +3056,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
     | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
     | VaTraitConstValue (trait_ref, const_name) ->
         let type_infos = ctx.type_ctx.type_infos in
-        let trait_ref =
-          translate_fwd_trait_ref ctx.fun_decl.meta type_infos trait_ref
-        in
+        let trait_ref = translate_fwd_trait_ref ctx.meta type_infos trait_ref in
         let qualif_id = TraitConst (trait_ref, const_name) in
         let qualif = { id = qualif_id; generics = empty_generic_args } in
         { e = Qualif qualif; ty = var.ty }
@@ -3218,7 +3197,7 @@ and translate_forward_end (ectx : C.eval_ctx)
       else pure_fwd_var :: back_vars
     in
     let vars = List.map mk_texpression_from_var vars in
-    let ret = mk_simpl_tuple_texpression ctx.fun_decl.meta vars in
+    let ret = mk_simpl_tuple_texpression ctx.meta vars in
 
     (* Introduce a fresh input state variable for the forward expression *)
     let _ctx, state_var, state_pat =
@@ -3229,10 +3208,8 @@ and translate_forward_end (ectx : C.eval_ctx)
     in
 
     let state_var = List.map mk_texpression_from_var state_var in
-    let ret =
-      mk_simpl_tuple_texpression ctx.fun_decl.meta (state_var @ [ ret ])
-    in
-    let ret = mk_result_return_texpression ctx.fun_decl.meta ret in
+    let ret = mk_simpl_tuple_texpression ctx.meta (state_var @ [ ret ]) in
+    let ret = mk_result_return_texpression ctx.meta ret in
 
     (* Introduce all the let-bindings *)
 
@@ -3405,7 +3382,7 @@ and translate_forward_end (ectx : C.eval_ctx)
         in
         let func_ty = mk_arrows input_tys ret_ty in
         let func = { e = Qualif func; ty = func_ty } in
-        let call = mk_apps ctx.fun_decl.meta func args in
+        let call = mk_apps ctx.meta func args in
         call
       in
 
@@ -3464,7 +3441,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
        (fun (sv : V.symbolic_value) ->
          V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var)
        loop.input_svalues)
-    ctx.fun_decl.meta;
+    ctx.meta;
 
   (* Translate the loop inputs *)
   let inputs =
@@ -3486,7 +3463,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
           (fun ty ->
             cassert __FILE__ __LINE__
               (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty))
-              !ctx.fun_decl.meta "The types shouldn't contain borrows";
+              !ctx.meta "The types shouldn't contain borrows";
             ctx_translate_fwd_ty !ctx ty)
           tys)
       loop.rg_to_given_back_tys
@@ -3567,7 +3544,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let ctx =
     sanity_check __FILE__ __LINE__
       (not (LoopId.Map.mem loop_id ctx.loops))
-      ctx.fun_decl.meta;
+      ctx.meta;
 
     (* Note that we will retrieve the input values later in the [ForwardEnd]
        (and will introduce the outputs at that moment, together with the actual
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 4c0f2e0d..348183c5 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -127,6 +127,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
 
   let ctx =
     {
+      meta = fdef.meta;
       decls_ctx = trans_ctx;
       SymbolicToPure.bid = None;
       sg;