diff --git a/charon-pin b/charon-pin
index c08bfe73..31428e5f 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.
-cdc1dcde447a50cbc20336c79b21b42ac977b7fd
+96448ed72c9e8838ca2ed6b8477b5f2fb9cc8058
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 7cda8389..153d1499 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -107,6 +107,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
             | Use _
             | RvRef _
             | Global _
+            | GlobalRef _
             | Discriminant _
             | Aggregate _
             | Len _
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index f52f35d9..425cd0e0 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -780,7 +780,9 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span)
   let v, cf_compute =
     (* Match on the aggregate kind *)
     match aggregate_kind with
-    | AggregatedAdt (type_id, opt_variant_id, generics) -> (
+    | AggregatedAdt (type_id, opt_variant_id, opt_field_id, generics) -> (
+        (* The opt_field_id is Some only for unions, that we don't support *)
+        sanity_check __FILE__ __LINE__ (opt_field_id = None) span;
         match type_id with
         | TTuple ->
             let tys = List.map (fun (v : typed_value) -> v.ty) values in
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 8abc876e..97783976 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -828,6 +828,26 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span)
                 regions_hierarchy,
                 inst_sg )))
 
+(** Helper: introduce a fresh symbolic value for a global *)
+let eval_global_as_fresh_symbolic_value (span : Meta.span)
+    (gref : global_decl_ref) (ctx : eval_ctx) : symbolic_value =
+  let generics = gref.global_generics in
+  let global = ctx_lookup_global_decl ctx gref.global_id in
+  cassert __FILE__ __LINE__ (ty_no_regions global.ty) span
+    "Const globals should not contain regions";
+  (* Instantiate the type  *)
+  (* There shouldn't be any reference to Self *)
+  let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
+  let generics = Subst.generic_args_erase_regions generics in
+  let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
+    Subst.make_subst_from_generics global.generics generics tr_self
+  in
+  let ty =
+    Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
+      global.ty
+  in
+  mk_fresh_symbolic_value span ty
+
 (** Evaluate a statement *)
 let rec eval_statement (config : config) (st : statement) : stl_cm_fun =
  fun ctx ->
@@ -865,6 +885,9 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
       | Global gref ->
           (* Evaluate the global *)
           eval_global config st.span p gref ctx
+      | GlobalRef (gref, rkind) ->
+          (* Evaluate the reference to the global *)
+          eval_global_ref config st.span p gref rkind ctx
       | _ ->
           (* Evaluate the rvalue *)
           let res, ctx, cc = eval_rvalue_not_global config st.span rvalue ctx in
@@ -884,7 +907,8 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
                  * reserved borrow, we later can't translate it to pure values...) *)
                 let cc =
                   match rvalue with
-                  | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable"
+                  | Global _ | GlobalRef _ ->
+                      craise __FILE__ __LINE__ st.span "Unreachable"
                   | Len _ ->
                       craise __FILE__ __LINE__ st.span "Len is not handled yet"
                   | Use _
@@ -973,31 +997,18 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
 and eval_global (config : config) (span : Meta.span) (dest : place)
     (gref : global_decl_ref) : stl_cm_fun =
  fun ctx ->
-  let generics = gref.global_generics in
-  let global = ctx_lookup_global_decl ctx gref.global_id in
   match config.mode with
   | ConcreteMode ->
       (* Treat the evaluation of the global as a call to the global body *)
+      let generics = gref.global_generics in
+      let global = ctx_lookup_global_decl ctx gref.global_id in
       let func = { func = FunId (FRegular global.body); generics } in
       let call = { func = FnOpRegular func; args = []; dest } in
       eval_transparent_function_call_concrete config span global.body call ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
-      cassert __FILE__ __LINE__ (ty_no_regions global.ty) span
-        "Const globals should not contain regions";
-      (* Instantiate the type  *)
-      (* There shouldn't be any reference to Self *)
-      let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
-      let generics = Subst.generic_args_erase_regions generics in
-      let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
-        Subst.make_subst_from_generics global.generics generics tr_self
-      in
-      let ty =
-        Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
-          global.ty
-      in
-      let sval = mk_fresh_symbolic_value span ty in
+      let sval = eval_global_as_fresh_symbolic_value span gref ctx in
       let ctx, cc =
         assign_to_place config span
           (mk_typed_value_from_symbolic_value sval)
@@ -1007,6 +1018,47 @@ and eval_global (config : config) (span : Meta.span) (dest : place)
         cc_singleton __FILE__ __LINE__ span
           (cc_comp (S.synthesize_global_eval gref sval) cc) )
 
+and eval_global_ref (config : config) (span : Meta.span) (dest : place)
+    (gref : global_decl_ref) (rk : ref_kind) : stl_cm_fun =
+ fun ctx ->
+  (* We only support shared references to globals *)
+  cassert __FILE__ __LINE__ (rk = RShared) span
+    "Can only create shared references to global values";
+  match config.mode with
+  | ConcreteMode ->
+      (* We should treat the evaluation of the global as a call to the global body,
+         then create a reference *)
+      craise __FILE__ __LINE__ span "Unimplemented"
+  | SymbolicMode ->
+      (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
+       * defined as equal to the value of the global (see {!S.synthesize_global_eval}).
+       * We then create a reference to the global.
+       *)
+      let sval = eval_global_as_fresh_symbolic_value span gref ctx in
+      let typed_sval = mk_typed_value_from_symbolic_value sval in
+      (* Create a shared loan containing the global, as well as a shared borrow *)
+      let bid = fresh_borrow_id () in
+      let loan : typed_value =
+        {
+          value = VLoan (VSharedLoan (BorrowId.Set.singleton bid, typed_sval));
+          ty = sval.sv_ty;
+        }
+      in
+      let borrow : typed_value =
+        {
+          value = VBorrow (VSharedBorrow bid);
+          ty = TRef (RErased, sval.sv_ty, RShared);
+        }
+      in
+      (* We need to push the shared loan in a dummy variable *)
+      let dummy_id = fresh_dummy_var_id () in
+      let ctx = ctx_push_dummy_var ctx dummy_id loan in
+      (* Assign the borrow to its destination *)
+      let ctx, cc = assign_to_place config span borrow dest ctx in
+      ( [ (ctx, Unit) ],
+        cc_singleton __FILE__ __LINE__ span
+          (cc_comp (S.synthesize_global_eval gref sval) cc) )
+
 (** Evaluate a switch *)
 and eval_switch (config : config) (span : Meta.span) (switch : switch) :
     stl_cm_fun =
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index a7e59a1d..98242235 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -298,6 +298,7 @@ let rvalue_get_place (rv : rvalue) : place option =
   | UnaryOp _
   | BinaryOp _
   | Global _
+  | GlobalRef _
   | Discriminant _
   | Aggregate _ -> None
 
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index f16fba86..02ae635d 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -110,7 +110,8 @@ let remove_useless_cf_merges (crate : crate) (f : fun_decl) : fun_decl =
     | Assign (_, rv) -> (
         match rv with
         | Use _ | RvRef _ -> not must_end_with_exit
-        | Aggregate (AggregatedAdt (TTuple, _, _), []) -> not must_end_with_exit
+        | Aggregate (AggregatedAdt (TTuple, _, _, _), []) ->
+            not must_end_with_exit
         | _ -> false)
     | FakeRead _ | Drop _ | Nop -> not must_end_with_exit
     | Panic | Return -> true
diff --git a/flake.lock b/flake.lock
index de4b5a75..b4e5486f 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1725287105,
-        "narHash": "sha256-KUxQtYXe3/BL9XwGfiTS3tjDe0nEEF9Npp5BOHCe8ig=",
+        "lastModified": 1725446626,
+        "narHash": "sha256-00hpqHnAo4gDS9qjOTZ6Uqu3taIZ6z7yqPm4OAiUKZ4=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "cdc1dcde447a50cbc20336c79b21b42ac977b7fd",
+        "rev": "96448ed72c9e8838ca2ed6b8477b5f2fb9cc8058",
         "type": "github"
       },
       "original": {
@@ -272,11 +272,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1725243956,
-        "narHash": "sha256-0A5ZP8uDCyBdYUzayZfy6JFdTefP79oZVAjyqA/yuSI=",
+        "lastModified": 1725416653,
+        "narHash": "sha256-iNBv7ILlZI6ubhW0ExYy8YgiLKUerudxY7n8R5UQK2E=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "a10c8092d5f82622be79ed4dd12289f72011f850",
+        "rev": "e5d3f9c2f24d852cddc79716daf0f65ce8468b28",
         "type": "github"
       },
       "original": {