Fix LLBC regressions (#4338)

Since the upgrade to the 2025-07-04 toolchain, which removed the
`let_chains` unstable feature, the LLBC regressions have been broken.
This was caused by the removal of the `let_chains` feature (which is
used in the Charon submodule) and requiring the 2024 edition to use let
chains.

The edition used in Charon was upgraded to 2024 since
AeneasVerif/charon@59b8ad6,
but the attempt to update Kani to use that commit ran into
AeneasVerif/charon#806. So, in the meantime,
apply a minimal patch to the Charon code after cloning it to allow it to
build.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: zhassan-aws

.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()
+     }
+