Fix LLBC regressions

.github/workflows/kani.yml

@@ -108,6 +108,13 @@ jobs:
         with:
           os: ubuntu-24.04
 
+      # Patch Charon so that it compiles. This is temporary until we're able to
+      # upgrade the pinned commit which requires fixing
+      # https://github.com/AeneasVerif/charon/issues/806 and updating the
+      # mir-to-ullbc code
+      - name: Patch Charon
+        run: cd charon && git apply ../scripts/charon-patch.diff
+
       - name: Build Kani with Charon
         run: cargo build-dev -- --features cprover --features llbc
 

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -69,6 +69,7 @@ use rustc_public::ty::{
     Ty, TyConst, TyConstKind, TyKind, UintTy,
 };
 use rustc_public::{CrateDef, CrateDefType, DefId};
+use rustc_public_bridge::IndexedVal;
 use std::collections::HashMap;
 use std::iter::zip;
 use std::path::PathBuf;
@@ -1009,7 +1010,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             name.push(CharonPathElem::Ident(crate_name, CharonDisambiguator::new(0)));
         }
 
-        if let Some(impl_defid_internal) = self.tcx.impl_of_method(def_id) {
+        if let Some(impl_defid_internal) = self.tcx.impl_of_assoc(def_id) {
             let traitref = self
                 .tcx
                 .impl_trait_ref(impl_defid_internal)

scripts/charon-patch.diff

@@ -0,0 +1,26 @@
+diff --git a/charon/Cargo.toml b/charon/Cargo.toml
+index 20f8a9df..a1bf1ee6 100644
+--- a/charon/Cargo.toml
++++ b/charon/Cargo.toml
+@@ -2,7 +2,7 @@
+ name = "charon"
+ version = "0.1.62"
+ authors = ["Son Ho <hosonmarc@gmail.com>"]
+-edition = "2021"
++edition = "2024"
+ license = "Apache-2.0"
+
+ [lib]
+diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs
+index 59f7eaab..21508e19 100644
+--- a/charon/src/ids/vector.rs
++++ b/charon/src/ids/vector.rs
+@@ -217,7 +217,7 @@ where
+         self.iter_indexed().map(|(id, _)| id)
+     }
+
+-    pub fn all_indices(&self) -> impl Iterator<Item = I> {
++    pub fn all_indices(&self) -> impl Iterator<Item = I> + use<I, T> {
+         self.vector.indices()
+     }
+