From 6d544d59a637cd51f606de49f59fb8d4d93f6947 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Jul 2026 00:21:43 +0000 Subject: [PATCH] Update Charon submodule to v0.1.69 Advance the Charon pin from v0.1.68 (63f7749d) to v0.1.69 (485bd36e), the next step of the incremental effort to catch the pinned Charon up with upstream (the endgame is dropping scripts/charon-patch.diff entirely). Charon v0.1.69 makes `Vector::elem_count` the way to obtain the number of non-empty slots (`len` is removed); adapt the tuple-field-projection translation in the LLBC backend accordingly. Refresh scripts/charon-patch.diff so its hunks apply against the v0.1.69 sources (context-line drift only; the patch content is unchanged). Co-authored-by: Kiro --- Cargo.lock | 2 +- charon | 2 +- .../src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 2 +- scripts/charon-patch.diff | 10 +++++----- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 6cf00175ead..fd004e68d4d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -288,7 +288,7 @@ checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" [[package]] name = "charon" -version = "0.1.68" +version = "0.1.69" dependencies = [ "annotate-snippets", "anstream 0.6.21", diff --git a/charon b/charon index 63f7749d305..485bd36e35c 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit 63f7749d3058befad8414b77b9138c193bad0fad +Subproject commit 485bd36e35cbb24b3ec09a79edec62e5bf8221f2 diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index c2c9d67cc24..4c9d566cf98 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -1873,7 +1873,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => { - let c_fprj = CharonFieldProjKind::Tuple(genargs.types.len()); + let c_fprj = CharonFieldProjKind::Tuple(genargs.types.elem_count()); current_ty = self.translate_ty(*ty); c_provec.push(( CharonProjectionElem::Field(c_fprj, c_fieldid), diff --git a/scripts/charon-patch.diff b/scripts/charon-patch.diff index f3f9736533e..31d121713d5 100644 --- a/scripts/charon-patch.diff +++ b/scripts/charon-patch.diff @@ -1,10 +1,10 @@ diff --git a/charon/Cargo.toml b/charon/Cargo.toml -index d76c223c..0b354b1c 100644 +index cbba6280f..8b5b4ece8 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -2,7 +2,7 @@ name = "charon" - version = "0.1.68" + version = "0.1.69" authors = ["Son Ho "] -edition = "2021" +edition = "2024" @@ -12,10 +12,10 @@ index d76c223c..0b354b1c 100644 [lib] diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs -index 141cabe3..37948679 100644 +index 24dd10839..3ef70b0bc 100644 --- a/charon/src/ids/vector.rs +++ b/charon/src/ids/vector.rs -@@ -254,7 +254,7 @@ where +@@ -260,7 +260,7 @@ where self.iter_indexed().map(|(id, _)| id) } @@ -25,7 +25,7 @@ index 141cabe3..37948679 100644 } diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs -index 225da182..54370990 100644 +index 2b8a5d162..4716da208 100644 --- a/charon/src/transform/expand_associated_types.rs +++ b/charon/src/transform/expand_associated_types.rs @@ -761,7 +761,7 @@ impl<'a> ComputeItemModifications<'a> {