From 1a40fee645d84f906aad12a3afd14c718329e2e1 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 26 Nov 2024 15:10:05 +0100
Subject: [PATCH] Update charon

---
 charon-pin                 |  2 +-
 flake.lock                 | 12 ++++++------
 src/extract/Extract.ml     |  6 ++++--
 src/extract/ExtractBase.ml |  5 +++--
 4 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/charon-pin b/charon-pin
index cb231975..03e7a85d 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.
-bab27dafb31080ef97d48e5589a33c0e95f2eb05
+f54e30a484a373514df354cfe3fd1ba238bdee6b
diff --git a/flake.lock b/flake.lock
index 071e9389..feb1476d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1732198416,
-        "narHash": "sha256-myAobBfSQCjjnDJsmtWCAwod5Y2oGJ3APhvBFdByaJ8=",
+        "lastModified": 1732629844,
+        "narHash": "sha256-OnDEQUoR9/XYXiyBKFMop1/nBaTtbFYSJY3iMQdE9JE=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "bab27dafb31080ef97d48e5589a33c0e95f2eb05",
+        "rev": "f54e30a484a373514df354cfe3fd1ba238bdee6b",
         "type": "github"
       },
       "original": {
@@ -285,11 +285,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1732156292,
-        "narHash": "sha256-XuTCME5ZausokOJ28AsIoayBVD1soscdoiKweT4VY50=",
+        "lastModified": 1732588352,
+        "narHash": "sha256-J2/hxOO1VtBA/u+a+9E+3iJpWT3xsBdghgYAVfoGCJo=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "2d484c7a0db32f2700e253160bcd2aaa6cdca3ba",
+        "rev": "414e748aae5c9e6ca63c5aafffda03e5dad57ceb",
         "type": "github"
       },
       "original": {
diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml
index 77a27b16..cb763581 100644
--- a/src/extract/Extract.ml
+++ b/src/extract/Extract.ml
@@ -1253,8 +1253,10 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   *)
   let ctx, trait_decl =
     match def.kind with
-    | TraitDeclItem (decl_id, _, true) ->
-        let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
+    | TraitDeclItem (trait_ref, _, true) ->
+        let trait_decl =
+          T.TraitDeclId.Map.find trait_ref.trait_decl_id ctx.trans_trait_decls
+        in
         let ctx, _ = ctx_add_trait_self_clause def.item_meta.span ctx in
         let ctx = { ctx with is_provided_method = true } in
         (ctx, Some trait_decl)
diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml
index 5bcef830..ca145577 100644
--- a/src/extract/ExtractBase.ml
+++ b/src/extract/ExtractBase.ml
@@ -2131,13 +2131,14 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
   *)
   let item_meta =
     match def.kind with
-    | TraitImplItem (_, trait_decl_id, item_name, _) -> (
+    | TraitImplItem (_, trait_decl_ref, item_name, _) -> (
         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. *)
           match
-            TraitDeclId.Map.find_opt trait_decl_id ctx.trans_trait_decls
+            TraitDeclId.Map.find_opt trait_decl_ref.trait_decl_id
+              ctx.trans_trait_decls
           with
           | None -> def.item_meta
           | Some trait_decl -> (